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 e. NN0 /\ M e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. ( ZZ>= ` M ) } e. ( Dioph ` N ) )

Proof

Step	Hyp	Ref	Expression
1		rabdiophlem1	|- ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ )
2		eluz	|- ( ( M e. ZZ /\ A e. ZZ ) -> ( A e. ( ZZ>= ` M ) <-> M <_ A ) )
3	2	ex	|- ( M e. ZZ -> ( A e. ZZ -> ( A e. ( ZZ>= ` M ) <-> M <_ A ) ) )
4	3	ralimdv	|- ( M e. ZZ -> ( A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ -> A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ( ZZ>= ` M ) <-> M <_ A ) ) )
5	4	imp	|- ( ( M e. ZZ /\ A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ( ZZ>= ` M ) <-> M <_ A ) )
6	1 5	sylan2	|- ( ( M e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ( ZZ>= ` M ) <-> M <_ A ) )
7		rabbi	|- ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ( ZZ>= ` M ) <-> M <_ A ) <-> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. ( ZZ>= ` M ) } = { t e. ( NN0 ^m ( 1 ... N ) ) | M <_ A } )
8	6 7	sylib	|- ( ( M e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. ( ZZ>= ` M ) } = { t e. ( NN0 ^m ( 1 ... N ) ) | M <_ A } )
9	8	3adant1	|- ( ( N e. NN0 /\ M e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. ( ZZ>= ` M ) } = { t e. ( NN0 ^m ( 1 ... N ) ) | M <_ A } )
10		ovex	|- ( 1 ... N ) e. _V
11		mzpconstmpt	|- ( ( ( 1 ... N ) e. _V /\ M e. ZZ ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> M ) e. ( mzPoly ` ( 1 ... N ) ) )
12	10 11	mpan	|- ( M e. ZZ -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> M ) e. ( mzPoly ` ( 1 ... N ) ) )
13		lerabdioph	|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> M ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | M <_ A } e. ( Dioph ` N ) )
14	12 13	syl3an2	|- ( ( N e. NN0 /\ M e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | M <_ A } e. ( Dioph ` N ) )
15	9 14	eqeltrd	|- ( ( N e. NN0 /\ M e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. ( ZZ>= ` M ) } e. ( Dioph ` N ) )