Theorem degltlem1

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

	Ref	Expression
Assertion	degltlem1	⊢ ( ( 𝑋 ∈ ( ℕ0 ∪ { -∞ } ) ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elun	⊢ ( 𝑋 ∈ ( ℕ0 ∪ { -∞ } ) ↔ ( 𝑋 ∈ ℕ0 ∨ 𝑋 ∈ { -∞ } ) )
2		nn0z	⊢ ( 𝑋 ∈ ℕ0 → 𝑋 ∈ ℤ )
3		zltlem1	⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )
4	2 3	sylan	⊢ ( ( 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )
5		zre	⊢ ( 𝑌 ∈ ℤ → 𝑌 ∈ ℝ )
6	5	mnfltd	⊢ ( 𝑌 ∈ ℤ → -∞ < 𝑌 )
7		peano2zm	⊢ ( 𝑌 ∈ ℤ → ( 𝑌 − 1 ) ∈ ℤ )
8	7	zred	⊢ ( 𝑌 ∈ ℤ → ( 𝑌 − 1 ) ∈ ℝ )
9	8	rexrd	⊢ ( 𝑌 ∈ ℤ → ( 𝑌 − 1 ) ∈ ℝ* )
10		mnfle	⊢ ( ( 𝑌 − 1 ) ∈ ℝ* → -∞ ≤ ( 𝑌 − 1 ) )
11	9 10	syl	⊢ ( 𝑌 ∈ ℤ → -∞ ≤ ( 𝑌 − 1 ) )
12	6 11	2thd	⊢ ( 𝑌 ∈ ℤ → ( -∞ < 𝑌 ↔ -∞ ≤ ( 𝑌 − 1 ) ) )
13		elsni	⊢ ( 𝑋 ∈ { -∞ } → 𝑋 = -∞ )
14		breq1	⊢ ( 𝑋 = -∞ → ( 𝑋 < 𝑌 ↔ -∞ < 𝑌 ) )
15		breq1	⊢ ( 𝑋 = -∞ → ( 𝑋 ≤ ( 𝑌 − 1 ) ↔ -∞ ≤ ( 𝑌 − 1 ) ) )
16	14 15	bibi12d	⊢ ( 𝑋 = -∞ → ( ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) ↔ ( -∞ < 𝑌 ↔ -∞ ≤ ( 𝑌 − 1 ) ) ) )
17	13 16	syl	⊢ ( 𝑋 ∈ { -∞ } → ( ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) ↔ ( -∞ < 𝑌 ↔ -∞ ≤ ( 𝑌 − 1 ) ) ) )
18	12 17	syl5ibrcom	⊢ ( 𝑌 ∈ ℤ → ( 𝑋 ∈ { -∞ } → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) ) )
19	18	impcom	⊢ ( ( 𝑋 ∈ { -∞ } ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )
20	4 19	jaoian	⊢ ( ( ( 𝑋 ∈ ℕ0 ∨ 𝑋 ∈ { -∞ } ) ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )
21	1 20	sylanb	⊢ ( ( 𝑋 ∈ ( ℕ0 ∪ { -∞ } ) ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < 𝑌 ↔ 𝑋 ≤ ( 𝑌 − 1 ) ) )