# 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}\in ℝ\to {A}<\mathrm{+\infty }$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{+\infty }=\mathrm{+\infty }$
2 orc ${⊢}\left({A}\in ℝ\wedge \mathrm{+\infty }=\mathrm{+\infty }\right)\to \left(\left({A}\in ℝ\wedge \mathrm{+\infty }=\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{+\infty }\in ℝ\right)\right)$
3 1 2 mpan2 ${⊢}{A}\in ℝ\to \left(\left({A}\in ℝ\wedge \mathrm{+\infty }=\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{+\infty }\in ℝ\right)\right)$
4 3 olcd ${⊢}{A}\in ℝ\to \left(\left(\left(\left({A}\in ℝ\wedge \mathrm{+\infty }\in ℝ\right)\wedge {A}{<}_{ℝ}\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{+\infty }=\mathrm{+\infty }\right)\right)\vee \left(\left({A}\in ℝ\wedge \mathrm{+\infty }=\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{+\infty }\in ℝ\right)\right)\right)$
5 rexr ${⊢}{A}\in ℝ\to {A}\in {ℝ}^{*}$
6 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
7 ltxr ${⊢}\left({A}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({A}<\mathrm{+\infty }↔\left(\left(\left(\left({A}\in ℝ\wedge \mathrm{+\infty }\in ℝ\right)\wedge {A}{<}_{ℝ}\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{+\infty }=\mathrm{+\infty }\right)\right)\vee \left(\left({A}\in ℝ\wedge \mathrm{+\infty }=\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{+\infty }\in ℝ\right)\right)\right)\right)$
8 5 6 7 sylancl ${⊢}{A}\in ℝ\to \left({A}<\mathrm{+\infty }↔\left(\left(\left(\left({A}\in ℝ\wedge \mathrm{+\infty }\in ℝ\right)\wedge {A}{<}_{ℝ}\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{+\infty }=\mathrm{+\infty }\right)\right)\vee \left(\left({A}\in ℝ\wedge \mathrm{+\infty }=\mathrm{+\infty }\right)\vee \left({A}=\mathrm{-\infty }\wedge \mathrm{+\infty }\in ℝ\right)\right)\right)\right)$
9 4 8 mpbird ${⊢}{A}\in ℝ\to {A}<\mathrm{+\infty }$