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