Step | Hyp | Ref
| Expression |
1 | | eldiophelnn0 37327 |
. . 3
⊢ (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈
ℕ0) |
2 | | id 22 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
3 | | zex 11386 |
. . . . . . 7
⊢ ℤ
∈ V |
4 | | difexg 4808 |
. . . . . . 7
⊢ (ℤ
∈ V → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈
V) |
5 | 3, 4 | mp1i 13 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ V) |
6 | | ominf 8172 |
. . . . . . 7
⊢ ¬
ω ∈ Fin |
7 | | nn0z 11400 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
8 | | lzenom 37333 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (ℤ
∖ (ℤ≥‘(𝑁 + 1))) ≈ ω) |
9 | | enfi 8176 |
. . . . . . . 8
⊢ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ≈ ω → ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈
Fin)) |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈
Fin)) |
11 | 6, 10 | mtbiri 317 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ¬ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin) |
12 | | fz1eqin 37332 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) = ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) |
13 | | inss1 3833 |
. . . . . . 7
⊢ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ
∖ (ℤ≥‘(𝑁 + 1))) |
14 | 12, 13 | syl6eqss 3655 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ⊆
(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) |
15 | | eldioph2b 37326 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖
(ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)})) |
16 | 2, 5, 11, 14, 15 | syl22anc 1327 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈
(Dioph‘𝑁) ↔
∃𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)})) |
17 | | nnex 11026 |
. . . . . . 7
⊢ ℕ
∈ V |
18 | 17 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ℕ ∈ V) |
19 | | 1z 11407 |
. . . . . . 7
⊢ 1 ∈
ℤ |
20 | | nnuz 11723 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
21 | 20 | uzinf 12764 |
. . . . . . 7
⊢ (1 ∈
ℤ → ¬ ℕ ∈ Fin) |
22 | 19, 21 | mp1i 13 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ¬ ℕ ∈ Fin) |
23 | | elfznn 12370 |
. . . . . . . 8
⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ) |
24 | 23 | ssriv 3607 |
. . . . . . 7
⊢
(1...𝑁) ⊆
ℕ |
25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ⊆
ℕ) |
26 | | eldioph2b 37326 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) →
(𝐵 ∈
(Dioph‘𝑁) ↔
∃𝑏 ∈
(mzPoly‘ℕ)𝐵 =
{𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})) |
27 | 2, 18, 22, 25, 26 | syl22anc 1327 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝐵 ∈
(Dioph‘𝑁) ↔
∃𝑏 ∈
(mzPoly‘ℕ)𝐵 =
{𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})) |
28 | 16, 27 | anbi12d 747 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈
(Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ
∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))) |
29 | | reeanv 3107 |
. . . . 5
⊢
(∃𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖
(ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})) |
30 | | inab 3895 |
. . . . . . . . 9
⊢ ({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} |
31 | | reeanv 3107 |
. . . . . . . . . . 11
⊢
(∃𝑑 ∈
(ℕ0 ↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) |
32 | | simplrl 800 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
33 | | simplrr 801 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑒 ∈ (ℕ0
↑𝑚 ℕ)) |
34 | 12 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁)) |
35 | 34 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (𝑑 ↾ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁))) |
36 | 35 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁))) |
37 | 34 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑒 ↾ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁))) |
38 | 37 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁))) |
39 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁))) |
40 | | simprll 802 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁))) |
41 | 38, 39, 40 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁))) |
42 | 36, 41 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ))) |
43 | | elmapresaun 37334 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ) ∧ (𝑑 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ))) → (𝑑 ∪ 𝑒) ∈ (ℕ0
↑𝑚 ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∪ ℕ))) |
44 | 32, 33, 42, 43 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ0
↑𝑚 ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∪ ℕ))) |
45 | 20 | uneq2i 3764 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∪
(ℤ≥‘1)) |
46 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℤ) |
47 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
48 | 47 | nnge1d 11063 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 1 ≤ (𝑁 +
1)) |
49 | | lzunuz 37331 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℤ ∧ 1 ∈
ℤ ∧ 1 ≤ (𝑁 +
1)) → ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪
(ℤ≥‘1)) = ℤ) |
50 | 7, 46, 48, 49 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪
(ℤ≥‘1)) = ℤ) |
51 | 45, 50 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ) =
ℤ) |
52 | 51 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (ℕ0 ↑𝑚 ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∪ ℕ)) =
(ℕ0 ↑𝑚 ℤ)) |
53 | 52 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (ℕ0
↑𝑚 ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∪ ℕ)) =
(ℕ0 ↑𝑚 ℤ)) |
54 | 44, 53 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ0
↑𝑚 ℤ)) |
55 | | unidm 3756 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∪ 𝑐) = 𝑐 |
56 | 40, 39 | uneq12d 3768 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 ∪ 𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))) |
57 | 55, 56 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))) |
58 | | resundir 5411 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))) |
59 | 57, 58 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))) |
60 | | uncom 3757 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 ∪ 𝑒) = (𝑒 ∪ 𝑑) |
61 | 60 | reseq1i 5392 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = ((𝑒 ∪ 𝑑) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) |
62 | | incom 3805 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℕ
∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ) |
63 | 62, 34 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = (1...𝑁)) |
64 | 63 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ (𝑒 ↾ (ℕ
∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁))) |
65 | 64 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁))) |
66 | 63 | reseq2d 5396 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (𝑑 ↾ (ℕ
∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁))) |
67 | 66 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁))) |
68 | 67, 40, 39 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁))) |
69 | 65, 68 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) |
70 | | elmapresaunres2 37335 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑒 ∈ (ℕ0
↑𝑚 ℕ) ∧ 𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = 𝑑) |
71 | 33, 32, 69, 70 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = 𝑑) |
72 | 61, 71 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = 𝑑) |
73 | 72 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑎‘𝑑)) |
74 | | simprlr 803 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘𝑑) = 0) |
75 | 73, 74 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) |
76 | | elmapresaunres2 37335 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ) ∧ (𝑑 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒) |
77 | 32, 33, 42, 76 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒) |
78 | 77 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = (𝑏‘𝑒)) |
79 | | simprrr 805 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘𝑒) = 0) |
80 | 78, 79 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0) |
81 | 59, 75, 80 | jca32 558 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) |
82 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))) |
83 | 82 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))) |
84 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = ((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
85 | 84 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) |
86 | 85 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0)) |
87 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ ℕ) = ((𝑑 ∪ 𝑒) ↾ ℕ)) |
88 | 87 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑏‘(𝑓 ↾ ℕ)) = (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ))) |
89 | 88 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)) |
90 | 86, 89 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) |
91 | 83, 90 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))) |
92 | 91 | rspcev 3309 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑑 ∪ 𝑒) ∈ (ℕ0
↑𝑚 ℤ) ∧ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) →
∃𝑓 ∈
(ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) |
93 | 54, 81, 92 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) |
94 | 93 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑𝑚 ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))) |
95 | 94 | rexlimdvva 3038 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑑 ∈
(ℕ0 ↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))) |
96 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) |
97 | | difss 3737 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℤ
∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ |
98 | | elmapssres 7882 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ (ℕ0
↑𝑚 ℤ) ∧ (ℤ ∖
(ℤ≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
99 | 96, 97, 98 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
100 | 99 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
101 | | nnssz 11397 |
. . . . . . . . . . . . . . . . . 18
⊢ ℕ
⊆ ℤ |
102 | | elmapssres 7882 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ (ℕ0
↑𝑚 ℤ) ∧ ℕ ⊆ ℤ) →
(𝑓 ↾ ℕ) ∈
(ℕ0 ↑𝑚 ℕ)) |
103 | 96, 101, 102 | sylancl 694 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ0
↑𝑚 ℕ)) |
104 | 103 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈
(ℕ0 ↑𝑚 ℕ)) |
105 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁))) |
106 | 14 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) |
107 | 106 | resabs1d 5428 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁))) |
108 | 105, 107 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁))) |
109 | | simprrl 804 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) |
110 | 108, 109 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0)) |
111 | | resabs1 5427 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1...𝑁) ⊆
ℕ → ((𝑓 ↾
ℕ) ↾ (1...𝑁)) =
(𝑓 ↾ (1...𝑁))) |
112 | 24, 111 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾
(1...𝑁)) = (𝑓 ↾ (1...𝑁))) |
113 | 105, 112 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))) |
114 | | simprrr 805 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0) |
115 | 110, 113,
114 | jca32 558 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) |
116 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁))) |
117 | 116 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)))) |
118 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → (𝑎‘𝑑) = (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) |
119 | 118 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → ((𝑎‘𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0)) |
120 | 117, 119 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0))) |
121 | 120 | anbi1d 741 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))) |
122 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁))) |
123 | 122 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))) |
124 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑏‘𝑒) = (𝑏‘(𝑓 ↾ ℕ))) |
125 | 124 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑏‘𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0)) |
126 | 123, 125 | anbi12d 747 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) |
127 | 126 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))) |
128 | 121, 127 | rspc2ev 3324 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈ (ℕ0
↑𝑚 ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) |
129 | 100, 104,
115, 128 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) |
130 | 129 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))) |
131 | 130 | rexlimdva 3031 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑓 ∈
(ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))) |
132 | 95, 131 | impbid 202 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑑 ∈
(ℕ0 ↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))) |
133 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
134 | | mzpf 37299 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ (mzPoly‘(ℤ
∖ (ℤ≥‘(𝑁 + 1)))) → 𝑎:(ℤ ↑𝑚 (ℤ
∖ (ℤ≥‘(𝑁 + 1))))⟶ℤ) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → 𝑎:(ℤ ↑𝑚 (ℤ
∖ (ℤ≥‘(𝑁 + 1))))⟶ℤ) |
136 | | nn0ssz 11398 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
ℕ0 ⊆ ℤ |
137 | | mapss 7900 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℤ
∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0
↑𝑚 ℤ) ⊆ (ℤ ↑𝑚
ℤ)) |
138 | 3, 136, 137 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℕ0 ↑𝑚 ℤ) ⊆
(ℤ ↑𝑚 ℤ) |
139 | 138 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ (ℕ0
↑𝑚 ℤ) → 𝑓 ∈ (ℤ ↑𝑚
ℤ)) |
140 | | elmapssres 7882 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ (ℤ
↑𝑚 ℤ) ∧ (ℤ ∖
(ℤ≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℤ
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
141 | 139, 97, 140 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (ℕ0
↑𝑚 ℤ) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℤ
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
142 | 141 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℤ
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
143 | 135, 142 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) ∈ ℤ) |
144 | 143 | zred 11482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) ∈ ℝ) |
145 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → 𝑏 ∈
(mzPoly‘ℕ)) |
146 | | mzpf 37299 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ (mzPoly‘ℕ)
→ 𝑏:(ℤ
↑𝑚 ℕ)⟶ℤ) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → 𝑏:(ℤ ↑𝑚
ℕ)⟶ℤ) |
148 | | elmapssres 7882 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ (ℤ
↑𝑚 ℤ) ∧ ℕ ⊆ ℤ) →
(𝑓 ↾ ℕ) ∈
(ℤ ↑𝑚 ℕ)) |
149 | 139, 101,
148 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (ℕ0
↑𝑚 ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ
↑𝑚 ℕ)) |
150 | 149 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ
↑𝑚 ℕ)) |
151 | 147, 150 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈
ℤ) |
152 | 151 | zred 11482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈
ℝ) |
153 | | sumsqeq0 12942 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) →
(((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) =
0)) |
154 | 144, 152,
153 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) =
0)) |
155 | 139 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → 𝑓 ∈ (ℤ ↑𝑚
ℤ)) |
156 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
157 | 156 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) |
158 | 157 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2)) |
159 | | reseq1 5390 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ)) |
160 | 159 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ))) |
161 | 160 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2)) |
162 | 158, 161 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2))) |
163 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) |
164 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈
V |
165 | 162, 163,
164 | fvmpt 6282 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (ℤ
↑𝑚 ℤ) → ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2))) |
166 | 155, 165 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2))) |
167 | 166 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) =
0)) |
168 | 154, 167 | bitr4d 271 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)) |
169 | 168 | anbi2d 740 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑𝑚 ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))) |
170 | 169 | rexbidva 3049 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑓 ∈
(ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))) |
171 | 132, 170 | bitrd 268 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑑 ∈
(ℕ0 ↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))) |
172 | 31, 171 | syl5bbr 274 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
((∃𝑑 ∈
(ℕ0 ↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))) |
173 | 172 | abbidv 2741 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
{𝑐 ∣ (∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)}) |
174 | 30, 173 | syl5eq 2668 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)}) |
175 | | simpl 473 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈
ℕ0) |
176 | | fzssuz 12382 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ⊆
(ℤ≥‘1) |
177 | | uzssz 11707 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘1) ⊆ ℤ |
178 | 176, 177 | sstri 3612 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
ℤ |
179 | 3, 178 | pm3.2i 471 |
. . . . . . . . . 10
⊢ (ℤ
∈ V ∧ (1...𝑁)
⊆ ℤ) |
180 | 179 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ)) |
181 | 3 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
ℤ ∈ V) |
182 | 97 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(ℤ ∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ) |
183 | | simprl 794 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ
∖ (ℤ≥‘(𝑁 + 1))))) |
184 | | mzpresrename 37313 |
. . . . . . . . . . . 12
⊢ ((ℤ
∈ V ∧ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ ∧
𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) ∈
(mzPoly‘ℤ)) |
185 | 181, 182,
183, 184 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) ∈
(mzPoly‘ℤ)) |
186 | | 2nn0 11309 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
187 | | mzpexpmpt 37308 |
. . . . . . . . . . 11
⊢ (((𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ)
∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2)) ∈
(mzPoly‘ℤ)) |
188 | 185, 186,
187 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2)) ∈
(mzPoly‘ℤ)) |
189 | 101 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
ℕ ⊆ ℤ) |
190 | | simprr 796 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈
(mzPoly‘ℕ)) |
191 | | mzpresrename 37313 |
. . . . . . . . . . . 12
⊢ ((ℤ
∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈
(mzPoly‘ℤ)) |
192 | 181, 189,
190, 191 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈
(mzPoly‘ℤ)) |
193 | | mzpexpmpt 37308 |
. . . . . . . . . . 11
⊢ (((𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈
(mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈
(mzPoly‘ℤ)) |
194 | 192, 186,
193 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈
(mzPoly‘ℤ)) |
195 | | mzpaddmpt 37304 |
. . . . . . . . . 10
⊢ (((𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2)) ∈
(mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈
(mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈
(mzPoly‘ℤ)) |
196 | 188, 194,
195 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈
(mzPoly‘ℤ)) |
197 | | eldioph2 37325 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈
(mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈
(Dioph‘𝑁)) |
198 | 175, 180,
196, 197 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
{𝑐 ∣ ∃𝑓 ∈ (ℕ0
↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚
ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈
(Dioph‘𝑁)) |
199 | 174, 198 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁)) |
200 | | ineq12 3809 |
. . . . . . . 8
⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})) |
201 | 200 | eleq1d 2686 |
. . . . . . 7
⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → ((𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁))) |
202 | 199, 201 | syl5ibrcom 237 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
203 | 202 | rexlimdvva 3038 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (∃𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
204 | 29, 203 | syl5bir 233 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((∃𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑𝑚 (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
205 | 28, 204 | sylbid 230 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈
(Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
206 | 1, 205 | syl 17 |
. 2
⊢ (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
207 | 206 | anabsi5 858 |
1
⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)) |