Major Section: ACL2-BUILT-INS

`(mod-expt r i m)`

is the result of raising the number `r`

to the
integer power `i`

and then taking the residue mod `m`

. That is,
`(mod-expt r i m)`

is equal to `(mod (expt r i) m)`

.

The guard for `(mod-expt r i m)`

is that `r`

is a rational number
and `i`

is an integer; if `r`

is `0`

then `i`

is nonnegative; and
`m`

is a non-zero rational number.

In some implementations (GCL Version 2.7.0 as of this writing), this function
is highly optimized when `r`

and `i`

are natural numbers, not both zero,
and `m`

is a positive integer. For other Lisp implementations, consider
using function `mod-expt-fast`

, defined in the community book
`arithmetic-3/floor-mod/mod-expt-fast.lisp`

, which should still provide
significantly improved performance over this function.

To see the ACL2 definition of this function, see pf.