Metamath Proof Explorer

Theorem rabdiophlem1

Description: Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi . (Contributed by Stefan O'Rear, 10-Oct-2014)

		Ref	Expression
	Assertion	rabdiophlem1	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) A \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		zex	$⊢ ℤ \in V$
2		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
3		mapss	$⊢ (ℤ \in V \land ℕ_{0} \subseteq ℤ) \to {ℕ_{0}}^{(1 \dots N)} \subseteq ℤ^{(1 \dots N)}$
4	1 2 3	mp2an	$⊢ {ℕ_{0}}^{(1 \dots N)} \subseteq ℤ^{(1 \dots N)}$
5		mzpf	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \to (t \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ$
6		eqid	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) = (t \in (ℤ^{(1 \dots N)}) ⟼ A)$
7	6	fmpt	$⊢ \forall t \in (ℤ^{(1 \dots N)}) A \in ℤ \leftrightarrow (t \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ$
8	5 7	sylibr	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \to \forall t \in (ℤ^{(1 \dots N)}) A \in ℤ$
9		ssralv	$⊢ {ℕ_{0}}^{(1 \dots N)} \subseteq ℤ^{(1 \dots N)} \to (\forall t \in (ℤ^{(1 \dots N)}) A \in ℤ \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) A \in ℤ)$
10	4 8 9	mpsyl	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) A \in ℤ$