This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( X e. ( NN0 u. { -oo } ) /\ Y e. ZZ ) -> ( X < Y <-> X <_ ( Y - 1 ) ) )

Proof

Step Hyp Ref Expression
1 elun 
 |-  ( X e. ( NN0 u. { -oo } ) <-> ( X e. NN0 \/ X e. { -oo } ) )
2 nn0z 
 |-  ( X e. NN0 -> X e. ZZ )
3 zltlem1 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( X < Y <-> X <_ ( Y - 1 ) ) )
4 2 3 sylan 
 |-  ( ( X e. NN0 /\ Y e. ZZ ) -> ( X < Y <-> X <_ ( Y - 1 ) ) )
5 zre 
 |-  ( Y e. ZZ -> Y e. RR )
6 5 mnfltd 
 |-  ( Y e. ZZ -> -oo < Y )
7 peano2zm 
 |-  ( Y e. ZZ -> ( Y - 1 ) e. ZZ )
8 7 zred 
 |-  ( Y e. ZZ -> ( Y - 1 ) e. RR )
9 8 rexrd 
 |-  ( Y e. ZZ -> ( Y - 1 ) e. RR* )
10 mnfle 
 |-  ( ( Y - 1 ) e. RR* -> -oo <_ ( Y - 1 ) )
11 9 10 syl 
 |-  ( Y e. ZZ -> -oo <_ ( Y - 1 ) )
12 6 11 2thd 
 |-  ( Y e. ZZ -> ( -oo < Y <-> -oo <_ ( Y - 1 ) ) )
13 elsni 
 |-  ( X e. { -oo } -> X = -oo )
14 breq1 
 |-  ( X = -oo -> ( X < Y <-> -oo < Y ) )
15 breq1 
 |-  ( X = -oo -> ( X <_ ( Y - 1 ) <-> -oo <_ ( Y - 1 ) ) )
16 14 15 bibi12d 
 |-  ( X = -oo -> ( ( X < Y <-> X <_ ( Y - 1 ) ) <-> ( -oo < Y <-> -oo <_ ( Y - 1 ) ) ) )
17 13 16 syl 
 |-  ( X e. { -oo } -> ( ( X < Y <-> X <_ ( Y - 1 ) ) <-> ( -oo < Y <-> -oo <_ ( Y - 1 ) ) ) )
18 12 17 syl5ibrcom 
 |-  ( Y e. ZZ -> ( X e. { -oo } -> ( X < Y <-> X <_ ( Y - 1 ) ) ) )
19 18 impcom 
 |-  ( ( X e. { -oo } /\ Y e. ZZ ) -> ( X < Y <-> X <_ ( Y - 1 ) ) )
20 4 19 jaoian 
 |-  ( ( ( X e. NN0 \/ X e. { -oo } ) /\ Y e. ZZ ) -> ( X < Y <-> X <_ ( Y - 1 ) ) )
21 1 20 sylanb 
 |-  ( ( X e. ( NN0 u. { -oo } ) /\ Y e. ZZ ) -> ( X < Y <-> X <_ ( Y - 1 ) ) )