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 \mathbb{N}\to n\in \mathbb{Z}$$
3	2	adantl	$$⊢\left(A\in {ℝ}^{+}\wedge n\in \mathbb{N}\right)\to n\in \mathbb{Z}$$
4		rpxr	$$⊢A\in {ℝ}^{+}\to A\in {ℝ}^{*}$$
5	4	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge n\in \mathbb{N}\right)\to A\in {ℝ}^{*}$$
6		xrsmulgzz	$$⊢\left(n\in \mathbb{Z}\wedge A\in {ℝ}^{*}\right)\to n{\cdot }_{{ℝ}_{𝑠}^{*}}A=n{\cdot }_{𝑒}A$$
7	3 5 6	syl2anc	$$⊢\left(A\in {ℝ}^{+}\wedge n\in \mathbb{N}\right)\to n{\cdot }_{{ℝ}_{𝑠}^{*}}A=n{\cdot }_{𝑒}A$$
8	3	zred	$$⊢\left(A\in {ℝ}^{+}\wedge n\in \mathbb{N}\right)\to n\in ℝ$$
9		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
10	9	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge n\in \mathbb{N}\right)\to A\in ℝ$$
11		rexmul	$$⊢\left(n\in ℝ\wedge A\in ℝ\right)\to n{\cdot }_{𝑒}A=nA$$
12		remulcl	$$⊢\left(n\in ℝ\wedge A\in ℝ\right)\to nA\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 \mathbb{N}\right)\to n{\cdot }_{𝑒}A\in ℝ$$
15	7 14	eqeltrd	$$⊢\left(A\in {ℝ}^{+}\wedge n\in \mathbb{N}\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 \mathbb{N}\right)\to n{\cdot }_{{ℝ}_{𝑠}^{*}}A<\mathrm{+\infty }$$
18	17	ralrimiva	$$⊢A\in {ℝ}^{+}\to \forall n\in \mathbb{N}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 }\leftrightarrow \left(0<A\wedge \forall n\in \mathbb{N}n{\cdot }_{{ℝ}_{𝑠}^{*}}A<\mathrm{+\infty }\right)\right)$$
26	19 20 25	mp3an13	$$⊢A\in {ℝ}^{*}\to \left(A⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }\leftrightarrow \left(0<A\wedge \forall n\in \mathbb{N}n{\cdot }_{{ℝ}_{𝑠}^{*}}A<\mathrm{+\infty }\right)\right)$$
27	4 26	syl	$$⊢A\in {ℝ}^{+}\to \left(A⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }\leftrightarrow \left(0<A\wedge \forall n\in \mathbb{N}n{\cdot }_{{ℝ}_{𝑠}^{*}}A<\mathrm{+\infty }\right)\right)$$
28	1 18 27	mpbir2and	$$⊢A\in {ℝ}^{+}\to A⋘\left({ℝ}_{𝑠}^{*}\right)\mathrm{+\infty }$$