eulerth

Description: Euler's theorem, a generalization of Fermat's little theorem. If A and N are coprime, then A ^ phi ( N ) == 1 (mod N ). This is Metamath 100 proof #10. Also called Euler-Fermat theorem, see theorem 5.17 in ApostolNT p. 113. (Contributed by Mario Carneiro, 28-Feb-2014)

		Ref	Expression
	Assertion	eulerth	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A^{ϕ (N)} \mod N = 1 \mod N$

Proof

Step	Hyp	Ref	Expression
1		phicl	$⊢ N \in ℕ \to ϕ (N) \in ℕ$
2	1	nnnn0d	$⊢ N \in ℕ \to ϕ (N) \in ℕ_{0}$
3		hashfz1	$⊢ ϕ (N) \in ℕ_{0} \to \|(1 \dots ϕ (N))\| = ϕ (N)$
4	2 3	syl	$⊢ N \in ℕ \to \|(1 \dots ϕ (N))\| = ϕ (N)$
5		dfphi2	$⊢ N \in ℕ \to ϕ (N) = \|\{k \in (0 ..^N) \| k \gcd N = 1\}\|$
6	4 5	eqtrd	$⊢ N \in ℕ \to \|(1 \dots ϕ (N))\| = \|\{k \in (0 ..^N) \| k \gcd N = 1\}\|$
7	6	3ad2ant1	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to \|(1 \dots ϕ (N))\| = \|\{k \in (0 ..^N) \| k \gcd N = 1\}\|$
8		fzfi	$⊢ (1 \dots ϕ (N)) \in Fin$
9		fzofi	$⊢ (0 ..^N) \in Fin$
10		ssrab2	$⊢ \{k \in (0 ..^N) \| k \gcd N = 1\} \subseteq (0 ..^N)$
11		ssfi	$⊢ ((0 ..^N) \in Fin \land \{k \in (0 ..^N) \| k \gcd N = 1\} \subseteq (0 ..^N)) \to \{k \in (0 ..^N) \| k \gcd N = 1\} \in Fin$
12	9 10 11	mp2an	$⊢ \{k \in (0 ..^N) \| k \gcd N = 1\} \in Fin$
13		hashen	$⊢ ((1 \dots ϕ (N)) \in Fin \land \{k \in (0 ..^N) \| k \gcd N = 1\} \in Fin) \to (\|(1 \dots ϕ (N))\| = \|\{k \in (0 ..^N) \| k \gcd N = 1\}\| \leftrightarrow (1 \dots ϕ (N)) \approx \{k \in (0 ..^N) \| k \gcd N = 1\})$
14	8 12 13	mp2an	$⊢ \|(1 \dots ϕ (N))\| = \|\{k \in (0 ..^N) \| k \gcd N = 1\}\| \leftrightarrow (1 \dots ϕ (N)) \approx \{k \in (0 ..^N) \| k \gcd N = 1\}$
15	7 14	sylib	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to (1 \dots ϕ (N)) \approx \{k \in (0 ..^N) \| k \gcd N = 1\}$
16		bren	$⊢ (1 \dots ϕ (N)) \approx \{k \in (0 ..^N) \| k \gcd N = 1\} \leftrightarrow \exists f f : (1 \dots ϕ (N)) \underset{1-1 onto}{⟶} \{k \in (0 ..^N) \| k \gcd N = 1\}$
17	15 16	sylib	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to \exists f f : (1 \dots ϕ (N)) \underset{1-1 onto}{⟶} \{k \in (0 ..^N) \| k \gcd N = 1\}$
18		simpl	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land f : (1 \dots ϕ (N)) \underset{1-1 onto}{⟶} \{k \in (0 ..^N) \| k \gcd N = 1\}) \to (N \in ℕ \land A \in ℤ \land A \gcd N = 1)$
19		oveq1	$⊢ k = y \to k \gcd N = y \gcd N$
20	19	eqeq1d	$⊢ k = y \to (k \gcd N = 1 \leftrightarrow y \gcd N = 1)$
21	20	cbvrabv	$⊢ \{k \in (0 ..^N) \| k \gcd N = 1\} = \{y \in (0 ..^N) \| y \gcd N = 1\}$
22		eqid	$⊢ (1 \dots ϕ (N)) = (1 \dots ϕ (N))$
23		simpr	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land f : (1 \dots ϕ (N)) \underset{1-1 onto}{⟶} \{k \in (0 ..^N) \| k \gcd N = 1\}) \to f : (1 \dots ϕ (N)) \underset{1-1 onto}{⟶} \{k \in (0 ..^N) \| k \gcd N = 1\}$
24		fveq2	$⊢ k = x \to f (k) = f (x)$
25	24	oveq2d	$⊢ k = x \to A f (k) = A f (x)$
26	25	oveq1d	$⊢ k = x \to A f (k) \mod N = A f (x) \mod N$
27	26	cbvmptv	$⊢ (k \in (1 \dots ϕ (N)) ⟼ A f (k) \mod N) = (x \in (1 \dots ϕ (N)) ⟼ A f (x) \mod N)$
28	18 21 22 23 27	eulerthlem2	$⊢ ((N \in ℕ \land A \in ℤ \land A \gcd N = 1) \land f : (1 \dots ϕ (N)) \underset{1-1 onto}{⟶} \{k \in (0 ..^N) \| k \gcd N = 1\}) \to A^{ϕ (N)} \mod N = 1 \mod N$
29	17 28	exlimddv	$⊢ (N \in ℕ \land A \in ℤ \land A \gcd N = 1) \to A^{ϕ (N)} \mod N = 1 \mod N$

Metamath Proof Explorer

Theorem eulerth

Proof