| Step | Hyp | Ref
| Expression |
| 1 | | rabdiophlem1 42812 |
. . . 4
⊢ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
→ ∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))𝐴 ∈ ℤ) |
| 2 | | rabdiophlem1 42812 |
. . . 4
⊢ ((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁))
→ ∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))𝐵 ∈ ℤ) |
| 3 | | divides 16292 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∃𝑎 ∈ ℤ (𝑎 · 𝐴) = 𝐵)) |
| 4 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (𝑎 · 𝐴) = (𝑏 · 𝐴)) |
| 5 | 4 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝑎 · 𝐴) = 𝐵 ↔ (𝑏 · 𝐴) = 𝐵)) |
| 6 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑎 = -𝑏 → (𝑎 · 𝐴) = (-𝑏 · 𝐴)) |
| 7 | 6 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑎 = -𝑏 → ((𝑎 · 𝐴) = 𝐵 ↔ (-𝑏 · 𝐴) = 𝐵)) |
| 8 | 5, 7 | rexzrexnn0 42815 |
. . . . . . 7
⊢
(∃𝑎 ∈
ℤ (𝑎 · 𝐴) = 𝐵 ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)) |
| 9 | 3, 8 | bitrdi 287 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵))) |
| 10 | 9 | ralimi 3083 |
. . . . 5
⊢
(∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))(𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∀𝑡 ∈ (ℕ0
↑m (1...𝑁))(𝐴 ∥ 𝐵 ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵))) |
| 11 | | r19.26 3111 |
. . . . 5
⊢
(∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))(𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ↔ (∀𝑡 ∈ (ℕ0
↑m (1...𝑁))𝐴 ∈ ℤ ∧ ∀𝑡 ∈ (ℕ0
↑m (1...𝑁))𝐵 ∈ ℤ)) |
| 12 | | rabbi 3467 |
. . . . 5
⊢
(∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))(𝐴 ∥ 𝐵 ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)) ↔ {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ 𝐴 ∥ 𝐵} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 ((𝑏
· 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)}) |
| 13 | 10, 11, 12 | 3imtr3i 291 |
. . . 4
⊢
((∀𝑡 ∈
(ℕ0 ↑m (1...𝑁))𝐴 ∈ ℤ ∧ ∀𝑡 ∈ (ℕ0
↑m (1...𝑁))𝐵 ∈ ℤ) → {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ 𝐴 ∥ 𝐵} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 ((𝑏
· 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)}) |
| 14 | 1, 2, 13 | syl2an 596 |
. . 3
⊢ (((𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∥ 𝐵} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 ((𝑏
· 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)}) |
| 15 | 14 | 3adant1 1131 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∥ 𝐵} = {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 ((𝑏
· 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)}) |
| 16 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑡(ℕ0 ↑m
(1...𝑁)) |
| 17 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑎(ℕ0 ↑m
(1...𝑁)) |
| 18 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑎∃𝑏 ∈ ℕ0
((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵) |
| 19 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑡ℕ0 |
| 20 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑡𝑏 |
| 21 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑡
· |
| 22 | | nfcsb1v 3923 |
. . . . . . . 8
⊢
Ⅎ𝑡⦋𝑎 / 𝑡⦌𝐴 |
| 23 | 20, 21, 22 | nfov 7461 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑏 · ⦋𝑎 / 𝑡⦌𝐴) |
| 24 | | nfcsb1v 3923 |
. . . . . . 7
⊢
Ⅎ𝑡⦋𝑎 / 𝑡⦌𝐵 |
| 25 | 23, 24 | nfeq 2919 |
. . . . . 6
⊢
Ⅎ𝑡(𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 |
| 26 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑡-𝑏 |
| 27 | 26, 21, 22 | nfov 7461 |
. . . . . . 7
⊢
Ⅎ𝑡(-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) |
| 28 | 27, 24 | nfeq 2919 |
. . . . . 6
⊢
Ⅎ𝑡(-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 |
| 29 | 25, 28 | nfor 1904 |
. . . . 5
⊢
Ⅎ𝑡((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵) |
| 30 | 19, 29 | nfrexw 3313 |
. . . 4
⊢
Ⅎ𝑡∃𝑏 ∈ ℕ0
((𝑏 ·
⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵) |
| 31 | | csbeq1a 3913 |
. . . . . . . 8
⊢ (𝑡 = 𝑎 → 𝐴 = ⦋𝑎 / 𝑡⦌𝐴) |
| 32 | 31 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑡 = 𝑎 → (𝑏 · 𝐴) = (𝑏 · ⦋𝑎 / 𝑡⦌𝐴)) |
| 33 | | csbeq1a 3913 |
. . . . . . 7
⊢ (𝑡 = 𝑎 → 𝐵 = ⦋𝑎 / 𝑡⦌𝐵) |
| 34 | 32, 33 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑡 = 𝑎 → ((𝑏 · 𝐴) = 𝐵 ↔ (𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)) |
| 35 | 31 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑡 = 𝑎 → (-𝑏 · 𝐴) = (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴)) |
| 36 | 35, 33 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑡 = 𝑎 → ((-𝑏 · 𝐴) = 𝐵 ↔ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)) |
| 37 | 34, 36 | orbi12d 919 |
. . . . 5
⊢ (𝑡 = 𝑎 → (((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵) ↔ ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵))) |
| 38 | 37 | rexbidv 3179 |
. . . 4
⊢ (𝑡 = 𝑎 → (∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵) ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵))) |
| 39 | 16, 17, 18, 30, 38 | cbvrabw 3473 |
. . 3
⊢ {𝑡 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 ((𝑏
· 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)} = {𝑎 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 ((𝑏
· ⦋𝑎 /
𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)} |
| 40 | | simp1 1137 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ 𝑁 ∈
ℕ0) |
| 41 | | peano2nn0 12566 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
| 42 | 41 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑁 + 1) ∈
ℕ0) |
| 43 | | ovex 7464 |
. . . . . . . . . 10
⊢
(1...(𝑁 + 1)) ∈
V |
| 44 | | nn0p1nn 12565 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
| 45 | | elfz1end 13594 |
. . . . . . . . . . 11
⊢ ((𝑁 + 1) ∈ ℕ ↔
(𝑁 + 1) ∈ (1...(𝑁 + 1))) |
| 46 | 44, 45 | sylib 218 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(1...(𝑁 +
1))) |
| 47 | | mzpproj 42748 |
. . . . . . . . . 10
⊢
(((1...(𝑁 + 1))
∈ V ∧ (𝑁 + 1)
∈ (1...(𝑁 + 1)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 48 | 43, 46, 47 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 49 | 48 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 50 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑁 + 1) = (𝑁 + 1) |
| 51 | 50 | rabdiophlem2 42813 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 52 | | mzpmulmpt 42753 |
. . . . . . . 8
⊢ (((𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1))) ∧ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) ∈ (mzPoly‘(1...(𝑁 + 1)))) → (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 53 | 49, 51, 52 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 54 | 53 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 55 | 50 | rabdiophlem2 42813 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 56 | 55 | 3adant2 1132 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 57 | | eqrabdioph 42788 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℕ0
∧ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1))) ∧ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵) ∈ (mzPoly‘(1...(𝑁 + 1)))) → {𝑐 ∈ (ℕ0
↑m (1...(𝑁
+ 1))) ∣ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) |
| 58 | 42, 54, 56, 57 | syl3anc 1373 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑐 ∈
(ℕ0 ↑m (1...(𝑁 + 1))) ∣ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) |
| 59 | | mzpnegmpt 42755 |
. . . . . . . . 9
⊢ ((𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1))) → (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ -(𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 60 | 49, 59 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ -(𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 61 | | mzpmulmpt 42753 |
. . . . . . . 8
⊢ (((𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ -(𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1))) ∧ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) ∈ (mzPoly‘(1...(𝑁 + 1)))) → (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 62 | 60, 51, 61 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 63 | 62 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
| 64 | | eqrabdioph 42788 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℕ0
∧ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1))) ∧ (𝑐 ∈ (ℤ
↑m (1...(𝑁
+ 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵) ∈ (mzPoly‘(1...(𝑁 + 1)))) → {𝑐 ∈ (ℕ0
↑m (1...(𝑁
+ 1))) ∣ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) |
| 65 | 42, 63, 56, 64 | syl3anc 1373 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑐 ∈
(ℕ0 ↑m (1...(𝑁 + 1))) ∣ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) |
| 66 | | orrabdioph 42792 |
. . . . 5
⊢ (({𝑐 ∈ (ℕ0
↑m (1...(𝑁
+ 1))) ∣ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1)) ∧ {𝑐 ∈ (ℕ0
↑m (1...(𝑁
+ 1))) ∣ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) → {𝑐 ∈ (ℕ0
↑m (1...(𝑁
+ 1))) ∣ (((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)} ∈ (Dioph‘(𝑁 + 1))) |
| 67 | 58, 65, 66 | syl2anc 584 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑐 ∈
(ℕ0 ↑m (1...(𝑁 + 1))) ∣ (((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)} ∈ (Dioph‘(𝑁 + 1))) |
| 68 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → (𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴)) |
| 69 | 68 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ↔ ((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)) |
| 70 | | negeq 11500 |
. . . . . . . 8
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → -𝑏 = -(𝑐‘(𝑁 + 1))) |
| 71 | 70 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴)) |
| 72 | 71 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → ((-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ↔ (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)) |
| 73 | 69, 72 | orbi12d 919 |
. . . . 5
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → (((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵) ↔ (((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵))) |
| 74 | | csbeq1 3902 |
. . . . . . . 8
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ⦋𝑎 / 𝑡⦌𝐴 = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) |
| 75 | 74 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) |
| 76 | | csbeq1 3902 |
. . . . . . 7
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ⦋𝑎 / 𝑡⦌𝐵 = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵) |
| 77 | 75, 76 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → (((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ↔ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)) |
| 78 | 74 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) |
| 79 | 78, 76 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ((-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ↔ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)) |
| 80 | 77, 79 | orbi12d 919 |
. . . . 5
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ((((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵) ↔ (((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵))) |
| 81 | 50, 73, 80 | rexrabdioph 42805 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ {𝑐 ∈
(ℕ0 ↑m (1...(𝑁 + 1))) ∣ (((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)} ∈ (Dioph‘(𝑁 + 1))) → {𝑎 ∈ (ℕ0
↑m (1...𝑁))
∣ ∃𝑏 ∈
ℕ0 ((𝑏
· ⦋𝑎 /
𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)} ∈ (Dioph‘𝑁)) |
| 82 | 40, 67, 81 | syl2anc 584 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑎 ∈
(ℕ0 ↑m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)} ∈ (Dioph‘𝑁)) |
| 83 | 39, 82 | eqeltrid 2845 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)} ∈ (Dioph‘𝑁)) |
| 84 | 15, 83 | eqeltrd 2841 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐴) ∈
(mzPoly‘(1...𝑁))
∧ (𝑡 ∈ (ℤ
↑m (1...𝑁))
↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑m (1...𝑁)) ∣ 𝐴 ∥ 𝐵} ∈ (Dioph‘𝑁)) |