Metamath Proof Explorer

Theorem 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 ⊢ ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) ∈ ℕ0 )
3 hashfz1 ⊢ ( ( ϕ ‘ 𝑁 ) ∈ ℕ0 → ( ♯ ‘ ( 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 𝑁 ) )