Metamath Proof Explorer

Theorem ltrabdioph

Description: Diophantine set builder for the strict less than relation. (Contributed by Stefan O'Rear, 11-Oct-2014)

		Ref	Expression
	Assertion	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)$

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		znnsub	$⊢ (A \in ℤ \land B \in ℤ) \to (A < B \leftrightarrow B - A \in ℕ)$
4	3	ralimi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \in ℤ \land B \in ℤ) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A < B \leftrightarrow B - A \in ℕ)$
5		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 ℤ)$
6		rabbi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A < B \leftrightarrow B - A \in ℕ) \leftrightarrow \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A < B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| B - A \in ℕ\}$
7	4 5 6	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)}) \| B - A \in ℕ\}$
8	1 2 7	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)}) \| B - A \in ℕ\}$
9	8	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)}) \| B - A \in ℕ\}$
10		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}$
11		mzpsubmpt	$⊢ ((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 (ℤ^{(1 \dots N)}) ⟼ B - A) \in mzPoly ((1 \dots N))$
12	11	ancoms	$⊢ ((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)}) ⟼ B - A) \in mzPoly ((1 \dots N))$
13	12	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)}) ⟼ B - A) \in mzPoly ((1 \dots N))$
14		elnnrabdioph	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ B - A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| B - A \in ℕ\} \in Dioph (N)$
15	10 13 14	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)}) \| B - A \in ℕ\} \in Dioph (N)$
16	9 15	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)$