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 f1oeq1 ⊢ ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) = ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
14 12 13 syl ⊢ ( if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
15 f1oeq2 ⊢ ( if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
16 14 15 bitrd ⊢ ( if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
17 10 11 16 3syl ⊢ ( 𝑁 ∈ ℕ → ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ ( Base ‘ 𝑌 ) ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) ) )
18 9 17 mpbid ⊢ ( 𝑁 ∈ ℕ → ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
19 f1ofn ⊢ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) )
20 elpreima ⊢ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ) ) )
21 18 19 20 3syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ) ) )
22 fvres ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) )
23 22 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) )
24 23 eleq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ∈ 𝑈 ) )
25 elfzoelz ⊢ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) → 𝑥 ∈ ℤ )
26 eqid ⊢ ( ℤRHom ‘ 𝑌 ) = ( ℤRHom ‘ 𝑌 )
27 1 2 26 znunit ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
28 4 25 27 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
29 24 28 bitrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
30 29 pm5.32da ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑥 ) ∈ 𝑈 ) ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑥 gcd 𝑁 ) = 1 ) ) )
31 21 30 bitrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ↔ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑥 gcd 𝑁 ) = 1 ) ) )
32 31 abbi2dv ⊢ ( 𝑁 ∈ ℕ → ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) = { 𝑥 ∣ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑥 gcd 𝑁 ) = 1 ) } )
33 df-rab ⊢ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } = { 𝑥 ∣ ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝑥 gcd 𝑁 ) = 1 ) }
34 32 33 eqtr4di ⊢ ( 𝑁 ∈ ℕ → ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) = { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
35 34 fveq2d ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ) = ( ♯ ‘ { 𝑥 ∈ ( 0 ..^ 𝑁 ) ∣ ( 𝑥 gcd 𝑁 ) = 1 } ) )
36 f1ocnv ⊢ ( ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
37 f1of1 ⊢ ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1-onto→ ( 0 ..^ 𝑁 ) → ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1→ ( 0 ..^ 𝑁 ) )
38 18 36 37 3syl ⊢ ( 𝑁 ∈ ℕ → ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1→ ( 0 ..^ 𝑁 ) )
39 ovexd ⊢ ( 𝑁 ∈ ℕ → ( 0 ..^ 𝑁 ) ∈ V )
40 5 2 unitss ⊢ 𝑈 ⊆ ( Base ‘ 𝑌 )
41 40 a1i ⊢ ( 𝑁 ∈ ℕ → 𝑈 ⊆ ( Base ‘ 𝑌 ) )
42 2 fvexi ⊢ 𝑈 ∈ V
43 42 a1i ⊢ ( 𝑁 ∈ ℕ → 𝑈 ∈ V )
44 f1imaen2g ⊢ ( ( ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) : ( Base ‘ 𝑌 ) –1-1→ ( 0 ..^ 𝑁 ) ∧ ( 0 ..^ 𝑁 ) ∈ V ) ∧ ( 𝑈 ⊆ ( Base ‘ 𝑌 ) ∧ 𝑈 ∈ V ) ) → ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ≈ 𝑈 )
45 38 39 41 43 44 syl22anc ⊢ ( 𝑁 ∈ ℕ → ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ≈ 𝑈 )
46 hasheni ⊢ ( ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ≈ 𝑈 → ( ♯ ‘ ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ) = ( ♯ ‘ 𝑈 ) )
47 45 46 syl ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( ◡ ( ( ℤRHom ‘ 𝑌 ) ↾ ( 0 ..^ 𝑁 ) ) “ 𝑈 ) ) = ( ♯ ‘ 𝑈 ) )
48 3 35 47 3eqtr2rd ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝑈 ) = ( ϕ ‘ 𝑁 ) )