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