Theorem diophin 36354

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.

Step	Hyp	Ref	Expression
1		eldiophelnn0 36345	. . 3 ⊢ (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈ ℕ0)
2		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0)
3		zex 11263	. . . . . . 7 ⊢ ℤ ∈ V
4		difexg 4735	. . . . . . 7 ⊢ (ℤ ∈ V → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ V)
5	3, 4	mp1i 13	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ V)
6		ominf 8057	. . . . . . 7 ⊢ ¬ ω ∈ Fin
7		nn0z 11277	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
8		lzenom 36351	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ≈ ω)
9		enfi 8061	. . . . . . . 8 ⊢ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ≈ ω → ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
10	7, 8, 9	3syl 18	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
11	6, 10	mtbiri 316	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → ¬ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin)
12		fz1eqin 36350	. . . . . . 7 ⊢ (𝑁 ∈ ℕ0 → (1...𝑁) = ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ))
13		inss1 3795	. . . . . . 7 ⊢ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))
14	12, 13	syl6eqss 3618	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (1...𝑁) ⊆ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))
15		eldioph2b 36344	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
16	2, 5, 11, 14, 15	syl22anc 1319	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
17		nnex 10903	. . . . . . 7 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → ℕ ∈ V)
19		1z 11284	. . . . . . 7 ⊢ 1 ∈ ℤ
20		nnuz 11599	. . . . . . . 8 ⊢ ℕ = (ℤ≥‘1)
21	20	uzinf 12626	. . . . . . 7 ⊢ (1 ∈ ℤ → ¬ ℕ ∈ Fin)
22	19, 21	mp1i 13	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → ¬ ℕ ∈ Fin)
23		elfznn 12241	. . . . . . . 8 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
24	23	ssriv 3572	. . . . . . 7 ⊢ (1...𝑁) ⊆ ℕ
25	24	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (1...𝑁) ⊆ ℕ)
26		eldioph2b 36344	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
27	2, 18, 22, 25, 26	syl22anc 1319	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
28	16, 27	anbi12d 743	. . . 4 ⊢ (𝑁 ∈ ℕ0 → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})))
29		reeanv 3086	. . . . 5 ⊢ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
30		inab 3854	. . . . . . . . 9 ⊢ ({𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))}
31		reeanv 3086	. . . . . . . . . . 11 ⊢ (∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
32		simplrl 796	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
33		simplrr 797	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))
34	12	eqcomd 2616	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁))
35	34	reseq2d 5317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ0 → (𝑑 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
36	35	ad3antrrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
37	34	reseq2d 5317	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ0 → (𝑒 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
38	37	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
39		simprrl 800	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁)))
40		simprll 798	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁)))
41	38, 39, 40	3eqtr2d 2650	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
42	36, 41	eqtr4d 2647	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)))
43		elmapresaun 36352	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ))) → (𝑑 ∪ 𝑒) ∈ (ℕ0 ↑𝑚 ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ)))
44	32, 33, 42, 43	syl3anc 1318	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ0 ↑𝑚 ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ)))
45	20	uneq2i 3726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ (ℤ≥‘1))
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℤ)
47		nn0p1nn 11209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)
48	47	nnge1d 10940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ0 → 1 ≤ (𝑁 + 1))
49		lzunuz 36349	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ (𝑁 + 1)) → ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ (ℤ≥‘1)) = ℤ)
50	7, 46, 48, 49	syl3anc 1318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ (ℤ≥‘1)) = ℤ)
51	45, 50	syl5eq 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 → ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ) = ℤ)
52	51	oveq2d 6565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → (ℕ0 ↑𝑚 ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ0 ↑𝑚 ℤ))
53	52	ad3antrrr 762	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (ℕ0 ↑𝑚 ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ0 ↑𝑚 ℤ))
54	44, 53	eleqtrd 2690	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ0 ↑𝑚 ℤ))
55		unidm 3718	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∪ 𝑐) = 𝑐
56	40, 39	uneq12d 3730	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 ∪ 𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
57	55, 56	syl5eqr 2658	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
58		resundir 5331	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))
59	57, 58	syl6eqr 2662	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
60		uncom 3719	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∪ 𝑒) = (𝑒 ∪ 𝑑)
61	60	reseq1i 5313	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))
62		incom 3767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)
63	62, 34	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ0 → (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = (1...𝑁))
64	63	reseq2d 5317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ0 → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
65	64	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
66	63	reseq2d 5317	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ0 → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
67	66	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
68	67, 40, 39	3eqtr2d 2650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
69	65, 68	eqtr4d 2647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))))
70		elmapresaunres2 36353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 ∈ (ℕ0 ↑𝑚 ℕ) ∧ 𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = 𝑑)
71	33, 32, 69, 70	syl3anc 1318	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = 𝑑)
72	61, 71	syl5eq 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = 𝑑)
73	72	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑎‘𝑑))
74		simprlr 799	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘𝑑) = 0)
75	73, 74	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0)
76		elmapresaunres2 36353	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ≥‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
77	32, 33, 42, 76	syl3anc 1318	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
78	77	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = (𝑏‘𝑒))
79		simprrr 801	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘𝑒) = 0)
80	78, 79	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)
81	59, 75, 80	jca32 556	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
82		reseq1 5311	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
83	82	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))))
84		reseq1 5311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
85	84	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))))
86	85	eqeq1d 2612	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0))
87		reseq1 5311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ ℕ) = ((𝑑 ∪ 𝑒) ↾ ℕ))
88	87	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑏‘(𝑓 ↾ ℕ)) = (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)))
89	88	eqeq1d 2612	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))
90	86, 89	anbi12d 743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
91	83, 90	anbi12d 743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))))
92	91	rspcev 3282	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 ∪ 𝑒) ∈ (ℕ0 ↑𝑚 ℤ) ∧ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) → ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
93	54, 81, 92	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
94	93	ex 449	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ0 ↑𝑚 ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
95	94	rexlimdvva 3020	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
96		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → 𝑓 ∈ (ℕ0 ↑𝑚 ℤ))
97		difss 3699	. . . . . . . . . . . . . . . . . 18 ⊢ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ
98		elmapssres 7768	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ (ℕ0 ↑𝑚 ℤ) ∧ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
99	96, 97, 98	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
100	99	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
101		nnssz 11274	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ ⊆ ℤ
102		elmapssres 7768	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ (ℕ0 ↑𝑚 ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℕ0 ↑𝑚 ℕ))
103	96, 101, 102	sylancl 693	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ0 ↑𝑚 ℕ))
104	103	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈ (ℕ0 ↑𝑚 ℕ))
105		simprl 790	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁)))
106	14	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))
107	106	resabs1d 5348	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
108	105, 107	eqtr4d 2647	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
109		simprrl 800	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0)
110	108, 109	jca 553	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0))
111		resabs1 5347	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1...𝑁) ⊆ ℕ → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
112	24, 111	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
113	105, 112	eqtr4d 2647	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
114		simprrr 801	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0)
115	110, 113, 114	jca32 556	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
116		reseq1 5311	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
117	116	eqeq2d 2620	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁))))
118		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) → (𝑎‘𝑑) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))))
119	118	eqeq1d 2612	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) → ((𝑎‘𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0))
120	117, 119	anbi12d 743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0)))
121	120	anbi1d 737	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
122		reseq1 5311	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
123	122	eqeq2d 2620	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))))
124		fveq2 6103	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑏‘𝑒) = (𝑏‘(𝑓 ↾ ℕ)))
125	124	eqeq1d 2612	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑏‘𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0))
126	123, 125	anbi12d 743	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
127	126	anbi2d 736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
128	121, 127	rspc2ev 3295	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈ (ℕ0 ↑𝑚 ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
129	100, 104, 115, 128	syl3anc 1318	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
130	129	ex 449	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
131	130	rexlimdva 3013	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
132	95, 131	impbid 201	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
133		simplrl 796	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
134		mzpf 36317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) → 𝑎:(ℤ ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))⟶ℤ)
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → 𝑎:(ℤ ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))⟶ℤ)
136		nn0ssz 11275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ0 ⊆ ℤ
137		mapss 7786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0 ↑𝑚 ℤ) ⊆ (ℤ ↑𝑚 ℤ))
138	3, 136, 137	mp2an 704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ0 ↑𝑚 ℤ) ⊆ (ℤ ↑𝑚 ℤ)
139	138	sseli 3564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (ℕ0 ↑𝑚 ℤ) → 𝑓 ∈ (ℤ ↑𝑚 ℤ))
140		elmapssres 7768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑𝑚 ℤ) ∧ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∈ (ℤ ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
141	139, 97, 140	sylancl 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ0 ↑𝑚 ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∈ (ℤ ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
142	141	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∈ (ℤ ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
143	135, 142	ffvelrnd 6268	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) ∈ ℤ)
144	143	zred 11358	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) ∈ ℝ)
145		simplrr 797	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → 𝑏 ∈ (mzPoly‘ℕ))
146		mzpf 36317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (mzPoly‘ℕ) → 𝑏:(ℤ ↑𝑚 ℕ)⟶ℤ)
147	145, 146	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → 𝑏:(ℤ ↑𝑚 ℕ)⟶ℤ)
148		elmapssres 7768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑𝑚 ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑𝑚 ℕ))
149	139, 101, 148	sylancl 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ0 ↑𝑚 ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑𝑚 ℕ))
150	149	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ ↑𝑚 ℕ))
151	147, 150	ffvelrnd 6268	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℤ)
152	151	zred 11358	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ)
153		sumsqeq0 12804	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
154	144, 152, 153	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
155	139	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → 𝑓 ∈ (ℤ ↑𝑚 ℤ))
156		reseq1 5311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
157	156	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))))
158	157	oveq1d 6564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2))
159		reseq1 5311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ))
160	159	fveq2d 6107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ)))
161	160	oveq1d 6564	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2))
162	158, 161	oveq12d 6567	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
163		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))
164		ovex 6577	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈ V
165	162, 163, 164	fvmpt 6191	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (ℤ ↑𝑚 ℤ) → ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
166	155, 165	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
167	166	eqeq1d 2612	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
168	154, 167	bitr4d 270	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))
169	168	anbi2d 736	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ0 ↑𝑚 ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
170	169	rexbidva 3031	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
171	132, 170	bitrd 267	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
172	31, 171	syl5bbr 273	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
173	172	abbidv 2728	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ (∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
174	30, 173	syl5eq 2656	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
175		simpl 472	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈ ℕ0)
176		fzssuz 12253	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ (ℤ≥‘1)
177		uzssz 11583	. . . . . . . . . . . 12 ⊢ (ℤ≥‘1) ⊆ ℤ
178	176, 177	sstri 3577	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℤ
179	3, 178	pm3.2i 470	. . . . . . . . . 10 ⊢ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ)
180	179	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ))
181	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℤ ∈ V)
182	97	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ)
183		simprl 790	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))))
184		mzpresrename 36331	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ (ℤ ∖ (ℤ≥‘(𝑁 + 1))) ⊆ ℤ ∧ 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
185	181, 182, 183, 184	syl3anc 1318	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
186		2nn0 11186	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ0
187		mzpexpmpt 36326	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
188	185, 186, 187	sylancl 693	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
189	101	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℕ ⊆ ℤ)
190		simprr 792	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈ (mzPoly‘ℕ))
191		mzpresrename 36331	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
192	181, 189, 190, 191	syl3anc 1318	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
193		mzpexpmpt 36326	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ0) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
194	192, 186, 193	sylancl 693	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
195		mzpaddmpt 36322	. . . . . . . . . 10 ⊢ (((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
196	188, 194, 195	syl2anc 691	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
197		eldioph2 36343	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
198	175, 180, 196, 197	syl3anc 1318	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ ∃𝑓 ∈ (ℕ0 ↑𝑚 ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑𝑚 ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
199	174, 198	eqeltrd 2688	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁))
200		ineq12 3771	. . . . . . . 8 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
201	200	eleq1d 2672	. . . . . . 7 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → ((𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁)))
202	199, 201	syl5ibrcom 236	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
203	202	rexlimdvva 3020	. . . . 5 ⊢ (𝑁 ∈ ℕ0 → (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
204	29, 203	syl5bir 232	. . . 4 ⊢ (𝑁 ∈ ℕ0 → ((∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ0 ↑𝑚 (ℤ ∖ (ℤ≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ0 ↑𝑚 ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
205	28, 204	sylbid 229	. . 3 ⊢ (𝑁 ∈ ℕ0 → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
206	1, 205	syl 17	. 2 ⊢ (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
207	206	anabsi5 854	1 ⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540   class class class wbr 4583   ↦ cmpt 4643   ↾ cres 5040  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ωcom 6957   ↑_𝑚 cmap 7744   ≈ cen 7838  Fincfn 7841  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   ≤ cle 9954  ℕcn 10897  2c2 10947  ℕ₀cn0 11169  ℤcz 11254  ℤ_≥cuz 11563  ...cfz 12197  ↑cexp 12722  mzPolycmzp 36303  Diophcdioph 36336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-seq 12664  df-exp 12723  df-hash 12980  df-mzpcl 36304  df-mzp 36305  df-dioph 36337

This theorem is referenced by:  anrabdioph  36362