Metamath Proof Explorer

Theorem eluzrabdioph

Description: Diophantine set builder for membership in a fixed upper set of integers. (Contributed by Stefan O'Rear, 11-Oct-2014)

		Ref	Expression
	Assertion	eluzrabdioph	$⊢ (N \in ℕ_{0} \land M \in ℤ \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A \in ℤ_{\geq M}\} \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		eluz	$⊢ (M \in ℤ \land A \in ℤ) \to (A \in ℤ_{\geq M} \leftrightarrow M \leq A)$
3	2	ex	$⊢ M \in ℤ \to (A \in ℤ \to (A \in ℤ_{\geq M} \leftrightarrow M \leq A))$
4	3	ralimdv	$⊢ M \in ℤ \to (\forall t \in ({ℕ_{0}}^{(1 \dots N)}) A \in ℤ \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \in ℤ_{\geq M} \leftrightarrow M \leq A))$
5	4	imp	$⊢ (M \in ℤ \land \forall t \in ({ℕ_{0}}^{(1 \dots N)}) A \in ℤ) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \in ℤ_{\geq M} \leftrightarrow M \leq A)$
6	1 5	sylan2	$⊢ (M \in ℤ \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \in ℤ_{\geq M} \leftrightarrow M \leq A)$
7		rabbi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A \in ℤ_{\geq M} \leftrightarrow M \leq A) \leftrightarrow \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A \in ℤ_{\geq M}\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| M \leq A\}$
8	6 7	sylib	$⊢ (M \in ℤ \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A \in ℤ_{\geq M}\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| M \leq A\}$
9	8	3adant1	$⊢ (N \in ℕ_{0} \land M \in ℤ \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A \in ℤ_{\geq M}\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| M \leq A\}$
10		ovex	$⊢ (1 \dots N) \in V$
11		mzpconstmpt	$⊢ ((1 \dots N) \in V \land M \in ℤ) \to (t \in (ℤ^{(1 \dots N)}) ⟼ M) \in mzPoly ((1 \dots N))$
12	10 11	mpan	$⊢ M \in ℤ \to (t \in (ℤ^{(1 \dots N)}) ⟼ M) \in mzPoly ((1 \dots N))$
13		lerabdioph	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ M) \in mzPoly ((1 \dots N)) \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| M \leq A\} \in Dioph (N)$
14	12 13	syl3an2	$⊢ (N \in ℕ_{0} \land M \in ℤ \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| M \leq A\} \in Dioph (N)$
15	9 14	eqeltrd	$⊢ (N \in ℕ_{0} \land M \in ℤ \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A \in ℤ_{\geq M}\} \in Dioph (N)$