Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  znrrg Structured version   Visualization version   GIF version

Theorem znrrg 19733
 Description: The regular elements of ℤ/nℤ are exactly the units. (This theorem fails for 𝑁 = 0, where all nonzero integers are regular, but only ±1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016.)
Hypotheses
Ref Expression
znchr.y 𝑌 = (ℤ/nℤ‘𝑁)
znunit.u 𝑈 = (Unit‘𝑌)
znrrg.e 𝐸 = (RLReg‘𝑌)
Assertion
Ref Expression
znrrg (𝑁 ∈ ℕ → 𝐸 = 𝑈)

Proof of Theorem znrrg
Dummy variables 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnnn0 11176 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
2 znchr.y . . . . . . . 8 𝑌 = (ℤ/nℤ‘𝑁)
3 eqid 2610 . . . . . . . 8 (Base‘𝑌) = (Base‘𝑌)
4 eqid 2610 . . . . . . . 8 (ℤRHom‘𝑌) = (ℤRHom‘𝑌)
52, 3, 4znzrhfo 19715 . . . . . . 7 (𝑁 ∈ ℕ0 → (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌))
61, 5syl 17 . . . . . 6 (𝑁 ∈ ℕ → (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌))
7 znrrg.e . . . . . . . 8 𝐸 = (RLReg‘𝑌)
87, 3rrgss 19113 . . . . . . 7 𝐸 ⊆ (Base‘𝑌)
98sseli 3564 . . . . . 6 (𝑥𝐸𝑥 ∈ (Base‘𝑌))
10 foelrn 6286 . . . . . 6 (((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) ∧ 𝑥 ∈ (Base‘𝑌)) → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛))
116, 9, 10syl2an 493 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑥𝐸) → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛))
1211ex 449 . . . 4 (𝑁 ∈ ℕ → (𝑥𝐸 → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛)))
13 nncn 10905 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
1413ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℂ)
15 simplr 788 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑛 ∈ ℤ)
16 nnz 11276 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
1716ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℤ)
18 nnne0 10930 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
1918ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ≠ 0)
20 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝑛 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
2120necon3ai 2807 . . . . . . . . . . . . . . . . . 18 (𝑁 ≠ 0 → ¬ (𝑛 = 0 ∧ 𝑁 = 0))
2219, 21syl 17 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ¬ (𝑛 = 0 ∧ 𝑁 = 0))
23 gcdn0cl 15062 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑛 = 0 ∧ 𝑁 = 0)) → (𝑛 gcd 𝑁) ∈ ℕ)
2415, 17, 22, 23syl21anc 1317 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℕ)
2524nncnd 10913 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℂ)
2624nnne0d 10942 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ≠ 0)
2714, 25, 26divcan2d 10682 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) = 𝑁)
28 gcddvds 15063 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑛 gcd 𝑁) ∥ 𝑛 ∧ (𝑛 gcd 𝑁) ∥ 𝑁))
2915, 17, 28syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑛 ∧ (𝑛 gcd 𝑁) ∥ 𝑁))
3029simpld 474 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 𝑛)
3124nnzd 11357 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℤ)
3229simprd 478 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 𝑁)
33 simpll 786 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℕ)
34 nndivdvds 14827 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ (𝑛 gcd 𝑁) ∈ ℕ) → ((𝑛 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ))
3533, 24, 34syl2anc 691 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ))
3632, 35mpbid 221 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ)
3736nnzd 11357 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ)
38 dvdsmulc 14847 . . . . . . . . . . . . . . . 16 (((𝑛 gcd 𝑁) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) → ((𝑛 gcd 𝑁) ∥ 𝑛 → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
3931, 15, 37, 38syl3anc 1318 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑛 → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
4030, 39mpd 15 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))
4127, 40eqbrtrrd 4607 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))
42 simpr 476 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸)
431ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℕ0)
4443, 5syl 17 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌))
45 fof 6028 . . . . . . . . . . . . . . . . 17 ((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌))
4644, 45syl 17 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌))
4746, 37ffvelrnd 6268 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) ∈ (Base‘𝑌))
48 eqid 2610 . . . . . . . . . . . . . . . 16 (.r𝑌) = (.r𝑌)
49 eqid 2610 . . . . . . . . . . . . . . . 16 (0g𝑌) = (0g𝑌)
507, 3, 48, 49rrgeq0i 19110 . . . . . . . . . . . . . . 15 ((((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 ∧ ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) ∈ (Base‘𝑌)) → ((((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) → ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g𝑌)))
5142, 47, 50syl2anc 691 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) → ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g𝑌)))
522zncrng 19712 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0𝑌 ∈ CRing)
531, 52syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑌 ∈ CRing)
54 crngring 18381 . . . . . . . . . . . . . . . . . . . 20 (𝑌 ∈ CRing → 𝑌 ∈ Ring)
5553, 54syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑌 ∈ Ring)
5655ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑌 ∈ Ring)
574zrhrhm 19679 . . . . . . . . . . . . . . . . . 18 (𝑌 ∈ Ring → (ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌))
5856, 57syl 17 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌))
59 zringbas 19643 . . . . . . . . . . . . . . . . . 18 ℤ = (Base‘ℤring)
60 zringmulr 19646 . . . . . . . . . . . . . . . . . 18 · = (.r‘ℤring)
6159, 60, 48rhmmul 18550 . . . . . . . . . . . . . . . . 17 (((ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌) ∧ 𝑛 ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) → ((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))))
6258, 15, 37, 61syl3anc 1318 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))))
6362eqeq1d 2612 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) ↔ (((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌)))
6415, 37zmulcld 11364 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) ∈ ℤ)
652, 4, 49zndvds0 19718 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0 ∧ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
6643, 64, 65syl2anc 691 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
6763, 66bitr3d 269 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
682, 4, 49zndvds0 19718 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g𝑌) ↔ 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁))))
6943, 37, 68syl2anc 691 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g𝑌) ↔ 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁))))
7051, 67, 693imtr3d 281 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) → 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁))))
7141, 70mpd 15 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁)))
7214, 25, 26divcan1d 10681 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) = 𝑁)
7336nncnd 10913 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℂ)
7473mulid1d 9936 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · 1) = (𝑁 / (𝑛 gcd 𝑁)))
7571, 72, 743brtr4d 4615 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1))
76 1zzd 11285 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 1 ∈ ℤ)
7736nnne0d 10942 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ≠ 0)
78 dvdscmulr 14848 . . . . . . . . . . . 12 (((𝑛 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ ∧ ((𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ≠ 0)) → (((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1) ↔ (𝑛 gcd 𝑁) ∥ 1))
7931, 76, 37, 77, 78syl112anc 1322 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1) ↔ (𝑛 gcd 𝑁) ∥ 1))
8075, 79mpbid 221 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 1)
8115, 17gcdcld 15068 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℕ0)
82 dvds1 14879 . . . . . . . . . . 11 ((𝑛 gcd 𝑁) ∈ ℕ0 → ((𝑛 gcd 𝑁) ∥ 1 ↔ (𝑛 gcd 𝑁) = 1))
8381, 82syl 17 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 1 ↔ (𝑛 gcd 𝑁) = 1))
8480, 83mpbid 221 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) = 1)
85 znunit.u . . . . . . . . . . 11 𝑈 = (Unit‘𝑌)
862, 85, 4znunit 19731 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℤ) → (((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈 ↔ (𝑛 gcd 𝑁) = 1))
8743, 15, 86syl2anc 691 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈 ↔ (𝑛 gcd 𝑁) = 1))
8884, 87mpbird 246 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈)
8988ex 449 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) → (((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈))
90 eleq1 2676 . . . . . . . 8 (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥𝐸 ↔ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸))
91 eleq1 2676 . . . . . . . 8 (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥𝑈 ↔ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈))
9290, 91imbi12d 333 . . . . . . 7 (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → ((𝑥𝐸𝑥𝑈) ↔ (((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈)))
9389, 92syl5ibrcom 236 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) → (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥𝐸𝑥𝑈)))
9493rexlimdva 3013 . . . . 5 (𝑁 ∈ ℕ → (∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥𝐸𝑥𝑈)))
9594com23 84 . . . 4 (𝑁 ∈ ℕ → (𝑥𝐸 → (∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛) → 𝑥𝑈)))
9612, 95mpdd 42 . . 3 (𝑁 ∈ ℕ → (𝑥𝐸𝑥𝑈))
9796ssrdv 3574 . 2 (𝑁 ∈ ℕ → 𝐸𝑈)
987, 85unitrrg 19114 . . 3 (𝑌 ∈ Ring → 𝑈𝐸)
9955, 98syl 17 . 2 (𝑁 ∈ ℕ → 𝑈𝐸)
10097, 99eqssd 3585 1 (𝑁 ∈ ℕ → 𝐸 = 𝑈)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∃wrex 2897   ⊆ wss 3540   class class class wbr 4583  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  0cc0 9815  1c1 9816   · cmul 9820   / cdiv 10563  ℕcn 10897  ℕ0cn0 11169  ℤcz 11254   ∥ cdvds 14821   gcd cgcd 15054  Basecbs 15695  .rcmulr 15769  0gc0g 15923  Ringcrg 18370  CRingccrg 18371  Unitcui 18462   RingHom crh 18535  RLRegcrlreg 19100  ℤringzring 19637  ℤRHomczrh 19667  ℤ/nℤczn 19670 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893  ax-addf 9894  ax-mulf 9895 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-tpos 7239  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-ec 7631  df-qs 7635  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-fz 12198  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-dvds 14822  df-gcd 15055  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-0g 15925  df-imas 15991  df-qus 15992  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-mhm 17158  df-grp 17248  df-minusg 17249  df-sbg 17250  df-mulg 17364  df-subg 17414  df-nsg 17415  df-eqg 17416  df-ghm 17481  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-ring 18372  df-cring 18373  df-oppr 18446  df-dvdsr 18464  df-unit 18465  df-invr 18495  df-rnghom 18538  df-subrg 18601  df-lmod 18688  df-lss 18754  df-lsp 18793  df-sra 18993  df-rgmod 18994  df-lidl 18995  df-rsp 18996  df-2idl 19053  df-rlreg 19104  df-cnfld 19568  df-zring 19638  df-zrh 19671  df-zn 19674 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator