Metamath Proof Explorer


Theorem znunithash

Description: The size of the unit group of Z/nZ . (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses znchr.y 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znunit.u 𝑈 = ( Unit ‘ 𝑌 )
Assertion znunithash ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝑈 ) = ( ϕ ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 znchr.y 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 znunit.u 𝑈 = ( Unit ‘ 𝑌 )
3 dfphi2 ( 𝑁 ∈ ℕ → ( ϕ ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
4 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
5 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
6 eqid ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) = ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) )
7 eqid if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
8 1 5 6 7 znf1o ( 𝑁 ∈ ℕ0 → ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) )
9 4 8 syl ( 𝑁 ∈ ℕ → ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) )
10 nnne0 ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
11 ifnefalse ( 𝑁 ≠ 0 → if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) )
12 reseq2 ( if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) → ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) = ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) )
13 12 f1oeq1d ( if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
14 f1oeq2 ( if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
15 13 14 bitrd ( if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
16 10 11 15 3syl ( 𝑁 ∈ ℕ → ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
17 9 16 mpbid ( 𝑁 ∈ ℕ → ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
18 f1ofn ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) )
19 elpreima ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ) ) )
20 17 18 19 3syl ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ) ) )
21 fvres ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) )
22 21 adantl ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) )
23 22 eleq1d ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ∈ 𝑈 ) )
24 elfzoelz ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → 𝑥 ∈ ℤ )
25 eqid ( ℤRHom ‘ 𝑌 ) = ( ℤRHom ‘ 𝑌 )
26 1 2 25 znunit ( ( 𝑁 ∈ ℕ0𝑥 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
27 4 24 26 syl2an ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
28 23 27 bitrd ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
29 28 pm5.32da ( 𝑁 ∈ ℕ → ( ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ) ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑥 gcd 𝑁 ) = 1 ) ) )
30 20 29 bitrd ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑥 gcd 𝑁 ) = 1 ) ) )
31 30 abbi2dv ( 𝑁 ∈ ℕ → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) = { 𝑥 ∣ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑥 gcd 𝑁 ) = 1 ) } )
32 df-rab { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } = { 𝑥 ∣ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑥 gcd 𝑁 ) = 1 ) }
33 31 32 eqtr4di ( 𝑁 ∈ ℕ → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) = { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
34 33 fveq2d ( 𝑁 ∈ ℕ → ( ♯ ‘ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
35 f1ocnv ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
36 f1of1 ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1-onto→ ( 0 ..^ 𝑁 ) → ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1→ ( 0 ..^ 𝑁 ) )
37 17 35 36 3syl ( 𝑁 ∈ ℕ → ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1→ ( 0 ..^ 𝑁 ) )
38 ovexd ( 𝑁 ∈ ℕ → ( 0 ..^ 𝑁 ) ∈ V )
39 5 2 unitss 𝑈 ⊆ ( Base ‘ 𝑌 )
40 39 a1i ( 𝑁 ∈ ℕ → 𝑈 ⊆ ( Base ‘ 𝑌 ) )
41 2 fvexi 𝑈 ∈ V
42 41 a1i ( 𝑁 ∈ ℕ → 𝑈 ∈ V )
43 f1imaen2g ( ( ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1→ ( 0 ..^ 𝑁 ) ∧ ( 0 ..^ 𝑁 ) ∈ V ) ∧ ( 𝑈 ⊆ ( Base ‘ 𝑌 ) ∧ 𝑈 ∈ V ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ≈ 𝑈 )
44 37 38 40 42 43 syl22anc ( 𝑁 ∈ ℕ → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ≈ 𝑈 )
45 hasheni ( ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ≈ 𝑈 → ( ♯ ‘ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ) = ( ♯ ‘ 𝑈 ) )
46 44 45 syl ( 𝑁 ∈ ℕ → ( ♯ ‘ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ) = ( ♯ ‘ 𝑈 ) )
47 3 34 46 3eqtr2rd ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝑈 ) = ( ϕ ‘ 𝑁 ) )