Metamath Proof Explorer

Theorem lerabdioph

Description: Diophantine set builder for the "less than or equal to" relation. (Contributed by Stefan O'Rear, 11-Oct-2014)

Ref Expression
Assertion lerabdioph 
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A <_ B } 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 rabdiophlem1 
 |-  ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) B e. ZZ )
3 znn0sub 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A <_ B <-> ( B - A ) e. NN0 ) )
4 3 ralimi 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ZZ /\ B e. ZZ ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) ( A <_ B <-> ( B - A ) e. NN0 ) )
5 r19.26 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A e. ZZ /\ B e. ZZ ) <-> ( A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ /\ A. t e. ( NN0 ^m ( 1 ... N ) ) B e. ZZ ) )
6 rabbi 
 |-  ( A. t e. ( NN0 ^m ( 1 ... N ) ) ( A <_ B <-> ( B - A ) e. NN0 ) <-> { t e. ( NN0 ^m ( 1 ... N ) ) | A <_ B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( B - A ) e. NN0 } )
7 4 5 6 3imtr3i 
 |-  ( ( A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ /\ A. t e. ( NN0 ^m ( 1 ... N ) ) B e. ZZ ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A <_ B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( B - A ) e. NN0 } )
8 1 2 7 syl2an 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A <_ B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( B - A ) e. NN0 } )
9 8 3adant1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A <_ B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( B - A ) e. NN0 } )
10 simp1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> N e. NN0 )
11 mzpsubmpt 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> ( B - A ) ) e. ( mzPoly ` ( 1 ... N ) ) )
12 11 ancoms 
 |-  ( ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> ( B - A ) ) e. ( mzPoly ` ( 1 ... N ) ) )
13 12 3adant1 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... N ) ) |-> ( B - A ) ) e. ( mzPoly ` ( 1 ... N ) ) )
14 elnn0rabdioph 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> ( B - A ) ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( B - A ) e. NN0 } e. ( Dioph ` N ) )
15 10 13 14 syl2anc 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( B - A ) e. NN0 } e. ( Dioph ` N ) )
16 9 15 eqeltrd 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. ( mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A <_ B } e. ( Dioph ` N ) )