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 38306
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 38297 . . 3 (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈ ℕ0)
2 id 22 . . . . . 6 (𝑁 ∈ ℕ0𝑁 ∈ ℕ0)
3 zex 11741 . . . . . . 7 ℤ ∈ V
4 difexg 5047 . . . . . . 7 (ℤ ∈ V → (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ V)
53, 4mp1i 13 . . . . . 6 (𝑁 ∈ ℕ0 → (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ V)
6 ominf 8462 . . . . . . 7 ¬ ω ∈ Fin
7 nn0z 11756 . . . . . . . 8 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
8 lzenom 38303 . . . . . . . 8 (𝑁 ∈ ℤ → (ℤ ∖ (ℤ‘(𝑁 + 1))) ≈ ω)
9 enfi 8466 . . . . . . . 8 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ≈ ω → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
107, 8, 93syl 18 . . . . . . 7 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
116, 10mtbiri 319 . . . . . 6 (𝑁 ∈ ℕ0 → ¬ (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin)
12 fz1eqin 38302 . . . . . . 7 (𝑁 ∈ ℕ0 → (1...𝑁) = ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ))
13 inss1 4053 . . . . . . 7 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1)))
1412, 13syl6eqss 3874 . . . . . 6 (𝑁 ∈ ℕ0 → (1...𝑁) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1))))
15 eldioph2b 38296 . . . . . 6 (((𝑁 ∈ ℕ0 ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)}))
162, 5, 11, 14, 15syl22anc 829 . . . . 5 (𝑁 ∈ ℕ0 → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)}))
17 nnex 11385 . . . . . . 7 ℕ ∈ V
1817a1i 11 . . . . . 6 (𝑁 ∈ ℕ0 → ℕ ∈ V)
19 1z 11763 . . . . . . 7 1 ∈ ℤ
20 nnuz 12033 . . . . . . . 8 ℕ = (ℤ‘1)
2120uzinf 13087 . . . . . . 7 (1 ∈ ℤ → ¬ ℕ ∈ Fin)
2219, 21mp1i 13 . . . . . 6 (𝑁 ∈ ℕ0 → ¬ ℕ ∈ Fin)
23 elfznn 12691 . . . . . . . 8 (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
2423ssriv 3825 . . . . . . 7 (1...𝑁) ⊆ ℕ
2524a1i 11 . . . . . 6 (𝑁 ∈ ℕ0 → (1...𝑁) ⊆ ℕ)
26 eldioph2b 38296 . . . . . 6 (((𝑁 ∈ ℕ0 ∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
272, 18, 22, 25, 26syl22anc 829 . . . . 5 (𝑁 ∈ ℕ0 → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
2816, 27anbi12d 624 . . . 4 (𝑁 ∈ ℕ0 → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)})))
29 reeanv 3293 . . . . 5 (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
30 inab 4121 . . . . . . . . 9 ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))}
31 reeanv 3293 . . . . . . . . . . 11 (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)))
32 simplrl 767 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
33 simplrr 768 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑒 ∈ (ℕ0𝑚 ℕ))
3412eqcomd 2784 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁))
3534reseq2d 5644 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
3635ad3antrrr 720 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
3734reseq2d 5644 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
3837ad3antrrr 720 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
39 simprrl 771 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁)))
40 simprll 769 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁)))
4138, 39, 403eqtr2d 2820 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
4236, 41eqtr4d 2817 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)))
43 elmapresaun 38304 . . . . . . . . . . . . . . . . . 18 ((𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ))) → (𝑑𝑒) ∈ (ℕ0𝑚 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)))
4432, 33, 42, 43syl3anc 1439 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑𝑒) ∈ (ℕ0𝑚 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)))
4520uneq2i 3987 . . . . . . . . . . . . . . . . . . . 20 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ (ℤ‘1))
4619a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → 1 ∈ ℤ)
47 nn0p1nn 11687 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)
4847nnge1d 11427 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → 1 ≤ (𝑁 + 1))
49 lzunuz 38301 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ (𝑁 + 1)) → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ (ℤ‘1)) = ℤ)
507, 46, 48, 49syl3anc 1439 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ (ℤ‘1)) = ℤ)
5145, 50syl5eq 2826 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ) = ℤ)
5251oveq2d 6940 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ0 → (ℕ0𝑚 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)) = (ℕ0𝑚 ℤ))
5352ad3antrrr 720 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (ℕ0𝑚 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)) = (ℕ0𝑚 ℤ))
5444, 53eleqtrd 2861 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑𝑒) ∈ (ℕ0𝑚 ℤ))
55 unidm 3979 . . . . . . . . . . . . . . . . . . 19 (𝑐𝑐) = 𝑐
5640, 39uneq12d 3991 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑐𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
5755, 56syl5eqr 2828 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
58 resundir 5663 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))
5957, 58syl6eqr 2832 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = ((𝑑𝑒) ↾ (1...𝑁)))
60 uncom 3980 . . . . . . . . . . . . . . . . . . . . 21 (𝑑𝑒) = (𝑒𝑑)
6160reseq1i 5640 . . . . . . . . . . . . . . . . . . . 20 ((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = ((𝑒𝑑) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))
62 incom 4028 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)
6362, 34syl5eq 2826 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ0 → (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = (1...𝑁))
6463reseq2d 5644 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ0 → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
6564ad3antrrr 720 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
6663reseq2d 5644 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ0 → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
6766ad3antrrr 720 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
6867, 40, 393eqtr2d 2820 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
6965, 68eqtr4d 2817 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))))
70 elmapresaunres2 38305 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ (ℕ0𝑚 ℕ) ∧ 𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) → ((𝑒𝑑) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = 𝑑)
7133, 32, 69, 70syl3anc 1439 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ((𝑒𝑑) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = 𝑑)
7261, 71syl5eq 2826 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = 𝑑)
7372fveq2d 6452 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑎𝑑))
74 simprlr 770 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑎𝑑) = 0)
7573, 74eqtrd 2814 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0)
76 elmapresaunres2 38305 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑𝑒) ↾ ℕ) = 𝑒)
7732, 33, 42, 76syl3anc 1439 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ((𝑑𝑒) ↾ ℕ) = 𝑒)
7877fveq2d 6452 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑏‘((𝑑𝑒) ↾ ℕ)) = (𝑏𝑒))
79 simprrr 772 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑏𝑒) = 0)
8078, 79eqtrd 2814 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0)
8159, 75, 80jca32 511 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑐 = ((𝑑𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0)))
82 reseq1 5638 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑑𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑𝑒) ↾ (1...𝑁)))
8382eqeq2d 2788 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑑𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑𝑒) ↾ (1...𝑁))))
84 reseq1 5638 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑑𝑒) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = ((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))
8584fveqeq2d 6456 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑑𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0))
86 reseq1 5638 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑑𝑒) → (𝑓 ↾ ℕ) = ((𝑑𝑒) ↾ ℕ))
8786fveqeq2d 6456 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑑𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0))
8885, 87anbi12d 624 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑑𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0)))
8983, 88anbi12d 624 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑑𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0))))
9089rspcev 3511 . . . . . . . . . . . . . . . 16 (((𝑑𝑒) ∈ (ℕ0𝑚 ℤ) ∧ (𝑐 = ((𝑑𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0))) → ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
9154, 81, 90syl2anc 579 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
9291ex 403 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0𝑚 ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) → ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
9392rexlimdvva 3221 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) → ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
94 simpr 479 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑓 ∈ (ℕ0𝑚 ℤ))
95 difss 3960 . . . . . . . . . . . . . . . . 17 (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ
96 elmapssres 8167 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (ℕ0𝑚 ℤ) ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
9794, 95, 96sylancl 580 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
9897adantr 474 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
99 nnssz 11752 . . . . . . . . . . . . . . . . 17 ℕ ⊆ ℤ
100 elmapssres 8167 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (ℕ0𝑚 ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℕ0𝑚 ℕ))
10194, 99, 100sylancl 580 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ0𝑚 ℕ))
102101adantr 474 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈ (ℕ0𝑚 ℕ))
103 simprl 761 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁)))
10414ad3antrrr 720 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1))))
105104resabs1d 5679 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
106103, 105eqtr4d 2817 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)))
107 simprrl 771 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0)
108106, 107jca 507 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0))
109 resabs1 5678 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) ⊆ ℕ → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
11024, 109mp1i 13 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
111103, 110eqtr4d 2817 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
112 simprrr 772 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0)
113108, 111, 112jca32 511 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
114 reseq1 5638 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)))
115114eqeq2d 2788 . . . . . . . . . . . . . . . . . 18 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁))))
116 fveqeq2 6457 . . . . . . . . . . . . . . . . . 18 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → ((𝑎𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0))
117115, 116anbi12d 624 . . . . . . . . . . . . . . . . 17 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0)))
118117anbi1d 623 . . . . . . . . . . . . . . . 16 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))))
119 reseq1 5638 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
120119eqeq2d 2788 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))))
121 fveqeq2 6457 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑓 ↾ ℕ) → ((𝑏𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0))
122120, 121anbi12d 624 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
123122anbi2d 622 . . . . . . . . . . . . . . . 16 (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
124118, 123rspc2ev 3526 . . . . . . . . . . . . . . 15 (((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈ (ℕ0𝑚 ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)))
12598, 102, 113, 124syl3anc 1439 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)))
126125rexlimdva2 3216 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))))
12793, 126impbid 204 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
128 simplrl 767 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))))
129 mzpf 38269 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) → 𝑎:(ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))⟶ℤ)
130128, 129syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑎:(ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))⟶ℤ)
131 nn0ssz 11754 . . . . . . . . . . . . . . . . . . . . . 22 0 ⊆ ℤ
132 mapss 8188 . . . . . . . . . . . . . . . . . . . . . 22 ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0𝑚 ℤ) ⊆ (ℤ ↑𝑚 ℤ))
1333, 131, 132mp2an 682 . . . . . . . . . . . . . . . . . . . . 21 (ℕ0𝑚 ℤ) ⊆ (ℤ ↑𝑚 ℤ)
134133sseli 3817 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ (ℕ0𝑚 ℤ) → 𝑓 ∈ (ℤ ↑𝑚 ℤ))
135 elmapssres 8167 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℤ ↑𝑚 ℤ) ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
136134, 95, 135sylancl 580 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℕ0𝑚 ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
137136adantl 475 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℤ ↑𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1)))))
138130, 137ffvelrnd 6626 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) ∈ ℤ)
139138zred 11838 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) ∈ ℝ)
140 simplrr 768 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑏 ∈ (mzPoly‘ℕ))
141 mzpf 38269 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ (mzPoly‘ℕ) → 𝑏:(ℤ ↑𝑚 ℕ)⟶ℤ)
142140, 141syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑏:(ℤ ↑𝑚 ℕ)⟶ℤ)
143 elmapssres 8167 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℤ ↑𝑚 ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑𝑚 ℕ))
144134, 99, 143sylancl 580 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℕ0𝑚 ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑𝑚 ℕ))
145144adantl 475 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ ↑𝑚 ℕ))
146142, 145ffvelrnd 6626 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℤ)
147146zred 11838 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ)
148 sumsqeq0 13265 . . . . . . . . . . . . . . . 16 (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
149139, 147, 148syl2anc 579 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
150134adantl 475 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → 𝑓 ∈ (ℤ ↑𝑚 ℤ))
151 reseq1 5638 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))
152151fveq2d 6452 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))))
153152oveq1d 6939 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2))
154 reseq1 5638 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ))
155154fveq2d 6452 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ)))
156155oveq1d 6939 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2))
157153, 156oveq12d 6942 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
158 eqid 2778 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))
159 ovex 6956 . . . . . . . . . . . . . . . . . 18 (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈ V
160157, 158, 159fvmpt 6544 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℤ ↑𝑚 ℤ) → ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
161150, 160syl 17 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
162161eqeq1d 2780 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
163149, 162bitr4d 274 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))
164163anbi2d 622 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0𝑚 ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
165164rexbidva 3234 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
166127, 165bitrd 271 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
16731, 166syl5bbr 277 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
168167abbidv 2906 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ (∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
16930, 168syl5eq 2826 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
170 simpl 476 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈ ℕ0)
171 fzssuz 12703 . . . . . . . . . . . 12 (1...𝑁) ⊆ (ℤ‘1)
172 uzssz 12016 . . . . . . . . . . . 12 (ℤ‘1) ⊆ ℤ
173171, 172sstri 3830 . . . . . . . . . . 11 (1...𝑁) ⊆ ℤ
1743, 173pm3.2i 464 . . . . . . . . . 10 (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ)
175174a1i 11 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ))
1763a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℤ ∈ V)
17795a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ)
178 simprl 761 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))))
179 mzpresrename 38283 . . . . . . . . . . . 12 ((ℤ ∈ V ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ ∧ 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
180176, 177, 178, 179syl3anc 1439 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
181 2nn0 11665 . . . . . . . . . . 11 2 ∈ ℕ0
182 mzpexpmpt 38278 . . . . . . . . . . 11 (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
183180, 181, 182sylancl 580 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
18499a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℕ ⊆ ℤ)
185 simprr 763 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈ (mzPoly‘ℕ))
186 mzpresrename 38283 . . . . . . . . . . . 12 ((ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
187176, 184, 185, 186syl3anc 1439 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
188 mzpexpmpt 38278 . . . . . . . . . . 11 (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
189187, 181, 188sylancl 580 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
190 mzpaddmpt 38274 . . . . . . . . . 10 (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
191183, 189, 190syl2anc 579 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
192 eldioph2 38295 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
193170, 175, 191, 192syl3anc 1439 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
194169, 193eqeltrd 2859 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) ∈ (Dioph‘𝑁))
195 ineq12 4032 . . . . . . . 8 ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
196195eleq1d 2844 . . . . . . 7 ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → ((𝐴𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) ∈ (Dioph‘𝑁)))
197194, 196syl5ibrcom 239 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
198197rexlimdvva 3221 . . . . 5 (𝑁 ∈ ℕ0 → (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
19929, 198syl5bir 235 . . . 4 (𝑁 ∈ ℕ0 → ((∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0𝑚 (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
20028, 199sylbid 232 . . 3 (𝑁 ∈ ℕ0 → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
2011, 200syl 17 . 2 (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
202201anabsi5 659 1 ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  {cab 2763  wrex 3091  Vcvv 3398  cdif 3789  cun 3790  cin 3791  wss 3792   class class class wbr 4888  cmpt 4967  cres 5359  wf 6133  cfv 6137  (class class class)co 6924  ωcom 7345  𝑚 cmap 8142  cen 8240  Fincfn 8243  cr 10273  0cc0 10274  1c1 10275   + caddc 10277  cle 10414  cn 11378  2c2 11434  0cn0 11646  cz 11732  cuz 11996  ...cfz 12647  cexp 13182  mzPolycmzp 38255  Diophcdioph 38288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-of 7176  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-oadd 7849  df-er 8028  df-map 8144  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-card 9100  df-cda 9327  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-nn 11379  df-2 11442  df-n0 11647  df-z 11733  df-uz 11997  df-fz 12648  df-seq 13124  df-exp 13183  df-hash 13440  df-mzpcl 38256  df-mzp 38257  df-dioph 38289
This theorem is referenced by:  anrabdioph  38314
  Copyright terms: Public domain W3C validator