Metamath Proof Explorer


Theorem ltpnf

Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion ltpnf A A < +∞

Proof

Step Hyp Ref Expression
1 eqid +∞ = +∞
2 orc A +∞ = +∞ A +∞ = +∞ A = −∞ +∞
3 1 2 mpan2 A A +∞ = +∞ A = −∞ +∞
4 3 olcd A A +∞ A < +∞ A = −∞ +∞ = +∞ A +∞ = +∞ A = −∞ +∞
5 rexr A A *
6 pnfxr +∞ *
7 ltxr A * +∞ * A < +∞ A +∞ A < +∞ A = −∞ +∞ = +∞ A +∞ = +∞ A = −∞ +∞
8 5 6 7 sylancl A A < +∞ A +∞ A < +∞ A = −∞ +∞ = +∞ A +∞ = +∞ A = −∞ +∞
9 4 8 mpbird A A < +∞