Theorem nltpnft

Description: An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006)

	Ref	Expression
Assertion	nltpnft	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = +∞ ↔ ¬ 𝐴 < +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		pnfxr	⊢ +∞ ∈ ℝ*
2		xrltnr	⊢ ( +∞ ∈ ℝ* → ¬ +∞ < +∞ )
3	1 2	ax-mp	⊢ ¬ +∞ < +∞
4		breq1	⊢ ( 𝐴 = +∞ → ( 𝐴 < +∞ ↔ +∞ < +∞ ) )
5	3 4	mtbiri	⊢ ( 𝐴 = +∞ → ¬ 𝐴 < +∞ )
6		pnfge	⊢ ( 𝐴 ∈ ℝ* → 𝐴 ≤ +∞ )
7		xrleloe	⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 ≤ +∞ ↔ ( 𝐴 < +∞ ∨ 𝐴 = +∞ ) ) )
8	1 7	mpan2	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ≤ +∞ ↔ ( 𝐴 < +∞ ∨ 𝐴 = +∞ ) ) )
9	6 8	mpbid	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 < +∞ ∨ 𝐴 = +∞ ) )
10	9	ord	⊢ ( 𝐴 ∈ ℝ* → ( ¬ 𝐴 < +∞ → 𝐴 = +∞ ) )
11	5 10	impbid2	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = +∞ ↔ ¬ 𝐴 < +∞ ) )