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

Proof

Step Hyp Ref Expression
1 peano2z ⊢ Y ∈ ℤ → Y + 1 ∈ ℤ
2 degltlem1 ⊢ X ∈ ℕ 0 ∪ −∞ ∧ Y + 1 ∈ ℤ → X < Y + 1 ↔ X ≤ Y + 1 - 1
3 1 2 sylan2 ⊢ X ∈ ℕ 0 ∪ −∞ ∧ Y ∈ ℤ → X < Y + 1 ↔ X ≤ Y + 1 - 1
4 zcn ⊢ Y ∈ ℤ → Y ∈ ℂ
5 ax-1cn ⊢ 1 ∈ ℂ
6 pncan ⊢ Y ∈ ℂ ∧ 1 ∈ ℂ → Y + 1 - 1 = Y
7 4 5 6 sylancl ⊢ Y ∈ ℤ → Y + 1 - 1 = Y
8 7 breq2d ⊢ Y ∈ ℤ → X ≤ Y + 1 - 1 ↔ X ≤ Y
9 8 adantl ⊢ X ∈ ℕ 0 ∪ −∞ ∧ Y ∈ ℤ → X ≤ Y + 1 - 1 ↔ X ≤ Y
10 3 9 bitrd ⊢ X ∈ ℕ 0 ∪ −∞ ∧ Y ∈ ℤ → X < Y + 1 ↔ X ≤ Y