| Step | Hyp | Ref
| Expression |
| 1 | | znchr.y |
. . . . 5
⊢ 𝑌 =
(ℤ/nℤ‘𝑁) |
| 2 | 1 | zncrng 21563 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑌 ∈
CRing) |
| 3 | 2 | adantr 480 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ 𝑌 ∈
CRing) |
| 4 | | znunit.u |
. . . 4
⊢ 𝑈 = (Unit‘𝑌) |
| 5 | | eqid 2737 |
. . . 4
⊢
(1r‘𝑌) = (1r‘𝑌) |
| 6 | | eqid 2737 |
. . . 4
⊢
(∥r‘𝑌) = (∥r‘𝑌) |
| 7 | 4, 5, 6 | crngunit 20378 |
. . 3
⊢ (𝑌 ∈ CRing → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐿‘𝐴)(∥r‘𝑌)(1r‘𝑌))) |
| 8 | 3, 7 | syl 17 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐿‘𝐴)(∥r‘𝑌)(1r‘𝑌))) |
| 9 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑌) =
(Base‘𝑌) |
| 10 | | znunit.l |
. . . . . . 7
⊢ 𝐿 = (ℤRHom‘𝑌) |
| 11 | 1, 9, 10 | znzrhfo 21566 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑌)) |
| 12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ 𝐿:ℤ–onto→(Base‘𝑌)) |
| 13 | | fof 6820 |
. . . . 5
⊢ (𝐿:ℤ–onto→(Base‘𝑌) → 𝐿:ℤ⟶(Base‘𝑌)) |
| 14 | 12, 13 | syl 17 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ 𝐿:ℤ⟶(Base‘𝑌)) |
| 15 | | ffvelcdm 7101 |
. . . 4
⊢ ((𝐿:ℤ⟶(Base‘𝑌) ∧ 𝐴 ∈ ℤ) → (𝐿‘𝐴) ∈ (Base‘𝑌)) |
| 16 | 14, 15 | sylancom 588 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (𝐿‘𝐴) ∈ (Base‘𝑌)) |
| 17 | | eqid 2737 |
. . . 4
⊢
(.r‘𝑌) = (.r‘𝑌) |
| 18 | 9, 6, 17 | dvdsr2 20363 |
. . 3
⊢ ((𝐿‘𝐴) ∈ (Base‘𝑌) → ((𝐿‘𝐴)(∥r‘𝑌)(1r‘𝑌) ↔ ∃𝑥 ∈ (Base‘𝑌)(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌))) |
| 19 | 16, 18 | syl 17 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ ((𝐿‘𝐴)(∥r‘𝑌)(1r‘𝑌) ↔ ∃𝑥 ∈ (Base‘𝑌)(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌))) |
| 20 | | forn 6823 |
. . . . . 6
⊢ (𝐿:ℤ–onto→(Base‘𝑌) → ran 𝐿 = (Base‘𝑌)) |
| 21 | 12, 20 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ ran 𝐿 =
(Base‘𝑌)) |
| 22 | 21 | rexeqdv 3327 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (∃𝑥 ∈ ran
𝐿(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑥 ∈ (Base‘𝑌)(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌))) |
| 23 | | ffn 6736 |
. . . . 5
⊢ (𝐿:ℤ⟶(Base‘𝑌) → 𝐿 Fn ℤ) |
| 24 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = (𝐿‘𝑛) → (𝑥(.r‘𝑌)(𝐿‘𝐴)) = ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴))) |
| 25 | 24 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑥 = (𝐿‘𝑛) → ((𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌))) |
| 26 | 25 | rexrn 7107 |
. . . . 5
⊢ (𝐿 Fn ℤ → (∃𝑥 ∈ ran 𝐿(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑛 ∈ ℤ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌))) |
| 27 | 14, 23, 26 | 3syl 18 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (∃𝑥 ∈ ran
𝐿(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑛 ∈ ℤ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌))) |
| 28 | 22, 27 | bitr3d 281 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (∃𝑥 ∈
(Base‘𝑌)(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑛 ∈ ℤ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌))) |
| 29 | | crngring 20242 |
. . . . . . . . . 10
⊢ (𝑌 ∈ CRing → 𝑌 ∈ Ring) |
| 30 | 3, 29 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ 𝑌 ∈
Ring) |
| 31 | 10 | zrhrhm 21522 |
. . . . . . . . 9
⊢ (𝑌 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑌)) |
| 32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ 𝐿 ∈
(ℤring RingHom 𝑌)) |
| 33 | 32 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ 𝐿 ∈
(ℤring RingHom 𝑌)) |
| 34 | | simpr 484 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ 𝑛 ∈
ℤ) |
| 35 | | simplr 769 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ 𝐴 ∈
ℤ) |
| 36 | | zringbas 21464 |
. . . . . . . 8
⊢ ℤ =
(Base‘ℤring) |
| 37 | | zringmulr 21468 |
. . . . . . . 8
⊢ ·
= (.r‘ℤring) |
| 38 | 36, 37, 17 | rhmmul 20486 |
. . . . . . 7
⊢ ((𝐿 ∈ (ℤring
RingHom 𝑌) ∧ 𝑛 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐿‘(𝑛 · 𝐴)) = ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴))) |
| 39 | 33, 34, 35, 38 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ (𝐿‘(𝑛 · 𝐴)) = ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴))) |
| 40 | 30 | adantr 480 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ 𝑌 ∈
Ring) |
| 41 | 10, 5 | zrh1 21523 |
. . . . . . 7
⊢ (𝑌 ∈ Ring → (𝐿‘1) =
(1r‘𝑌)) |
| 42 | 40, 41 | syl 17 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ (𝐿‘1) =
(1r‘𝑌)) |
| 43 | 39, 42 | eqeq12d 2753 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ ((𝐿‘(𝑛 · 𝐴)) = (𝐿‘1) ↔ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌))) |
| 44 | | simpll 767 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ 𝑁 ∈
ℕ0) |
| 45 | 34, 35 | zmulcld 12728 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ (𝑛 · 𝐴) ∈
ℤ) |
| 46 | | 1zzd 12648 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ 1 ∈ ℤ) |
| 47 | 1, 10 | zndvds 21568 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑛 · 𝐴) ∈ ℤ ∧ 1 ∈
ℤ) → ((𝐿‘(𝑛 · 𝐴)) = (𝐿‘1) ↔ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) |
| 48 | 44, 45, 46, 47 | syl3anc 1373 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ ((𝐿‘(𝑛 · 𝐴)) = (𝐿‘1) ↔ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) |
| 49 | 43, 48 | bitr3d 281 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ (((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) |
| 50 | 49 | rexbidva 3177 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (∃𝑛 ∈
ℤ ((𝐿‘𝑛)(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ ∃𝑛 ∈ ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) |
| 51 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 𝐴 ∈ ℤ) |
| 52 | | nn0z 12638 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 53 | 52 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 𝑁 ∈ ℤ) |
| 54 | | gcddvds 16540 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 gcd 𝑁) ∥ 𝐴 ∧ (𝐴 gcd 𝑁) ∥ 𝑁)) |
| 55 | 51, 53, 54 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝐴 gcd 𝑁) ∥ 𝐴 ∧ (𝐴 gcd 𝑁) ∥ 𝑁)) |
| 56 | 55 | simpld 494 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ 𝐴) |
| 57 | 51, 53 | gcdcld 16545 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∈
ℕ0) |
| 58 | 57 | nn0zd 12639 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∈ ℤ) |
| 59 | 34 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 𝑛 ∈ ℤ) |
| 60 | | dvdsmultr2 16335 |
. . . . . . . . 9
⊢ (((𝐴 gcd 𝑁) ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 gcd 𝑁) ∥ 𝐴 → (𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴))) |
| 61 | 58, 59, 51, 60 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝐴 gcd 𝑁) ∥ 𝐴 → (𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴))) |
| 62 | 56, 61 | mpd 15 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴)) |
| 63 | 45 | adantrr 717 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝑛 · 𝐴) ∈ ℤ) |
| 64 | | 1zzd 12648 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 1 ∈
ℤ) |
| 65 | | peano2zm 12660 |
. . . . . . . . . 10
⊢ ((𝑛 · 𝐴) ∈ ℤ → ((𝑛 · 𝐴) − 1) ∈
ℤ) |
| 66 | 63, 65 | syl 17 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝑛 · 𝐴) − 1) ∈
ℤ) |
| 67 | 55 | simprd 495 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ 𝑁) |
| 68 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → 𝑁 ∥ ((𝑛 · 𝐴) − 1)) |
| 69 | 58, 53, 66, 67, 68 | dvdstrd 16332 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ ((𝑛 · 𝐴) − 1)) |
| 70 | | dvdssub2 16338 |
. . . . . . . 8
⊢ ((((𝐴 gcd 𝑁) ∈ ℤ ∧ (𝑛 · 𝐴) ∈ ℤ ∧ 1 ∈ ℤ)
∧ (𝐴 gcd 𝑁) ∥ ((𝑛 · 𝐴) − 1)) → ((𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴) ↔ (𝐴 gcd 𝑁) ∥ 1)) |
| 71 | 58, 63, 64, 69, 70 | syl31anc 1375 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝐴 gcd 𝑁) ∥ (𝑛 · 𝐴) ↔ (𝐴 gcd 𝑁) ∥ 1)) |
| 72 | 62, 71 | mpbid 232 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) ∥ 1) |
| 73 | | dvds1 16356 |
. . . . . . 7
⊢ ((𝐴 gcd 𝑁) ∈ ℕ0 → ((𝐴 gcd 𝑁) ∥ 1 ↔ (𝐴 gcd 𝑁) = 1)) |
| 74 | 57, 73 | syl 17 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → ((𝐴 gcd 𝑁) ∥ 1 ↔ (𝐴 gcd 𝑁) = 1)) |
| 75 | 72, 74 | mpbid 232 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ (𝑛 ∈ ℤ
∧ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) → (𝐴 gcd 𝑁) = 1) |
| 76 | 75 | rexlimdvaa 3156 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (∃𝑛 ∈
ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1) → (𝐴 gcd 𝑁) = 1)) |
| 77 | | simpr 484 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ 𝐴 ∈
ℤ) |
| 78 | 52 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ 𝑁 ∈
ℤ) |
| 79 | | bezout 16580 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
∃𝑛 ∈ ℤ
∃𝑚 ∈ ℤ
(𝐴 gcd 𝑁) = ((𝐴 · 𝑛) + (𝑁 · 𝑚))) |
| 80 | 77, 78, 79 | syl2anc 584 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ ∃𝑛 ∈
ℤ ∃𝑚 ∈
ℤ (𝐴 gcd 𝑁) = ((𝐴 · 𝑛) + (𝑁 · 𝑚))) |
| 81 | | eqeq1 2741 |
. . . . . . 7
⊢ ((𝐴 gcd 𝑁) = 1 → ((𝐴 gcd 𝑁) = ((𝐴 · 𝑛) + (𝑁 · 𝑚)) ↔ 1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚)))) |
| 82 | 81 | 2rexbidv 3222 |
. . . . . 6
⊢ ((𝐴 gcd 𝑁) = 1 → (∃𝑛 ∈ ℤ ∃𝑚 ∈ ℤ (𝐴 gcd 𝑁) = ((𝐴 · 𝑛) + (𝑁 · 𝑚)) ↔ ∃𝑛 ∈ ℤ ∃𝑚 ∈ ℤ 1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚)))) |
| 83 | 80, 82 | syl5ibcom 245 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ ((𝐴 gcd 𝑁) = 1 → ∃𝑛 ∈ ℤ ∃𝑚 ∈ ℤ 1 = ((𝐴 · 𝑛) + (𝑁 · 𝑚)))) |
| 84 | 52 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ 𝑁 ∈
ℤ) |
| 85 | | dvdsmul1 16315 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → 𝑁 ∥ (𝑁 · 𝑚)) |
| 86 | 84, 85 | sylancom 588 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ 𝑁 ∥ (𝑁 · 𝑚)) |
| 87 | | zmulcl 12666 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑁 · 𝑚) ∈ ℤ) |
| 88 | 84, 87 | sylancom 588 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ (𝑁 · 𝑚) ∈
ℤ) |
| 89 | | dvdsnegb 16311 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 · 𝑚) ∈ ℤ) → (𝑁 ∥ (𝑁 · 𝑚) ↔ 𝑁 ∥ -(𝑁 · 𝑚))) |
| 90 | 84, 88, 89 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ (𝑁 ∥ (𝑁 · 𝑚) ↔ 𝑁 ∥ -(𝑁 · 𝑚))) |
| 91 | 86, 90 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ 𝑁 ∥ -(𝑁 · 𝑚)) |
| 92 | 35 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ 𝐴 ∈
ℤ) |
| 93 | 92 | zcnd 12723 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ 𝐴 ∈
ℂ) |
| 94 | | zcn 12618 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
| 95 | 94 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ 𝑛 ∈
ℂ) |
| 96 | 93, 95 | mulcomd 11282 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ (𝐴 · 𝑛) = (𝑛 · 𝐴)) |
| 97 | 96 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ ((𝐴 · 𝑛) + (𝑁 · 𝑚)) = ((𝑛 · 𝐴) + (𝑁 · 𝑚))) |
| 98 | 95, 93 | mulcld 11281 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ (𝑛 · 𝐴) ∈
ℂ) |
| 99 | 88 | zcnd 12723 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ (𝑁 · 𝑚) ∈
ℂ) |
| 100 | 98, 99 | subnegd 11627 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ ((𝑛 · 𝐴) − -(𝑁 · 𝑚)) = ((𝑛 · 𝐴) + (𝑁 · 𝑚))) |
| 101 | 97, 100 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ ((𝐴 · 𝑛) + (𝑁 · 𝑚)) = ((𝑛 · 𝐴) − -(𝑁 · 𝑚))) |
| 102 | 101 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚))) = ((𝑛 · 𝐴) − ((𝑛 · 𝐴) − -(𝑁 · 𝑚)))) |
| 103 | 99 | negcld 11607 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ -(𝑁 · 𝑚) ∈
ℂ) |
| 104 | 98, 103 | nncand 11625 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ ((𝑛 · 𝐴) − ((𝑛 · 𝐴) − -(𝑁 · 𝑚))) = -(𝑁 · 𝑚)) |
| 105 | 102, 104 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚))) = -(𝑁 · 𝑚)) |
| 106 | 91, 105 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ 𝑁 ∥ ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚)))) |
| 107 | | oveq2 7439 |
. . . . . . . . 9
⊢ (1 =
((𝐴 · 𝑛) + (𝑁 · 𝑚)) → ((𝑛 · 𝐴) − 1) = ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚)))) |
| 108 | 107 | breq2d 5155 |
. . . . . . . 8
⊢ (1 =
((𝐴 · 𝑛) + (𝑁 · 𝑚)) → (𝑁 ∥ ((𝑛 · 𝐴) − 1) ↔ 𝑁 ∥ ((𝑛 · 𝐴) − ((𝐴 · 𝑛) + (𝑁 · 𝑚))))) |
| 109 | 106, 108 | syl5ibrcom 247 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
∧ 𝑚 ∈ ℤ)
→ (1 = ((𝐴 ·
𝑛) + (𝑁 · 𝑚)) → 𝑁 ∥ ((𝑛 · 𝐴) − 1))) |
| 110 | 109 | rexlimdva 3155 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
∧ 𝑛 ∈ ℤ)
→ (∃𝑚 ∈
ℤ 1 = ((𝐴 ·
𝑛) + (𝑁 · 𝑚)) → 𝑁 ∥ ((𝑛 · 𝐴) − 1))) |
| 111 | 110 | reximdva 3168 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (∃𝑛 ∈
ℤ ∃𝑚 ∈
ℤ 1 = ((𝐴 ·
𝑛) + (𝑁 · 𝑚)) → ∃𝑛 ∈ ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) |
| 112 | 83, 111 | syld 47 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ ((𝐴 gcd 𝑁) = 1 → ∃𝑛 ∈ ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1))) |
| 113 | 76, 112 | impbid 212 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (∃𝑛 ∈
ℤ 𝑁 ∥ ((𝑛 · 𝐴) − 1) ↔ (𝐴 gcd 𝑁) = 1)) |
| 114 | 28, 50, 113 | 3bitrd 305 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ (∃𝑥 ∈
(Base‘𝑌)(𝑥(.r‘𝑌)(𝐿‘𝐴)) = (1r‘𝑌) ↔ (𝐴 gcd 𝑁) = 1)) |
| 115 | 8, 19, 114 | 3bitrd 305 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐴 ∈ ℤ)
→ ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐴 gcd 𝑁) = 1)) |