ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  znrrg GIF version

Theorem znrrg 14125
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 9237 . . . . . . 7 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
2 znchr.y . . . . . . . 8 𝑌 = (ℤ/nℤ‘𝑁)
3 eqid 2193 . . . . . . . 8 (Base‘𝑌) = (Base‘𝑌)
4 eqid 2193 . . . . . . . 8 (ℤRHom‘𝑌) = (ℤRHom‘𝑌)
52, 3, 4znzrhfo 14113 . . . . . . 7 (𝑁 ∈ ℕ0 → (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌))
61, 5syl 14 . . . . . 6 (𝑁 ∈ ℕ → (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌))
7 znrrg.e . . . . . . . 8 𝐸 = (RLReg‘𝑌)
87, 3rrgss 13746 . . . . . . 7 𝐸 ⊆ (Base‘𝑌)
98sseli 3175 . . . . . 6 (𝑥𝐸𝑥 ∈ (Base‘𝑌))
10 foelrn 5787 . . . . . 6 (((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) ∧ 𝑥 ∈ (Base‘𝑌)) → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛))
116, 9, 10syl2an 289 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑥𝐸) → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛))
1211ex 115 . . . 4 (𝑁 ∈ ℕ → (𝑥𝐸 → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛)))
13 nncn 8980 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
1413ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℂ)
15 simplr 528 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑛 ∈ ℤ)
16 nnz 9326 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
1716ad2antrr 488 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℤ)
18 nnne0 9000 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑁 ≠ 0)
1918ad2antrr 488 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ≠ 0)
20 simpr 110 . . . . . . . . . . . . . . . . . . 19 ((𝑛 = 0 ∧ 𝑁 = 0) → 𝑁 = 0)
2120necon3ai 2413 . . . . . . . . . . . . . . . . . 18 (𝑁 ≠ 0 → ¬ (𝑛 = 0 ∧ 𝑁 = 0))
2219, 21syl 14 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ¬ (𝑛 = 0 ∧ 𝑁 = 0))
23 gcdn0cl 12089 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑛 = 0 ∧ 𝑁 = 0)) → (𝑛 gcd 𝑁) ∈ ℕ)
2415, 17, 22, 23syl21anc 1248 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℕ)
2524nncnd 8986 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℂ)
2624nnap0d 9018 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) # 0)
2714, 25, 26divcanap2d 8801 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) = 𝑁)
28 gcddvds 12090 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑛 gcd 𝑁) ∥ 𝑛 ∧ (𝑛 gcd 𝑁) ∥ 𝑁))
2915, 17, 28syl2anc 411 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑛 ∧ (𝑛 gcd 𝑁) ∥ 𝑁))
3029simpld 112 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 𝑛)
3124nnzd 9428 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℤ)
3229simprd 114 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 𝑁)
33 simpll 527 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℕ)
34 nndivdvds 11929 . . . . . . . . . . . . . . . . . . 19 ((𝑁 ∈ ℕ ∧ (𝑛 gcd 𝑁) ∈ ℕ) → ((𝑛 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ))
3533, 24, 34syl2anc 411 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ))
3632, 35mpbid 147 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ)
3736nnzd 9428 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ)
38 dvdsmulc 11952 . . . . . . . . . . . . . . . 16 (((𝑛 gcd 𝑁) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) → ((𝑛 gcd 𝑁) ∥ 𝑛 → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
3931, 15, 37, 38syl3anc 1249 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑛 → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
4030, 39mpd 13 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))
4127, 40eqbrtrrd 4053 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))
42 simpr 110 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸)
431ad2antrr 488 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℕ0)
4443, 5syl 14 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌))
45 fof 5468 . . . . . . . . . . . . . . . . 17 ((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌))
4644, 45syl 14 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌))
4746, 37ffvelcdmd 5686 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) ∈ (Base‘𝑌))
48 eqid 2193 . . . . . . . . . . . . . . . 16 (.r𝑌) = (.r𝑌)
49 eqid 2193 . . . . . . . . . . . . . . . 16 (0g𝑌) = (0g𝑌)
507, 3, 48, 49rrgeq0i 13744 . . . . . . . . . . . . . . 15 ((((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 ∧ ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) ∈ (Base‘𝑌)) → ((((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) → ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g𝑌)))
5142, 47, 50syl2anc 411 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) → ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g𝑌)))
522zncrng 14110 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0𝑌 ∈ CRing)
531, 52syl 14 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ → 𝑌 ∈ CRing)
5453crngringd 13489 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ → 𝑌 ∈ Ring)
5554ad2antrr 488 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑌 ∈ Ring)
564zrhrhm 14088 . . . . . . . . . . . . . . . . . 18 (𝑌 ∈ Ring → (ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌))
5755, 56syl 14 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌))
58 zringbas 14062 . . . . . . . . . . . . . . . . . 18 ℤ = (Base‘ℤring)
59 zringmulr 14065 . . . . . . . . . . . . . . . . . 18 · = (.r‘ℤring)
6058, 59, 48rhmmul 13644 . . . . . . . . . . . . . . . . 17 (((ℤRHom‘𝑌) ∈ (ℤring RingHom 𝑌) ∧ 𝑛 ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) → ((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))))
6157, 15, 37, 60syl3anc 1249 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))))
6261eqeq1d 2202 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) ↔ (((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌)))
6315, 37zmulcld 9435 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) ∈ ℤ)
642, 4, 49zndvds0 14115 . . . . . . . . . . . . . . . 16 ((𝑁 ∈ ℕ0 ∧ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
6543, 63, 64syl2anc 411 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
6662, 65bitr3d 190 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((((ℤRHom‘𝑌)‘𝑛)(.r𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))))
672, 4, 49zndvds0 14115 . . . . . . . . . . . . . . 15 ((𝑁 ∈ ℕ0 ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) → (((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g𝑌) ↔ 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁))))
6843, 37, 67syl2anc 411 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g𝑌) ↔ 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁))))
6951, 66, 683imtr3d 202 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) → 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁))))
7041, 69mpd 13 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁)))
7114, 25, 26divcanap1d 8800 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) = 𝑁)
7236nncnd 8986 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℂ)
7372mulridd 8026 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · 1) = (𝑁 / (𝑛 gcd 𝑁)))
7470, 71, 733brtr4d 4061 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1))
75 1zzd 9334 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 1 ∈ ℤ)
7636nnne0d 9017 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ≠ 0)
77 dvdscmulr 11953 . . . . . . . . . . . 12 (((𝑛 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ ∧ ((𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ≠ 0)) → (((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1) ↔ (𝑛 gcd 𝑁) ∥ 1))
7831, 75, 37, 76, 77syl112anc 1253 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1) ↔ (𝑛 gcd 𝑁) ∥ 1))
7974, 78mpbid 147 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 1)
8015, 17gcdcld 12095 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℕ0)
81 dvds1 11985 . . . . . . . . . . 11 ((𝑛 gcd 𝑁) ∈ ℕ0 → ((𝑛 gcd 𝑁) ∥ 1 ↔ (𝑛 gcd 𝑁) = 1))
8280, 81syl 14 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 1 ↔ (𝑛 gcd 𝑁) = 1))
8379, 82mpbid 147 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) = 1)
84 znunit.u . . . . . . . . . . 11 𝑈 = (Unit‘𝑌)
852, 84, 4znunit 14124 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝑛 ∈ ℤ) → (((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈 ↔ (𝑛 gcd 𝑁) = 1))
8643, 15, 85syl2anc 411 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈 ↔ (𝑛 gcd 𝑁) = 1))
8783, 86mpbird 167 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈)
8887ex 115 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) → (((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈))
89 eleq1 2256 . . . . . . . 8 (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥𝐸 ↔ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸))
90 eleq1 2256 . . . . . . . 8 (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥𝑈 ↔ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈))
9189, 90imbi12d 234 . . . . . . 7 (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → ((𝑥𝐸𝑥𝑈) ↔ (((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈)))
9288, 91syl5ibrcom 157 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) → (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥𝐸𝑥𝑈)))
9392rexlimdva 2611 . . . . 5 (𝑁 ∈ ℕ → (∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥𝐸𝑥𝑈)))
9493com23 78 . . . 4 (𝑁 ∈ ℕ → (𝑥𝐸 → (∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛) → 𝑥𝑈)))
9512, 94mpdd 41 . . 3 (𝑁 ∈ ℕ → (𝑥𝐸𝑥𝑈))
9695ssrdv 3185 . 2 (𝑁 ∈ ℕ → 𝐸𝑈)
977, 84unitrrg 13747 . . 3 (𝑌 ∈ Ring → 𝑈𝐸)
9854, 97syl 14 . 2 (𝑁 ∈ ℕ → 𝑈𝐸)
9996, 98eqssd 3196 1 (𝑁 ∈ ℕ → 𝐸 = 𝑈)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105   = wceq 1364  wcel 2164  wne 2364  wrex 2473  wss 3153   class class class wbr 4029  wf 5242  ontowfo 5244  cfv 5246  (class class class)co 5910  cc 7860  0cc0 7862  1c1 7863   · cmul 7867   / cdiv 8681  cn 8972  0cn0 9230  cz 9307  cdvds 11920   gcd cgcd 12069  Basecbs 12608  .rcmulr 12686  0gc0g 12857  Ringcrg 13476  CRingccrg 13477  Unitcui 13567   RingHom crh 13630  RLRegcrlreg 13735  ringczring 14056  ℤRHomczrh 14076  ℤ/nczn 14078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4462  ax-setind 4565  ax-iinf 4616  ax-cnex 7953  ax-resscn 7954  ax-1cn 7955  ax-1re 7956  ax-icn 7957  ax-addcl 7958  ax-addrcl 7959  ax-mulcl 7960  ax-mulrcl 7961  ax-addcom 7962  ax-mulcom 7963  ax-addass 7964  ax-mulass 7965  ax-distr 7966  ax-i2m1 7967  ax-0lt1 7968  ax-1rid 7969  ax-0id 7970  ax-rnegex 7971  ax-precex 7972  ax-cnre 7973  ax-pre-ltirr 7974  ax-pre-ltwlin 7975  ax-pre-lttrn 7976  ax-pre-apti 7977  ax-pre-ltadd 7978  ax-pre-mulgt0 7979  ax-pre-mulext 7980  ax-arch 7981  ax-caucvg 7982  ax-addf 7984  ax-mulf 7985
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-tp 3626  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4322  df-po 4325  df-iso 4326  df-iord 4395  df-on 4397  df-ilim 4398  df-suc 4400  df-iom 4619  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-iota 5207  df-fun 5248  df-fn 5249  df-f 5250  df-f1 5251  df-fo 5252  df-f1o 5253  df-fv 5254  df-riota 5865  df-ov 5913  df-oprab 5914  df-mpo 5915  df-1st 6184  df-2nd 6185  df-tpos 6289  df-recs 6349  df-frec 6435  df-er 6578  df-ec 6580  df-qs 6584  df-map 6695  df-sup 7033  df-pnf 8046  df-mnf 8047  df-xr 8048  df-ltxr 8049  df-le 8050  df-sub 8182  df-neg 8183  df-reap 8584  df-ap 8591  df-div 8682  df-inn 8973  df-2 9031  df-3 9032  df-4 9033  df-5 9034  df-6 9035  df-7 9036  df-8 9037  df-9 9038  df-n0 9231  df-z 9308  df-dec 9439  df-uz 9583  df-q 9675  df-rp 9710  df-fz 10065  df-fzo 10199  df-fl 10329  df-mod 10384  df-seqfrec 10509  df-exp 10600  df-cj 10976  df-re 10977  df-im 10978  df-rsqrt 11132  df-abs 11133  df-dvds 11921  df-gcd 12070  df-struct 12610  df-ndx 12611  df-slot 12612  df-base 12614  df-sets 12615  df-iress 12616  df-plusg 12698  df-mulr 12699  df-starv 12700  df-sca 12701  df-vsca 12702  df-ip 12703  df-ple 12705  df-0g 12859  df-iimas 12875  df-qus 12876  df-mgm 12929  df-sgrp 12975  df-mnd 12988  df-mhm 13021  df-grp 13065  df-minusg 13066  df-sbg 13067  df-mulg 13180  df-subg 13229  df-nsg 13230  df-eqg 13231  df-ghm 13300  df-cmn 13345  df-abl 13346  df-mgp 13401  df-rng 13413  df-ur 13440  df-srg 13444  df-ring 13478  df-cring 13479  df-oppr 13548  df-dvdsr 13569  df-unit 13570  df-invr 13601  df-rhm 13632  df-subrg 13699  df-rlreg 13738  df-lmod 13769  df-lssm 13833  df-lsp 13867  df-sra 13915  df-rgmod 13916  df-lidl 13949  df-rsp 13950  df-2idl 13980  df-icnfld 14032  df-zring 14057  df-zrh 14079  df-zn 14081
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator