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 = ( 0_g ‘ ℝ^*_𝑠 )
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	⊢ ( 𝐴 ∈ ℝ⁺ → 𝐴 ( ⋘ ‘ ℝ^*_𝑠 ) +∞ )

Metamath Proof Explorer

Theorem pnfinf

Proof