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 e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ )

Proof

Step	Hyp	Ref	Expression
1		zex	|- ZZ e. _V
2		nn0ssz	|- NN0 C_ ZZ
3		mapss	|- ( ( ZZ e. _V /\ NN0 C_ ZZ ) -> ( NN0 ^m ( 1 ... N ) ) C_ ( ZZ ^m ( 1 ... N ) ) )
4	1 2 3	mp2an	|- ( NN0 ^m ( 1 ... N ) ) C_ ( ZZ ^m ( 1 ... N ) )
5		mzpf	|- ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ )
6		eqid	|- ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) = ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A )
7	6	fmpt	|- ( A. t e. ( ZZ ^m ( 1 ... N ) ) A e. ZZ <-> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) : ( ZZ ^m ( 1 ... N ) ) --> ZZ )
8	5 7	sylibr	|- ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> A. t e. ( ZZ ^m ( 1 ... N ) ) A e. ZZ )
9		ssralv	|- ( ( NN0 ^m ( 1 ... N ) ) C_ ( ZZ ^m ( 1 ... N ) ) -> ( A. t e. ( ZZ ^m ( 1 ... N ) ) A e. ZZ -> A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ ) )
10	4 8 9	mpsyl	|- ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ )