Euler's theorem
In number theory, Euler's theorem (also known as the FermatEuler theorem) states that if n is a positive integer and a is relatively prime to n, then
 a^{φ(n)} = 1 (mod n)
The theorem is a generalization of Fermat's little theorem.
The theorem may be used to easily reduce large powers modulo n. For example, consider finding the last decimal digit of 7^{222}, i.e. 7^{222} mod 10. Note that 7 and 10 are coprime, and φ(10) = 4. So Euler's theorem yields 7^{4} = 1 (mod 10), and we get 7^{222} = 7^{4·55 + 2} = (7^{4})^{55}·7^{2} = 1^{55}·7^{2} = 49 = 9 (mod 10).
In general, when reducing a power of a modulo n (where a and n are coprime), one needs to work modulo φ(n) in the exponent of a:
 if x = y (mod φ(n)), then a^{x} = a^{y} (mod n).
Proofs of Euler's theorem
Leonhard Euler published a proof in 1736. Using modern terminology, one may prove the theorem as follows: the numbers a which are relatively prime to n form a group under multiplication mod n, the group of units of the ring Z/nZ. This group has φ(n) elements, and the statement of Euler's theorem follows then from Lagrange's theorem.
Another direct proof: if a is coprime to n, then multiplication by a permutes the residue classes mod n that are coprime to n; in other words (writing R for the set consisting of the φ(n) different such classes) the sets { x : x in R } and { ax : x in R } are equal; therefore, their products are equal. Hence, P = a^{φ(n)}P (mod n) where P is the first of those products. Since P is coprime to n, it follows that a^{φ(n)} = 1 (mod n).
The Mizar project has completely formalized and automatically checked a proof of Euler's theorem in the EULER_2 file.
