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 42759
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 42751 . . 3 (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈ ℕ0)
2 id 22 . . . . . 6 (𝑁 ∈ ℕ0𝑁 ∈ ℕ0)
3 zex 12619 . . . . . . 7 ℤ ∈ V
4 difexg 5334 . . . . . . 7 (ℤ ∈ V → (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ V)
53, 4mp1i 13 . . . . . 6 (𝑁 ∈ ℕ0 → (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ V)
6 ominf 9291 . . . . . . 7 ¬ ω ∈ Fin
7 nn0z 12635 . . . . . . . 8 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
8 lzenom 42757 . . . . . . . 8 (𝑁 ∈ ℤ → (ℤ ∖ (ℤ‘(𝑁 + 1))) ≈ ω)
9 enfi 9224 . . . . . . . 8 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ≈ ω → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
107, 8, 93syl 18 . . . . . . 7 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
116, 10mtbiri 327 . . . . . 6 (𝑁 ∈ ℕ0 → ¬ (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin)
12 fz1eqin 42756 . . . . . . 7 (𝑁 ∈ ℕ0 → (1...𝑁) = ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ))
13 inss1 4244 . . . . . . 7 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1)))
1412, 13eqsstrdi 4049 . . . . . 6 (𝑁 ∈ ℕ0 → (1...𝑁) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1))))
15 eldioph2b 42750 . . . . . 6 (((𝑁 ∈ ℕ0 ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ ∖ (ℤ‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)}))
162, 5, 11, 14, 15syl22anc 839 . . . . 5 (𝑁 ∈ ℕ0 → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)}))
17 nnex 12269 . . . . . . 7 ℕ ∈ V
1817a1i 11 . . . . . 6 (𝑁 ∈ ℕ0 → ℕ ∈ V)
19 1z 12644 . . . . . . 7 1 ∈ ℤ
20 nnuz 12918 . . . . . . . 8 ℕ = (ℤ‘1)
2120uzinf 14002 . . . . . . 7 (1 ∈ ℤ → ¬ ℕ ∈ Fin)
2219, 21mp1i 13 . . . . . 6 (𝑁 ∈ ℕ0 → ¬ ℕ ∈ Fin)
23 elfznn 13589 . . . . . . . 8 (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
2423ssriv 3998 . . . . . . 7 (1...𝑁) ⊆ ℕ
2524a1i 11 . . . . . 6 (𝑁 ∈ ℕ0 → (1...𝑁) ⊆ ℕ)
26 eldioph2b 42750 . . . . . 6 (((𝑁 ∈ ℕ0 ∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
272, 18, 22, 25, 26syl22anc 839 . . . . 5 (𝑁 ∈ ℕ0 → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
2816, 27anbi12d 632 . . . 4 (𝑁 ∈ ℕ0 → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)})))
29 reeanv 3226 . . . . 5 (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
30 inab 4314 . . . . . . . . 9 ({𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))}
31 reeanv 3226 . . . . . . . . . . 11 (∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)))
32 simplrl 777 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))))
33 simplrr 778 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑒 ∈ (ℕ0m ℕ))
3412eqcomd 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁))
3534reseq2d 5999 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
3635ad3antrrr 730 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
3734reseq2d 5999 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
3837ad3antrrr 730 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
39 simprrl 781 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁)))
40 simprll 779 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁)))
4138, 39, 403eqtr2d 2780 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
4236, 41eqtr4d 2777 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)))
43 elmapresaun 8918 . . . . . . . . . . . . . . . . . 18 ((𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ))) → (𝑑𝑒) ∈ (ℕ0m ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)))
4432, 33, 42, 43syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑𝑒) ∈ (ℕ0m ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)))
4520uneq2i 4174 . . . . . . . . . . . . . . . . . . . 20 ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ (ℤ‘1))
4619a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → 1 ∈ ℤ)
47 nn0p1nn 12562 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)
4847nnge1d 12311 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℕ0 → 1 ≤ (𝑁 + 1))
49 lzunuz 42755 . . . . . . . . . . . . . . . . . . . . 21 ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ (𝑁 + 1)) → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ (ℤ‘1)) = ℤ)
507, 46, 48, 49syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ (ℤ‘1)) = ℤ)
5145, 50eqtrid 2786 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ) = ℤ)
5251oveq2d 7446 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ ℕ0 → (ℕ0m ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)) = (ℕ0m ℤ))
5352ad3antrrr 730 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (ℕ0m ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∪ ℕ)) = (ℕ0m ℤ))
5444, 53eleqtrd 2840 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑𝑒) ∈ (ℕ0m ℤ))
55 unidm 4166 . . . . . . . . . . . . . . . . . . 19 (𝑐𝑐) = 𝑐
5640, 39uneq12d 4178 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑐𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
5755, 56eqtr3id 2788 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
58 resundir 6014 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))
5957, 58eqtr4di 2792 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → 𝑐 = ((𝑑𝑒) ↾ (1...𝑁)))
60 uncom 4167 . . . . . . . . . . . . . . . . . . . . 21 (𝑑𝑒) = (𝑒𝑑)
6160reseq1i 5995 . . . . . . . . . . . . . . . . . . . 20 ((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = ((𝑒𝑑) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))
62 incom 4216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)
6362, 34eqtrid 2786 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ0 → (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = (1...𝑁))
6463reseq2d 5999 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ0 → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
6564ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
6663reseq2d 5999 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ0 → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
6766ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
6867, 40, 393eqtr2d 2780 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
6965, 68eqtr4d 2777 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))))
70 elmapresaunres2 42758 . . . . . . . . . . . . . . . . . . . . 21 ((𝑒 ∈ (ℕ0m ℕ) ∧ 𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) → ((𝑒𝑑) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = 𝑑)
7133, 32, 69, 70syl3anc 1370 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ((𝑒𝑑) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = 𝑑)
7261, 71eqtrid 2786 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = 𝑑)
7372fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑎𝑑))
74 simprlr 780 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑎𝑑) = 0)
7573, 74eqtrd 2774 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0)
76 elmapresaunres2 42758 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑𝑒) ↾ ℕ) = 𝑒)
7732, 33, 42, 76syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ((𝑑𝑒) ↾ ℕ) = 𝑒)
7877fveq2d 6910 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑏‘((𝑑𝑒) ↾ ℕ)) = (𝑏𝑒))
79 simprrr 782 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑏𝑒) = 0)
8078, 79eqtrd 2774 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0)
8159, 75, 80jca32 515 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → (𝑐 = ((𝑑𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0)))
82 reseq1 5993 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑑𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑𝑒) ↾ (1...𝑁)))
8382eqeq2d 2745 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑑𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑𝑒) ↾ (1...𝑁))))
84 reseq1 5993 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑑𝑒) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = ((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))
8584fveqeq2d 6914 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑑𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0))
86 reseq1 5993 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = (𝑑𝑒) → (𝑓 ↾ ℕ) = ((𝑑𝑒) ↾ ℕ))
8786fveqeq2d 6914 . . . . . . . . . . . . . . . . . . 19 (𝑓 = (𝑑𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0))
8885, 87anbi12d 632 . . . . . . . . . . . . . . . . . 18 (𝑓 = (𝑑𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0)))
8983, 88anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑓 = (𝑑𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0))))
9089rspcev 3621 . . . . . . . . . . . . . . . 16 (((𝑑𝑒) ∈ (ℕ0m ℤ) ∧ (𝑐 = ((𝑑𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑𝑒) ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑𝑒) ↾ ℕ)) = 0))) → ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
9154, 81, 90syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))) → ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
9291ex 412 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0m ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) → ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
9392rexlimdvva 3210 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) → ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
94 simpr 484 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → 𝑓 ∈ (ℕ0m ℤ))
95 difss 4145 . . . . . . . . . . . . . . . . 17 (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ
96 elmapssres 8905 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (ℕ0m ℤ) ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))))
9794, 95, 96sylancl 586 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))))
9897adantr 480 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))))
99 nnssz 12632 . . . . . . . . . . . . . . . . 17 ℕ ⊆ ℤ
100 elmapssres 8905 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (ℕ0m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℕ0m ℕ))
10194, 99, 100sylancl 586 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ0m ℕ))
102101adantr 480 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈ (ℕ0m ℕ))
103 simprl 771 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁)))
10414ad3antrrr 730 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖ (ℤ‘(𝑁 + 1))))
105104resabs1d 6027 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
106103, 105eqtr4d 2777 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)))
107 simprrl 781 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0)
108106, 107jca 511 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0))
109 resabs1 6026 . . . . . . . . . . . . . . . . . 18 ((1...𝑁) ⊆ ℕ → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
11024, 109mp1i 13 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
111103, 110eqtr4d 2777 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
112 simprrr 782 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0)
113108, 111, 112jca32 515 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
114 reseq1 5993 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)))
115114eqeq2d 2745 . . . . . . . . . . . . . . . . . 18 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁))))
116 fveqeq2 6915 . . . . . . . . . . . . . . . . . 18 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → ((𝑎𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0))
117115, 116anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0)))
118117anbi1d 631 . . . . . . . . . . . . . . . 16 (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))))
119 reseq1 5993 . . . . . . . . . . . . . . . . . . 19 (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
120119eqeq2d 2745 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))))
121 fveqeq2 6915 . . . . . . . . . . . . . . . . . 18 (𝑒 = (𝑓 ↾ ℕ) → ((𝑏𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0))
122120, 121anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
123122anbi2d 630 . . . . . . . . . . . . . . . 16 (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
124118, 123rspc2ev 3634 . . . . . . . . . . . . . . 15 (((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈ (ℕ0m ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)))
12598, 102, 113, 124syl3anc 1370 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)))
126125rexlimdva2 3154 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))))
12793, 126impbid 212 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
128 simplrl 777 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))))
129 mzpf 42723 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) → 𝑎:(ℤ ↑m (ℤ ∖ (ℤ‘(𝑁 + 1))))⟶ℤ)
130128, 129syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → 𝑎:(ℤ ↑m (ℤ ∖ (ℤ‘(𝑁 + 1))))⟶ℤ)
131 nn0ssz 12633 . . . . . . . . . . . . . . . . . . . . . 22 0 ⊆ ℤ
132 mapss 8927 . . . . . . . . . . . . . . . . . . . . . 22 ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0m ℤ) ⊆ (ℤ ↑m ℤ))
1333, 131, 132mp2an 692 . . . . . . . . . . . . . . . . . . . . 21 (ℕ0m ℤ) ⊆ (ℤ ↑m ℤ)
134133sseli 3990 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ (ℕ0m ℤ) → 𝑓 ∈ (ℤ ↑m ℤ))
135 elmapssres 8905 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℤ ↑m ℤ) ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℤ ↑m (ℤ ∖ (ℤ‘(𝑁 + 1)))))
136134, 95, 135sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℕ0m ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℤ ↑m (ℤ ∖ (ℤ‘(𝑁 + 1)))))
137136adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) ∈ (ℤ ↑m (ℤ ∖ (ℤ‘(𝑁 + 1)))))
138130, 137ffvelcdmd 7104 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) ∈ ℤ)
139138zred 12719 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) ∈ ℝ)
140 simplrr 778 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → 𝑏 ∈ (mzPoly‘ℕ))
141 mzpf 42723 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ (mzPoly‘ℕ) → 𝑏:(ℤ ↑m ℕ)⟶ℤ)
142140, 141syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → 𝑏:(ℤ ↑m ℕ)⟶ℤ)
143 elmapssres 8905 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (ℤ ↑m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑m ℕ))
144134, 99, 143sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (ℕ0m ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑m ℕ))
145144adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ ↑m ℕ))
146142, 145ffvelcdmd 7104 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℤ)
147146zred 12719 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ)
148 sumsqeq0 14214 . . . . . . . . . . . . . . . 16 (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
149139, 147, 148syl2anc 584 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
150134adantl 481 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → 𝑓 ∈ (ℤ ↑m ℤ))
151 reseq1 5993 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))
152151fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))))
153152oveq1d 7445 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2))
154 reseq1 5993 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ))
155154fveq2d 6910 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ)))
156155oveq1d 7445 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2))
157153, 156oveq12d 7448 . . . . . . . . . . . . . . . . . 18 (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
158 eqid 2734 . . . . . . . . . . . . . . . . . 18 (𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))
159 ovex 7463 . . . . . . . . . . . . . . . . . 18 (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈ V
160157, 158, 159fvmpt 7015 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (ℤ ↑m ℤ) → ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
161150, 160syl 17 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
162161eqeq1d 2736 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
163149, 162bitr4d 282 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))
164163anbi2d 630 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0m ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
165164rexbidva 3174 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
166127, 165bitrd 279 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
16731, 166bitr3id 285 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
168167abbidv 2805 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ (∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
16930, 168eqtrid 2786 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
170 simpl 482 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈ ℕ0)
171 fzssuz 13601 . . . . . . . . . . . 12 (1...𝑁) ⊆ (ℤ‘1)
172 uzssz 12896 . . . . . . . . . . . 12 (ℤ‘1) ⊆ ℤ
173171, 172sstri 4004 . . . . . . . . . . 11 (1...𝑁) ⊆ ℤ
1743, 173pm3.2i 470 . . . . . . . . . 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 771 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))))
179 mzpresrename 42737 . . . . . . . . . . . 12 ((ℤ ∈ V ∧ (ℤ ∖ (ℤ‘(𝑁 + 1))) ⊆ ℤ ∧ 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
180176, 177, 178, 179syl3anc 1370 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
181 2nn0 12540 . . . . . . . . . . 11 2 ∈ ℕ0
182 mzpexpmpt 42732 . . . . . . . . . . 11 (((𝑔 ∈ (ℤ ↑m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
183180, 181, 182sylancl 586 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
18499a1i 11 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℕ ⊆ ℤ)
185 simprr 773 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈ (mzPoly‘ℕ))
186 mzpresrename 42737 . . . . . . . . . . . 12 ((ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
187176, 184, 185, 186syl3anc 1370 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
188 mzpexpmpt 42732 . . . . . . . . . . 11 (((𝑔 ∈ (ℤ ↑m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
189187, 181, 188sylancl 586 . . . . . . . . . 10 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
190 mzpaddmpt 42728 . . . . . . . . . 10 (((𝑔 ∈ (ℤ ↑m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
191183, 189, 190syl2anc 584 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
192 eldioph2 42749 . . . . . . . . 9 ((𝑁 ∈ ℕ0 ∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
193170, 175, 191, 192syl3anc 1370 . . . . . . . 8 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
194169, 193eqeltrd 2838 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) ∈ (Dioph‘𝑁))
195 ineq12 4222 . . . . . . . 8 ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}))
196195eleq1d 2823 . . . . . . 7 ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → ((𝐴𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) ∈ (Dioph‘𝑁)))
197194, 196syl5ibrcom 247 . . . . . 6 ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
198197rexlimdvva 3210 . . . . 5 (𝑁 ∈ ℕ0 → (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
19929, 198biimtrrid 243 . . . 4 (𝑁 ∈ ℕ0 → ((∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0m (ℤ ∖ (ℤ‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏𝑒) = 0)}) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
20028, 199sylbid 240 . . 3 (𝑁 ∈ ℕ0 → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
2011, 200syl 17 . 2 (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁)))
202201anabsi5 669 1 ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴𝐵) ∈ (Dioph‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  {cab 2711  wrex 3067  Vcvv 3477  cdif 3959  cun 3960  cin 3961  wss 3962   class class class wbr 5147  cmpt 5230  cres 5690  wf 6558  cfv 6562  (class class class)co 7430  ωcom 7886  m cmap 8864  cen 8980  Fincfn 8983  cr 11151  0cc0 11152  1c1 11153   + caddc 11155  cle 11293  cn 12263  2c2 12318  0cn0 12523  cz 12610  cuz 12875  ...cfz 13543  cexp 14098  mzPolycmzp 42709  Diophcdioph 42742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-oadd 8508  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-dju 9938  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264  df-2 12326  df-n0 12524  df-z 12611  df-uz 12876  df-fz 13544  df-seq 14039  df-exp 14099  df-hash 14366  df-mzpcl 42710  df-mzp 42711  df-dioph 42743
This theorem is referenced by:  anrabdioph  42767
  Copyright terms: Public domain W3C validator