Step | Hyp | Ref
| Expression |
1 | | rabdiophlem1 38835 |
. . . 4
⊢ ((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → ∀𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))𝐴 ∈ ℤ) |
2 | | rabdiophlem1 38835 |
. . . 4
⊢ ((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁)) → ∀𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))𝐵 ∈ ℤ) |
3 | | divides 15475 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∃𝑎 ∈ ℤ (𝑎 · 𝐴) = 𝐵)) |
4 | | oveq1 6989 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (𝑎 · 𝐴) = (𝑏 · 𝐴)) |
5 | 4 | eqeq1d 2782 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝑎 · 𝐴) = 𝐵 ↔ (𝑏 · 𝐴) = 𝐵)) |
6 | | oveq1 6989 |
. . . . . . . . 9
⊢ (𝑎 = -𝑏 → (𝑎 · 𝐴) = (-𝑏 · 𝐴)) |
7 | 6 | eqeq1d 2782 |
. . . . . . . 8
⊢ (𝑎 = -𝑏 → ((𝑎 · 𝐴) = 𝐵 ↔ (-𝑏 · 𝐴) = 𝐵)) |
8 | 5, 7 | rexzrexnn0 38838 |
. . . . . . 7
⊢
(∃𝑎 ∈
ℤ (𝑎 · 𝐴) = 𝐵 ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)) |
9 | 3, 8 | syl6bb 279 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵))) |
10 | 9 | ralimi 3112 |
. . . . 5
⊢
(∀𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))(𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∀𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))(𝐴 ∥ 𝐵 ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵))) |
11 | | r19.26 3122 |
. . . . 5
⊢
(∀𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))(𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ↔ (∀𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))𝐴 ∈ ℤ ∧ ∀𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))𝐵 ∈ ℤ)) |
12 | | rabbi 3324 |
. . . . 5
⊢
(∀𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))(𝐴 ∥ 𝐵 ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)) ↔ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ 𝐴 ∥ 𝐵} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)}) |
13 | 10, 11, 12 | 3imtr3i 283 |
. . . 4
⊢
((∀𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁))𝐴 ∈ ℤ ∧ ∀𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁))𝐵 ∈ ℤ) → {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ 𝐴 ∥ 𝐵} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)}) |
14 | 1, 2, 13 | syl2an 587 |
. . 3
⊢ (((𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∥ 𝐵} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)}) |
15 | 14 | 3adant1 1111 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∥ 𝐵} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)}) |
16 | | nfcv 2934 |
. . . 4
⊢
Ⅎ𝑡(ℕ0
↑𝑚 (1...𝑁)) |
17 | | nfcv 2934 |
. . . 4
⊢
Ⅎ𝑎(ℕ0
↑𝑚 (1...𝑁)) |
18 | | nfv 1874 |
. . . 4
⊢
Ⅎ𝑎∃𝑏 ∈ ℕ0
((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵) |
19 | | nfcv 2934 |
. . . . 5
⊢
Ⅎ𝑡ℕ0 |
20 | | nfcv 2934 |
. . . . . . . 8
⊢
Ⅎ𝑡𝑏 |
21 | | nfcv 2934 |
. . . . . . . 8
⊢
Ⅎ𝑡
· |
22 | | nfcsb1v 3806 |
. . . . . . . 8
⊢
Ⅎ𝑡⦋𝑎 / 𝑡⦌𝐴 |
23 | 20, 21, 22 | nfov 7012 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑏 · ⦋𝑎 / 𝑡⦌𝐴) |
24 | | nfcsb1v 3806 |
. . . . . . 7
⊢
Ⅎ𝑡⦋𝑎 / 𝑡⦌𝐵 |
25 | 23, 24 | nfeq 2945 |
. . . . . 6
⊢
Ⅎ𝑡(𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 |
26 | | nfcv 2934 |
. . . . . . . 8
⊢
Ⅎ𝑡-𝑏 |
27 | 26, 21, 22 | nfov 7012 |
. . . . . . 7
⊢
Ⅎ𝑡(-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) |
28 | 27, 24 | nfeq 2945 |
. . . . . 6
⊢
Ⅎ𝑡(-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 |
29 | 25, 28 | nfor 1868 |
. . . . 5
⊢
Ⅎ𝑡((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵) |
30 | 19, 29 | nfrex 3255 |
. . . 4
⊢
Ⅎ𝑡∃𝑏 ∈ ℕ0
((𝑏 ·
⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵) |
31 | | csbeq1a 3797 |
. . . . . . . 8
⊢ (𝑡 = 𝑎 → 𝐴 = ⦋𝑎 / 𝑡⦌𝐴) |
32 | 31 | oveq2d 6998 |
. . . . . . 7
⊢ (𝑡 = 𝑎 → (𝑏 · 𝐴) = (𝑏 · ⦋𝑎 / 𝑡⦌𝐴)) |
33 | | csbeq1a 3797 |
. . . . . . 7
⊢ (𝑡 = 𝑎 → 𝐵 = ⦋𝑎 / 𝑡⦌𝐵) |
34 | 32, 33 | eqeq12d 2795 |
. . . . . 6
⊢ (𝑡 = 𝑎 → ((𝑏 · 𝐴) = 𝐵 ↔ (𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)) |
35 | 31 | oveq2d 6998 |
. . . . . . 7
⊢ (𝑡 = 𝑎 → (-𝑏 · 𝐴) = (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴)) |
36 | 35, 33 | eqeq12d 2795 |
. . . . . 6
⊢ (𝑡 = 𝑎 → ((-𝑏 · 𝐴) = 𝐵 ↔ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)) |
37 | 34, 36 | orbi12d 903 |
. . . . 5
⊢ (𝑡 = 𝑎 → (((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵) ↔ ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵))) |
38 | 37 | rexbidv 3244 |
. . . 4
⊢ (𝑡 = 𝑎 → (∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵) ↔ ∃𝑏 ∈ ℕ0 ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵))) |
39 | 16, 17, 18, 30, 38 | cbvrab 3413 |
. . 3
⊢ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)} = {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)} |
40 | | simp1 1117 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ 𝑁 ∈
ℕ0) |
41 | | peano2nn0 11755 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
42 | 41 | 3ad2ant1 1114 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑁 + 1) ∈
ℕ0) |
43 | | ovex 7014 |
. . . . . . . . . 10
⊢
(1...(𝑁 + 1)) ∈
V |
44 | | nn0p1nn 11754 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
45 | | elfz1end 12759 |
. . . . . . . . . . 11
⊢ ((𝑁 + 1) ∈ ℕ ↔
(𝑁 + 1) ∈ (1...(𝑁 + 1))) |
46 | 44, 45 | sylib 210 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(1...(𝑁 +
1))) |
47 | | mzpproj 38770 |
. . . . . . . . . 10
⊢
(((1...(𝑁 + 1))
∈ V ∧ (𝑁 + 1)
∈ (1...(𝑁 + 1)))
→ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
48 | 43, 46, 47 | sylancr 579 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
49 | 48 | adantr 473 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑐 ∈ (ℤ ↑𝑚
(1...(𝑁 + 1))) ↦
(𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
50 | | eqid 2780 |
. . . . . . . . 9
⊢ (𝑁 + 1) = (𝑁 + 1) |
51 | 50 | rabdiophlem2 38836 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑐 ∈ (ℤ ↑𝑚
(1...(𝑁 + 1))) ↦
⦋(𝑐 ↾
(1...𝑁)) / 𝑡⦌𝐴) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
52 | | mzpmulmpt 38775 |
. . . . . . . 8
⊢ (((𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1))) ∧ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) ∈ (mzPoly‘(1...(𝑁 + 1)))) → (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
53 | 49, 51, 52 | syl2anc 576 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑐 ∈ (ℤ ↑𝑚
(1...(𝑁 + 1))) ↦
((𝑐‘(𝑁 + 1)) ·
⦋(𝑐 ↾
(1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
54 | 53 | 3adant3 1113 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
55 | 50 | rabdiophlem2 38836 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐵) ∈ (mzPoly‘(1...𝑁))) → (𝑐 ∈ (ℤ ↑𝑚
(1...(𝑁 + 1))) ↦
⦋(𝑐 ↾
(1...𝑁)) / 𝑡⦌𝐵) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
56 | 55 | 3adant2 1112 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
57 | | eqrabdioph 38811 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℕ0
∧ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1))) ∧ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵) ∈ (mzPoly‘(1...(𝑁 + 1)))) → {𝑐 ∈ (ℕ0
↑𝑚 (1...(𝑁 + 1))) ∣ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) |
58 | 42, 54, 56, 57 | syl3anc 1352 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑐 ∈
(ℕ0 ↑𝑚 (1...(𝑁 + 1))) ∣ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) |
59 | | mzpnegmpt 38777 |
. . . . . . . . 9
⊢ ((𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ (𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1))) → (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ -(𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
60 | 49, 59 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑐 ∈ (ℤ ↑𝑚
(1...(𝑁 + 1))) ↦
-(𝑐‘(𝑁 + 1))) ∈
(mzPoly‘(1...(𝑁 +
1)))) |
61 | | mzpmulmpt 38775 |
. . . . . . . 8
⊢ (((𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ -(𝑐‘(𝑁 + 1))) ∈ (mzPoly‘(1...(𝑁 + 1))) ∧ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) ∈ (mzPoly‘(1...(𝑁 + 1)))) → (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
62 | 60, 51, 61 | syl2anc 576 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑐 ∈ (ℤ ↑𝑚
(1...(𝑁 + 1))) ↦
(-(𝑐‘(𝑁 + 1)) ·
⦋(𝑐 ↾
(1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
63 | 62 | 3adant3 1113 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1)))) |
64 | | eqrabdioph 38811 |
. . . . . 6
⊢ (((𝑁 + 1) ∈ ℕ0
∧ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) ∈ (mzPoly‘(1...(𝑁 + 1))) ∧ (𝑐 ∈ (ℤ
↑𝑚 (1...(𝑁 + 1))) ↦ ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵) ∈ (mzPoly‘(1...(𝑁 + 1)))) → {𝑐 ∈ (ℕ0
↑𝑚 (1...(𝑁 + 1))) ∣ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) |
65 | 42, 63, 56, 64 | syl3anc 1352 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑐 ∈
(ℕ0 ↑𝑚 (1...(𝑁 + 1))) ∣ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) |
66 | | orrabdioph 38815 |
. . . . 5
⊢ (({𝑐 ∈ (ℕ0
↑𝑚 (1...(𝑁 + 1))) ∣ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1)) ∧ {𝑐 ∈ (ℕ0
↑𝑚 (1...(𝑁 + 1))) ∣ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵} ∈ (Dioph‘(𝑁 + 1))) → {𝑐 ∈ (ℕ0
↑𝑚 (1...(𝑁 + 1))) ∣ (((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)} ∈ (Dioph‘(𝑁 + 1))) |
67 | 58, 65, 66 | syl2anc 576 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑐 ∈
(ℕ0 ↑𝑚 (1...(𝑁 + 1))) ∣ (((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)} ∈ (Dioph‘(𝑁 + 1))) |
68 | | oveq1 6989 |
. . . . . . 7
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → (𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴)) |
69 | 68 | eqeq1d 2782 |
. . . . . 6
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ↔ ((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)) |
70 | | negeq 10684 |
. . . . . . . 8
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → -𝑏 = -(𝑐‘(𝑁 + 1))) |
71 | 70 | oveq1d 6997 |
. . . . . . 7
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴)) |
72 | 71 | eqeq1d 2782 |
. . . . . 6
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → ((-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ↔ (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)) |
73 | 69, 72 | orbi12d 903 |
. . . . 5
⊢ (𝑏 = (𝑐‘(𝑁 + 1)) → (((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵) ↔ (((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵))) |
74 | | csbeq1 3791 |
. . . . . . . 8
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ⦋𝑎 / 𝑡⦌𝐴 = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) |
75 | 74 | oveq2d 6998 |
. . . . . . 7
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) |
76 | | csbeq1 3791 |
. . . . . . 7
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ⦋𝑎 / 𝑡⦌𝐵 = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵) |
77 | 75, 76 | eqeq12d 2795 |
. . . . . 6
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → (((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ↔ ((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)) |
78 | 74 | oveq2d 6998 |
. . . . . . 7
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴)) |
79 | 78, 76 | eqeq12d 2795 |
. . . . . 6
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ((-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ↔ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)) |
80 | 77, 79 | orbi12d 903 |
. . . . 5
⊢ (𝑎 = (𝑐 ↾ (1...𝑁)) → ((((𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵) ↔ (((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵))) |
81 | 50, 73, 80 | rexrabdioph 38828 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ {𝑐 ∈
(ℕ0 ↑𝑚 (1...(𝑁 + 1))) ∣ (((𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵 ∨ (-(𝑐‘(𝑁 + 1)) · ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐴) = ⦋(𝑐 ↾ (1...𝑁)) / 𝑡⦌𝐵)} ∈ (Dioph‘(𝑁 + 1))) → {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)} ∈ (Dioph‘𝑁)) |
82 | 40, 67, 81 | syl2anc 576 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑎 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵 ∨ (-𝑏 · ⦋𝑎 / 𝑡⦌𝐴) = ⦋𝑎 / 𝑡⦌𝐵)} ∈ (Dioph‘𝑁)) |
83 | 39, 82 | syl5eqel 2872 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 ((𝑏 · 𝐴) = 𝐵 ∨ (-𝑏 · 𝐴) = 𝐵)} ∈ (Dioph‘𝑁)) |
84 | 15, 83 | eqeltrd 2868 |
1
⊢ ((𝑁 ∈ ℕ0
∧ (𝑡 ∈ (ℤ
↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) ∧ (𝑡 ∈ (ℤ ↑𝑚
(1...𝑁)) ↦ 𝐵) ∈
(mzPoly‘(1...𝑁)))
→ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ 𝐴 ∥ 𝐵} ∈ (Dioph‘𝑁)) |