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 ∈ ℕ 0 ∪ −∞ ∧ Y ∈ ℤ → X < Y ↔ X ≤ Y − 1

Proof

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