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 ⊢ Y = ℤ/Nℤ
znunit.u ⊢ U = Unit ⁡ Y
Assertion znunithash ⊢ N ∈ ℕ → U = ϕ ⁡ N

Proof

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