This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑋 ∈ ( ℕ0 ∪ { -∞ } ) ∧ 𝑌 ∈ ℤ ) → ( 𝑋 < ( 𝑌 + 1 ) ↔ 𝑋 ≤ 𝑌 ) )

Proof

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