ltpnf

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

		Ref	Expression
	Assertion	ltpnf	$⊢ A \in ℝ \to A < +∞$

Step	Hyp	Ref	Expression
1		eqid	$⊢ +∞ = +∞$
2		orc	$⊢ (A \in ℝ \land +∞ = +∞) \to ((A \in ℝ \land +∞ = +∞) \lor (A = −∞ \land +∞ \in ℝ))$
3	1 2	mpan2	$⊢ A \in ℝ \to ((A \in ℝ \land +∞ = +∞) \lor (A = −∞ \land +∞ \in ℝ))$
4	3	olcd	$⊢ A \in ℝ \to ((((A \in ℝ \land +∞ \in ℝ) \land A <_{ℝ} +∞) \lor (A = −∞ \land +∞ = +∞)) \lor ((A \in ℝ \land +∞ = +∞) \lor (A = −∞ \land +∞ \in ℝ)))$
5		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
6		pnfxr	$⊢ +∞ \in ℝ^{*}$
7		ltxr	$⊢ (A \in ℝ^{} \land +∞ \in ℝ^{}) \to (A < +∞ \leftrightarrow ((((A \in ℝ \land +∞ \in ℝ) \land A <_{ℝ} +∞) \lor (A = −∞ \land +∞ = +∞)) \lor ((A \in ℝ \land +∞ = +∞) \lor (A = −∞ \land +∞ \in ℝ))))$
8	5 6 7	sylancl	$⊢ A \in ℝ \to (A < +∞ \leftrightarrow ((((A \in ℝ \land +∞ \in ℝ) \land A <_{ℝ} +∞) \lor (A = −∞ \land +∞ = +∞)) \lor ((A \in ℝ \land +∞ = +∞) \lor (A = −∞ \land +∞ \in ℝ))))$
9	4 8	mpbird	$⊢ A \in ℝ \to A < +∞$

Metamath Proof Explorer