# 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 ( 𝐴 ∈ ℝ+𝐴 ( ⋘ ‘ ℝ*𝑠 ) +∞ )

### Proof

Step Hyp Ref Expression
1 rpgt0 ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
2 nnz ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
3 2 adantl ( ( 𝐴 ∈ ℝ+𝑛 ∈ ℕ ) → 𝑛 ∈ ℤ )
4 rpxr ( 𝐴 ∈ ℝ+𝐴 ∈ ℝ* )
5 4 adantr ( ( 𝐴 ∈ ℝ+𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ* )
6 xrsmulgzz ( ( 𝑛 ∈ ℤ ∧ 𝐴 ∈ ℝ* ) → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) = ( 𝑛 ·e 𝐴 ) )
7 3 5 6 syl2anc ( ( 𝐴 ∈ ℝ+𝑛 ∈ ℕ ) → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) = ( 𝑛 ·e 𝐴 ) )
8 3 zred ( ( 𝐴 ∈ ℝ+𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ )
9 rpre ( 𝐴 ∈ ℝ+𝐴 ∈ ℝ )
10 9 adantr ( ( 𝐴 ∈ ℝ+𝑛 ∈ ℕ ) → 𝐴 ∈ ℝ )
11 rexmul ( ( 𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑛 ·e 𝐴 ) = ( 𝑛 · 𝐴 ) )
12 remulcl ( ( 𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑛 · 𝐴 ) ∈ ℝ )
13 11 12 eqeltrd ( ( 𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑛 ·e 𝐴 ) ∈ ℝ )
14 8 10 13 syl2anc ( ( 𝐴 ∈ ℝ+𝑛 ∈ ℕ ) → ( 𝑛 ·e 𝐴 ) ∈ ℝ )
15 7 14 eqeltrd ( ( 𝐴 ∈ ℝ+𝑛 ∈ ℕ ) → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) ∈ ℝ )
16 ltpnf ( ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) ∈ ℝ → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) < +∞ )
17 15 16 syl ( ( 𝐴 ∈ ℝ+𝑛 ∈ ℕ ) → ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) < +∞ )
18 17 ralrimiva ( 𝐴 ∈ ℝ+ → ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) < +∞ )
19 xrsex *𝑠 ∈ V
20 pnfxr +∞ ∈ ℝ*
21 xrsbas * = ( Base ‘ ℝ*𝑠 )
22 xrs0 0 = ( 0g ‘ ℝ*𝑠 )
23 eqid ( .g ‘ ℝ*𝑠 ) = ( .g ‘ ℝ*𝑠 )
24 xrslt < = ( lt ‘ ℝ*𝑠 )
25 21 22 23 24 isinftm ( ( ℝ*𝑠 ∈ V ∧ 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 ( ⋘ ‘ ℝ*𝑠 ) +∞ ↔ ( 0 < 𝐴 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) < +∞ ) ) )
26 19 20 25 mp3an13 ( 𝐴 ∈ ℝ* → ( 𝐴 ( ⋘ ‘ ℝ*𝑠 ) +∞ ↔ ( 0 < 𝐴 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) < +∞ ) ) )
27 4 26 syl ( 𝐴 ∈ ℝ+ → ( 𝐴 ( ⋘ ‘ ℝ*𝑠 ) +∞ ↔ ( 0 < 𝐴 ∧ ∀ 𝑛 ∈ ℕ ( 𝑛 ( .g ‘ ℝ*𝑠 ) 𝐴 ) < +∞ ) ) )
28 1 18 27 mpbir2and ( 𝐴 ∈ ℝ+𝐴 ( ⋘ ‘ ℝ*𝑠 ) +∞ )