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 0 t 1 N A mzPoly 1 N t 1 N B mzPoly 1 N t 0 1 N | A B Dioph N

Proof

Step Hyp Ref Expression
1 rabdiophlem1 t 1 N A mzPoly 1 N t 0 1 N A
2 rabdiophlem1 t 1 N B mzPoly 1 N t 0 1 N B
3 znn0sub A B A B B A 0
4 3 ralimi t 0 1 N A B t 0 1 N A B B A 0
5 r19.26 t 0 1 N A B t 0 1 N A t 0 1 N B
6 rabbi t 0 1 N A B B A 0 t 0 1 N | A B = t 0 1 N | B A 0
7 4 5 6 3imtr3i t 0 1 N A t 0 1 N B t 0 1 N | A B = t 0 1 N | B A 0
8 1 2 7 syl2an t 1 N A mzPoly 1 N t 1 N B mzPoly 1 N t 0 1 N | A B = t 0 1 N | B A 0
9 8 3adant1 N 0 t 1 N A mzPoly 1 N t 1 N B mzPoly 1 N t 0 1 N | A B = t 0 1 N | B A 0
10 simp1 N 0 t 1 N A mzPoly 1 N t 1 N B mzPoly 1 N N 0
11 mzpsubmpt t 1 N B mzPoly 1 N t 1 N A mzPoly 1 N t 1 N B A mzPoly 1 N
12 11 ancoms t 1 N A mzPoly 1 N t 1 N B mzPoly 1 N t 1 N B A mzPoly 1 N
13 12 3adant1 N 0 t 1 N A mzPoly 1 N t 1 N B mzPoly 1 N t 1 N B A mzPoly 1 N
14 elnn0rabdioph N 0 t 1 N B A mzPoly 1 N t 0 1 N | B A 0 Dioph N
15 10 13 14 syl2anc N 0 t 1 N A mzPoly 1 N t 1 N B mzPoly 1 N t 0 1 N | B A 0 Dioph N
16 9 15 eqeltrd N 0 t 1 N A mzPoly 1 N t 1 N B mzPoly 1 N t 0 1 N | A B Dioph N