| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnnn0 12533 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 2 |  | znchr.y | . . . . . . . 8
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) | 
| 3 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘𝑌) =
(Base‘𝑌) | 
| 4 |  | eqid 2737 | . . . . . . . 8
⊢
(ℤRHom‘𝑌) = (ℤRHom‘𝑌) | 
| 5 | 2, 3, 4 | znzrhfo 21566 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌)) | 
| 6 | 1, 5 | syl 17 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌)) | 
| 7 |  | znrrg.e | . . . . . . . 8
⊢ 𝐸 = (RLReg‘𝑌) | 
| 8 | 7, 3 | rrgss 20702 | . . . . . . 7
⊢ 𝐸 ⊆ (Base‘𝑌) | 
| 9 | 8 | sseli 3979 | . . . . . 6
⊢ (𝑥 ∈ 𝐸 → 𝑥 ∈ (Base‘𝑌)) | 
| 10 |  | foelrn 7127 | . . . . . 6
⊢
(((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) ∧ 𝑥 ∈ (Base‘𝑌)) → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛)) | 
| 11 | 6, 9, 10 | syl2an 596 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐸) → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛)) | 
| 12 | 11 | ex 412 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝐸 → ∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛))) | 
| 13 |  | nncn 12274 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 14 | 13 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℂ) | 
| 15 |  | simplr 769 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑛 ∈ ℤ) | 
| 16 |  | nnz 12634 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 17 | 16 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℤ) | 
| 18 |  | nnne0 12300 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) | 
| 19 | 18 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ≠ 0) | 
| 20 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) | 
| 21 | 20 | necon3ai 2965 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ≠ 0 → ¬ (𝑛 = 0 ∧ 𝑁 = 0)) | 
| 22 | 19, 21 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ¬ (𝑛 = 0 ∧ 𝑁 = 0)) | 
| 23 |  | gcdn0cl 16539 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑛 = 0 ∧ 𝑁 = 0)) → (𝑛 gcd 𝑁) ∈ ℕ) | 
| 24 | 15, 17, 22, 23 | syl21anc 838 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℕ) | 
| 25 | 24 | nncnd 12282 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℂ) | 
| 26 | 24 | nnne0d 12316 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ≠ 0) | 
| 27 | 14, 25, 26 | divcan2d 12045 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) = 𝑁) | 
| 28 |  | gcddvds 16540 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑛 gcd 𝑁) ∥ 𝑛 ∧ (𝑛 gcd 𝑁) ∥ 𝑁)) | 
| 29 | 15, 17, 28 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑛 ∧ (𝑛 gcd 𝑁) ∥ 𝑁)) | 
| 30 | 29 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 𝑛) | 
| 31 | 24 | nnzd 12640 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈ ℤ) | 
| 32 | 29 | simprd 495 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 𝑁) | 
| 33 |  | simpll 767 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈ ℕ) | 
| 34 |  | nndivdvds 16299 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℕ ∧ (𝑛 gcd 𝑁) ∈ ℕ) → ((𝑛 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ)) | 
| 35 | 33, 24, 34 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑁 ↔ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ)) | 
| 36 | 32, 35 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℕ) | 
| 37 | 36 | nnzd 12640 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) | 
| 38 |  | dvdsmulc 16321 | . . . . . . . . . . . . . . . 16
⊢ (((𝑛 gcd 𝑁) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) → ((𝑛 gcd 𝑁) ∥ 𝑛 → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) | 
| 39 | 31, 15, 37, 38 | syl3anc 1373 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 𝑛 → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) | 
| 40 | 30, 39 | mpd 15 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) · (𝑁 / (𝑛 gcd 𝑁))) ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) | 
| 41 | 27, 40 | eqbrtrrd 5167 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) | 
| 42 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) | 
| 43 | 1 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∈
ℕ0) | 
| 44 | 43, 5 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌)) | 
| 45 |  | fof 6820 | . . . . . . . . . . . . . . . . 17
⊢
((ℤRHom‘𝑌):ℤ–onto→(Base‘𝑌) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌)) | 
| 46 | 44, 45 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌):ℤ⟶(Base‘𝑌)) | 
| 47 | 46, 37 | ffvelcdmd 7105 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) ∈ (Base‘𝑌)) | 
| 48 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(.r‘𝑌) = (.r‘𝑌) | 
| 49 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢
(0g‘𝑌) = (0g‘𝑌) | 
| 50 | 7, 3, 48, 49 | rrgeq0i 20699 | . . . . . . . . . . . . . . 15
⊢
((((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 ∧ ((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) ∈ (Base‘𝑌)) → ((((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) →
((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g‘𝑌))) | 
| 51 | 42, 47, 50 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) →
((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g‘𝑌))) | 
| 52 | 2 | zncrng 21563 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) | 
| 53 | 1, 52 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ CRing) | 
| 54 |  | crngring 20242 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) | 
| 55 | 53, 54 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑌 ∈ Ring) | 
| 56 | 55 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑌 ∈ Ring) | 
| 57 | 4 | zrhrhm 21522 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑌 ∈ Ring →
(ℤRHom‘𝑌)
∈ (ℤring RingHom 𝑌)) | 
| 58 | 56, 57 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (ℤRHom‘𝑌) ∈ (ℤring
RingHom 𝑌)) | 
| 59 |  | zringbas 21464 | . . . . . . . . . . . . . . . . . 18
⊢ ℤ =
(Base‘ℤring) | 
| 60 |  | zringmulr 21468 | . . . . . . . . . . . . . . . . . 18
⊢  ·
= (.r‘ℤring) | 
| 61 | 59, 60, 48 | rhmmul 20486 | . . . . . . . . . . . . . . . . 17
⊢
(((ℤRHom‘𝑌) ∈ (ℤring RingHom
𝑌) ∧ 𝑛 ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) →
((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))))) | 
| 62 | 58, 15, 37, 61 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))))) | 
| 63 | 62 | eqeq1d 2739 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) ↔
(((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌))) | 
| 64 | 15, 37 | zmulcld 12728 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) ∈ ℤ) | 
| 65 | 2, 4, 49 | zndvds0 21569 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) | 
| 66 | 43, 64, 65 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑛 · (𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) | 
| 67 | 63, 66 | bitr3d 281 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((((ℤRHom‘𝑌)‘𝑛)(.r‘𝑌)((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁)))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))))) | 
| 68 | 2, 4, 49 | zndvds0 21569 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ) →
(((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁)))) | 
| 69 | 43, 37, 68 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘(𝑁 / (𝑛 gcd 𝑁))) = (0g‘𝑌) ↔ 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁)))) | 
| 70 | 51, 67, 69 | 3imtr3d 293 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 ∥ (𝑛 · (𝑁 / (𝑛 gcd 𝑁))) → 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁)))) | 
| 71 | 41, 70 | mpd 15 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 𝑁 ∥ (𝑁 / (𝑛 gcd 𝑁))) | 
| 72 | 14, 25, 26 | divcan1d 12044 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) = 𝑁) | 
| 73 | 36 | nncnd 12282 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ∈ ℂ) | 
| 74 | 73 | mulridd 11278 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · 1) = (𝑁 / (𝑛 gcd 𝑁))) | 
| 75 | 71, 72, 74 | 3brtr4d 5175 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1)) | 
| 76 |  | 1zzd 12648 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → 1 ∈ ℤ) | 
| 77 | 36 | nnne0d 12316 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑁 / (𝑛 gcd 𝑁)) ≠ 0) | 
| 78 |  | dvdscmulr 16322 | . . . . . . . . . . . 12
⊢ (((𝑛 gcd 𝑁) ∈ ℤ ∧ 1 ∈ ℤ
∧ ((𝑁 / (𝑛 gcd 𝑁)) ∈ ℤ ∧ (𝑁 / (𝑛 gcd 𝑁)) ≠ 0)) → (((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1) ↔ (𝑛 gcd 𝑁) ∥ 1)) | 
| 79 | 31, 76, 37, 77, 78 | syl112anc 1376 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((𝑁 / (𝑛 gcd 𝑁)) · (𝑛 gcd 𝑁)) ∥ ((𝑁 / (𝑛 gcd 𝑁)) · 1) ↔ (𝑛 gcd 𝑁) ∥ 1)) | 
| 80 | 75, 79 | mpbid 232 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∥ 1) | 
| 81 | 15, 17 | gcdcld 16545 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) ∈
ℕ0) | 
| 82 |  | dvds1 16356 | . . . . . . . . . . 11
⊢ ((𝑛 gcd 𝑁) ∈ ℕ0 → ((𝑛 gcd 𝑁) ∥ 1 ↔ (𝑛 gcd 𝑁) = 1)) | 
| 83 | 81, 82 | syl 17 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((𝑛 gcd 𝑁) ∥ 1 ↔ (𝑛 gcd 𝑁) = 1)) | 
| 84 | 80, 83 | mpbid 232 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (𝑛 gcd 𝑁) = 1) | 
| 85 |  | znunit.u | . . . . . . . . . . 11
⊢ 𝑈 = (Unit‘𝑌) | 
| 86 | 2, 85, 4 | znunit 21582 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈ ℤ)
→ (((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈 ↔ (𝑛 gcd 𝑁) = 1)) | 
| 87 | 43, 15, 86 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → (((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈 ↔ (𝑛 gcd 𝑁) = 1)) | 
| 88 | 84, 87 | mpbird 257 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) ∧
((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸) → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈) | 
| 89 | 88 | ex 412 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) →
(((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈)) | 
| 90 |  | eleq1 2829 | . . . . . . . 8
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥 ∈ 𝐸 ↔ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸)) | 
| 91 |  | eleq1 2829 | . . . . . . . 8
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥 ∈ 𝑈 ↔ ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈)) | 
| 92 | 90, 91 | imbi12d 344 | . . . . . . 7
⊢ (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → ((𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈) ↔ (((ℤRHom‘𝑌)‘𝑛) ∈ 𝐸 → ((ℤRHom‘𝑌)‘𝑛) ∈ 𝑈))) | 
| 93 | 89, 92 | syl5ibrcom 247 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑛 ∈ ℤ) → (𝑥 = ((ℤRHom‘𝑌)‘𝑛) → (𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈))) | 
| 94 | 93 | rexlimdva 3155 | . . . . 5
⊢ (𝑁 ∈ ℕ →
(∃𝑛 ∈ ℤ
𝑥 =
((ℤRHom‘𝑌)‘𝑛) → (𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈))) | 
| 95 | 94 | com23 86 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝐸 → (∃𝑛 ∈ ℤ 𝑥 = ((ℤRHom‘𝑌)‘𝑛) → 𝑥 ∈ 𝑈))) | 
| 96 | 12, 95 | mpdd 43 | . . 3
⊢ (𝑁 ∈ ℕ → (𝑥 ∈ 𝐸 → 𝑥 ∈ 𝑈)) | 
| 97 | 96 | ssrdv 3989 | . 2
⊢ (𝑁 ∈ ℕ → 𝐸 ⊆ 𝑈) | 
| 98 | 7, 85 | unitrrg 20703 | . . 3
⊢ (𝑌 ∈ Ring → 𝑈 ⊆ 𝐸) | 
| 99 | 55, 98 | syl 17 | . 2
⊢ (𝑁 ∈ ℕ → 𝑈 ⊆ 𝐸) | 
| 100 | 97, 99 | eqssd 4001 | 1
⊢ (𝑁 ∈ ℕ → 𝐸 = 𝑈) |