Description: Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | degltlem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elun | |
|
2 | nn0z | |
|
3 | zltlem1 | |
|
4 | 2 3 | sylan | |
5 | zre | |
|
6 | 5 | mnfltd | |
7 | peano2zm | |
|
8 | 7 | zred | |
9 | 8 | rexrd | |
10 | mnfle | |
|
11 | 9 10 | syl | |
12 | 6 11 | 2thd | |
13 | elsni | |
|
14 | breq1 | |
|
15 | breq1 | |
|
16 | 14 15 | bibi12d | |
17 | 13 16 | syl | |
18 | 12 17 | syl5ibrcom | |
19 | 18 | impcom | |
20 | 4 19 | jaoian | |
21 | 1 20 | sylanb | |