| Step | Hyp | Ref
| Expression |
| 1 | | eldiophelnn0 42775 |
. . 3
⊢ (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈
ℕ0) |
| 2 | | id 22 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
| 3 | | zex 12622 |
. . . . . . 7
⊢ ℤ
∈ V |
| 4 | | difexg 5329 |
. . . . . . 7
⊢ (ℤ
∈ V → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈
V) |
| 5 | 3, 4 | mp1i 13 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ V) |
| 6 | | ominf 9294 |
. . . . . . 7
⊢ ¬
ω ∈ Fin |
| 7 | | nn0z 12638 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 8 | | lzenom 42781 |
. . . . . . . 8
⊢ (𝑁 ∈ ℤ → (ℤ
∖ (ℤ≥‘(𝑁 + 1))) ≈ ω) |
| 9 | | enfi 9227 |
. . . . . . . 8
⊢ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ≈ ω → ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈
Fin)) |
| 10 | 7, 8, 9 | 3syl 18 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈
Fin)) |
| 11 | 6, 10 | mtbiri 327 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ¬ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin) |
| 12 | | fz1eqin 42780 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) = ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) |
| 13 | | inss1 4237 |
. . . . . . 7
⊢ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ
∖ (ℤ≥‘(𝑁 + 1))) |
| 14 | 12, 13 | eqsstrdi 4028 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ⊆
(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) |
| 15 | | eldioph2b 42774 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖
(ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)})) |
| 16 | 2, 5, 11, 14, 15 | syl22anc 839 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝐴 ∈
(Dioph‘𝑁) ↔
∃𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)})) |
| 17 | | nnex 12272 |
. . . . . . 7
⊢ ℕ
∈ V |
| 18 | 17 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ℕ ∈ V) |
| 19 | | 1z 12647 |
. . . . . . 7
⊢ 1 ∈
ℤ |
| 20 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 21 | 20 | uzinf 14006 |
. . . . . . 7
⊢ (1 ∈
ℤ → ¬ ℕ ∈ Fin) |
| 22 | 19, 21 | mp1i 13 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ¬ ℕ ∈ Fin) |
| 23 | | elfznn 13593 |
. . . . . . . 8
⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ) |
| 24 | 23 | ssriv 3987 |
. . . . . . 7
⊢
(1...𝑁) ⊆
ℕ |
| 25 | 24 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (1...𝑁) ⊆
ℕ) |
| 26 | | eldioph2b 42774 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) →
(𝐵 ∈
(Dioph‘𝑁) ↔
∃𝑏 ∈
(mzPoly‘ℕ)𝐵 =
{𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})) |
| 27 | 2, 18, 22, 25, 26 | syl22anc 839 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝐵 ∈
(Dioph‘𝑁) ↔
∃𝑏 ∈
(mzPoly‘ℕ)𝐵 =
{𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})) |
| 28 | 16, 27 | anbi12d 632 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈
(Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ
∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))) |
| 29 | | reeanv 3229 |
. . . . 5
⊢
(∃𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖
(ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})) |
| 30 | | inab 4309 |
. . . . . . . . 9
⊢ ({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} |
| 31 | | reeanv 3229 |
. . . . . . . . . . 11
⊢
(∃𝑑 ∈
(ℕ0 ↑m (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) |
| 32 | | simplrl 777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) |
| 33 | | simplrr 778 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑒 ∈ (ℕ0
↑m ℕ)) |
| 34 | 12 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁)) |
| 35 | 34 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ (𝑑 ↾ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁))) |
| 36 | 35 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁))) |
| 37 | 34 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑒 ↾ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁))) |
| 38 | 37 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁))) |
| 39 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁))) |
| 40 | | simprll 779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁))) |
| 41 | 38, 39, 40 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁))) |
| 42 | 36, 41 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ))) |
| 43 | | elmapresaun 8920 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ) ∧ (𝑑 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ))) → (𝑑 ∪ 𝑒) ∈ (ℕ0
↑m ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪
ℕ))) |
| 44 | 32, 33, 42, 43 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ0
↑m ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪
ℕ))) |
| 45 | 20 | uneq2i 4165 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℤ
∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∪
(ℤ≥‘1)) |
| 46 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℤ) |
| 47 | | nn0p1nn 12565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
| 48 | 47 | nnge1d 12314 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ 1 ≤ (𝑁 +
1)) |
| 49 | | lzunuz 42779 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈ ℤ ∧ 1 ∈
ℤ ∧ 1 ≤ (𝑁 +
1)) → ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪
(ℤ≥‘1)) = ℤ) |
| 50 | 7, 46, 48, 49 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪
(ℤ≥‘1)) = ℤ) |
| 51 | 45, 50 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ) =
ℤ) |
| 52 | 51 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (ℕ0 ↑m ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∪ ℕ)) =
(ℕ0 ↑m ℤ)) |
| 53 | 52 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (ℕ0
↑m ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ)) =
(ℕ0 ↑m ℤ)) |
| 54 | 44, 53 | eleqtrd 2843 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ0
↑m ℤ)) |
| 55 | | unidm 4157 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∪ 𝑐) = 𝑐 |
| 56 | 40, 39 | uneq12d 4169 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 ∪ 𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))) |
| 57 | 55, 56 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))) |
| 58 | | resundir 6012 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))) |
| 59 | 57, 58 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))) |
| 60 | | uncom 4158 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 ∪ 𝑒) = (𝑒 ∪ 𝑑) |
| 61 | 60 | reseq1i 5993 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = ((𝑒 ∪ 𝑑) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) |
| 62 | | incom 4209 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℕ
∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ) |
| 63 | 62, 34 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = (1...𝑁)) |
| 64 | 63 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ (𝑒 ↾ (ℕ
∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁))) |
| 65 | 64 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁))) |
| 66 | 63 | reseq2d 5997 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (𝑑 ↾ (ℕ
∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁))) |
| 67 | 66 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁))) |
| 68 | 67, 40, 39 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁))) |
| 69 | 65, 68 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) |
| 70 | | elmapresaunres2 42782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑒 ∈ (ℕ0
↑m ℕ) ∧ 𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ
∖ (ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = 𝑑) |
| 71 | 33, 32, 69, 70 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = 𝑑) |
| 72 | 61, 71 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = 𝑑) |
| 73 | 72 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑎‘𝑑)) |
| 74 | | simprlr 780 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘𝑑) = 0) |
| 75 | 73, 74 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) |
| 76 | | elmapresaunres2 42782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ) ∧ (𝑑 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖
(ℤ≥‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒) |
| 77 | 32, 33, 42, 76 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒) |
| 78 | 77 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = (𝑏‘𝑒)) |
| 79 | | simprrr 782 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘𝑒) = 0) |
| 80 | 78, 79 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0) |
| 81 | 59, 75, 80 | jca32 515 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) |
| 82 | | reseq1 5991 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))) |
| 83 | 82 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))) |
| 84 | | reseq1 5991 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = ((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
| 85 | 84 | fveqeq2d 6914 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0)) |
| 86 | | reseq1 5991 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ ℕ) = ((𝑑 ∪ 𝑒) ↾ ℕ)) |
| 87 | 86 | fveqeq2d 6914 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)) |
| 88 | 85, 87 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑑 ∪ 𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) |
| 89 | 83, 88 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))) |
| 90 | 89 | rspcev 3622 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑑 ∪ 𝑒) ∈ (ℕ0
↑m ℤ) ∧ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) →
∃𝑓 ∈
(ℕ0 ↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) |
| 91 | 54, 81, 90 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) |
| 92 | 91 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0
↑m ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))) |
| 93 | 92 | rexlimdvva 3213 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑑 ∈
(ℕ0 ↑m (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))) |
| 94 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → 𝑓 ∈ (ℕ0
↑m ℤ)) |
| 95 | | difss 4136 |
. . . . . . . . . . . . . . . . 17
⊢ (ℤ
∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ |
| 96 | | elmapssres 8907 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ (ℕ0
↑m ℤ) ∧ (ℤ ∖
(ℤ≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) |
| 97 | 94, 95, 96 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) |
| 98 | 97 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) |
| 99 | | nnssz 12635 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ
⊆ ℤ |
| 100 | | elmapssres 8907 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ (ℕ0
↑m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈
(ℕ0 ↑m ℕ)) |
| 101 | 94, 99, 100 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ0
↑m ℕ)) |
| 102 | 101 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈
(ℕ0 ↑m ℕ)) |
| 103 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁))) |
| 104 | 14 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) |
| 105 | 104 | resabs1d 6026 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁))) |
| 106 | 103, 105 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁))) |
| 107 | | simprrl 781 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) |
| 108 | 106, 107 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0)) |
| 109 | | resabs1 6024 |
. . . . . . . . . . . . . . . . . 18
⊢
((1...𝑁) ⊆
ℕ → ((𝑓 ↾
ℕ) ↾ (1...𝑁)) =
(𝑓 ↾ (1...𝑁))) |
| 110 | 24, 109 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾
(1...𝑁)) = (𝑓 ↾ (1...𝑁))) |
| 111 | 103, 110 | eqtr4d 2780 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))) |
| 112 | | simprrr 782 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0) |
| 113 | 108, 111,
112 | jca32 515 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) |
| 114 | | reseq1 5991 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁))) |
| 115 | 114 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)))) |
| 116 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → ((𝑎‘𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0)) |
| 117 | 115, 116 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0))) |
| 118 | 117 | anbi1d 631 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))) |
| 119 | | reseq1 5991 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁))) |
| 120 | 119 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))) |
| 121 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑏‘𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0)) |
| 122 | 120, 121 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) |
| 123 | 122 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))) |
| 124 | 118, 123 | rspc2ev 3635 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈
(ℕ0 ↑m ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) |
| 125 | 98, 102, 113, 124 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) |
| 126 | 125 | rexlimdva2 3157 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑓 ∈
(ℕ0 ↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))) |
| 127 | 93, 126 | impbid 212 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑑 ∈
(ℕ0 ↑m (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))) |
| 128 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
| 129 | | mzpf 42747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ (mzPoly‘(ℤ
∖ (ℤ≥‘(𝑁 + 1)))) → 𝑎:(ℤ ↑m (ℤ ∖
(ℤ≥‘(𝑁 + 1))))⟶ℤ) |
| 130 | 128, 129 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → 𝑎:(ℤ ↑m (ℤ ∖
(ℤ≥‘(𝑁 + 1))))⟶ℤ) |
| 131 | | nn0ssz 12636 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
ℕ0 ⊆ ℤ |
| 132 | | mapss 8929 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℤ
∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0
↑m ℤ) ⊆ (ℤ ↑m
ℤ)) |
| 133 | 3, 131, 132 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℕ0 ↑m ℤ) ⊆ (ℤ
↑m ℤ) |
| 134 | 133 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ (ℕ0
↑m ℤ) → 𝑓 ∈ (ℤ ↑m
ℤ)) |
| 135 | | elmapssres 8907 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ (ℤ
↑m ℤ) ∧ (ℤ ∖
(ℤ≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℤ ↑m
(ℤ ∖ (ℤ≥‘(𝑁 + 1))))) |
| 136 | 134, 95, 135 | sylancl 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (ℕ0
↑m ℤ) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℤ ↑m
(ℤ ∖ (ℤ≥‘(𝑁 + 1))))) |
| 137 | 136 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) ∈ (ℤ ↑m
(ℤ ∖ (ℤ≥‘(𝑁 + 1))))) |
| 138 | 130, 137 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) ∈ ℤ) |
| 139 | 138 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) ∈ ℝ) |
| 140 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → 𝑏 ∈
(mzPoly‘ℕ)) |
| 141 | | mzpf 42747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ (mzPoly‘ℕ)
→ 𝑏:(ℤ
↑m ℕ)⟶ℤ) |
| 142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → 𝑏:(ℤ ↑m
ℕ)⟶ℤ) |
| 143 | | elmapssres 8907 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ (ℤ
↑m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈
(ℤ ↑m ℕ)) |
| 144 | 134, 99, 143 | sylancl 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ (ℕ0
↑m ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ
↑m ℕ)) |
| 145 | 144 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ
↑m ℕ)) |
| 146 | 142, 145 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈
ℤ) |
| 147 | 146 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈
ℝ) |
| 148 | | sumsqeq0 14218 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) →
(((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) =
0)) |
| 149 | 139, 147,
148 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) =
0)) |
| 150 | 134 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → 𝑓 ∈ (ℤ ↑m
ℤ)) |
| 151 | | reseq1 5991 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) |
| 152 | 151 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) |
| 153 | 152 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2)) |
| 154 | | reseq1 5991 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ)) |
| 155 | 154 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ))) |
| 156 | 155 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2)) |
| 157 | 153, 156 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2))) |
| 158 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∈ (ℤ
↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ
↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) |
| 159 | | ovex 7464 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈
V |
| 160 | 157, 158,
159 | fvmpt 7016 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ (ℤ
↑m ℤ) → ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2))) |
| 161 | 150, 160 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2))) |
| 162 | 161 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) =
0)) |
| 163 | 149, 162 | bitr4d 282 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ
↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)) |
| 164 | 163 | anbi2d 630 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0
↑m ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))) |
| 165 | 164 | rexbidva 3177 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑓 ∈
(ℕ0 ↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))) |
| 166 | 127, 165 | bitrd 279 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(∃𝑑 ∈
(ℕ0 ↑m (ℤ ∖
(ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0
↑m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))) |
| 167 | 31, 166 | bitr3id 285 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
((∃𝑑 ∈
(ℕ0 ↑m (ℤ ∖
(ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))) |
| 168 | 167 | abbidv 2808 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
{𝑐 ∣ (∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)}) |
| 169 | 30, 168 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)}) |
| 170 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈
ℕ0) |
| 171 | | fzssuz 13605 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ⊆
(ℤ≥‘1) |
| 172 | | uzssz 12899 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘1) ⊆ ℤ |
| 173 | 171, 172 | sstri 3993 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
ℤ |
| 174 | 3, 173 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (ℤ
∈ V ∧ (1...𝑁)
⊆ ℤ) |
| 175 | 174 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ)) |
| 176 | 3 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
ℤ ∈ V) |
| 177 | 95 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(ℤ ∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ) |
| 178 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ
∖ (ℤ≥‘(𝑁 + 1))))) |
| 179 | | mzpresrename 42761 |
. . . . . . . . . . . 12
⊢ ((ℤ
∈ V ∧ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ ∧
𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑m ℤ)
↦ (𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) ∈
(mzPoly‘ℤ)) |
| 180 | 176, 177,
178, 179 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) ∈
(mzPoly‘ℤ)) |
| 181 | | 2nn0 12543 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
| 182 | | mzpexpmpt 42756 |
. . . . . . . . . . 11
⊢ (((𝑔 ∈ (ℤ
↑m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ)
∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑m ℤ)
↦ ((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2)) ∈
(mzPoly‘ℤ)) |
| 183 | 180, 181,
182 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2)) ∈
(mzPoly‘ℤ)) |
| 184 | 99 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
ℕ ⊆ ℤ) |
| 185 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈
(mzPoly‘ℕ)) |
| 186 | | mzpresrename 42761 |
. . . . . . . . . . . 12
⊢ ((ℤ
∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ
↑m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈
(mzPoly‘ℤ)) |
| 187 | 176, 184,
185, 186 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈
(mzPoly‘ℤ)) |
| 188 | | mzpexpmpt 42756 |
. . . . . . . . . . 11
⊢ (((𝑔 ∈ (ℤ
↑m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈
(mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ
↑m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈
(mzPoly‘ℤ)) |
| 189 | 187, 181,
188 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈
(mzPoly‘ℤ)) |
| 190 | | mzpaddmpt 42752 |
. . . . . . . . . 10
⊢ (((𝑔 ∈ (ℤ
↑m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2)) ∈
(mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑m ℤ)
↦ ((𝑏‘(𝑔 ↾ ℕ))↑2))
∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈
(mzPoly‘ℤ)) |
| 191 | 183, 189,
190 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
(𝑔 ∈ (ℤ
↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈
(mzPoly‘ℤ)) |
| 192 | | eldioph2 42773 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈
(mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈
(Dioph‘𝑁)) |
| 193 | 170, 175,
191, 192 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
{𝑐 ∣ ∃𝑓 ∈ (ℕ0
↑m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ)
↦ (((𝑎‘(𝑔 ↾ (ℤ ∖
(ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈
(Dioph‘𝑁)) |
| 194 | 169, 193 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁)) |
| 195 | | ineq12 4215 |
. . . . . . . 8
⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})) |
| 196 | 195 | eleq1d 2826 |
. . . . . . 7
⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → ((𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁))) |
| 197 | 194, 196 | syl5ibrcom 247 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ (𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) →
((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
| 198 | 197 | rexlimdvva 3213 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (∃𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
| 199 | 29, 198 | biimtrrid 243 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((∃𝑎 ∈
(mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0
↑m (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0
↑m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
| 200 | 28, 199 | sylbid 240 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐴 ∈
(Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
| 201 | 1, 200 | syl 17 |
. 2
⊢ (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))) |
| 202 | 201 | anabsi5 669 |
1
⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)) |