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	⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		zex	⊢ ℤ ∈ V
2		nn0ssz	⊢ ℕ0 ⊆ ℤ
3		mapss	⊢ ( ( ℤ ∈ V ∧ ℕ0 ⊆ ℤ ) → ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℤ ↑m ( 1 ... 𝑁 ) ) )
4	1 2 3	mp2an	⊢ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℤ ↑m ( 1 ... 𝑁 ) )
5		mzpf	⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ )
6		eqid	⊢ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) = ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 )
7	6	fmpt	⊢ ( ∀ 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ↔ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ )
8	5 7	sylibr	⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )
9		ssralv	⊢ ( ( ℕ0 ↑m ( 1 ... 𝑁 ) ) ⊆ ( ℤ ↑m ( 1 ... 𝑁 ) ) → ( ∀ 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ) )
10	4 8 9	mpsyl	⊢ ( ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( ℕ0 ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )