Metamath Proof Explorer

Theorem lerabdioph

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

		Ref	Expression
	Assertion	lerabdioph	$⊢ (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 \leq 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		znn0sub	$⊢ (A \in ℤ \land B \in ℤ) \to (A \leq B \leftrightarrow B - A \in ℕ_{0})$
4	3	ralimi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \in ℤ \land B \in ℤ) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \leq B \leftrightarrow B - A \in ℕ_{0})$
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 \leq B \leftrightarrow B - A \in ℕ_{0}) \leftrightarrow \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A \leq B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| B - A \in ℕ_{0}\}$
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 \leq B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| B - A \in ℕ_{0}\}$
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 \leq B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| B - A \in ℕ_{0}\}$
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 \leq B\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| B - A \in ℕ_{0}\}$
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		elnn0rabdioph	$⊢ (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 ℕ_{0}\} \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 ℕ_{0}\} \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 \leq B\} \in Dioph (N)$