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 39362

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 39354	. . 3 ⊢ (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈ ℕ₀)
2		id 22	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℕ₀)
3		zex 11984	. . . . . . 7 ⊢ ℤ ∈ V
4		difexg 5223	. . . . . . 7 ⊢ (ℤ ∈ V → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
5	3, 4	mp1i 13	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
6		ominf 8724	. . . . . . 7 ⊢ ¬ ω ∈ Fin
7		nn0z 11999	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
8		lzenom 39360	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ≈ ω)
9		enfi 8728	. . . . . . . 8 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ≈ ω → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
10	7, 8, 9	3syl 18	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
11	6, 10	mtbiri 329	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ¬ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin)
12		fz1eqin 39359	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))
13		inss1 4204	. . . . . . 7 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))
14	12, 13	eqsstrdi 4020	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
15		eldioph2b 39353	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
16	2, 5, 11, 14, 15	syl22anc 836	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
17		nnex 11638	. . . . . . 7 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ℕ ∈ V)
19		1z 12006	. . . . . . 7 ⊢ 1 ∈ ℤ
20		nnuz 12275	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
21	20	uzinf 13327	. . . . . . 7 ⊢ (1 ∈ ℤ → ¬ ℕ ∈ Fin)
22	19, 21	mp1i 13	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ¬ ℕ ∈ Fin)
23		elfznn 12930	. . . . . . . 8 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
24	23	ssriv 3970	. . . . . . 7 ⊢ (1...𝑁) ⊆ ℕ
25	24	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ ℕ)
26		eldioph2b 39353	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
27	2, 18, 22, 25, 26	syl22anc 836	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
28	16, 27	anbi12d 632	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})))
29		reeanv 3367	. . . . 5 ⊢ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
30		inab 4270	. . . . . . . . 9 ⊢ ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))}
31		reeanv 3367	. . . . . . . . . . 11 ⊢ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
32		simplrl 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
33		simplrr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑒 ∈ (ℕ₀ ↑_m ℕ))
34	12	eqcomd 2827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁))
35	34	reseq2d 5847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
36	35	ad3antrrr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
37	34	reseq2d 5847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
38	37	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
39		simprrl 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁)))
40		simprll 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁)))
41	38, 39, 40	3eqtr2d 2862	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
42	36, 41	eqtr4d 2859	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)))
43		elmapresaun 8438	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)))
44	32, 33, 42, 43	syl3anc 1367	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)))
45	20	uneq2i 4135	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1))
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ∈ ℤ)
47		nn0p1nn 11930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
48	47	nnge1d 11679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ≤ (𝑁 + 1))
49		lzunuz 39358	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ (𝑁 + 1)) → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
50	7, 46, 48, 49	syl3anc 1367	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
51	45, 50	syl5eq 2868	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ℤ)
52	51	oveq2d 7166	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ₀ ↑_m ℤ))
53	52	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ₀ ↑_m ℤ))
54	44, 53	eleqtrd 2915	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ℤ))
55		unidm 4127	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∪ 𝑐) = 𝑐
56	40, 39	uneq12d 4139	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 ∪ 𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
57	55, 56	syl5eqr 2870	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
58		resundir 5862	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))
59	57, 58	syl6eqr 2874	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
60		uncom 4128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∪ 𝑒) = (𝑒 ∪ 𝑑)
61	60	reseq1i 5843	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
62		incom 4177	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)
63	62, 34	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (1...𝑁))
64	63	reseq2d 5847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
65	64	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
66	63	reseq2d 5847	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
67	66	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
68	67, 40, 39	3eqtr2d 2862	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
69	65, 68	eqtr4d 2859	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
70		elmapresaunres2 39361	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ 𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
71	33, 32, 69, 70	syl3anc 1367	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
72	61, 71	syl5eq 2868	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
73	72	fveq2d 6668	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘𝑑))
74		simprlr 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘𝑑) = 0)
75	73, 74	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
76		elmapresaunres2 39361	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
77	32, 33, 42, 76	syl3anc 1367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
78	77	fveq2d 6668	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = (𝑏‘𝑒))
79		simprrr 780	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘𝑒) = 0)
80	78, 79	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)
81	59, 75, 80	jca32 518	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
82		reseq1 5841	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
83	82	eqeq2d 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))))
84		reseq1 5841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
85	84	fveqeq2d 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
86		reseq1 5841	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ ℕ) = ((𝑑 ∪ 𝑒) ↾ ℕ))
87	86	fveqeq2d 6672	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))
88	85, 87	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
89	83, 88	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))))
90	89	rspcev 3622	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ℤ) ∧ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
91	54, 81, 90	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
92	91	ex 415	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
93	92	rexlimdvva 3294	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
94		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℕ₀ ↑_m ℤ))
95		difss 4107	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ
96		elmapssres 8425	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
97	94, 95, 96	sylancl 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
98	97	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
99		nnssz 11996	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℤ
100		elmapssres 8425	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
101	94, 99, 100	sylancl 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
102	101	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
103		simprl 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁)))
104	14	ad3antrrr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
105	104	resabs1d 5878	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
106	103, 105	eqtr4d 2859	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
107		simprrl 779	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
108	106, 107	jca 514	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
109		resabs1 5877	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) ⊆ ℕ → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
110	24, 109	mp1i 13	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
111	103, 110	eqtr4d 2859	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
112		simprrr 780	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0)
113	108, 111, 112	jca32 518	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
114		reseq1 5841	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
115	114	eqeq2d 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁))))
116		fveqeq2 6673	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑎‘𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
117	115, 116	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)))
118	117	anbi1d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
119		reseq1 5841	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
120	119	eqeq2d 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))))
121		fveqeq2 6673	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑏‘𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0))
122	120, 121	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
123	122	anbi2d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
124	118, 123	rspc2ev 3634	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
125	98, 102, 113, 124	syl3anc 1367	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
126	125	rexlimdva2 3287	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
127	93, 126	impbid 214	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
128		simplrl 775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
129		mzpf 39326	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
131		nn0ssz 11997	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ₀ ⊆ ℤ
132		mapss 8447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℤ ∈ V ∧ ℕ₀ ⊆ ℤ) → (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ))
133	3, 131, 132	mp2an 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ)
134	133	sseli 3962	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → 𝑓 ∈ (ℤ ↑_m ℤ))
135		elmapssres 8425	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
136	134, 95, 135	sylancl 588	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
137	136	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
138	130, 137	ffvelrnd 6846	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℤ)
139	138	zred 12081	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ)
140		simplrr 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏 ∈ (mzPoly‘ℕ))
141		mzpf 39326	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (mzPoly‘ℕ) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
143		elmapssres 8425	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
144	134, 99, 143	sylancl 588	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
145	144	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
146	142, 145	ffvelrnd 6846	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℤ)
147	146	zred 12081	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ)
148		sumsqeq0 13536	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
149	139, 147, 148	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
150	134	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℤ ↑_m ℤ))
151		reseq1 5841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
152	151	fveq2d 6668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
153	152	oveq1d 7165	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2))
154		reseq1 5841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ))
155	154	fveq2d 6668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ)))
156	155	oveq1d 7165	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2))
157	153, 156	oveq12d 7168	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
158		eqid 2821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))
159		ovex 7183	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈ V
160	157, 158, 159	fvmpt 6762	. . . . . . . . . . . . . . . . 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 2823	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
163	149, 162	bitr4d 284	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))
164	163	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
165	164	rexbidva 3296	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
166	127, 165	bitrd 281	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
167	31, 166	syl5bbr 287	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
168	167	abbidv 2885	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
169	30, 168	syl5eq 2868	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
170		simpl 485	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈ ℕ₀)
171		fzssuz 12942	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
172		uzssz 12258	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘1) ⊆ ℤ
173	171, 172	sstri 3975	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℤ
174	3, 173	pm3.2i 473	. . . . . . . . . 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 769	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
179		mzpresrename 39340	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ ∧ 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
180	176, 177, 178, 179	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
181		2nn0 11908	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
182		mzpexpmpt 39335	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
183	180, 181, 182	sylancl 588	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
184	99	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℕ ⊆ ℤ)
185		simprr 771	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈ (mzPoly‘ℕ))
186		mzpresrename 39340	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
187	176, 184, 185, 186	syl3anc 1367	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
188		mzpexpmpt 39335	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
189	187, 181, 188	sylancl 588	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
190		mzpaddmpt 39331	. . . . . . . . . 10 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
191	183, 189, 190	syl2anc 586	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
192		eldioph2 39352	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
193	170, 175, 191, 192	syl3anc 1367	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
194	169, 193	eqeltrd 2913	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁))
195		ineq12 4183	. . . . . . . 8 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
196	195	eleq1d 2897	. . . . . . 7 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → ((𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁)))
197	194, 196	syl5ibrcom 249	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
198	197	rexlimdvva 3294	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
199	29, 198	syl5bir 245	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → ((∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
200	28, 199	sylbid 242	. . 3 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
201	1, 200	syl 17	. 2 ⊢ (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
202	201	anabsi5 667	1 ⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 {cab 2799 ∃wrex 3139 Vcvv 3494 ∖ cdif 3932 ∪ cun 3933 ∩ cin 3934 ⊆ wss 3935 class class class wbr 5058 ↦ cmpt 5138 ↾ cres 5551 ⟶wf 6345 ‘cfv 6349 (class class class)co 7150 ωcom 7574 ↑_m cmap 8400 ≈ cen 8500 Fincfn 8503 ℝcr 10530 0cc0 10531 1c1 10532 + caddc 10534 ≤ cle 10670 ℕcn 11632 2c2 11686 ℕ₀cn0 11891 ℤcz 11975 ℤ_≥cuz 12237 ...cfz 12886 ↑cexp 13423 mzPolycmzp 39312 Diophcdioph 39345

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-of 7403 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-er 8283 df-map 8402 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-dju 9324 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-nn 11633 df-2 11694 df-n0 11892 df-z 11976 df-uz 12238 df-fz 12887 df-seq 13364 df-exp 13424 df-hash 13685 df-mzpcl 39313 df-mzp 39314 df-dioph 39346

This theorem is referenced by: anrabdioph 39370

W3C validator