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 ) ) )