diophin

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)

		Ref	Expression
	Assertion	diophin	$⊢ (A \in Dioph (N) \land B \in Dioph (N)) \to A \cap B \in Dioph (N)$

Proof

Step	Hyp	Ref	Expression
1		eldiophelnn0	$⊢ A \in Dioph (N) \to N \in ℕ_{0}$
2		id	$⊢ N \in ℕ_{0} \to N \in ℕ_{0}$
3		zex	$⊢ ℤ \in V$
4		difexg	$⊢ ℤ \in V \to ℤ ∖ ℤ_{\geq (N + 1)} \in V$
5	3 4	mp1i	$⊢ N \in ℕ_{0} \to ℤ ∖ ℤ_{\geq (N + 1)} \in V$
6		ominf	$⊢ \neg ω \in Fin$
7		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
8		lzenom	$⊢ N \in ℤ \to (ℤ ∖ ℤ_{\geq (N + 1)}) \approx ω$
9		enfi	$⊢ (ℤ ∖ ℤ_{\geq (N + 1)}) \approx ω \to (ℤ ∖ ℤ_{\geq (N + 1)} \in Fin \leftrightarrow ω \in Fin)$
10	7 8 9	3syl	$⊢ N \in ℕ_{0} \to (ℤ ∖ ℤ_{\geq (N + 1)} \in Fin \leftrightarrow ω \in Fin)$
11	6 10	mtbiri	$⊢ N \in ℕ_{0} \to \neg ℤ ∖ ℤ_{\geq (N + 1)} \in Fin$
12		fz1eqin	$⊢ N \in ℕ_{0} \to (1 \dots N) = (ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ$
13		inss1	$⊢ (ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ \subseteq ℤ ∖ ℤ_{\geq (N + 1)}$
14	12 13	eqsstrdi	$⊢ N \in ℕ_{0} \to (1 \dots N) \subseteq ℤ ∖ ℤ_{\geq (N + 1)}$
15		eldioph2b	$⊢ ((N \in ℕ_{0} \land ℤ ∖ ℤ_{\geq (N + 1)} \in V) \land (\neg ℤ ∖ ℤ_{\geq (N + 1)} \in Fin \land (1 \dots N) \subseteq ℤ ∖ ℤ_{\geq (N + 1)})) \to (A \in Dioph (N) \leftrightarrow \exists a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\})$
16	2 5 11 14 15	syl22anc	$⊢ N \in ℕ_{0} \to (A \in Dioph (N) \leftrightarrow \exists a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\})$
17		nnex	$⊢ ℕ \in V$
18	17	a1i	$⊢ N \in ℕ_{0} \to ℕ \in V$
19		1z	$⊢ 1 \in ℤ$
20		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
21	20	uzinf	$⊢ 1 \in ℤ \to \neg ℕ \in Fin$
22	19 21	mp1i	$⊢ N \in ℕ_{0} \to \neg ℕ \in Fin$
23		elfznn	$⊢ a \in (1 \dots N) \to a \in ℕ$
24	23	ssriv	$⊢ (1 \dots N) \subseteq ℕ$
25	24	a1i	$⊢ N \in ℕ_{0} \to (1 \dots N) \subseteq ℕ$
26		eldioph2b	$⊢ ((N \in ℕ_{0} \land ℕ \in V) \land (\neg ℕ \in Fin \land (1 \dots N) \subseteq ℕ)) \to (B \in Dioph (N) \leftrightarrow \exists b \in mzPoly (ℕ) B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\})$
27	2 18 22 25 26	syl22anc	$⊢ N \in ℕ_{0} \to (B \in Dioph (N) \leftrightarrow \exists b \in mzPoly (ℕ) B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\})$
28	16 27	anbi12d	$⊢ N \in ℕ_{0} \to ((A \in Dioph (N) \land B \in Dioph (N)) \leftrightarrow (\exists a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land \exists b \in mzPoly (ℕ) B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\}))$
29		reeanv	$⊢ \exists a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \exists b \in mzPoly (ℕ) (A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\}) \leftrightarrow (\exists a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land \exists b \in mzPoly (ℕ) B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\})$
30		inab	$⊢ \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cap \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\} = \{c \| (\exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))\}$
31		reeanv	$⊢ \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \exists e \in ({ℕ_{0}}^{ℕ}) ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)) \leftrightarrow (\exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))$
32		simplrl	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})})$
33		simplrr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to e \in ({ℕ_{0}}^{ℕ})$
34	12	eqcomd	$⊢ N \in ℕ_{0} \to (ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ = (1 \dots N)$
35	34	reseq2d	$⊢ N \in ℕ_{0} \to {d ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)} = {d ↾}_{(1 \dots N)}$
36	35	ad3antrrr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {d ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)} = {d ↾}_{(1 \dots N)}$
37	34	reseq2d	$⊢ N \in ℕ_{0} \to {e ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)} = {e ↾}_{(1 \dots N)}$
38	37	ad3antrrr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {e ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)} = {e ↾}_{(1 \dots N)}$
39		simprrl	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to c = {e ↾}_{(1 \dots N)}$
40		simprll	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to c = {d ↾}_{(1 \dots N)}$
41	38 39 40	3eqtr2d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {e ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)} = {d ↾}_{(1 \dots N)}$
42	36 41	eqtr4d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {d ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)} = {e ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)}$
43		elmapresaun	$⊢ (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}) \land {d ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)} = {e ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)}) \to d \cup e \in ({ℕ_{0}}^{((ℤ ∖ ℤ_{\geq (N + 1)}) \cup ℕ)})$
44	32 33 42 43	syl3anc	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to d \cup e \in ({ℕ_{0}}^{((ℤ ∖ ℤ_{\geq (N + 1)}) \cup ℕ)})$
45	20	uneq2i	$⊢ (ℤ ∖ ℤ_{\geq (N + 1)}) \cup ℕ = (ℤ ∖ ℤ_{\geq (N + 1)}) \cup ℤ_{\geq 1}$
46	19	a1i	$⊢ N \in ℕ_{0} \to 1 \in ℤ$
47		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
48	47	nnge1d	$⊢ N \in ℕ_{0} \to 1 \leq N + 1$
49		lzunuz	$⊢ (N \in ℤ \land 1 \in ℤ \land 1 \leq N + 1) \to (ℤ ∖ ℤ_{\geq (N + 1)}) \cup ℤ_{\geq 1} = ℤ$
50	7 46 48 49	syl3anc	$⊢ N \in ℕ_{0} \to (ℤ ∖ ℤ_{\geq (N + 1)}) \cup ℤ_{\geq 1} = ℤ$
51	45 50	eqtrid	$⊢ N \in ℕ_{0} \to (ℤ ∖ ℤ_{\geq (N + 1)}) \cup ℕ = ℤ$
52	51	oveq2d	$⊢ N \in ℕ_{0} \to {ℕ_{0}}^{((ℤ ∖ ℤ_{\geq (N + 1)}) \cup ℕ)} = {ℕ_{0}}^{ℤ}$
53	52	ad3antrrr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {ℕ_{0}}^{((ℤ ∖ ℤ_{\geq (N + 1)}) \cup ℕ)} = {ℕ_{0}}^{ℤ}$
54	44 53	eleqtrd	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to d \cup e \in ({ℕ_{0}}^{ℤ})$
55		unidm	$⊢ c \cup c = c$
56	40 39	uneq12d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to c \cup c = ({d ↾}_{(1 \dots N)}) \cup ({e ↾}_{(1 \dots N)})$
57	55 56	eqtr3id	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to c = ({d ↾}_{(1 \dots N)}) \cup ({e ↾}_{(1 \dots N)})$
58		resundir	$⊢ {(d \cup e) ↾}_{(1 \dots N)} = ({d ↾}_{(1 \dots N)}) \cup ({e ↾}_{(1 \dots N)})$
59	57 58	eqtr4di	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to c = {(d \cup e) ↾}_{(1 \dots N)}$
60		uncom	$⊢ d \cup e = e \cup d$
61	60	reseq1i	$⊢ {(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} = {(e \cup d) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}$
62		incom	$⊢ ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}) = (ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ$
63	62 34	eqtrid	$⊢ N \in ℕ_{0} \to ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}) = (1 \dots N)$
64	63	reseq2d	$⊢ N \in ℕ_{0} \to {e ↾}_{(ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}))} = {e ↾}_{(1 \dots N)}$
65	64	ad3antrrr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {e ↾}_{(ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}))} = {e ↾}_{(1 \dots N)}$
66	63	reseq2d	$⊢ N \in ℕ_{0} \to {d ↾}_{(ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}))} = {d ↾}_{(1 \dots N)}$
67	66	ad3antrrr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {d ↾}_{(ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}))} = {d ↾}_{(1 \dots N)}$
68	67 40 39	3eqtr2d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {d ↾}_{(ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}))} = {e ↾}_{(1 \dots N)}$
69	65 68	eqtr4d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {e ↾}_{(ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}))} = {d ↾}_{(ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}))}$
70		elmapresaunres2	$⊢ (e \in ({ℕ_{0}}^{ℕ}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land {e ↾}_{(ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}))} = {d ↾}_{(ℕ \cap (ℤ ∖ ℤ_{\geq (N + 1)}))}) \to {(e \cup d) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} = d$
71	33 32 69 70	syl3anc	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {(e \cup d) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} = d$
72	61 71	eqtrid	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} = d$
73	72	fveq2d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to a ({(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = a (d)$
74		simprlr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to a (d) = 0$
75	73 74	eqtrd	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to a ({(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0$
76		elmapresaunres2	$⊢ (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}) \land {d ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)} = {e ↾}_{((ℤ ∖ ℤ_{\geq (N + 1)}) \cap ℕ)}) \to {(d \cup e) ↾}_{ℕ} = e$
77	32 33 42 76	syl3anc	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to {(d \cup e) ↾}_{ℕ} = e$
78	77	fveq2d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to b ({(d \cup e) ↾}_{ℕ}) = b (e)$
79		simprrr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to b (e) = 0$
80	78 79	eqtrd	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to b ({(d \cup e) ↾}_{ℕ}) = 0$
81	59 75 80	jca32	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to (c = {(d \cup e) ↾}_{(1 \dots N)} \land (a ({(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({(d \cup e) ↾}_{ℕ}) = 0))$
82		reseq1	$⊢ f = d \cup e \to {f ↾}_{(1 \dots N)} = {(d \cup e) ↾}_{(1 \dots N)}$
83	82	eqeq2d	$⊢ f = d \cup e \to (c = {f ↾}_{(1 \dots N)} \leftrightarrow c = {(d \cup e) ↾}_{(1 \dots N)})$
84		reseq1	$⊢ f = d \cup e \to {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} = {(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}$
85	84	fveqeq2d	$⊢ f = d \cup e \to (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \leftrightarrow a ({(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0)$
86		reseq1	$⊢ f = d \cup e \to {f ↾}_{ℕ} = {(d \cup e) ↾}_{ℕ}$
87	86	fveqeq2d	$⊢ f = d \cup e \to (b ({f ↾}_{ℕ}) = 0 \leftrightarrow b ({(d \cup e) ↾}_{ℕ}) = 0)$
88	85 87	anbi12d	$⊢ f = d \cup e \to ((a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0) \leftrightarrow (a ({(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({(d \cup e) ↾}_{ℕ}) = 0))$
89	83 88	anbi12d	$⊢ f = d \cup e \to ((c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0)) \leftrightarrow (c = {(d \cup e) ↾}_{(1 \dots N)} \land (a ({(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({(d \cup e) ↾}_{ℕ}) = 0)))$
90	89	rspcev	$⊢ (d \cup e \in ({ℕ_{0}}^{ℤ}) \land (c = {(d \cup e) ↾}_{(1 \dots N)} \land (a ({(d \cup e) ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({(d \cup e) ↾}_{ℕ}) = 0))) \to \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))$
91	54 81 90	syl2anc	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \land ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))) \to \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))$
92	91	ex	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land (d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land e \in ({ℕ_{0}}^{ℕ}))) \to (((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)) \to \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0)))$
93	92	rexlimdvva	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (\exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \exists e \in ({ℕ_{0}}^{ℕ}) ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)) \to \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0)))$
94		simpr	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to f \in ({ℕ_{0}}^{ℤ})$
95		difss	$⊢ ℤ ∖ ℤ_{\geq (N + 1)} \subseteq ℤ$
96		elmapssres	$⊢ (f \in ({ℕ_{0}}^{ℤ}) \land ℤ ∖ ℤ_{\geq (N + 1)} \subseteq ℤ) \to {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})})$
97	94 95 96	sylancl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})})$
98	97	adantr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})})$
99		nnssz	$⊢ ℕ \subseteq ℤ$
100		elmapssres	$⊢ (f \in ({ℕ_{0}}^{ℤ}) \land ℕ \subseteq ℤ) \to {f ↾}_{ℕ} \in ({ℕ_{0}}^{ℕ})$
101	94 99 100	sylancl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to {f ↾}_{ℕ} \in ({ℕ_{0}}^{ℕ})$
102	101	adantr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to {f ↾}_{ℕ} \in ({ℕ_{0}}^{ℕ})$
103		simprl	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to c = {f ↾}_{(1 \dots N)}$
104	14	ad3antrrr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to (1 \dots N) \subseteq ℤ ∖ ℤ_{\geq (N + 1)}$
105	104	resabs1d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)} = {f ↾}_{(1 \dots N)}$
106	103 105	eqtr4d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to c = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)}$
107		simprrl	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0$
108	106 107	jca	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to (c = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)} \land a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0)$
109		resabs1	$⊢ (1 \dots N) \subseteq ℕ \to {({f ↾}_{ℕ}) ↾}_{(1 \dots N)} = {f ↾}_{(1 \dots N)}$
110	24 109	mp1i	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to {({f ↾}_{ℕ}) ↾}_{(1 \dots N)} = {f ↾}_{(1 \dots N)}$
111	103 110	eqtr4d	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to c = {({f ↾}_{ℕ}) ↾}_{(1 \dots N)}$
112		simprrr	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to b ({f ↾}_{ℕ}) = 0$
113	108 111 112	jca32	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to ((c = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)} \land a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0) \land (c = {({f ↾}_{ℕ}) ↾}_{(1 \dots N)} \land b ({f ↾}_{ℕ}) = 0))$
114		reseq1	$⊢ d = {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \to {d ↾}_{(1 \dots N)} = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)}$
115	114	eqeq2d	$⊢ d = {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \to (c = {d ↾}_{(1 \dots N)} \leftrightarrow c = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)})$
116		fveqeq2	$⊢ d = {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \to (a (d) = 0 \leftrightarrow a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0)$
117	115 116	anbi12d	$⊢ d = {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \to ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \leftrightarrow (c = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)} \land a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0))$
118	117	anbi1d	$⊢ d = {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \to (((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)) \leftrightarrow ((c = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)} \land a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)))$
119		reseq1	$⊢ e = {f ↾}_{ℕ} \to {e ↾}_{(1 \dots N)} = {({f ↾}_{ℕ}) ↾}_{(1 \dots N)}$
120	119	eqeq2d	$⊢ e = {f ↾}_{ℕ} \to (c = {e ↾}_{(1 \dots N)} \leftrightarrow c = {({f ↾}_{ℕ}) ↾}_{(1 \dots N)})$
121		fveqeq2	$⊢ e = {f ↾}_{ℕ} \to (b (e) = 0 \leftrightarrow b ({f ↾}_{ℕ}) = 0)$
122	120 121	anbi12d	$⊢ e = {f ↾}_{ℕ} \to ((c = {e ↾}_{(1 \dots N)} \land b (e) = 0) \leftrightarrow (c = {({f ↾}_{ℕ}) ↾}_{(1 \dots N)} \land b ({f ↾}_{ℕ}) = 0))$
123	122	anbi2d	$⊢ e = {f ↾}_{ℕ} \to (((c = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)} \land a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)) \leftrightarrow ((c = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)} \land a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0) \land (c = {({f ↾}_{ℕ}) ↾}_{(1 \dots N)} \land b ({f ↾}_{ℕ}) = 0)))$
124	118 123	rspc2ev	$⊢ ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \land {f ↾}_{ℕ} \in ({ℕ_{0}}^{ℕ}) \land ((c = {({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) ↾}_{(1 \dots N)} \land a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0) \land (c = {({f ↾}_{ℕ}) ↾}_{(1 \dots N)} \land b ({f ↾}_{ℕ}) = 0))) \to \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \exists e \in ({ℕ_{0}}^{ℕ}) ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))$
125	98 102 113 124	syl3anc	$⊢ (((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \land (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0))) \to \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \exists e \in ({ℕ_{0}}^{ℕ}) ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))$
126	125	rexlimdva2	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (\exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0)) \to \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \exists e \in ({ℕ_{0}}^{ℕ}) ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)))$
127	93 126	impbid	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (\exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \exists e \in ({ℕ_{0}}^{ℕ}) ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)) \leftrightarrow \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0)))$
128		simplrl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)})$
129		mzpf	$⊢ a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \to a : ℤ^{(ℤ ∖ ℤ_{\geq (N + 1)})} ⟶ ℤ$
130	128 129	syl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to a : ℤ^{(ℤ ∖ ℤ_{\geq (N + 1)})} ⟶ ℤ$
131		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
132		mapss	$⊢ (ℤ \in V \land ℕ_{0} \subseteq ℤ) \to {ℕ_{0}}^{ℤ} \subseteq ℤ^{ℤ}$
133	3 131 132	mp2an	$⊢ {ℕ_{0}}^{ℤ} \subseteq ℤ^{ℤ}$
134	133	sseli	$⊢ f \in ({ℕ_{0}}^{ℤ}) \to f \in (ℤ^{ℤ})$
135		elmapssres	$⊢ (f \in (ℤ^{ℤ}) \land ℤ ∖ ℤ_{\geq (N + 1)} \subseteq ℤ) \to {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \in (ℤ^{(ℤ ∖ ℤ_{\geq (N + 1)})})$
136	134 95 135	sylancl	$⊢ f \in ({ℕ_{0}}^{ℤ}) \to {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \in (ℤ^{(ℤ ∖ ℤ_{\geq (N + 1)})})$
137	136	adantl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} \in (ℤ^{(ℤ ∖ ℤ_{\geq (N + 1)})})$
138	130 137	ffvelcdmd	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) \in ℤ$
139	138	zred	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) \in ℝ$
140		simplrr	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to b \in mzPoly (ℕ)$
141		mzpf	$⊢ b \in mzPoly (ℕ) \to b : ℤ^{ℕ} ⟶ ℤ$
142	140 141	syl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to b : ℤ^{ℕ} ⟶ ℤ$
143		elmapssres	$⊢ (f \in (ℤ^{ℤ}) \land ℕ \subseteq ℤ) \to {f ↾}_{ℕ} \in (ℤ^{ℕ})$
144	134 99 143	sylancl	$⊢ f \in ({ℕ_{0}}^{ℤ}) \to {f ↾}_{ℕ} \in (ℤ^{ℕ})$
145	144	adantl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to {f ↾}_{ℕ} \in (ℤ^{ℕ})$
146	142 145	ffvelcdmd	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to b ({f ↾}_{ℕ}) \in ℤ$
147	146	zred	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to b ({f ↾}_{ℕ}) \in ℝ$
148		sumsqeq0	$⊢ (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) \in ℝ \land b ({f ↾}_{ℕ}) \in ℝ) \to ((a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0) \leftrightarrow {a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({f ↾}_{ℕ})}^{2} = 0)$
149	139 147 148	syl2anc	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to ((a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0) \leftrightarrow {a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({f ↾}_{ℕ})}^{2} = 0)$
150	134	adantl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to f \in (ℤ^{ℤ})$
151		reseq1	$⊢ g = f \to {g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})} = {f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}$
152	151	fveq2d	$⊢ g = f \to a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})$
153	152	oveq1d	$⊢ g = f \to {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} = {a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2}$
154		reseq1	$⊢ g = f \to {g ↾}_{ℕ} = {f ↾}_{ℕ}$
155	154	fveq2d	$⊢ g = f \to b ({g ↾}_{ℕ}) = b ({f ↾}_{ℕ})$
156	155	oveq1d	$⊢ g = f \to {b ({g ↾}_{ℕ})}^{2} = {b ({f ↾}_{ℕ})}^{2}$
157	153 156	oveq12d	$⊢ g = f \to {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2} = {a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({f ↾}_{ℕ})}^{2}$
158		eqid	$⊢ (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) = (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2})$
159		ovex	$⊢ {a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({f ↾}_{ℕ})}^{2} \in V$
160	157 158 159	fvmpt	$⊢ f \in (ℤ^{ℤ}) \to (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = {a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({f ↾}_{ℕ})}^{2}$
161	150 160	syl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = {a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({f ↾}_{ℕ})}^{2}$
162	161	eqeq1d	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to ((g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0 \leftrightarrow {a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({f ↾}_{ℕ})}^{2} = 0)$
163	149 162	bitr4d	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to ((a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0) \leftrightarrow (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0)$
164	163	anbi2d	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \land f \in ({ℕ_{0}}^{ℤ})) \to ((c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0)) \leftrightarrow (c = {f ↾}_{(1 \dots N)} \land (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0))$
165	164	rexbidva	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (\exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (a ({f ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})}) = 0 \land b ({f ↾}_{ℕ}) = 0)) \leftrightarrow \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0))$
166	127 165	bitrd	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (\exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) \exists e \in ({ℕ_{0}}^{ℕ}) ((c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)) \leftrightarrow \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0))$
167	31 166	bitr3id	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to ((\exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)) \leftrightarrow \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0))$
168	167	abbidv	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to \{c \| (\exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0) \land \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0))\} = \{c \| \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0)\}$
169	30 168	eqtrid	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cap \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\} = \{c \| \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0)\}$
170		simpl	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to N \in ℕ_{0}$
171		fzssuz	$⊢ (1 \dots N) \subseteq ℤ_{\geq 1}$
172		uzssz	$⊢ ℤ_{\geq 1} \subseteq ℤ$
173	171 172	sstri	$⊢ (1 \dots N) \subseteq ℤ$
174	3 173	pm3.2i	$⊢ (ℤ \in V \land (1 \dots N) \subseteq ℤ)$
175	174	a1i	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (ℤ \in V \land (1 \dots N) \subseteq ℤ)$
176	3	a1i	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to ℤ \in V$
177	95	a1i	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to ℤ ∖ ℤ_{\geq (N + 1)} \subseteq ℤ$
178		simprl	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)})$
179		mzpresrename	$⊢ (ℤ \in V \land ℤ ∖ ℤ_{\geq (N + 1)} \subseteq ℤ \land a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)})) \to (g \in (ℤ^{ℤ}) ⟼ a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})) \in mzPoly (ℤ)$
180	176 177 178 179	syl3anc	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (g \in (ℤ^{ℤ}) ⟼ a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})) \in mzPoly (ℤ)$
181		2nn0	$⊢ 2 \in ℕ_{0}$
182		mzpexpmpt	$⊢ ((g \in (ℤ^{ℤ}) ⟼ a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})) \in mzPoly (ℤ) \land 2 \in ℕ_{0}) \to (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2}) \in mzPoly (ℤ)$
183	180 181 182	sylancl	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2}) \in mzPoly (ℤ)$
184	99	a1i	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to ℕ \subseteq ℤ$
185		simprr	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to b \in mzPoly (ℕ)$
186		mzpresrename	$⊢ (ℤ \in V \land ℕ \subseteq ℤ \land b \in mzPoly (ℕ)) \to (g \in (ℤ^{ℤ}) ⟼ b ({g ↾}_{ℕ})) \in mzPoly (ℤ)$
187	176 184 185 186	syl3anc	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (g \in (ℤ^{ℤ}) ⟼ b ({g ↾}_{ℕ})) \in mzPoly (ℤ)$
188		mzpexpmpt	$⊢ ((g \in (ℤ^{ℤ}) ⟼ b ({g ↾}_{ℕ})) \in mzPoly (ℤ) \land 2 \in ℕ_{0}) \to (g \in (ℤ^{ℤ}) ⟼ {b ({g ↾}_{ℕ})}^{2}) \in mzPoly (ℤ)$
189	187 181 188	sylancl	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (g \in (ℤ^{ℤ}) ⟼ {b ({g ↾}_{ℕ})}^{2}) \in mzPoly (ℤ)$
190		mzpaddmpt	$⊢ ((g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2}) \in mzPoly (ℤ) \land (g \in (ℤ^{ℤ}) ⟼ {b ({g ↾}_{ℕ})}^{2}) \in mzPoly (ℤ)) \to (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) \in mzPoly (ℤ)$
191	183 189 190	syl2anc	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) \in mzPoly (ℤ)$
192		eldioph2	$⊢ (N \in ℕ_{0} \land (ℤ \in V \land (1 \dots N) \subseteq ℤ) \land (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) \in mzPoly (ℤ)) \to \{c \| \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0)\} \in Dioph (N)$
193	170 175 191 192	syl3anc	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to \{c \| \exists f \in ({ℕ_{0}}^{ℤ}) (c = {f ↾}_{(1 \dots N)} \land (g \in (ℤ^{ℤ}) ⟼ {a ({g ↾}_{(ℤ ∖ ℤ_{\geq (N + 1)})})}^{2} + {b ({g ↾}_{ℕ})}^{2}) (f) = 0)\} \in Dioph (N)$
194	169 193	eqeltrd	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cap \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\} \in Dioph (N)$
195		ineq12	$⊢ (A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\}) \to A \cap B = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cap \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\}$
196	195	eleq1d	$⊢ (A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\}) \to (A \cap B \in Dioph (N) \leftrightarrow \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cap \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\} \in Dioph (N))$
197	194 196	syl5ibrcom	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \land b \in mzPoly (ℕ))) \to ((A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\}) \to A \cap B \in Dioph (N))$
198	197	rexlimdvva	$⊢ N \in ℕ_{0} \to (\exists a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) \exists b \in mzPoly (ℕ) (A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\}) \to A \cap B \in Dioph (N))$
199	29 198	biimtrrid	$⊢ N \in ℕ_{0} \to ((\exists a \in mzPoly (ℤ ∖ ℤ_{\geq (N + 1)}) A = \{c \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℤ_{\geq (N + 1)})}) (c = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land \exists b \in mzPoly (ℕ) B = \{c \| \exists e \in ({ℕ_{0}}^{ℕ}) (c = {e ↾}_{(1 \dots N)} \land b (e) = 0)\}) \to A \cap B \in Dioph (N))$
200	28 199	sylbid	$⊢ N \in ℕ_{0} \to ((A \in Dioph (N) \land B \in Dioph (N)) \to A \cap B \in Dioph (N))$
201	1 200	syl	$⊢ A \in Dioph (N) \to ((A \in Dioph (N) \land B \in Dioph (N)) \to A \cap B \in Dioph (N))$
202	201	anabsi5	$⊢ (A \in Dioph (N) \land B \in Dioph (N)) \to A \cap B \in Dioph (N)$

Metamath Proof Explorer

Theorem diophin

Proof