Metamath Proof Explorer

Theorem degltp1le

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

Ref Expression
Assertion degltp1le 
|- ( ( X e. ( NN0 u. { -oo } ) /\ Y e. ZZ ) -> ( X < ( Y + 1 ) <-> X <_ Y ) )

Proof

Step Hyp Ref Expression
1 peano2z 
 |-  ( Y e. ZZ -> ( Y + 1 ) e. ZZ )
2 degltlem1 
 |-  ( ( X e. ( NN0 u. { -oo } ) /\ ( Y + 1 ) e. ZZ ) -> ( X < ( Y + 1 ) <-> X <_ ( ( Y + 1 ) - 1 ) ) )
3 1 2 sylan2 
 |-  ( ( X e. ( NN0 u. { -oo } ) /\ Y e. ZZ ) -> ( X < ( Y + 1 ) <-> X <_ ( ( Y + 1 ) - 1 ) ) )
4 zcn 
 |-  ( Y e. ZZ -> Y e. CC )
5 ax-1cn 
 |-  1 e. CC
6 pncan 
 |-  ( ( Y e. CC /\ 1 e. CC ) -> ( ( Y + 1 ) - 1 ) = Y )
7 4 5 6 sylancl 
 |-  ( Y e. ZZ -> ( ( Y + 1 ) - 1 ) = Y )
8 7 breq2d 
 |-  ( Y e. ZZ -> ( X <_ ( ( Y + 1 ) - 1 ) <-> X <_ Y ) )
9 8 adantl 
 |-  ( ( X e. ( NN0 u. { -oo } ) /\ Y e. ZZ ) -> ( X <_ ( ( Y + 1 ) - 1 ) <-> X <_ Y ) )
10 3 9 bitrd 
 |-  ( ( X e. ( NN0 u. { -oo } ) /\ Y e. ZZ ) -> ( X < ( Y + 1 ) <-> X <_ Y ) )