This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nepnfltpnf

Description: An extended real that is not +oo is less than +oo . (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses nepnfltpnf.1 ⊢ φ → A ≠ +∞
nepnfltpnf.2 ⊢ φ → A ∈ ℝ *
Assertion nepnfltpnf ⊢ φ → A < +∞

Proof

Step Hyp Ref Expression
1 nepnfltpnf.1 ⊢ φ → A ≠ +∞
2 nepnfltpnf.2 ⊢ φ → A ∈ ℝ *
3 1 neneqd ⊢ φ → ¬ A = +∞
4 nltpnft ⊢ A ∈ ℝ * → A = +∞ ↔ ¬ A < +∞
5 2 4 syl ⊢ φ → A = +∞ ↔ ¬ A < +∞
6 3 5 mtbid ⊢ φ → ¬ ¬ A < +∞
7 notnotb ⊢ A < +∞ ↔ ¬ ¬ A < +∞
8 6 7 sylibr ⊢ φ → A < +∞