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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		phicl	⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ )
2	1	nnnn0d	⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ₀ )
3		hashfz1	⊢ ( ( ϕ ‘ 𝑁 ) ∈ ℕ₀ → ( ♯ ‘ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) = ( ϕ ‘ 𝑁 ) )
4	2 3	syl	⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) = ( ϕ ‘ 𝑁 ) )
5		dfphi2	⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ) )
6	4 5	eqtrd	⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) = ( ♯ ‘ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ) )
7	6	3ad2ant1	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ♯ ‘ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) = ( ♯ ‘ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ) )
8		fzfi	⊢ ( 1 ... ( ϕ ‘ 𝑁 ) ) ∈ Fin
9		fzofi	⊢ ( 0 ..^ 𝑁 ) ∈ Fin
10		ssrab2	⊢ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ⊆ ( 0 ..^ 𝑁 )
11		ssfi	⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ⊆ ( 0 ..^ 𝑁 ) ) → { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ∈ Fin )
12	9 10 11	mp2an	⊢ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ∈ Fin
13		hashen	⊢ ( ( ( 1 ... ( ϕ ‘ 𝑁 ) ) ∈ Fin ∧ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ∈ Fin ) → ( ( ♯ ‘ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) = ( ♯ ‘ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ) ↔ ( 1 ... ( ϕ ‘ 𝑁 ) ) ≈ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ) )
14	8 12 13	mp2an	⊢ ( ( ♯ ‘ ( 1 ... ( ϕ ‘ 𝑁 ) ) ) = ( ♯ ‘ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ) ↔ ( 1 ... ( ϕ ‘ 𝑁 ) ) ≈ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } )
15	7 14	sylib	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 1 ... ( ϕ ‘ 𝑁 ) ) ≈ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } )
16		bren	⊢ ( ( 1 ... ( ϕ ‘ 𝑁 ) ) ≈ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ↔ ∃ 𝑓 𝑓 : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } )
17	15 16	sylib	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ∃ 𝑓 𝑓 : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } )
18		simpl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑓 : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ) → ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) )
19		oveq1	⊢ ( 𝑘 = 𝑦 → ( 𝑘 gcd 𝑁 ) = ( 𝑦 gcd 𝑁 ) )
20	19	eqeq1d	⊢ ( 𝑘 = 𝑦 → ( ( 𝑘 gcd 𝑁 ) = 1 ↔ ( 𝑦 gcd 𝑁 ) = 1 ) )
21	20	cbvrabv	⊢ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } = { 𝑦 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑦 gcd 𝑁 ) = 1 }
22		eqid	⊢ ( 1 ... ( ϕ ‘ 𝑁 ) ) = ( 1 ... ( ϕ ‘ 𝑁 ) )
23		simpr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑓 : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ) → 𝑓 : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } )
24		fveq2	⊢ ( 𝑘 = 𝑥 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑥 ) )
25	24	oveq2d	⊢ ( 𝑘 = 𝑥 → ( 𝐴 · ( 𝑓 ‘ 𝑘 ) ) = ( 𝐴 · ( 𝑓 ‘ 𝑥 ) ) )
26	25	oveq1d	⊢ ( 𝑘 = 𝑥 → ( ( 𝐴 · ( 𝑓 ‘ 𝑘 ) ) mod 𝑁 ) = ( ( 𝐴 · ( 𝑓 ‘ 𝑥 ) ) mod 𝑁 ) )
27	26	cbvmptv	⊢ ( 𝑘 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ↦ ( ( 𝐴 · ( 𝑓 ‘ 𝑘 ) ) mod 𝑁 ) ) = ( 𝑥 ∈ ( 1 ... ( ϕ ‘ 𝑁 ) ) ↦ ( ( 𝐴 · ( 𝑓 ‘ 𝑥 ) ) mod 𝑁 ) )
28	18 21 22 23 27	eulerthlem2	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ∧ 𝑓 : ( 1 ... ( ϕ ‘ 𝑁 ) ) –1-1-onto→ { 𝑘 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑘 gcd 𝑁 ) = 1 } ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) )
29	17 28	exlimddv	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 ↑ ( ϕ ‘ 𝑁 ) ) mod 𝑁 ) = ( 1 mod 𝑁 ) )

Metamath Proof Explorer

Theorem eulerth

Proof