# Metamath Proof Explorer

## Theorem pnfinf

Description: Plus infinity is an infinite for the completed real line, as any real number is infinitesimal compared to it. (Contributed by Thierry Arnoux, 1-Feb-2018)

Ref Expression
Assertion pnfinf ${⊢}{A}\in {ℝ}^{+}\to {A}⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }$

### Proof

Step Hyp Ref Expression
1 rpgt0 ${⊢}{A}\in {ℝ}^{+}\to 0<{A}$
2 nnz ${⊢}{n}\in ℕ\to {n}\in ℤ$
3 2 adantl ${⊢}\left({A}\in {ℝ}^{+}\wedge {n}\in ℕ\right)\to {n}\in ℤ$
4 rpxr ${⊢}{A}\in {ℝ}^{+}\to {A}\in {ℝ}^{*}$
5 4 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge {n}\in ℕ\right)\to {A}\in {ℝ}^{*}$
6 xrsmulgzz ${⊢}\left({n}\in ℤ\wedge {A}\in {ℝ}^{*}\right)\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}={n}{\cdot }_{𝑒}{A}$
7 3 5 6 syl2anc ${⊢}\left({A}\in {ℝ}^{+}\wedge {n}\in ℕ\right)\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}={n}{\cdot }_{𝑒}{A}$
8 3 zred ${⊢}\left({A}\in {ℝ}^{+}\wedge {n}\in ℕ\right)\to {n}\in ℝ$
9 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
10 9 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge {n}\in ℕ\right)\to {A}\in ℝ$
11 rexmul ${⊢}\left({n}\in ℝ\wedge {A}\in ℝ\right)\to {n}{\cdot }_{𝑒}{A}={n}{A}$
12 remulcl ${⊢}\left({n}\in ℝ\wedge {A}\in ℝ\right)\to {n}{A}\in ℝ$
13 11 12 eqeltrd ${⊢}\left({n}\in ℝ\wedge {A}\in ℝ\right)\to {n}{\cdot }_{𝑒}{A}\in ℝ$
14 8 10 13 syl2anc ${⊢}\left({A}\in {ℝ}^{+}\wedge {n}\in ℕ\right)\to {n}{\cdot }_{𝑒}{A}\in ℝ$
15 7 14 eqeltrd ${⊢}\left({A}\in {ℝ}^{+}\wedge {n}\in ℕ\right)\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}\in ℝ$
16 ltpnf ${⊢}{n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}\in ℝ\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}<\mathrm{+\infty }$
17 15 16 syl ${⊢}\left({A}\in {ℝ}^{+}\wedge {n}\in ℕ\right)\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}<\mathrm{+\infty }$
18 17 ralrimiva ${⊢}{A}\in {ℝ}^{+}\to \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}<\mathrm{+\infty }$
19 xrsex ${⊢}{ℝ}_{𝑠}^{*}\in \mathrm{V}$
20 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
21 xrsbas ${⊢}{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$
22 xrs0 ${⊢}0={0}_{{ℝ}_{𝑠}^{*}}$
23 eqid ${⊢}{\cdot }_{{ℝ}_{𝑠}^{*}}={\cdot }_{{ℝ}_{𝑠}^{*}}$
24 xrslt ${⊢}<={<}_{{ℝ}_{𝑠}^{*}}$
25 21 22 23 24 isinftm ${⊢}\left({ℝ}_{𝑠}^{*}\in \mathrm{V}\wedge {A}\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({A}⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }↔\left(0<{A}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}<\mathrm{+\infty }\right)\right)$
26 19 20 25 mp3an13 ${⊢}{A}\in {ℝ}^{*}\to \left({A}⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }↔\left(0<{A}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}<\mathrm{+\infty }\right)\right)$
27 4 26 syl ${⊢}{A}\in {ℝ}^{+}\to \left({A}⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }↔\left(0<{A}\wedge \forall {n}\in ℕ\phantom{\rule{.4em}{0ex}}{n}{\cdot }_{{ℝ}_{𝑠}^{*}}{A}<\mathrm{+\infty }\right)\right)$
28 1 18 27 mpbir2and ${⊢}{A}\in {ℝ}^{+}\to {A}⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }$