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 ) ↔ 𝑋 ≤ 𝑌 ) )