Theorem ltpnf

Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005)

	Ref	Expression
Assertion	ltpnf	⊢ ( 𝐴 ∈ ℝ → 𝐴 < +∞ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ +∞ = +∞
2		orc	⊢ ( ( 𝐴 ∈ ℝ ∧ +∞ = +∞ ) → ( ( 𝐴 ∈ ℝ ∧ +∞ = +∞ ) ∨ ( 𝐴 = -∞ ∧ +∞ ∈ ℝ ) ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 ∈ ℝ ∧ +∞ = +∞ ) ∨ ( 𝐴 = -∞ ∧ +∞ ∈ ℝ ) ) )
4	3	olcd	⊢ ( 𝐴 ∈ ℝ → ( ( ( ( 𝐴 ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ 𝐴 <ℝ +∞ ) ∨ ( 𝐴 = -∞ ∧ +∞ = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ +∞ = +∞ ) ∨ ( 𝐴 = -∞ ∧ +∞ ∈ ℝ ) ) ) )
5		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
6		pnfxr	⊢ +∞ ∈ ℝ*
7		ltxr	⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 < +∞ ↔ ( ( ( ( 𝐴 ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ 𝐴 <ℝ +∞ ) ∨ ( 𝐴 = -∞ ∧ +∞ = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ +∞ = +∞ ) ∨ ( 𝐴 = -∞ ∧ +∞ ∈ ℝ ) ) ) ) )
8	5 6 7	sylancl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < +∞ ↔ ( ( ( ( 𝐴 ∈ ℝ ∧ +∞ ∈ ℝ ) ∧ 𝐴 <ℝ +∞ ) ∨ ( 𝐴 = -∞ ∧ +∞ = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ +∞ = +∞ ) ∨ ( 𝐴 = -∞ ∧ +∞ ∈ ℝ ) ) ) ) )
9	4 8	mpbird	⊢ ( 𝐴 ∈ ℝ → 𝐴 < +∞ )