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 43503

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 43495	. . 3 ⊢ (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈ ℕ₀)
2		id 23	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℕ₀)
3		zex 12595	. . . . . . 7 ⊢ ℤ ∈ V
4		difexg 5300	. . . . . . 7 ⊢ (ℤ ∈ V → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
5	3, 4	mp1i 14	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
6		ominf 9220	. . . . . . 7 ⊢ ¬ ω ∈ Fin
7		nn0z 12610	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
8		lzenom 43501	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ≈ ω)
9		enfi 9167	. . . . . . . 8 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ≈ ω → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
10	7, 8, 9	3syl 19	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ↔ ω ∈ Fin))
11	6, 10	mtbiri 330	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ¬ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin)
12		fz1eqin 43500	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))
13		inss1 4189	. . . . . . 7 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))
14	12, 13	eqsstrdi 3981	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
15		eldioph2b 43494	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
16	2, 5, 11, 14, 15	syl22anc 851	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
17		nnex 12234	. . . . . . 7 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ℕ ∈ V)
19		1z 12619	. . . . . . 7 ⊢ 1 ∈ ℤ
20		nnuz 12896	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
21	20	uzinf 13997	. . . . . . 7 ⊢ (1 ∈ ℤ → ¬ ℕ ∈ Fin)
22	19, 21	mp1i 14	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ¬ ℕ ∈ Fin)
23		elfznn 13577	. . . . . . . 8 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
24	23	ssriv 3941	. . . . . . 7 ⊢ (1...𝑁) ⊆ ℕ
25	24	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ ℕ)
26		eldioph2b 43494	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
27	2, 18, 22, 25, 26	syl22anc 851	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
28	16, 27	anbi12d 643	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})))
29		reeanv 3237	. . . . 5 ⊢ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
30		inab 4262	. . . . . . . . 9 ⊢ ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))}
31		reeanv 3237	. . . . . . . . . . 11 ⊢ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
32		simplrl 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
33		simplrr 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑒 ∈ (ℕ₀ ↑_m ℕ))
34	12	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁))
35	34	reseq2d 5978	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
36	35	ad3antrrr 742	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
37	34	reseq2d 5978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
38	37	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
39		simprrl 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁)))
40		simprll 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁)))
41	38, 39, 40	3eqtr2d 2804	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
42	36, 41	eqtr4d 2801	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)))
43		elmapresaun 8874	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)))
44	32, 33, 42, 43	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)))
45	20	uneq2i 4119	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1))
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ∈ ℤ)
47		nn0p1nn 12538	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
48	47	nnge1d 12279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ≤ (𝑁 + 1))
49		lzunuz 43499	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ (𝑁 + 1)) → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
50	7, 46, 48, 49	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
51	45, 50	eqtrid 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ℤ)
52	51	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ₀ ↑_m ℤ))
53	52	ad3antrrr 742	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ₀ ↑_m ℤ))
54	44, 53	eleqtrd 2865	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ℤ))
55		unidm 4111	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∪ 𝑐) = 𝑐
56	40, 39	uneq12d 4123	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 ∪ 𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
57	55, 56	eqtr3id 2812	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
58		resundir 5993	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))
59	57, 58	eqtr4di 2816	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
60		uncom 4112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∪ 𝑒) = (𝑒 ∪ 𝑑)
61	60	reseq1i 5974	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
62		incom 4162	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)
63	62, 34	eqtrid 2810	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (1...𝑁))
64	63	reseq2d 5978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
65	64	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
66	63	reseq2d 5978	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
67	66	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
68	67, 40, 39	3eqtr2d 2804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
69	65, 68	eqtr4d 2801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
70		elmapresaunres2 43502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ 𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
71	33, 32, 69, 70	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
72	61, 71	eqtrid 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
73	72	fveq2d 6885	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘𝑑))
74		simprlr 791	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘𝑑) = 0)
75	73, 74	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
76		elmapresaunres2 43502	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ) ∧ (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
77	32, 33, 42, 76	syl3anc 1398	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ ℕ) = 𝑒)
78	77	fveq2d 6885	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = (𝑏‘𝑒))
79		simprrr 793	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘𝑒) = 0)
80	78, 79	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)
81	59, 75, 80	jca32 524	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
82		reseq1 5972	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
83	82	eqeq2d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))))
84		reseq1 5972	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
85	84	fveqeq2d 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
86		reseq1 5972	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ ℕ) = ((𝑑 ∪ 𝑒) ↾ ℕ))
87	86	fveqeq2d 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))
88	85, 87	anbi12d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
89	83, 88	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))))
90	89	rspcev 3581	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ℤ) ∧ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
91	54, 81, 90	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
92	91	ex 417	. . . . . . . . . . . . . 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 489	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℕ₀ ↑_m ℤ))
95		difss 4090	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ
96		elmapssres 8860	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
97	94, 95, 96	sylancl 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
98	97	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
99		nnssz 12608	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℤ
100		elmapssres 8860	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
101	94, 99, 100	sylancl 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
102	101	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
103		simprl 782	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁)))
104	14	ad3antrrr 742	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
105	104	resabs1d 6007	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
106	103, 105	eqtr4d 2801	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
107		simprrl 792	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
108	106, 107	jca 520	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
109		resabs1 6005	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) ⊆ ℕ → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
110	24, 109	mp1i 14	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
111	103, 110	eqtr4d 2801	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
112		simprrr 793	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0)
113	108, 111, 112	jca32 524	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
114		reseq1 5972	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
115	114	eqeq2d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁))))
116		fveqeq2 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑎‘𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
117	115, 116	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)))
118	117	anbi1d 642	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
119		reseq1 5972	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
120	119	eqeq2d 2774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))))
121		fveqeq2 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑏‘𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0))
122	120, 121	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
123	122	anbi2d 641	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
124	118, 123	rspc2ev 3594	. . . . . . . . . . . . . . 15 ⊢ (((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ) ∧ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
125	98, 102, 113, 124	syl3anc 1398	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
126	125	rexlimdva2 3168	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) → ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
127	93, 126	impbid 215	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
128		simplrl 788	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
129		mzpf 43467	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
130	128, 129	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
131		nn0ssz 12609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ₀ ⊆ ℤ
132		mapss 8883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℤ ∈ V ∧ ℕ₀ ⊆ ℤ) → (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ))
133	3, 131, 132	mp2an 704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ)
134	133	sseli 3933	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → 𝑓 ∈ (ℤ ↑_m ℤ))
135		elmapssres 8860	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
136	134, 95, 135	sylancl 597	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
137	136	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
138	130, 137	ffvelcdmd 7080	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℤ)
139	138	zred 12695	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ)
140		simplrr 789	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏 ∈ (mzPoly‘ℕ))
141		mzpf 43467	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (mzPoly‘ℕ) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
142	140, 141	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
143		elmapssres 8860	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
144	134, 99, 143	sylancl 597	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
145	144	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
146	142, 145	ffvelcdmd 7080	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℤ)
147	146	zred 12695	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ)
148		sumsqeq0 14211	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
149	139, 147, 148	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
150	134	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℤ ↑_m ℤ))
151		reseq1 5972	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
152	151	fveq2d 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
153	152	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2))
154		reseq1 5972	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ))
155	154	fveq2d 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ)))
156	155	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2))
157	153, 156	oveq12d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
158		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))
159		ovex 7443	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈ V
160	157, 158, 159	fvmpt 6989	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (ℤ ↑_m ℤ) → ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
161	150, 160	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
162	161	eqeq1d 2765	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0 ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
163	149, 162	bitr4d 285	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0))
164	163	anbi2d 641	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
165	164	rexbidva 3187	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
166	127, 165	bitrd 282	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
167	31, 166	bitr3id 288	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ((∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
168	167	abbidv 2829	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
169	30, 168	eqtrid 2810	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
170		simpl 487	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈ ℕ₀)
171		fzssuz 13589	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
172		uzssz 12878	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘1) ⊆ ℤ
173	171, 172	sstri 3946	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℤ
174	3, 173	pm3.2i 475	. . . . . . . . . 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 782	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
179		mzpresrename 43481	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ ∧ 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
180	176, 177, 178, 179	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
181		2nn0 12516	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
182		mzpexpmpt 43476	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
183	180, 181, 182	sylancl 597	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
184	99	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℕ ⊆ ℤ)
185		simprr 784	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈ (mzPoly‘ℕ))
186		mzpresrename 43481	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
187	176, 184, 185, 186	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
188		mzpexpmpt 43476	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
189	187, 181, 188	sylancl 597	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
190		mzpaddmpt 43472	. . . . . . . . . 10 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
191	183, 189, 190	syl2anc 595	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
192		eldioph2 43493	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (ℤ ∈ V ∧ (1...𝑁) ⊆ ℤ) ∧ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ)) → {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
193	170, 175, 191, 192	syl3anc 1398	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)} ∈ (Dioph‘𝑁))
194	169, 193	eqeltrd 2863	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁))
195		ineq12 4168	. . . . . . . 8 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
196	195	eleq1d 2848	. . . . . . 7 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → ((𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁) ↔ ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁)))
197	194, 196	syl5ibrcom 250	. . . . . 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	biimtrrid 246	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → ((∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
200	28, 199	sylbid 243	. . 3 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
201	1, 200	syl 18	. 2 ⊢ (𝐴 ∈ (Dioph‘𝑁) → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁)))
202	201	anabsi5 681	1 ⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 {cab 2741 ∃wrex 3089 Vcvv 3455 ∖ cdif 3902 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 class class class wbr 5109 ↦ cmpt 5192 ↾ cres 5663 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ωcom 7858 ↑_m cmap 8820 ≈ cen 8936 Fincfn 8939 ℝcr 11094 0cc0 11095 1c1 11096 + caddc 11098 ≤ cle 11239 ℕcn 12228 2c2 12290 ℕ₀cn0 12499 ℤcz 12586 ℤ_≥cuz 12857 ...cfz 13530 ↑cexp 14093 mzPolycmzp 43453 Diophcdioph 43486

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9606 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-oadd 8453 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-dju 9883 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-n0 12500 df-z 12587 df-uz 12858 df-fz 13531 df-seq 14034 df-exp 14094 df-hash 14363 df-mzpcl 43454 df-mzp 43455 df-dioph 43487

This theorem is referenced by: anrabdioph 43511

W3C validator