This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znrrg

Description: The regular elements of Z/nZ are exactly the units. (This theorem fails for N = 0 , where all nonzero integers are regular, but only +- 1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses znchr.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znunit.u ⊢ 𝑈 = ( Unit ‘ 𝑌 )
znrrg.e ⊢ 𝐸 = ( RLReg ‘ 𝑌 )
Assertion znrrg ( 𝑁 ∈ ℕ → 𝐸 = 𝑈 )

Proof

Step Hyp Ref Expression
1 znchr.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 znunit.u ⊢ 𝑈 = ( Unit ‘ 𝑌 )
3 znrrg.e ⊢ 𝐸 = ( RLReg ‘ 𝑌 )
4 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
5 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
6 eqid ⊢ ( ℤRHom ‘ 𝑌 ) = ( ℤRHom ‘ 𝑌 )
7 1 5 6 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) )
8 4 7 syl ⊢ ( 𝑁 ∈ ℕ → ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) )
9 3 5 rrgss ⊢ 𝐸 ⊆ ( Base ‘ 𝑌 )
10 9 sseli ⊢ ( 𝑥 ∈ 𝐸 → 𝑥 ∈ ( Base ‘ 𝑌 ) )
11 foelrn ⊢ ( ( ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) ∧ 𝑥 ∈ ( Base ‘ 𝑌 ) ) → ∃ 𝑛 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) )
12 8 10 11 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐸 ) → ∃ 𝑛 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) )
13 12 ex ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝐸 → ∃ 𝑛 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ) )
14 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
15 14 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 𝑁 ∈ ℂ )
16 simplr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 𝑛 ∈ ℤ )
17 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
18 17 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 𝑁 ∈ ℤ )
19 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
20 19 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 𝑁 ≠ 0 )
21 simpr ⊢ ( ( 𝑛 = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
22 21 necon3ai ⊢ ( 𝑁 ≠ 0 → ¬ ( 𝑛 = 0 ∧ 𝑁 = 0 ) )
23 20 22 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ¬ ( 𝑛 = 0 ∧ 𝑁 = 0 ) )
24 gcdn0cl ⊢ ( ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑛 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑛 gcd 𝑁 ) ∈ ℕ )
25 16 18 23 24 syl21anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 gcd 𝑁 ) ∈ ℕ )
26 25 nncnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 gcd 𝑁 ) ∈ ℂ )
27 25 nnne0d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 gcd 𝑁 ) ≠ 0 )
28 15 26 27 divcan2d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( 𝑛 gcd 𝑁 ) · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) = 𝑁 )
29 gcddvds ⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑛 gcd 𝑁 ) ∥ 𝑛 ∧ ( 𝑛 gcd 𝑁 ) ∥ 𝑁 ) )
30 16 18 29 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( 𝑛 gcd 𝑁 ) ∥ 𝑛 ∧ ( 𝑛 gcd 𝑁 ) ∥ 𝑁 ) )
31 30 simpld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 gcd 𝑁 ) ∥ 𝑛 )
32 25 nnzd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 gcd 𝑁 ) ∈ ℤ )
33 30 simprd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 gcd 𝑁 ) ∥ 𝑁 )
34 simpll ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 𝑁 ∈ ℕ )
35 nndivdvds ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑛 gcd 𝑁 ) ∈ ℕ ) → ( ( 𝑛 gcd 𝑁 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ∈ ℕ ) )
36 34 25 35 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( 𝑛 gcd 𝑁 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ∈ ℕ ) )
37 33 36 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ∈ ℕ )
38 37 nnzd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ∈ ℤ )
39 dvdsmulc ⊢ ( ( ( 𝑛 gcd 𝑁 ) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ∈ ℤ ) → ( ( 𝑛 gcd 𝑁 ) ∥ 𝑛 → ( ( 𝑛 gcd 𝑁 ) · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ∥ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) )
40 32 16 38 39 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( 𝑛 gcd 𝑁 ) ∥ 𝑛 → ( ( 𝑛 gcd 𝑁 ) · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ∥ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) )
41 31 40 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( 𝑛 gcd 𝑁 ) · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ∥ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) )
42 28 41 eqbrtrrd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 𝑁 ∥ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) )
43 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 )
44 4 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 𝑁 ∈ ℕ0 )
45 44 7 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) )
46 fof ⊢ ( ( ℤRHom ‘ 𝑌 ) : ℤ –onto→ ( Base ‘ 𝑌 ) → ( ℤRHom ‘ 𝑌 ) : ℤ ⟶ ( Base ‘ 𝑌 ) )
47 45 46 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ℤRHom ‘ 𝑌 ) : ℤ ⟶ ( Base ‘ 𝑌 ) )
48 47 38 ffvelcdmd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ∈ ( Base ‘ 𝑌 ) )
49 eqid ⊢ ( .r ‘ 𝑌 ) = ( .r ‘ 𝑌 )
50 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
51 3 5 49 50 rrgeq0i ⊢ ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ∈ ( Base ‘ 𝑌 ) ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) = ( 0g ‘ 𝑌 ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) = ( 0g ‘ 𝑌 ) ) )
52 43 48 51 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) = ( 0g ‘ 𝑌 ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) = ( 0g ‘ 𝑌 ) ) )
53 1 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CRing )
54 4 53 syl ⊢ ( 𝑁 ∈ ℕ → 𝑌 ∈ CRing )
55 crngring ⊢ ( 𝑌 ∈ CRing → 𝑌 ∈ Ring )
56 54 55 syl ⊢ ( 𝑁 ∈ ℕ → 𝑌 ∈ Ring )
57 56 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 𝑌 ∈ Ring )
58 6 zrhrhm ⊢ ( 𝑌 ∈ Ring → ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) )
59 57 58 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) )
60 zringbas ⊢ ℤ = ( Base ‘ ℤring )
61 zringmulr ⊢ · = ( .r ‘ ℤring )
62 60 61 49 rhmmul ⊢ ( ( ( ℤRHom ‘ 𝑌 ) ∈ ( ℤring RingHom 𝑌 ) ∧ 𝑛 ∈ ℤ ∧ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ∈ ℤ ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) = ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) )
63 59 16 38 62 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) = ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) )
64 63 eqeq1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) = ( 0g ‘ 𝑌 ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) = ( 0g ‘ 𝑌 ) ) )
65 16 38 zmulcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ∈ ℤ )
66 1 6 50 zndvds0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) )
67 44 65 66 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) )
68 64 67 bitr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ( .r ‘ 𝑌 ) ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) ) )
69 1 6 50 zndvds0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) )
70 44 38 69 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) = ( 0g ‘ 𝑌 ) ↔ 𝑁 ∥ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) )
71 52 68 70 3imtr3d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑁 ∥ ( 𝑛 · ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) → 𝑁 ∥ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ) )
72 42 71 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 𝑁 ∥ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) )
73 15 26 27 divcan1d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) · ( 𝑛 gcd 𝑁 ) ) = 𝑁 )
74 37 nncnd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ∈ ℂ )
75 74 mulridd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) · 1 ) = ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) )
76 72 73 75 3brtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) · ( 𝑛 gcd 𝑁 ) ) ∥ ( ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) · 1 ) )
77 1zzd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → 1 ∈ ℤ )
78 37 nnne0d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ≠ 0 )
79 dvdscmulr ⊢ ( ( ( 𝑛 gcd 𝑁 ) ∈ ℤ ∧ 1 ∈ ℤ ∧ ( ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ∈ ℤ ∧ ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) ≠ 0 ) ) → ( ( ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) · ( 𝑛 gcd 𝑁 ) ) ∥ ( ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) · 1 ) ↔ ( 𝑛 gcd 𝑁 ) ∥ 1 ) )
80 32 77 38 78 79 syl112anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) · ( 𝑛 gcd 𝑁 ) ) ∥ ( ( 𝑁 / ( 𝑛 gcd 𝑁 ) ) · 1 ) ↔ ( 𝑛 gcd 𝑁 ) ∥ 1 ) )
81 76 80 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 gcd 𝑁 ) ∥ 1 )
82 16 18 gcdcld ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 gcd 𝑁 ) ∈ ℕ0 )
83 dvds1 ⊢ ( ( 𝑛 gcd 𝑁 ) ∈ ℕ0 → ( ( 𝑛 gcd 𝑁 ) ∥ 1 ↔ ( 𝑛 gcd 𝑁 ) = 1 ) )
84 82 83 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( 𝑛 gcd 𝑁 ) ∥ 1 ↔ ( 𝑛 gcd 𝑁 ) = 1 ) )
85 81 84 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( 𝑛 gcd 𝑁 ) = 1 )
86 1 2 6 znunit ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝑈 ↔ ( 𝑛 gcd 𝑁 ) = 1 ) )
87 44 16 86 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝑈 ↔ ( 𝑛 gcd 𝑁 ) = 1 ) )
88 85 87 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) ∧ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝑈 )
89 88 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) → ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝑈 ) )
90 eleq1 ⊢ ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) → ( 𝑥 ∈ 𝐸 ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 ) )
91 eleq1 ⊢ ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) → ( 𝑥 ∈ 𝑈 ↔ ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝑈 ) )
92 90 91 imbi12d ⊢ ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) → ( ( 𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈 ) ↔ ( ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝐸 → ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) ∈ 𝑈 ) ) )
93 89 92 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ ) → ( 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) → ( 𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈 ) ) )
94 93 rexlimdva ⊢ ( 𝑁 ∈ ℕ → ( ∃ 𝑛 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) → ( 𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈 ) ) )
95 94 com23 ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝐸 → ( ∃ 𝑛 ∈ ℤ 𝑥 = ( ( ℤRHom ‘ 𝑌 ) ‘ 𝑛 ) → 𝑥 ∈ 𝑈 ) ) )
96 13 95 mpdd ⊢ ( 𝑁 ∈ ℕ → ( 𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈 ) )
97 96 ssrdv ⊢ ( 𝑁 ∈ ℕ → 𝐸 ⊆ 𝑈 )
98 3 2 unitrrg ⊢ ( 𝑌 ∈ Ring → 𝑈 ⊆ 𝐸 )
99 56 98 syl ⊢ ( 𝑁 ∈ ℕ → 𝑈 ⊆ 𝐸 )
100 97 99 eqssd ⊢ ( 𝑁 ∈ ℕ → 𝐸 = 𝑈 )