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 ( 𝜑𝐴 ≠ +∞ )
nepnfltpnf.2 ( 𝜑𝐴 ∈ ℝ* )
Assertion nepnfltpnf ( 𝜑𝐴 < +∞ )

Proof

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