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