Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  diophin Structured version   Visualization version   GIF version

Theorem diophin 36244
Description: If two sets are Diophantine, so is their intersection. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
Assertion
Ref Expression
diophin ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁))

Proof of Theorem diophin
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldiophelnn0 36235 . . 3 (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈ ℕ0)
2 id 22 . . . . . 6 (𝑁 ∈ ℕ0𝑁 ∈ ℕ0)
3 zex 11127 . . . . . . 7 ℤ ∈ V
4 difexg 4634 . . . . . . 7 (ℤ ∈ V → (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ V)
53, 4mp1i 13 . . . . . 6 (𝑁 ∈ ℕ0 → (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ V)
6 ominf 7933 . . . . . . 7 ¬ ω ∈ Fin
7 nn0z 11141 . . . . . . . 8 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
8 lzenom 36241 . . . . . . . 8 (𝑁 ∈ ℤ → (ℤ ∖ (ℤ‘(𝑁 + 1))) ≈ ω)
9 enfi 7937 . . . . . . . 8 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ≈ ω → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
107, 8, 93syl 18 . . . . . . 7 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
116, 10mtbiri 315 . . . . . 6 (𝑁 ∈ ℕ0 → ¬ (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin)
12 fz1eqin 36240 . . . . . . 7 (𝑁 ∈ ℕ0 → (1...𝑁) = ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ))
13 inss1 3698 . . . . . . 7 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1)))
1412, 13syl6eqss 3522 . . . . . 6 (𝑁 ∈ ℕ0 → (1...𝑁) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1))))
15 eldioph2b 36234 . . . . . 6 (((𝑁 ∈ ℕ0 ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)}))
162, 5, 11, 14, 15syl22anc 1318 . . . . 5 (𝑁 ∈ ℕ0 → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)}))
17 nnex 10781 . . . . . . 7 ℕ ∈ V
1817a1i 11 . . . . . 6 (𝑁 ∈ ℕ0 → ℕ ∈ V)
19 1z 11148 . . . . . . 7 1 ∈ ℤ
20 nnuz 11463 . . . . . . . 8 ℕ = (ℤ‘1)
2120uzinf 12494 . . . . . . 7 (1 ∈ ℤ → ¬ ℕ ∈ Fin)
2219, 21mp1i 13 . . . . . 6 (𝑁 ∈ ℕ0 → ¬ ℕ ∈ Fin)
23 elfznn 12109 . . . . . . . 8 (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
2423ssriv 3476 . . . . . . 7 (1...𝑁) ⊆ ℕ
2524a1i 11 . . . . . 6 (𝑁 ∈ ℕ0 → (1...𝑁) ⊆ ℕ)
26 eldioph2b 36234 . . . . . 6 (((𝑁 ∈ ℕ0 ∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
272, 18, 22, 25, 26syl22anc 1318 . . . . 5 (𝑁 ∈ ℕ0 → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
2816, 27anbi12d 742 . . . 4 (𝑁 ∈ ℕ0 → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)})))
29 reeanv 2990 . . . . 5 (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
30 inab 3757 . . . . . . . . 9 ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))}
31 reeanv 2990 . . . . . . . . . . 11 (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)))
32 simplrl 795 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
33 simplrr 796 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑒 ∈ (ℕ0𝑚 ℕ))
3412eqcomd 2520 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁))
3534reseq2d 5208 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
3635ad3antrrr 761 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
3734reseq2d 5208 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
3837ad3antrrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
39 simprrl 799 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁)))
40 simprll 797 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁)))
4138, 39, 403eqtr2d 2554 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
4236, 41eqtr4d 2551 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)))
43 elmapresaun 36242 . . . . . . . . . . . . . . . . . 18 ((𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ))) → (𝑑𝑒) ∈ (ℕ0𝑚 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)))
4432, 33, 42, 43syl3anc 1317 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑𝑒) ∈ (ℕ0𝑚 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)))
4520uneq2i 3630 . . . . . . . . . . . . . . . . . . . 20 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ (ℤ‘1))
4619a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → 1 ∈ ℤ)
47 nn0p1nn 11087 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)
4847nnge1d 10818 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → 1 ≤ (𝑁 + 1))
49 lzunuz 36239 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ (𝑁 + 1)) → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ (ℤ‘1)) = ℤ)
507, 46, 48, 49syl3anc 1317 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ (ℤ‘1)) = ℤ)
5145, 50syl5eq 2560 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ) = ℤ)
5251oveq2d 6442 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ0 → (ℕ0𝑚 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)) = (ℕ0𝑚 ℤ))
5352ad3antrrr 761 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (ℕ0𝑚 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)) = (ℕ0𝑚 ℤ))
5444, 53eleqtrd 2594 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑𝑒) ∈ (ℕ0𝑚 ℤ))
55 unidm 3622 . . . . . . . . . . . . . . . . . . 19 (𝑐𝑐) = 𝑐
5640, 39uneq12d 3634 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑐𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
5755, 56syl5eqr 2562 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
58 resundir 5222 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))
5957, 58syl6eqr 2566 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = ((𝑑𝑒) ↾ (1...𝑁)))
60 uncom 3623 . . . . . . . . . . . . . . . . . . . . 21 (𝑑𝑒) = (𝑒𝑑)
6160reseq1i 5204 . . . . . . . . . . . . . . . . . . . 20 ((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = ((𝑒𝑑) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))
62 incom 3670 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)
6362, 34syl5eq 2560 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ0 → (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = (1...𝑁))
6463reseq2d 5208 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ0 → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
6564ad3antrrr 761 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
6663reseq2d 5208 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ0 → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
6766ad3antrrr 761 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
6867, 40, 393eqtr2d 2554 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
6965, 68eqtr4d 2551 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))))
70 elmapresaunres2 36243 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ (ℕ0𝑚 ℕ) ∧ 𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) → ((𝑒𝑑) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = 𝑑)
7133, 32, 69, 70syl3anc 1317 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ((𝑒𝑑) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = 𝑑)
7261, 71syl5eq 2560 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = 𝑑)
7372fveq2d 5991 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑎𝑑))
74 simprlr 798 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑎𝑑) = 0)
7573, 74eqtrd 2548 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0)
76 elmapresaunres2 36243 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑𝑒) ↾ ℕ) = 𝑒)
7732, 33, 42, 76syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ((𝑑𝑒) ↾ ℕ) = 𝑒)
7877fveq2d 5991 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑏‘((𝑑𝑒) ↾ ℕ)) = (𝑏𝑒))
79 simprrr 800 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑏𝑒) = 0)
8078, 79eqtrd 2548 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0)
8159, 75, 80jca32 555 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑐 = ((𝑑𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0)))
82 reseq1 5202 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑑𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑𝑒) ↾ (1...𝑁)))
8382eqeq2d 2524 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑑𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑𝑒) ↾ (1...𝑁))))
84 reseq1 5202 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑑𝑒) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = ((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))
8584fveq2d 5991 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑑𝑒) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))))
8685eqeq1d 2516 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑑𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0))
87 reseq1 5202 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = (𝑑𝑒) → (𝑓 ↾ ℕ) = ((𝑑𝑒) ↾ ℕ))
8887fveq2d 5991 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑑𝑒) → (𝑏‘(𝑓 ↾ ℕ)) = (𝑏‘((𝑑𝑒) ↾ ℕ)))
8988eqeq1d 2516 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑑𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0))
9086, 89anbi12d 742 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑑𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0)))
9183, 90anbi12d 742 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑑𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0))))
9291rspcev 3186 . . . . . . . . . . . . . . . 16 (((𝑑𝑒) ∈ (ℕ0𝑚 ℤ) ∧ (𝑐 = ((𝑑𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0))) → ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
9354, 81, 92syl2anc 690 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
9493ex 448 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) → ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
9594rexlimdvva 2924 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) → ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
96 simpr 475 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑓 ∈ (ℕ0𝑚 ℤ))
97 difss 3603 . . . . . . . . . . . . . . . . . 18 (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ
98 elmapssres 7644 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (ℕ0𝑚 ℤ) ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
9996, 97, 98sylancl 692 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
10099adantr 479 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
101 nnssz 11138 . . . . . . . . . . . . . . . . . 18 ℕ ⊆ ℤ
102 elmapssres 7644 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (ℕ0𝑚 ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℕ0𝑚 ℕ))
10396, 101, 102sylancl 692 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ0𝑚 ℕ))
104103adantr 479 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈ (ℕ0𝑚 ℕ))
105 simprl 789 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁)))
10614ad3antrrr 761 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1))))
107106resabs1d 5239 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
108105, 107eqtr4d 2551 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)))
109 simprrl 799 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0)
110108, 109jca 552 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0))
111 resabs1 5238 . . . . . . . . . . . . . . . . . . 19 ((1...𝑁) ⊆ ℕ → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
11224, 111mp1i 13 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
113105, 112eqtr4d 2551 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
114 simprrr 800 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0)
115110, 113, 114jca32 555 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
116 reseq1 5202 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)))
117116eqeq2d 2524 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁))))
118 fveq2 5987 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (𝑎𝑑) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))))
119118eqeq1d 2516 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → ((𝑎𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0))
120117, 119anbi12d 742 . . . . . . . . . . . . . . . . . 18 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0)))
121120anbi1d 736 . . . . . . . . . . . . . . . . 17 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))))
122 reseq1 5202 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
123122eqeq2d 2524 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))))
124 fveq2 5987 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = (𝑓 ↾ ℕ) → (𝑏𝑒) = (𝑏‘(𝑓 ↾ ℕ)))
125124eqeq1d 2516 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑓 ↾ ℕ) → ((𝑏𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0))
126123, 125anbi12d 742 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
127126anbi2d 735 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
128121, 127rspc2ev 3199 . . . . . . . . . . . . . . . 16 (((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈ (ℕ0𝑚 ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)))
129100, 104, 115, 128syl3anc 1317 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)))
130129ex 448 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))))
131130rexlimdva 2917 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))))
13295, 131impbid 200 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
133 simplrl 795 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))))
134 mzpf 36207 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) → 𝑎:(ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))⟶ℤ)
135133, 134syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑎:(ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))⟶ℤ)
136 nn0ssz 11139 . . . . . . . . . . . . . . . . . . . . . 22 0 ⊆ ℤ
137 mapss 7662 . . . . . . . . . . . . . . . . . . . . . 22 ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0𝑚 ℤ) ⊆ (ℤ ↑𝑚 ℤ))
1383, 136, 137mp2an 703 . . . . . . . . . . . . . . . . . . . . 21 (ℕ0𝑚 ℤ) ⊆ (ℤ ↑𝑚 ℤ)
139138sseli 3468 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ (ℕ0𝑚 ℤ) → 𝑓 ∈ (ℤ ↑𝑚 ℤ))
140 elmapssres 7644 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℤ ↑𝑚 ℤ) ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
141139, 97, 140sylancl 692 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℕ0𝑚 ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
142141adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
143135, 142ffvelrnd 6152 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) ∈ ℤ)
144143zred 11222 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) ∈ ℝ)
145 simplrr 796 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑏 ∈ (mzPoly‘ℕ))
146 mzpf 36207 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ (mzPoly‘ℕ) → 𝑏:(ℤ ↑𝑚 ℕ)⟶ℤ)
147145, 146syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑏:(ℤ ↑𝑚 ℕ)⟶ℤ)
148 elmapssres 7644 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℤ ↑𝑚 ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑𝑚 ℕ))
149139, 101, 148sylancl 692 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℕ0𝑚 ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑𝑚 ℕ))
150149adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ ↑𝑚 ℕ))
151147, 150ffvelrnd 6152 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℤ)
152151zred 11222 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ)
153 sumsqeq0 12672 . . . . . . . . . . . . . . . 16 (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
154144, 152, 153syl2anc 690 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
155139adantl 480 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑓 ∈ (ℤ ↑𝑚 ℤ))
156 reseq1 5202 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))
157156fveq2d 5991 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))))
158157oveq1d 6441 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2))
159 reseq1 5202 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ))
160159fveq2d 5991 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ)))
161160oveq1d 6441 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2))
162158, 161oveq12d 6444 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
163 eqid 2514 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))
164 ovex 6454 . . . . . . . . . . . . . . . . . 18 (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈ V
165162, 163, 164fvmpt 6075 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℤ ↑𝑚 ℤ) → ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
166155, 165syl 17 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
167166eqeq1d 2516 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
168154, 167bitr4d 269 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))
169168anbi2d 735 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
170169rexbidva 2935 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
171132, 170bitrd 266 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
17231, 171syl5bbr 272 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
173172abbidv 2632 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
17430, 173syl5eq 2560 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
175 simpl 471 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈ ℕ0)
176 fzssuz 12121 . . . . . . . . . . . 12 (1...𝑁) ⊆ (ℤ‘1)
177 uzssz 11447 . . . . . . . . . . . 12 (ℤ‘1) ⊆ ℤ
178176, 177sstri 3481 . . . . . . . . . . 11 (1...𝑁) ⊆ ℤ
1793, 178pm3.2i 469 . . . . . . . . . 10 (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ)
180179a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ))
1813a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℤ ∈ V)
18297a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ)
183 simprl 789 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))))
184 mzpresrename 36221 . . . . . . . . . . . 12 ((ℤ ∈ V ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ ∧ 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
185181, 182, 183, 184syl3anc 1317 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
186 2nn0 11064 . . . . . . . . . . 11 2 ∈ ℕ0
187 mzpexpmpt 36216 . . . . . . . . . . 11 (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
188185, 186, 187sylancl 692 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
189101a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℕ ⊆ ℤ)
190 simprr 791 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈ (mzPoly‘ℕ))
191 mzpresrename 36221 . . . . . . . . . . . 12 ((ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
192181, 189, 190, 191syl3anc 1317 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
193 mzpexpmpt 36216 . . . . . . . . . . 11 (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
194192, 186, 193sylancl 692 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
195 mzpaddmpt 36212 . . . . . . . . . 10 (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
196188, 194, 195syl2anc 690 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
197 eldioph2 36233 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
198175, 180, 196, 197syl3anc 1317 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
199174, 198eqeltrd 2592 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) ∈ (Dioph‘𝑁))
200 ineq12 3674 . . . . . . . 8 ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
201200eleq1d 2576 . . . . . . 7 ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → ((𝐴𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) ∈ (Dioph‘𝑁)))
202199, 201syl5ibrcom 235 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
203202rexlimdvva 2924 . . . . 5 (𝑁 ∈ ℕ0 → (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
20429, 203syl5bir 231 . . . 4 (𝑁 ∈ ℕ0 → ((∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
20528, 204sylbid 228 . . 3 (𝑁 ∈ ℕ0 → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
2061, 205syl 17 . 2 (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
207206anabsi5 853 1 ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1938  {cab 2500  wrex 2801  Vcvv 3077  cdif 3441  cun 3442  cin 3443  wss 3444   class class class wbr 4481  cmpt 4541  cres 4934  wf 5685  cfv 5689  (class class class)co 6426  ωcom 6833  𝑚 cmap 7620  cen 7714  Fincfn 7717  cr 9690  0cc0 9691  1c1 9692   + caddc 9694  cle 9830  cn 10775  2c2 10825  0cn0 11047  cz 11118  cuz 11427  ...cfz 12065  cexp 12590  mzPolycmzp 36193  Diophcdioph 36226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-inf2 8297  ax-cnex 9747  ax-resscn 9748  ax-1cn 9749  ax-icn 9750  ax-addcl 9751  ax-addrcl 9752  ax-mulcl 9753  ax-mulrcl 9754  ax-mulcom 9755  ax-addass 9756  ax-mulass 9757  ax-distr 9758  ax-i2m1 9759  ax-1ne0 9760  ax-1rid 9761  ax-rnegex 9762  ax-rrecex 9763  ax-cnre 9764  ax-pre-lttri 9765  ax-pre-lttrn 9766  ax-pre-ltadd 9767  ax-pre-mulgt0 9768
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-riota 6388  df-ov 6429  df-oprab 6430  df-mpt2 6431  df-of 6671  df-om 6834  df-1st 6934  df-2nd 6935  df-wrecs 7169  df-recs 7231  df-rdg 7269  df-1o 7323  df-oadd 7327  df-er 7505  df-map 7622  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-card 8524  df-cda 8749  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835  df-sub 10019  df-neg 10020  df-nn 10776  df-2 10834  df-n0 11048  df-z 11119  df-uz 11428  df-fz 12066  df-seq 12532  df-exp 12591  df-hash 12848  df-mzpcl 36194  df-mzp 36195  df-dioph 36227
This theorem is referenced by:  anrabdioph  36252
  Copyright terms: Public domain W3C validator