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 40510

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 40502	. . 3 ⊢ (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈ ℕ₀)
2		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℕ₀)
3		zex 12258	. . . . . . 7 ⊢ ℤ ∈ V
4		difexg 5246	. . . . . . 7 ⊢ (ℤ ∈ V → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
5	3, 4	mp1i 13	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
6		ominf 8964	. . . . . . 7 ⊢ ¬ ω ∈ Fin
7		nn0z 12273	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
8		lzenom 40508	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ≈ ω)
9		enfi 8933	. . . . . . . 8 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ≈ ω → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
10	7, 8, 9	3syl 18	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
11	6, 10	mtbiri 326	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ¬ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin)
12		fz1eqin 40507	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))
13		inss1 4159	. . . . . . 7 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))
14	12, 13	eqsstrdi 3971	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
15		eldioph2b 40501	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
16	2, 5, 11, 14, 15	syl22anc 835	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
17		nnex 11909	. . . . . . 7 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ℕ ∈ V)
19		1z 12280	. . . . . . 7 ⊢ 1 ∈ ℤ
20		nnuz 12550	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
21	20	uzinf 13613	. . . . . . 7 ⊢ (1 ∈ ℤ → ¬ ℕ ∈ Fin)
22	19, 21	mp1i 13	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ¬ ℕ ∈ Fin)
23		elfznn 13214	. . . . . . . 8 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
24	23	ssriv 3921	. . . . . . 7 ⊢ (1...𝑁) ⊆ ℕ
25	24	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ ℕ)
26		eldioph2b 40501	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
27	2, 18, 22, 25, 26	syl22anc 835	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
28	16, 27	anbi12d 630	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})))
29		reeanv 3292	. . . . 5 ⊢ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
30		inab 4230	. . . . . . . . 9 ⊢ ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))}
31		reeanv 3292	. . . . . . . . . . 11 ⊢ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
32		simplrl 773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
33		simplrr 774	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑒 ∈ (ℕ₀ ↑_m ℕ))
34	12	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁))
35	34	reseq2d 5880	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
36	35	ad3antrrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
37	34	reseq2d 5880	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
38	37	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
39		simprrl 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁)))
40		simprll 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁)))
41	38, 39, 40	3eqtr2d 2784	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
42	36, 41	eqtr4d 2781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)))
43		elmapresaun 8626	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)))
44	32, 33, 42, 43	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)))
45	20	uneq2i 4090	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1))
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ∈ ℤ)
47		nn0p1nn 12202	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
48	47	nnge1d 11951	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ≤ (𝑁 + 1))
49		lzunuz 40506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ (𝑁 + 1)) → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
50	7, 46, 48, 49	syl3anc 1369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
51	45, 50	syl5eq 2791	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ℤ)
52	51	oveq2d 7271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ₀ ↑_m ℤ))
53	52	ad3antrrr 726	. . . . . . . . . . . . . . . . 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 4082	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∪ 𝑐) = 𝑐
56	40, 39	uneq12d 4094	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 ∪ 𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
57	55, 56	eqtr3id 2793	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
58		resundir 5895	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))
59	57, 58	eqtr4di 2797	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
60		uncom 4083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∪ 𝑒) = (𝑒 ∪ 𝑑)
61	60	reseq1i 5876	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
62		incom 4131	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)
63	62, 34	syl5eq 2791	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (1...𝑁))
64	63	reseq2d 5880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
65	64	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
66	63	reseq2d 5880	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
67	66	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
68	67, 40, 39	3eqtr2d 2784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
69	65, 68	eqtr4d 2781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
70		elmapresaunres2 40509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ 𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
71	33, 32, 69, 70	syl3anc 1369	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
72	61, 71	syl5eq 2791	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
73	72	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘𝑑))
74		simprlr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘𝑑) = 0)
75	73, 74	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
76		elmapresaunres2 40509	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
77	32, 33, 42, 76	syl3anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
78	77	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = (𝑏‘𝑒))
79		simprrr 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘𝑒) = 0)
80	78, 79	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)
81	59, 75, 80	jca32 515	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
82		reseq1 5874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
83	82	eqeq2d 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))))
84		reseq1 5874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
85	84	fveqeq2d 6764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
86		reseq1 5874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ ℕ) = ((𝑑 ∪ 𝑒) ↾ ℕ))
87	86	fveqeq2d 6764	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))
88	85, 87	anbi12d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
89	83, 88	anbi12d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))))
90	89	rspcev 3552	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ℤ) ∧ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
91	54, 81, 90	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
92	91	ex 412	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
93	92	rexlimdvva 3222	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
94		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℕ₀ ↑_m ℤ))
95		difss 4062	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ
96		elmapssres 8613	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
97	94, 95, 96	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
98	97	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
99		nnssz 12270	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℤ
100		elmapssres 8613	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
101	94, 99, 100	sylancl 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
103		simprl 767	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁)))
104	14	ad3antrrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
105	104	resabs1d 5911	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
106	103, 105	eqtr4d 2781	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
107		simprrl 777	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
108	106, 107	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
109		resabs1 5910	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) ⊆ ℕ → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
110	24, 109	mp1i 13	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
111	103, 110	eqtr4d 2781	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
112		simprrr 778	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0)
113	108, 111, 112	jca32 515	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
114		reseq1 5874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
115	114	eqeq2d 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁))))
116		fveqeq2 6765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑎‘𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
117	115, 116	anbi12d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)))
118	117	anbi1d 629	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
119		reseq1 5874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
120	119	eqeq2d 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))))
121		fveqeq2 6765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑏‘𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0))
122	120, 121	anbi12d 630	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
123	122	anbi2d 628	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
124	118, 123	rspc2ev 3564	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
125	98, 102, 113, 124	syl3anc 1369	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
126	125	rexlimdva2 3215	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
127	93, 126	impbid 211	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
128		simplrl 773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
129		mzpf 40474	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
131		nn0ssz 12271	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ₀ ⊆ ℤ
132		mapss 8635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℤ ∈ V ∧ ℕ₀ ⊆ ℤ) → (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ))
133	3, 131, 132	mp2an 688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ)
134	133	sseli 3913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → 𝑓 ∈ (ℤ ↑_m ℤ))
135		elmapssres 8613	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
136	134, 95, 135	sylancl 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
137	136	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
138	130, 137	ffvelrnd 6944	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℤ)
139	138	zred 12355	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ)
140		simplrr 774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏 ∈ (mzPoly‘ℕ))
141		mzpf 40474	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (mzPoly‘ℕ) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
143		elmapssres 8613	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
144	134, 99, 143	sylancl 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
145	144	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
146	142, 145	ffvelrnd 6944	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℤ)
147	146	zred 12355	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ)
148		sumsqeq0 13824	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
149	139, 147, 148	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
150	134	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℤ ↑_m ℤ))
151		reseq1 5874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
152	151	fveq2d 6760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
153	152	oveq1d 7270	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2))
154		reseq1 5874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ))
155	154	fveq2d 6760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ)))
156	155	oveq1d 7270	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2))
157	153, 156	oveq12d 7273	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
158		eqid 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))
159		ovex 7288	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈ V
160	157, 158, 159	fvmpt 6857	. . . . . . . . . . . . . . . . 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 2740	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
163	149, 162	bitr4d 281	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))
164	163	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
165	164	rexbidva 3224	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
166	127, 165	bitrd 278	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
167	31, 166	bitr3id 284	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
168	167	abbidv 2808	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
169	30, 168	syl5eq 2791	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
170		simpl 482	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈ ℕ₀)
171		fzssuz 13226	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
172		uzssz 12532	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘1) ⊆ ℤ
173	171, 172	sstri 3926	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℤ
174	3, 173	pm3.2i 470	. . . . . . . . . 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 767	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
179		mzpresrename 40488	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ ∧ 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
180	176, 177, 178, 179	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
181		2nn0 12180	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
182		mzpexpmpt 40483	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
183	180, 181, 182	sylancl 585	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
184	99	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℕ ⊆ ℤ)
185		simprr 769	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈ (mzPoly‘ℕ))
186		mzpresrename 40488	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
187	176, 184, 185, 186	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
188		mzpexpmpt 40483	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
189	187, 181, 188	sylancl 585	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
190		mzpaddmpt 40479	. . . . . . . . . 10 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
191	183, 189, 190	syl2anc 583	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
192		eldioph2 40500	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
193	170, 175, 191, 192	syl3anc 1369	. . . . . . . 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 4138	. . . . . . . 8 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
196	195	eleq1d 2823	. . . . . . 7 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → ((𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁)))
197	194, 196	syl5ibrcom 246	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
198	197	rexlimdvva 3222	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
199	29, 198	syl5bir 242	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → ((∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
200	28, 199	sylbid 239	. . 3 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
201	1, 200	syl 17	. 2 ⊢ (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
202	201	anabsi5 665	1 ⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 {cab 2715 ∃wrex 3064 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 class class class wbr 5070 ↦ cmpt 5153 ↾ cres 5582 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ωcom 7687 ↑_m cmap 8573 ≈ cen 8688 Fincfn 8691 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 ≤ cle 10941 ℕcn 11903 2c2 11958 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 ...cfz 13168 ↑cexp 13710 mzPolycmzp 40460 Diophcdioph 40493

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-oadd 8271 df-er 8456 df-map 8575 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-n0 12164 df-z 12250 df-uz 12512 df-fz 13169 df-seq 13650 df-exp 13711 df-hash 13973 df-mzpcl 40461 df-mzp 40462 df-dioph 40494

This theorem is referenced by: anrabdioph 40518

W3C validator