eqrabdioph

Description: Diophantine set builder for equality of polynomial expressions. Note that the two expressions need not be nonnegative; only variables are so constrained. (Contributed by Stefan O'Rear, 10-Oct-2014)

		Ref	Expression
	Assertion	eqrabdioph	$⊢ (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		nfmpt1	$⊢ \underline{Ⅎ} t (t \in (ℤ^{(1 \dots N)}) ⟼ A)$
2	1	nfel1	$⊢ Ⅎ t (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))$
3		nfmpt1	$⊢ \underline{Ⅎ} t (t \in (ℤ^{(1 \dots N)}) ⟼ B)$
4	3	nfel1	$⊢ Ⅎ t (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))$
5	2 4	nfan	$⊢ Ⅎ t ((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N)))$
6		mzpf	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \to (t \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ$
7	6	ad2antrr	$⊢ (((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to (t \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ$
8		zex	$⊢ ℤ \in V$
9		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
10		mapss	$⊢ (ℤ \in V \land ℕ_{0} \subseteq ℤ) \to {ℕ_{0}}^{(1 \dots N)} \subseteq ℤ^{(1 \dots N)}$
11	8 9 10	mp2an	$⊢ {ℕ_{0}}^{(1 \dots N)} \subseteq ℤ^{(1 \dots N)}$
12	11	sseli	$⊢ t \in ({ℕ_{0}}^{(1 \dots N)}) \to t \in (ℤ^{(1 \dots N)})$
13	12	adantl	$⊢ (((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to t \in (ℤ^{(1 \dots N)})$
14		mptfcl	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ \to (t \in (ℤ^{(1 \dots N)}) \to A \in ℤ)$
15	7 13 14	sylc	$⊢ (((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to A \in ℤ$
16	15	zcnd	$⊢ (((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to A \in ℂ$
17		mzpf	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N)) \to (t \in (ℤ^{(1 \dots N)}) ⟼ B) : ℤ^{(1 \dots N)} ⟶ ℤ$
18	17	ad2antlr	$⊢ (((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to (t \in (ℤ^{(1 \dots N)}) ⟼ B) : ℤ^{(1 \dots N)} ⟶ ℤ$
19		mptfcl	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ B) : ℤ^{(1 \dots N)} ⟶ ℤ \to (t \in (ℤ^{(1 \dots N)}) \to B \in ℤ)$
20	18 13 19	sylc	$⊢ (((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to B \in ℤ$
21	20	zcnd	$⊢ (((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to B \in ℂ$
22	16 21	subeq0ad	$⊢ (((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to (A - B = 0 \leftrightarrow A = B)$
23	22	bicomd	$⊢ (((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to (A = B \leftrightarrow A - B = 0)$
24	23	ex	$⊢ ((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)}) \to (A = B \leftrightarrow A - B = 0))$
25	5 24	ralrimi	$⊢ ((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N))) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A = B \leftrightarrow A - B = 0)$
26		rabbi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A = B \leftrightarrow A - B = 0) \leftrightarrow \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A = B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A - B = 0\}$
27	25 26	sylib	$⊢ ((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)}) \| A - B = 0\}$
28	27	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)}) \| A - B = 0\}$
29		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}$
30		mzpsubmpt	$⊢ ((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 (ℤ^{(1 \dots N)}) ⟼ A - B) \in mzPoly ((1 \dots N))$
31	30	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 (ℤ^{(1 \dots N)}) ⟼ A - B) \in mzPoly ((1 \dots N))$
32		eq0rabdioph	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A - B) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A - B = 0\} \in Dioph (N)$
33	29 31 32	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 \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A - B = 0\} \in Dioph (N)$
34	28 33	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 eqrabdioph

Proof