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 43890

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 43882	. . 3 ⊢ (𝐴 ∈ (Dioph‘𝑁) → 𝑁 ∈ ℕ₀)
2		id 23	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℕ₀)
3		zex 12707	. . . . . . 7 ⊢ ℤ ∈ V
4		difexg 5290	. . . . . . 7 ⊢ (ℤ ∈ V → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
5	3, 4	mp1i 14	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V)
6		ominf 9260	. . . . . . 7 ⊢ ¬ ω ∈ Fin
7		nn0z 12722	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
8		lzenom 43888	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ≈ ω)
9		enfi 9207	. . . . . . . 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 43887	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ))
13		inss1 4132	. . . . . . 7 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))
14	12, 13	eqsstrdi 3953	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
15		eldioph2b 43881	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ V) ∧ (¬ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∈ Fin ∧ (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
16	2, 5, 11, 14, 15	syl22anc 852	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ∈ (Dioph‘𝑁) ↔ ∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)}))
17		nnex 12346	. . . . . . 7 ⊢ ℕ ∈ V
18	17	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ℕ ∈ V)
19		1z 12731	. . . . . . 7 ⊢ 1 ∈ ℤ
20		nnuz 13009	. . . . . . . 8 ⊢ ℕ = (ℤ_≥‘1)
21	20	uzinf 14113	. . . . . . 7 ⊢ (1 ∈ ℤ → ¬ ℕ ∈ Fin)
22	19, 21	mp1i 14	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ¬ ℕ ∈ Fin)
23		elfznn 13692	. . . . . . . 8 ⊢ (𝑎 ∈ (1...𝑁) → 𝑎 ∈ ℕ)
24	23	ssriv 3913	. . . . . . 7 ⊢ (1...𝑁) ⊆ ℕ
25	24	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (1...𝑁) ⊆ ℕ)
26		eldioph2b 43881	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ ℕ ∈ V) ∧ (¬ ℕ ∈ Fin ∧ (1...𝑁) ⊆ ℕ)) → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
27	2, 18, 22, 25, 26	syl22anc 852	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐵 ∈ (Dioph‘𝑁) ↔ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
28	16, 27	anbi12d 644	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)})))
29		reeanv 3234	. . . . 5 ⊢ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑏 ∈ (mzPoly‘ℕ)(𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ↔ (∃𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ ∃𝑏 ∈ (mzPoly‘ℕ)𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
30		inab 4253	. . . . . . . . 9 ⊢ ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))}
31		reeanv 3234	. . . . . . . . . . 11 ⊢ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)))
32		simplrl 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
33		simplrr 790	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑒 ∈ (ℕ₀ ↑_m ℕ))
34	12	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ) = (1...𝑁))
35	34	reseq2d 5970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
36	35	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
37	34	reseq2d 5970	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
38	37	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ (1...𝑁)))
39		simprrl 793	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑒 ↾ (1...𝑁)))
40		simprll 791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = (𝑑 ↾ (1...𝑁)))
41	38, 39, 40	3eqtr2d 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑑 ↾ (1...𝑁)))
42	36, 41	eqtr4d 2798	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)) = (𝑒 ↾ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)))
43		elmapresaun 8913	. . . . . . . . . . . . . . . . . 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 4163	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1))
46	19	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ∈ ℤ)
47		nn0p1nn 12650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
48	47	nnge1d 12391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ≤ (𝑁 + 1))
49		lzunuz 43886	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ≤ (𝑁 + 1)) → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
50	7, 46, 48, 49	syl3anc 1398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ (ℤ_≥‘1)) = ℤ)
51	45, 50	eqtrid 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ) = ℤ)
52	51	oveq2d 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ₀ → (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ₀ ↑_m ℤ))
53	52	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (ℕ₀ ↑_m ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∪ ℕ)) = (ℕ₀ ↑_m ℤ))
54	44, 53	eleqtrd 2862	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ℤ))
55		unidm 4155	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∪ 𝑐) = 𝑐
56	40, 39	uneq12d 4167	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 ∪ 𝑐) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
57	55, 56	eqtr3id 2809	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁))))
58		resundir 5985	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) = ((𝑑 ↾ (1...𝑁)) ∪ (𝑒 ↾ (1...𝑁)))
59	57, 58	eqtr4di 2813	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
60		uncom 4156	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∪ 𝑒) = (𝑒 ∪ 𝑑)
61	60	reseq1i 5966	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑒 ∪ 𝑑) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
62		incom 4105	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ∩ ℕ)
63	62, 34	eqtrid 2807	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (1...𝑁))
64	63	reseq2d 5970	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ₀ → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
65	64	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
66	63	reseq2d 5970	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
67	66	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (1...𝑁)))
68	67, 40, 39	3eqtr2d 2801	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑒 ↾ (1...𝑁)))
69	65, 68	eqtr4d 2798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑒 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑑 ↾ (ℕ ∩ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
70		elmapresaunres2 43889	. . . . . . . . . . . . . . . . . . . . 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 2807	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = 𝑑)
73	72	fveq2d 6892	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘𝑑))
74		simprlr 792	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘𝑑) = 0)
75	73, 74	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
76		elmapresaunres2 43889	. . . . . . . . . . . . . . . . . . . 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 6892	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = (𝑏‘𝑒))
79		simprrr 794	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘𝑒) = 0)
80	78, 79	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)
81	59, 75, 80	jca32 525	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
82		reseq1 5964	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (1...𝑁)) = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)))
83	82	eqeq2d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑐 = (𝑓 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁))))
84		reseq1 5964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = ((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
85	84	fveqeq2d 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ↔ (𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
86		reseq1 5964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (𝑓 ↾ ℕ) = ((𝑑 ∪ 𝑒) ↾ ℕ))
87	86	fveqeq2d 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑏‘(𝑓 ↾ ℕ)) = 0 ↔ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))
88	85, 87	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0)))
89	83, 88	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (𝑑 ∪ 𝑒) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))))
90	89	rspcev 3576	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 ∪ 𝑒) ∈ (ℕ₀ ↑_m ℤ) ∧ (𝑐 = ((𝑑 ∪ 𝑒) ↾ (1...𝑁)) ∧ ((𝑎‘((𝑑 ∪ 𝑒) ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘((𝑑 ∪ 𝑒) ↾ ℕ)) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
91	54, 81, 90	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) ∧ ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
92	91	ex 418	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ (𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑒 ∈ (ℕ₀ ↑_m ℕ))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
93	92	rexlimdvva 3219	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))∃𝑒 ∈ (ℕ₀ ↑_m ℕ)((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) → ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
94		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℕ₀ ↑_m ℤ))
95		difss 4071	. . . . . . . . . . . . . . . . 17 ⊢ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ
96		elmapssres 8899	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
97	94, 95, 96	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
98	97	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
99		nnssz 12720	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℤ
100		elmapssres 8899	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ (ℕ₀ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
101	94, 99, 100	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
102	101	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑓 ↾ ℕ) ∈ (ℕ₀ ↑_m ℕ))
103		simprl 783	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = (𝑓 ↾ (1...𝑁)))
104	14	ad3antrrr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (1...𝑁) ⊆ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))
105	104	resabs1d 6000	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
106	103, 105	eqtr4d 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
107		simprrl 793	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)
108	106, 107	jca 521	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
109		resabs1 5998	. . . . . . . . . . . . . . . . . 18 ⊢ ((1...𝑁) ⊆ ℕ → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
110	24, 109	mp1i 14	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑓 ↾ ℕ) ↾ (1...𝑁)) = (𝑓 ↾ (1...𝑁)))
111	103, 110	eqtr4d 2798	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
112		simprrr 794	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → (𝑏‘(𝑓 ↾ ℕ)) = 0)
113	108, 111, 112	jca32 525	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) ∧ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))) → ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
114		reseq1 5964	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑑 ↾ (1...𝑁)) = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)))
115	114	eqeq2d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (𝑐 = (𝑑 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁))))
116		fveqeq2 6897	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑎‘𝑑) = 0 ↔ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0))
117	115, 116	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → ((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ↔ (𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0)))
118	117	anbi1d 643	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → (((𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))))
119		reseq1 5964	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑒 ↾ (1...𝑁)) = ((𝑓 ↾ ℕ) ↾ (1...𝑁)))
120	119	eqeq2d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (𝑐 = (𝑒 ↾ (1...𝑁)) ↔ 𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁))))
121		fveqeq2 6897	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑏‘𝑒) = 0 ↔ (𝑏‘(𝑓 ↾ ℕ)) = 0))
122	120, 121	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = (𝑓 ↾ ℕ) → ((𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0) ↔ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)))
123	122	anbi2d 642	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = (𝑓 ↾ ℕ) → (((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)) ↔ ((𝑐 = ((𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ↾ (1...𝑁)) ∧ (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0) ∧ (𝑐 = ((𝑓 ↾ ℕ) ↾ (1...𝑁)) ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0))))
124	118, 123	rspc2ev 3588	. . . . . . . . . . . . . . 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 3165	. . . . . . . . . . . . 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 789	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
129		mzpf 43854	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
130	128, 129	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑎:(ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))⟶ℤ)
131		nn0ssz 12721	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ℕ₀ ⊆ ℤ
132		mapss 8922	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℤ ∈ V ∧ ℕ₀ ⊆ ℤ) → (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ))
133	3, 131, 132	mp2an 705	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℕ₀ ↑_m ℤ) ⊆ (ℤ ↑_m ℤ)
134	133	sseli 3905	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → 𝑓 ∈ (ℤ ↑_m ℤ))
135		elmapssres 8899	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
136	134, 95, 135	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
137	136	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∈ (ℤ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
138	130, 137	ffvelcdmd 7088	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℤ)
139	138	zred 12808	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ)
140		simplrr 790	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏 ∈ (mzPoly‘ℕ))
141		mzpf 43854	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ (mzPoly‘ℕ) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
142	140, 141	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑏:(ℤ ↑_m ℕ)⟶ℤ)
143		elmapssres 8899	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∈ (ℤ ↑_m ℤ) ∧ ℕ ⊆ ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
144	134, 99, 143	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ (ℕ₀ ↑_m ℤ) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
145	144	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑓 ↾ ℕ) ∈ (ℤ ↑_m ℕ))
146	142, 145	ffvelcdmd 7088	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℤ)
147	146	zred 12808	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ)
148		sumsqeq0 14327	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) ∈ ℝ ∧ (𝑏‘(𝑓 ↾ ℕ)) ∈ ℝ) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
149	139, 147, 148	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0) ↔ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) = 0))
150	134	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → 𝑓 ∈ (ℤ ↑_m ℤ))
151		reseq1 5964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) = (𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
152	151	fveq2d 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = (𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))))
153	152	oveq1d 7437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) = ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2))
154		reseq1 5964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑓 → (𝑔 ↾ ℕ) = (𝑓 ↾ ℕ))
155	154	fveq2d 6892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑓 → (𝑏‘(𝑔 ↾ ℕ)) = (𝑏‘(𝑓 ↾ ℕ)))
156	155	oveq1d 7437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 = 𝑓 → ((𝑏‘(𝑔 ↾ ℕ))↑2) = ((𝑏‘(𝑓 ↾ ℕ))↑2))
157	153, 156	oveq12d 7440	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = 𝑓 → (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)) = (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)))
158		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) = (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))
159		ovex 7455	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑓 ↾ ℕ))↑2)) ∈ V
160	157, 158, 159	fvmpt 6996	. . . . . . . . . . . . . . . . 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 2762	. . . . . . . . . . . . . . 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 642	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) ∧ 𝑓 ∈ (ℕ₀ ↑_m ℤ)) → ((𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑎‘(𝑓 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) = 0 ∧ (𝑏‘(𝑓 ↾ ℕ)) = 0)) ↔ (𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)))
165	164	rexbidva 3184	. . . . . . . . . . . 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 2826	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → {𝑐 ∣ (∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0) ∧ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0))} = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
169	30, 168	eqtrid 2807	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) = {𝑐 ∣ ∃𝑓 ∈ (ℕ₀ ↑_m ℤ)(𝑐 = (𝑓 ↾ (1...𝑁)) ∧ ((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2)))‘𝑓) = 0)})
170		simpl 488	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑁 ∈ ℕ₀)
171		fzssuz 13704	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
172		uzssz 12991	. . . . . . . . . . . 12 ⊢ (ℤ_≥‘1) ⊆ ℤ
173	171, 172	sstri 3918	. . . . . . . . . . 11 ⊢ (1...𝑁) ⊆ ℤ
174	3, 173	pm3.2i 476	. . . . . . . . . 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 783	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))
179		mzpresrename 43868	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ (ℤ ∖ (ℤ_≥‘(𝑁 + 1))) ⊆ ℤ ∧ 𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1))))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
180	176, 177, 178, 179	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ))
181		2nn0 12628	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
182		mzpexpmpt 43863	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
183	180, 181, 182	sylancl 598	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ))
184	99	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ℕ ⊆ ℤ)
185		simprr 785	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → 𝑏 ∈ (mzPoly‘ℕ))
186		mzpresrename 43868	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ ℕ ⊆ ℤ ∧ 𝑏 ∈ (mzPoly‘ℕ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
187	176, 184, 185, 186	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ))
188		mzpexpmpt 43863	. . . . . . . . . . 11 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ (𝑏‘(𝑔 ↾ ℕ))) ∈ (mzPoly‘ℤ) ∧ 2 ∈ ℕ₀) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
189	187, 181, 188	sylancl 598	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ))
190		mzpaddmpt 43859	. . . . . . . . . 10 ⊢ (((𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2)) ∈ (mzPoly‘ℤ) ∧ (𝑔 ∈ (ℤ ↑_m ℤ) ↦ ((𝑏‘(𝑔 ↾ ℕ))↑2)) ∈ (mzPoly‘ℤ)) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
191	183, 189, 190	syl2anc 596	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → (𝑔 ∈ (ℤ ↑_m ℤ) ↦ (((𝑎‘(𝑔 ↾ (ℤ ∖ (ℤ_≥‘(𝑁 + 1)))))↑2) + ((𝑏‘(𝑔 ↾ ℕ))↑2))) ∈ (mzPoly‘ℤ))
192		eldioph2 43880	. . . . . . . . 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 2860	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑎 ∈ (mzPoly‘(ℤ ∖ (ℤ_≥‘(𝑁 + 1)))) ∧ 𝑏 ∈ (mzPoly‘ℕ))) → ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) ∈ (Dioph‘𝑁))
195		ineq12 4111	. . . . . . . 8 ⊢ ((𝐴 = {𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∧ 𝐵 = {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}) → (𝐴 ∩ 𝐵) = ({𝑐 ∣ ∃𝑑 ∈ (ℕ₀ ↑_m (ℤ ∖ (ℤ_≥‘(𝑁 + 1))))(𝑐 = (𝑑 ↾ (1...𝑁)) ∧ (𝑎‘𝑑) = 0)} ∩ {𝑐 ∣ ∃𝑒 ∈ (ℕ₀ ↑_m ℕ)(𝑐 = (𝑒 ↾ (1...𝑁)) ∧ (𝑏‘𝑒) = 0)}))
196	195	eleq1d 2845	. . . . . . 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 3219	. . . . 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 682	1 ⊢ ((𝐴 ∈ (Dioph‘𝑁) ∧ 𝐵 ∈ (Dioph‘𝑁)) → (𝐴 ∩ 𝐵) ∈ (Dioph‘𝑁))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 {cab 2738 ∃wrex 3086 Vcvv 3450 ⊆ wss 3896 ∖ cdif 4044 ∩ cin 4088 ∪ cun 4148 class class class wbr 5102 ↦ cmpt 5185 ↾ cres 5652 ⟶wf 6537 ‘cfv 6541 (class class class)co 7422 ωcom 7879 ↑_m cmap 8852 ≈ cen 8975 Fincfn 8978 ℝcr 11204 0cc0 11205 1c1 11206 + caddc 11208 ≤ cle 11349 ℕcn 12340 2c2 12402 ℕ₀cn0 12611 ℤcz 12698 ℤ_≥cuz 12970 ...cfz 13644 ↑cexp 14209 mzPolycmzp 43840 Diophcdioph 43873

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7753 ax-inf2 9647 ax-cnex 11261 ax-resscn 11262 ax-1cn 11263 ax-icn 11264 ax-addcl 11265 ax-addrcl 11266 ax-mulcl 11267 ax-mulrcl 11268 ax-mulcom 11269 ax-addass 11270 ax-mulass 11271 ax-distr 11272 ax-i2m1 11273 ax-1ne0 11274 ax-1rid 11275 ax-rnegex 11276 ax-rrecex 11277 ax-cnre 11278 ax-pre-lttri 11279 ax-pre-lttrn 11280 ax-pre-ltadd 11281 ax-pre-mulgt0 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-of 7695 df-om 7880 df-1st 8003 df-2nd 8004 df-frecs 8304 df-wrecs 8335 df-recs 8384 df-rdg 8423 df-1o 8481 df-oadd 8485 df-er 8722 df-map 8854 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-dju 9987 df-card 10025 df-pnf 11350 df-mnf 11351 df-xr 11352 df-ltxr 11353 df-le 11354 df-sub 11548 df-neg 11549 df-nn 12341 df-2 12410 df-n0 12612 df-z 12699 df-uz 12971 df-fz 13645 df-seq 14150 df-exp 14210 df-hash 14480 df-mzpcl 43841 df-mzp 43842 df-dioph 43874

This theorem is used by: anrabdioph 43898

W3C validator