diophin - Mathbox for Stefan O'Rear

	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 43221

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 43213	. . 3 ⊢ (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈ ℕ₀)
2		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℕ₀)
3		zex 12524	. . . . . . 7 ⊢ ℤ ∈ V
4		difexg 5257	. . . . . . 7 ⊢ (ℤ ∈ V → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
5	3, 4	mp1i 13	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
6		ominf 9164	. . . . . . 7 ⊢ ¬ ω ∈ Fin
7		nn0z 12539	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
8		lzenom 43219	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ≈ ω)
9		enfi 9111	. . . . . . . 8 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ≈ ω → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
10	7, 8, 9	3syl 18	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
11	6, 10	mtbiri 328	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ¬ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin)
12		fz1eqin 43218	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))
13		inss1 4165	. . . . . . 7 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))
14	12, 13	eqsstrdi 3959	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
15		eldioph2b 43212	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
16	2, 5, 11, 14, 15	syl22anc 844	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
17		nnex 12171	. . . . . . 7 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ℕ ∈ V)
19		1z 12548	. . . . . . 7 ⊢ 1 ∈ ℤ
20		nnuz 12818	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
21	20	uzinf 13918	. . . . . . 7 ⊢ (1 ∈ ℤ → ¬ ℕ ∈ Fin)
22	19, 21	mp1i 13	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ¬ ℕ ∈ Fin)
23		elfznn 13498	. . . . . . . 8 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
24	23	ssriv 3919	. . . . . . 7 ⊢ (1...𝑁) ⊆ ℕ
25	24	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ ℕ)
26		eldioph2b 43212	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
27	2, 18, 22, 25, 26	syl22anc 844	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
28	16, 27	anbi12d 638	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})))
29		reeanv 3211	. . . . 5 ⊢ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
30		inab 4237	. . . . . . . . 9 ⊢ ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))}
31		reeanv 3211	. . . . . . . . . . 11 ⊢ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
32		simplrl 782	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
33		simplrr 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑒 ∈ (ℕ₀ ↑_m ℕ))
34	12	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁))
35	34	reseq2d 5931	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
36	35	ad3antrrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
37	34	reseq2d 5931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
38	37	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
39		simprrl 786	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁)))
40		simprll 784	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁)))
41	38, 39, 40	3eqtr2d 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
42	36, 41	eqtr4d 2777	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)))
43		elmapresaun 8818	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)))
44	32, 33, 42, 43	syl3anc 1379	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)))
45	20	uneq2i 4095	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1))
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ∈ ℤ)
47		nn0p1nn 12467	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
48	47	nnge1d 12216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ≤ (𝑁 + 1))
49		lzunuz 43217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ (𝑁 + 1)) → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
50	7, 46, 48, 49	syl3anc 1379	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
51	45, 50	eqtrid 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ℤ)
52	51	oveq2d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ₀ ↑_m ℤ))
53	52	ad3antrrr 736	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ₀ ↑_m ℤ))
54	44, 53	eleqtrd 2841	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ℤ))
55		unidm 4087	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∪ 𝑐) = 𝑐
56	40, 39	uneq12d 4099	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 ∪ 𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
57	55, 56	eqtr3id 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
58		resundir 5946	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))
59	57, 58	eqtr4di 2792	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
60		uncom 4088	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∪ 𝑒) = (𝑒 ∪ 𝑑)
61	60	reseq1i 5927	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
62		incom 4138	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)
63	62, 34	eqtrid 2786	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (1...𝑁))
64	63	reseq2d 5931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
65	64	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
66	63	reseq2d 5931	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
67	66	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
68	67, 40, 39	3eqtr2d 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
69	65, 68	eqtr4d 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
70		elmapresaunres2 43220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ 𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
71	33, 32, 69, 70	syl3anc 1379	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
72	61, 71	eqtrid 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
73	72	fveq2d 6831	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘𝑑))
74		simprlr 785	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘𝑑) = 0)
75	73, 74	eqtrd 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
76		elmapresaunres2 43220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
77	32, 33, 42, 76	syl3anc 1379	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
78	77	fveq2d 6831	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = (𝑏‘𝑒))
79		simprrr 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘𝑒) = 0)
80	78, 79	eqtrd 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)
81	59, 75, 80	jca32 520	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
82		reseq1 5925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
83	82	eqeq2d 2750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))))
84		reseq1 5925	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
85	84	fveqeq2d 6835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
86		reseq1 5925	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ ℕ) = ((𝑑 ∪ 𝑒) ↾ ℕ))
87	86	fveqeq2d 6835	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))
88	85, 87	anbi12d 638	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
89	83, 88	anbi12d 638	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))))
90	89	rspcev 3560	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ℤ) ∧ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
91	54, 81, 90	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
92	91	ex 413	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
93	92	rexlimdvva 3196	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
94		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℕ₀ ↑_m ℤ))
95		difss 4066	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ
96		elmapssres 8804	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
97	94, 95, 96	sylancl 592	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
98	97	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
99		nnssz 12537	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℤ
100		elmapssres 8804	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
101	94, 99, 100	sylancl 592	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
102	101	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
103		simprl 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁)))
104	14	ad3antrrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
105	104	resabs1d 5960	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
106	103, 105	eqtr4d 2777	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
107		simprrl 786	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
108	106, 107	jca 516	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
109		resabs1 5958	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) ⊆ ℕ → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
110	24, 109	mp1i 13	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
111	103, 110	eqtr4d 2777	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
112		simprrr 787	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0)
113	108, 111, 112	jca32 520	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
114		reseq1 5925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
115	114	eqeq2d 2750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁))))
116		fveqeq2 6836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑎‘𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
117	115, 116	anbi12d 638	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)))
118	117	anbi1d 637	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
119		reseq1 5925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
120	119	eqeq2d 2750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))))
121		fveqeq2 6836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑏‘𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0))
122	120, 121	anbi12d 638	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
123	122	anbi2d 636	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
124	118, 123	rspc2ev 3573	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
125	98, 102, 113, 124	syl3anc 1379	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
126	125	rexlimdva2 3142	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
127	93, 126	impbid 213	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
128		simplrl 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
129		mzpf 43185	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
131		nn0ssz 12538	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ₀ ⊆ ℤ
132		mapss 8827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℤ ∈ V ∧ ℕ₀ ⊆ ℤ) → (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ))
133	3, 131, 132	mp2an 698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ)
134	133	sseli 3911	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → 𝑓 ∈ (ℤ ↑_m ℤ))
135		elmapssres 8804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
136	134, 95, 135	sylancl 592	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
137	136	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
138	130, 137	ffvelcdmd 7026	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℤ)
139	138	zred 12624	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ)
140		simplrr 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏 ∈ (mzPoly‘ℕ))
141		mzpf 43185	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (mzPoly‘ℕ) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
143		elmapssres 8804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
144	134, 99, 143	sylancl 592	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
145	144	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
146	142, 145	ffvelcdmd 7026	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℤ)
147	146	zred 12624	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ)
148		sumsqeq0 14132	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
149	139, 147, 148	syl2anc 590	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
150	134	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℤ ↑_m ℤ))
151		reseq1 5925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
152	151	fveq2d 6831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
153	152	oveq1d 7371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2))
154		reseq1 5925	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ))
155	154	fveq2d 6831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ)))
156	155	oveq1d 7371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2))
157	153, 156	oveq12d 7374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
158		eqid 2739	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))
159		ovex 7389	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈ V
160	157, 158, 159	fvmpt 6935	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (ℤ ↑_m ℤ) → ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
161	150, 160	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
162	161	eqeq1d 2741	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
163	149, 162	bitr4d 283	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))
164	163	anbi2d 636	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
165	164	rexbidva 3161	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
166	127, 165	bitrd 280	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
167	31, 166	bitr3id 286	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
168	167	abbidv 2805	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
169	30, 168	eqtrid 2786	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
170		simpl 483	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈ ℕ₀)
171		fzssuz 13510	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
172		uzssz 12800	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘1) ⊆ ℤ
173	171, 172	sstri 3924	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℤ
174	3, 173	pm3.2i 471	. . . . . . . . . 10 ⊢ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ)
175	174	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ))
176	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℤ ∈ V)
177	95	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ)
178		simprl 776	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
179		mzpresrename 43199	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ ∧ 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
180	176, 177, 178, 179	syl3anc 1379	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
181		2nn0 12445	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
182		mzpexpmpt 43194	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
183	180, 181, 182	sylancl 592	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
184	99	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℕ ⊆ ℤ)
185		simprr 778	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈ (mzPoly‘ℕ))
186		mzpresrename 43199	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
187	176, 184, 185, 186	syl3anc 1379	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
188		mzpexpmpt 43194	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
189	187, 181, 188	sylancl 592	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
190		mzpaddmpt 43190	. . . . . . . . . 10 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
191	183, 189, 190	syl2anc 590	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
192		eldioph2 43211	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
193	170, 175, 191, 192	syl3anc 1379	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
194	169, 193	eqeltrd 2839	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁))
195		ineq12 4144	. . . . . . . 8 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
196	195	eleq1d 2824	. . . . . . 7 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → ((𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁)))
197	194, 196	syl5ibrcom 248	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
198	197	rexlimdvva 3196	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
199	29, 198	biimtrrid 244	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → ((∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
200	28, 199	sylbid 241	. . 3 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
201	1, 200	syl 17	. 2 ⊢ (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
202	201	anabsi5 675	1 ⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1547 ∈ wcel 2119 {cab 2717 ∃wrex 3063 Vcvv 3431 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 class class class wbr 5072 ↦ cmpt 5153 ↾ cres 5620 ⟶wf 6481 ‘cfv 6485 (class class class)co 7356 ωcom 7806 ↑_m cmap 8763 ≈ cen 8880 Fincfn 8883 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 ≤ cle 11171 ℕcn 12165 2c2 12227 ℕ₀cn0 12428 ℤcz 12515 ℤ_≥cuz 12779 ...cfz 13452 ↑cexp 14014 mzPolycmzp 43171 Diophcdioph 43204

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-oadd 8399 df-er 8633 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-dju 9816 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-n0 12429 df-z 12516 df-uz 12780 df-fz 13453 df-seq 13955 df-exp 14015 df-hash 14284 df-mzpcl 43172 df-mzp 43173 df-dioph 43205

This theorem is referenced by: anrabdioph 43229

W3C validator