nerabdioph

Description: Diophantine set builder for inequality. This not quite trivial theorem touches on something important; Diophantine sets are not closed under negation, but they contain an important subclass that is, namely the recursive sets. With this theorem and De Morgan's laws, all quantifier-free formulas can be negated. (Contributed by Stefan O'Rear, 11-Oct-2014)

		Ref	Expression
	Assertion	nerabdioph	$⊢ (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 \neq 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		zre	$⊢ A \in ℤ \to A \in ℝ$
4		zre	$⊢ B \in ℤ \to B \in ℝ$
5		lttri2	$⊢ (A \in ℝ \land B \in ℝ) \to (A \neq B \leftrightarrow (A < B \lor B < A))$
6	3 4 5	syl2an	$⊢ (A \in ℤ \land B \in ℤ) \to (A \neq B \leftrightarrow (A < B \lor B < A))$
7	6	ralimi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \in ℤ \land B \in ℤ) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \neq B \leftrightarrow (A < B \lor B < A))$
8		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 ℤ)$
9		rabbi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \neq B \leftrightarrow (A < B \lor B < A)) \leftrightarrow \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A \neq B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (A < B \lor B < A)\}$
10	7 8 9	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 \neq B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (A < B \lor B < A)\}$
11	1 2 10	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 \neq B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (A < B \lor B < A)\}$
12	11	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 \neq B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (A < B \lor B < A)\}$
13		ltrabdioph	$⊢ (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)$
14		ltrabdioph	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ B) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| B < A\} \in Dioph (N)$
15	14	3com23	$⊢ (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)}) \| B < A\} \in Dioph (N)$
16		orrabdioph	$⊢ (\{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A < B\} \in Dioph (N) \land \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| B < A\} \in Dioph (N)) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (A < B \lor B < A)\} \in Dioph (N)$
17	13 15 16	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 \lor B < A)\} \in Dioph (N)$
18	12 17	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 \neq B\} \in Dioph (N)$

Metamath Proof Explorer

Theorem nerabdioph

Proof