diophun

Description: If two sets are Diophantine, so is their union. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Stefan O'Rear, 6-May-2015)

		Ref	Expression
	Assertion	diophun	$⊢ (A \in Dioph (N) \land B \in Dioph (N)) \to A \cup B \in Dioph (N)$

Proof

Step	Hyp	Ref	Expression
1		eldiophelnn0	$⊢ A \in Dioph (N) \to N \in ℕ_{0}$
2		nnex	$⊢ ℕ \in V$
3	2	jctr	$⊢ N \in ℕ_{0} \to (N \in ℕ_{0} \land ℕ \in V)$
4		1z	$⊢ 1 \in ℤ$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6	5	uzinf	$⊢ 1 \in ℤ \to \neg ℕ \in Fin$
7	4 6	ax-mp	$⊢ \neg ℕ \in Fin$
8		elfznn	$⊢ a \in (1 \dots N) \to a \in ℕ$
9	8	ssriv	$⊢ (1 \dots N) \subseteq ℕ$
10	7 9	pm3.2i	$⊢ (\neg ℕ \in Fin \land (1 \dots N) \subseteq ℕ)$
11		eldioph2b	$⊢ ((N \in ℕ_{0} \land ℕ \in V) \land (\neg ℕ \in Fin \land (1 \dots N) \subseteq ℕ)) \to (A \in Dioph (N) \leftrightarrow \exists a \in mzPoly (ℕ) A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\})$
12		eldioph2b	$⊢ ((N \in ℕ_{0} \land ℕ \in V) \land (\neg ℕ \in Fin \land (1 \dots N) \subseteq ℕ)) \to (B \in Dioph (N) \leftrightarrow \exists c \in mzPoly (ℕ) B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\})$
13	11 12	anbi12d	$⊢ ((N \in ℕ_{0} \land ℕ \in V) \land (\neg ℕ \in Fin \land (1 \dots N) \subseteq ℕ)) \to ((A \in Dioph (N) \land B \in Dioph (N)) \leftrightarrow (\exists a \in mzPoly (ℕ) A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land \exists c \in mzPoly (ℕ) B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\}))$
14	3 10 13	sylancl	$⊢ N \in ℕ_{0} \to ((A \in Dioph (N) \land B \in Dioph (N)) \leftrightarrow (\exists a \in mzPoly (ℕ) A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land \exists c \in mzPoly (ℕ) B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\}))$
15		reeanv	$⊢ \exists a \in mzPoly (ℕ) \exists c \in mzPoly (ℕ) (A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\}) \leftrightarrow (\exists a \in mzPoly (ℕ) A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land \exists c \in mzPoly (ℕ) B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\})$
16		unab	$⊢ \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cup \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\} = \{b \| (\exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0) \lor \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0))\}$
17		r19.43	$⊢ \exists d \in ({ℕ_{0}}^{ℕ}) ((b = {d ↾}_{(1 \dots N)} \land a (d) = 0) \lor (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)) \leftrightarrow (\exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0) \lor \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0))$
18		andi	$⊢ (b = {d ↾}_{(1 \dots N)} \land (a (d) = 0 \lor c (d) = 0)) \leftrightarrow ((b = {d ↾}_{(1 \dots N)} \land a (d) = 0) \lor (b = {d ↾}_{(1 \dots N)} \land c (d) = 0))$
19		zex	$⊢ ℤ \in V$
20		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
21		mapss	$⊢ (ℤ \in V \land ℕ_{0} \subseteq ℤ) \to {ℕ_{0}}^{ℕ} \subseteq ℤ^{ℕ}$
22	19 20 21	mp2an	$⊢ {ℕ_{0}}^{ℕ} \subseteq ℤ^{ℕ}$
23	22	sseli	$⊢ d \in ({ℕ_{0}}^{ℕ}) \to d \in (ℤ^{ℕ})$
24	23	adantl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to d \in (ℤ^{ℕ})$
25		fveq2	$⊢ e = d \to a (e) = a (d)$
26		fveq2	$⊢ e = d \to c (e) = c (d)$
27	25 26	oveq12d	$⊢ e = d \to a (e) c (e) = a (d) c (d)$
28		eqid	$⊢ (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) = (e \in (ℤ^{ℕ}) ⟼ a (e) c (e))$
29		ovex	$⊢ a (d) c (d) \in V$
30	27 28 29	fvmpt	$⊢ d \in (ℤ^{ℕ}) \to (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = a (d) c (d)$
31	24 30	syl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = a (d) c (d)$
32	31	eqeq1d	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to ((e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0 \leftrightarrow a (d) c (d) = 0)$
33		simplrl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to a \in mzPoly (ℕ)$
34		mzpf	$⊢ a \in mzPoly (ℕ) \to a : ℤ^{ℕ} ⟶ ℤ$
35	33 34	syl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to a : ℤ^{ℕ} ⟶ ℤ$
36	35 24	ffvelrnd	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to a (d) \in ℤ$
37	36	zcnd	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to a (d) \in ℂ$
38		simplrr	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to c \in mzPoly (ℕ)$
39		mzpf	$⊢ c \in mzPoly (ℕ) \to c : ℤ^{ℕ} ⟶ ℤ$
40	38 39	syl	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to c : ℤ^{ℕ} ⟶ ℤ$
41	40 24	ffvelrnd	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to c (d) \in ℤ$
42	41	zcnd	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to c (d) \in ℂ$
43	37 42	mul0ord	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to (a (d) c (d) = 0 \leftrightarrow (a (d) = 0 \lor c (d) = 0))$
44	32 43	bitr2d	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to ((a (d) = 0 \lor c (d) = 0) \leftrightarrow (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0)$
45	44	anbi2d	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to ((b = {d ↾}_{(1 \dots N)} \land (a (d) = 0 \lor c (d) = 0)) \leftrightarrow (b = {d ↾}_{(1 \dots N)} \land (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0))$
46	18 45	bitr3id	$⊢ ((N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \land d \in ({ℕ_{0}}^{ℕ})) \to (((b = {d ↾}_{(1 \dots N)} \land a (d) = 0) \lor (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)) \leftrightarrow (b = {d ↾}_{(1 \dots N)} \land (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0))$
47	46	rexbidva	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to (\exists d \in ({ℕ_{0}}^{ℕ}) ((b = {d ↾}_{(1 \dots N)} \land a (d) = 0) \lor (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)) \leftrightarrow \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0))$
48	17 47	bitr3id	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to ((\exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0) \lor \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)) \leftrightarrow \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0))$
49	48	abbidv	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to \{b \| (\exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0) \lor \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0))\} = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0)\}$
50	16 49	syl5eq	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cup \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\} = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0)\}$
51		simpl	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to N \in ℕ_{0}$
52	2 9	pm3.2i	$⊢ (ℕ \in V \land (1 \dots N) \subseteq ℕ)$
53	52	a1i	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to (ℕ \in V \land (1 \dots N) \subseteq ℕ)$
54		simprl	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to a \in mzPoly (ℕ)$
55	54 34	syl	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to a : ℤ^{ℕ} ⟶ ℤ$
56	55	feqmptd	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to a = (e \in (ℤ^{ℕ}) ⟼ a (e))$
57	56 54	eqeltrrd	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to (e \in (ℤ^{ℕ}) ⟼ a (e)) \in mzPoly (ℕ)$
58		simprr	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to c \in mzPoly (ℕ)$
59	58 39	syl	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to c : ℤ^{ℕ} ⟶ ℤ$
60	59	feqmptd	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to c = (e \in (ℤ^{ℕ}) ⟼ c (e))$
61	60 58	eqeltrrd	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to (e \in (ℤ^{ℕ}) ⟼ c (e)) \in mzPoly (ℕ)$
62		mzpmulmpt	$⊢ ((e \in (ℤ^{ℕ}) ⟼ a (e)) \in mzPoly (ℕ) \land (e \in (ℤ^{ℕ}) ⟼ c (e)) \in mzPoly (ℕ)) \to (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) \in mzPoly (ℕ)$
63	57 61 62	syl2anc	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) \in mzPoly (ℕ)$
64		eldioph2	$⊢ (N \in ℕ_{0} \land (ℕ \in V \land (1 \dots N) \subseteq ℕ) \land (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) \in mzPoly (ℕ)) \to \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0)\} \in Dioph (N)$
65	51 53 63 64	syl3anc	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land (e \in (ℤ^{ℕ}) ⟼ a (e) c (e)) (d) = 0)\} \in Dioph (N)$
66	50 65	eqeltrd	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cup \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\} \in Dioph (N)$
67		uneq12	$⊢ (A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\}) \to A \cup B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cup \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\}$
68	67	eleq1d	$⊢ (A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\}) \to (A \cup B \in Dioph (N) \leftrightarrow \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \cup \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\} \in Dioph (N))$
69	66 68	syl5ibrcom	$⊢ (N \in ℕ_{0} \land (a \in mzPoly (ℕ) \land c \in mzPoly (ℕ))) \to ((A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\}) \to A \cup B \in Dioph (N))$
70	69	rexlimdvva	$⊢ N \in ℕ_{0} \to (\exists a \in mzPoly (ℕ) \exists c \in mzPoly (ℕ) (A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\}) \to A \cup B \in Dioph (N))$
71	15 70	syl5bir	$⊢ N \in ℕ_{0} \to ((\exists a \in mzPoly (ℕ) A = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land a (d) = 0)\} \land \exists c \in mzPoly (ℕ) B = \{b \| \exists d \in ({ℕ_{0}}^{ℕ}) (b = {d ↾}_{(1 \dots N)} \land c (d) = 0)\}) \to A \cup B \in Dioph (N))$
72	14 71	sylbid	$⊢ N \in ℕ_{0} \to ((A \in Dioph (N) \land B \in Dioph (N)) \to A \cup B \in Dioph (N))$
73	1 72	syl	$⊢ A \in Dioph (N) \to ((A \in Dioph (N) \land B \in Dioph (N)) \to A \cup B \in Dioph (N))$
74	73	anabsi5	$⊢ (A \in Dioph (N) \land B \in Dioph (N)) \to A \cup B \in Dioph (N)$

Metamath Proof Explorer

Theorem diophun

Proof