Metamath Proof Explorer


Theorem degltlem1

Description: Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Assertion degltlem1 X0−∞YX<YXY1

Proof

Step Hyp Ref Expression
1 elun X0−∞X0X−∞
2 nn0z X0X
3 zltlem1 XYX<YXY1
4 2 3 sylan X0YX<YXY1
5 zre YY
6 5 mnfltd Y−∞<Y
7 peano2zm YY1
8 7 zred YY1
9 8 rexrd YY1*
10 mnfle Y1*−∞Y1
11 9 10 syl Y−∞Y1
12 6 11 2thd Y−∞<Y−∞Y1
13 elsni X−∞X=−∞
14 breq1 X=−∞X<Y−∞<Y
15 breq1 X=−∞XY1−∞Y1
16 14 15 bibi12d X=−∞X<YXY1−∞<Y−∞Y1
17 13 16 syl X−∞X<YXY1−∞<Y−∞Y1
18 12 17 syl5ibrcom YX−∞X<YXY1
19 18 impcom X−∞YX<YXY1
20 4 19 jaoian X0X−∞YX<YXY1
21 1 20 sylanb X0−∞YX<YXY1