Metamath Proof Explorer

Theorem ltrabdioph

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

Ref Expression
Assertion ltrabdioph 
|- ( ( 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 znnsub 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( B - A ) e. NN ) )
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. NN ) )
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. NN ) <-> { t e. ( NN0 ^m ( 1 ... N ) ) | A < B } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( B - A ) e. NN } )
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. NN } )
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. NN } )
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. NN } )
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 elnnrabdioph 
 |-  ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> ( B - A ) ) e. ( mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( B - A ) e. NN } 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. NN } 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 ) )