Theorem pnfnlt

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

	Ref	Expression
Assertion	pnfnlt	⊢ ( 𝐴 ∈ ℝ* → ¬ +∞ < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pnfnre	⊢ +∞ ∉ ℝ
2	1	neli	⊢ ¬ +∞ ∈ ℝ
3	2	intnanr	⊢ ¬ ( +∞ ∈ ℝ ∧ 𝐴 ∈ ℝ )
4	3	intnanr	⊢ ¬ ( ( +∞ ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ +∞ <ℝ 𝐴 )
5		pnfnemnf	⊢ +∞ ≠ -∞
6	5	neii	⊢ ¬ +∞ = -∞
7	6	intnanr	⊢ ¬ ( +∞ = -∞ ∧ 𝐴 = +∞ )
8	4 7	pm3.2ni	⊢ ¬ ( ( ( +∞ ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ +∞ <ℝ 𝐴 ) ∨ ( +∞ = -∞ ∧ 𝐴 = +∞ ) )
9	2	intnanr	⊢ ¬ ( +∞ ∈ ℝ ∧ 𝐴 = +∞ )
10	6	intnanr	⊢ ¬ ( +∞ = -∞ ∧ 𝐴 ∈ ℝ )
11	9 10	pm3.2ni	⊢ ¬ ( ( +∞ ∈ ℝ ∧ 𝐴 = +∞ ) ∨ ( +∞ = -∞ ∧ 𝐴 ∈ ℝ ) )
12	8 11	pm3.2ni	⊢ ¬ ( ( ( ( +∞ ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ +∞ <ℝ 𝐴 ) ∨ ( +∞ = -∞ ∧ 𝐴 = +∞ ) ) ∨ ( ( +∞ ∈ ℝ ∧ 𝐴 = +∞ ) ∨ ( +∞ = -∞ ∧ 𝐴 ∈ ℝ ) ) )
13		pnfxr	⊢ +∞ ∈ ℝ*
14		ltxr	⊢ ( ( +∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( +∞ < 𝐴 ↔ ( ( ( ( +∞ ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ +∞ <ℝ 𝐴 ) ∨ ( +∞ = -∞ ∧ 𝐴 = +∞ ) ) ∨ ( ( +∞ ∈ ℝ ∧ 𝐴 = +∞ ) ∨ ( +∞ = -∞ ∧ 𝐴 ∈ ℝ ) ) ) ) )
15	13 14	mpan	⊢ ( 𝐴 ∈ ℝ* → ( +∞ < 𝐴 ↔ ( ( ( ( +∞ ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ +∞ <ℝ 𝐴 ) ∨ ( +∞ = -∞ ∧ 𝐴 = +∞ ) ) ∨ ( ( +∞ ∈ ℝ ∧ 𝐴 = +∞ ) ∨ ( +∞ = -∞ ∧ 𝐴 ∈ ℝ ) ) ) ) )
16	12 15	mtbiri	⊢ ( 𝐴 ∈ ℝ* → ¬ +∞ < 𝐴 )