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 ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝑈 ) = ( ϕ ‘ 𝑁 ) )