dvdsrabdioph

Description: Divisibility is a Diophantine relation. (Contributed by Stefan O'Rear, 11-Oct-2014)

		Ref	Expression
	Assertion	dvdsrabdioph	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A ∥ B\} \in Dioph (N)$

Proof

Step	Hyp	Ref	Expression
1		rabdiophlem1	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) A \in ℤ$
2		rabdiophlem1	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N)) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) B \in ℤ$
3		divides	$⊢ (A \in ℤ \land B \in ℤ) \to (A ∥ B \leftrightarrow \exists a \in ℤ a A = B)$
4		oveq1	$⊢ a = b \to a A = b A$
5	4	eqeq1d	$⊢ a = b \to (a A = B \leftrightarrow b A = B)$
6		oveq1	$⊢ a = - b \to a A = (- b) A$
7	6	eqeq1d	$⊢ a = - b \to (a A = B \leftrightarrow (- b) A = B)$
8	5 7	rexzrexnn0	$⊢ \exists a \in ℤ a A = B \leftrightarrow \exists b \in ℕ_{0} (b A = B \lor (- b) A = B)$
9	3 8	bitrdi	$⊢ (A \in ℤ \land B \in ℤ) \to (A ∥ B \leftrightarrow \exists b \in ℕ_{0} (b A = B \lor (- b) A = B))$
10	9	ralimi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \in ℤ \land B \in ℤ) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A ∥ B \leftrightarrow \exists b \in ℕ_{0} (b A = B \lor (- b) A = B))$
11		r19.26	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \in ℤ \land B \in ℤ) \leftrightarrow (\forall t \in ({ℕ_{0}}^{(1 \dots N)}) A \in ℤ \land \forall t \in ({ℕ_{0}}^{(1 \dots N)}) B \in ℤ)$
12		rabbi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A ∥ B \leftrightarrow \exists b \in ℕ_{0} (b A = B \lor (- b) A = B)) \leftrightarrow \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A ∥ B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} (b A = B \lor (- b) A = B)\}$
13	10 11 12	3imtr3i	$⊢ (\forall t \in ({ℕ_{0}}^{(1 \dots N)}) A \in ℤ \land \forall t \in ({ℕ_{0}}^{(1 \dots N)}) B \in ℤ) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A ∥ B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} (b A = B \lor (- b) A = B)\}$
14	1 2 13	syl2an	$⊢ ((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A ∥ B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} (b A = B \lor (- b) A = B)\}$
15	14	3adant1	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A ∥ B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} (b A = B \lor (- b) A = B)\}$
16		nfcv	$⊢ \underline{Ⅎ} t ({ℕ_{0}}^{(1 \dots N)})$
17		nfcv	$⊢ \underline{Ⅎ} a ({ℕ_{0}}^{(1 \dots N)})$
18		nfv	$⊢ Ⅎ a \exists b \in ℕ_{0} (b A = B \lor (- b) A = B)$
19		nfcv	$⊢ \underline{Ⅎ} t ℕ_{0}$
20		nfcv	$⊢ \underline{Ⅎ} t b$
21		nfcv	$⊢ \underline{Ⅎ} t \times$
22		nfcsb1v	$⊢ \underline{Ⅎ} t ⦋ a / t ⦌ A$
23	20 21 22	nfov	$⊢ \underline{Ⅎ} t b ⦋ a / t ⦌ A$
24		nfcsb1v	$⊢ \underline{Ⅎ} t ⦋ a / t ⦌ B$
25	23 24	nfeq	$⊢ Ⅎ t b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B$
26		nfcv	$⊢ \underline{Ⅎ} t (- b)$
27	26 21 22	nfov	$⊢ \underline{Ⅎ} t (- b) ⦋ a / t ⦌ A$
28	27 24	nfeq	$⊢ Ⅎ t (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B$
29	25 28	nfor	$⊢ Ⅎ t (b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B)$
30	19 29	nfrexw	$⊢ Ⅎ t \exists b \in ℕ_{0} (b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B)$
31		csbeq1a	$⊢ t = a \to A = ⦋ a / t ⦌ A$
32	31	oveq2d	$⊢ t = a \to b A = b ⦋ a / t ⦌ A$
33		csbeq1a	$⊢ t = a \to B = ⦋ a / t ⦌ B$
34	32 33	eqeq12d	$⊢ t = a \to (b A = B \leftrightarrow b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B)$
35	31	oveq2d	$⊢ t = a \to (- b) A = (- b) ⦋ a / t ⦌ A$
36	35 33	eqeq12d	$⊢ t = a \to ((- b) A = B \leftrightarrow (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B)$
37	34 36	orbi12d	$⊢ t = a \to ((b A = B \lor (- b) A = B) \leftrightarrow (b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B))$
38	37	rexbidv	$⊢ t = a \to (\exists b \in ℕ_{0} (b A = B \lor (- b) A = B) \leftrightarrow \exists b \in ℕ_{0} (b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B))$
39	16 17 18 30 38	cbvrabw	$⊢ \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} (b A = B \lor (- b) A = B)\} = \{a \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} (b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B)\}$
40		simp1	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to N \in ℕ_{0}$
41		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
42	41	3ad2ant1	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to N + 1 \in ℕ_{0}$
43		ovex	$⊢ (1 \dots N + 1) \in V$
44		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
45		elfz1end	$⊢ N + 1 \in ℕ \leftrightarrow N + 1 \in (1 \dots N + 1)$
46	44 45	sylib	$⊢ N \in ℕ_{0} \to N + 1 \in (1 \dots N + 1)$
47		mzpproj	$⊢ ((1 \dots N + 1) \in V \land N + 1 \in (1 \dots N + 1)) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ c (N + 1)) \in mzPoly ((1 \dots N + 1))$
48	43 46 47	sylancr	$⊢ N \in ℕ_{0} \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ c (N + 1)) \in mzPoly ((1 \dots N + 1))$
49	48	adantr	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ c (N + 1)) \in mzPoly ((1 \dots N + 1))$
50		eqid	$⊢ N + 1 = N + 1$
51	50	rabdiophlem2	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1))$
52		mzpmulmpt	$⊢ ((c \in (ℤ^{(1 \dots N + 1)}) ⟼ c (N + 1)) \in mzPoly ((1 \dots N + 1)) \land (c \in (ℤ^{(1 \dots N + 1)}) ⟼ ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1))$
53	49 51 52	syl2anc	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1))$
54	53	3adant3	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1))$
55	50	rabdiophlem2	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B) \in mzPoly ((1 \dots N + 1))$
56	55	3adant2	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B) \in mzPoly ((1 \dots N + 1))$
57		eqrabdioph	$⊢ (N + 1 \in ℕ_{0} \land (c \in (ℤ^{(1 \dots N + 1)}) ⟼ c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1)) \land (c \in (ℤ^{(1 \dots N + 1)}) ⟼ ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B) \in mzPoly ((1 \dots N + 1))) \to \{c \in ({ℕ_{0}}^{(1 \dots N + 1)}) \| c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B\} \in Dioph (N + 1)$
58	42 54 56 57	syl3anc	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \{c \in ({ℕ_{0}}^{(1 \dots N + 1)}) \| c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B\} \in Dioph (N + 1)$
59		mzpnegmpt	$⊢ (c \in (ℤ^{(1 \dots N + 1)}) ⟼ c (N + 1)) \in mzPoly ((1 \dots N + 1)) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ - c (N + 1)) \in mzPoly ((1 \dots N + 1))$
60	49 59	syl	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ - c (N + 1)) \in mzPoly ((1 \dots N + 1))$
61		mzpmulmpt	$⊢ ((c \in (ℤ^{(1 \dots N + 1)}) ⟼ - c (N + 1)) \in mzPoly ((1 \dots N + 1)) \land (c \in (ℤ^{(1 \dots N + 1)}) ⟼ ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1))$
62	60 51 61	syl2anc	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1))$
63	62	3adant3	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to (c \in (ℤ^{(1 \dots N + 1)}) ⟼ (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1))$
64		eqrabdioph	$⊢ (N + 1 \in ℕ_{0} \land (c \in (ℤ^{(1 \dots N + 1)}) ⟼ (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A) \in mzPoly ((1 \dots N + 1)) \land (c \in (ℤ^{(1 \dots N + 1)}) ⟼ ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B) \in mzPoly ((1 \dots N + 1))) \to \{c \in ({ℕ_{0}}^{(1 \dots N + 1)}) \| (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B\} \in Dioph (N + 1)$
65	42 63 56 64	syl3anc	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \{c \in ({ℕ_{0}}^{(1 \dots N + 1)}) \| (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B\} \in Dioph (N + 1)$
66		orrabdioph	$⊢ (\{c \in ({ℕ_{0}}^{(1 \dots N + 1)}) \| c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B\} \in Dioph (N + 1) \land \{c \in ({ℕ_{0}}^{(1 \dots N + 1)}) \| (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B\} \in Dioph (N + 1)) \to \{c \in ({ℕ_{0}}^{(1 \dots N + 1)}) \| (c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B \lor (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B)\} \in Dioph (N + 1)$
67	58 65 66	syl2anc	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \{c \in ({ℕ_{0}}^{(1 \dots N + 1)}) \| (c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B \lor (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B)\} \in Dioph (N + 1)$
68		oveq1	$⊢ b = c (N + 1) \to b ⦋ a / t ⦌ A = c (N + 1) ⦋ a / t ⦌ A$
69	68	eqeq1d	$⊢ b = c (N + 1) \to (b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \leftrightarrow c (N + 1) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B)$
70		negeq	$⊢ b = c (N + 1) \to - b = - c (N + 1)$
71	70	oveq1d	$⊢ b = c (N + 1) \to (- b) ⦋ a / t ⦌ A = (- c (N + 1)) ⦋ a / t ⦌ A$
72	71	eqeq1d	$⊢ b = c (N + 1) \to ((- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \leftrightarrow (- c (N + 1)) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B)$
73	69 72	orbi12d	$⊢ b = c (N + 1) \to ((b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B) \leftrightarrow (c (N + 1) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- c (N + 1)) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B))$
74		csbeq1	$⊢ a = {c ↾}_{(1 \dots N)} \to ⦋ a / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A$
75	74	oveq2d	$⊢ a = {c ↾}_{(1 \dots N)} \to c (N + 1) ⦋ a / t ⦌ A = c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A$
76		csbeq1	$⊢ a = {c ↾}_{(1 \dots N)} \to ⦋ a / t ⦌ B = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B$
77	75 76	eqeq12d	$⊢ a = {c ↾}_{(1 \dots N)} \to (c (N + 1) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \leftrightarrow c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B)$
78	74	oveq2d	$⊢ a = {c ↾}_{(1 \dots N)} \to (- c (N + 1)) ⦋ a / t ⦌ A = (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A$
79	78 76	eqeq12d	$⊢ a = {c ↾}_{(1 \dots N)} \to ((- c (N + 1)) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \leftrightarrow (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B)$
80	77 79	orbi12d	$⊢ a = {c ↾}_{(1 \dots N)} \to ((c (N + 1) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- c (N + 1)) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B) \leftrightarrow (c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B \lor (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B))$
81	50 73 80	rexrabdioph	$⊢ (N \in ℕ_{0} \land \{c \in ({ℕ_{0}}^{(1 \dots N + 1)}) \| (c (N + 1) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B \lor (- c (N + 1)) ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ A = ⦋ ({c ↾}_{(1 \dots N)}) / t ⦌ B)\} \in Dioph (N + 1)) \to \{a \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} (b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B)\} \in Dioph (N)$
82	40 67 81	syl2anc	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \{a \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} (b ⦋ a / t ⦌ A = ⦋ a / t ⦌ B \lor (- b) ⦋ a / t ⦌ A = ⦋ a / t ⦌ B)\} \in Dioph (N)$
83	39 82	eqeltrid	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists b \in ℕ_{0} (b A = B \lor (- b) A = B)\} \in Dioph (N)$
84	15 83	eqeltrd	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A ∥ B\} \in Dioph (N)$

Metamath Proof Explorer

Theorem dvdsrabdioph

Proof