pnfnlt

Description: No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005)

		Ref	Expression
	Assertion	pnfnlt	$⊢ A \in ℝ^{*} \to \neg +∞ < A$

Step	Hyp	Ref	Expression
1		pnfnre	$⊢ +∞ \notin ℝ$
2	1	neli	$⊢ \neg +∞ \in ℝ$
3	2	intnanr	$⊢ \neg (+∞ \in ℝ \land A \in ℝ)$
4	3	intnanr	$⊢ \neg ((+∞ \in ℝ \land A \in ℝ) \land +∞ <_{ℝ} A)$
5		pnfnemnf	$⊢ +∞ \neq −∞$
6	5	neii	$⊢ \neg +∞ = −∞$
7	6	intnanr	$⊢ \neg (+∞ = −∞ \land A = +∞)$
8	4 7	pm3.2ni	$⊢ \neg (((+∞ \in ℝ \land A \in ℝ) \land +∞ <_{ℝ} A) \lor (+∞ = −∞ \land A = +∞))$
9	2	intnanr	$⊢ \neg (+∞ \in ℝ \land A = +∞)$
10	6	intnanr	$⊢ \neg (+∞ = −∞ \land A \in ℝ)$
11	9 10	pm3.2ni	$⊢ \neg ((+∞ \in ℝ \land A = +∞) \lor (+∞ = −∞ \land A \in ℝ))$
12	8 11	pm3.2ni	$⊢ \neg ((((+∞ \in ℝ \land A \in ℝ) \land +∞ <_{ℝ} A) \lor (+∞ = −∞ \land A = +∞)) \lor ((+∞ \in ℝ \land A = +∞) \lor (+∞ = −∞ \land A \in ℝ)))$
13		pnfxr	$⊢ +∞ \in ℝ^{*}$
14		ltxr	$⊢ (+∞ \in ℝ^{} \land A \in ℝ^{}) \to (+∞ < A \leftrightarrow ((((+∞ \in ℝ \land A \in ℝ) \land +∞ <_{ℝ} A) \lor (+∞ = −∞ \land A = +∞)) \lor ((+∞ \in ℝ \land A = +∞) \lor (+∞ = −∞ \land A \in ℝ))))$
15	13 14	mpan	$⊢ A \in ℝ^{*} \to (+∞ < A \leftrightarrow ((((+∞ \in ℝ \land A \in ℝ) \land +∞ <_{ℝ} A) \lor (+∞ = −∞ \land A = +∞)) \lor ((+∞ \in ℝ \land A = +∞) \lor (+∞ = −∞ \land A \in ℝ))))$
16	12 15	mtbiri	$⊢ A \in ℝ^{*} \to \neg +∞ < A$

Metamath Proof Explorer