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+A𝑠*+∞

Proof

Step Hyp Ref Expression
1 rpgt0 A+0<A
2 nnz nn
3 2 adantl A+nn
4 rpxr A+A*
5 4 adantr A+nA*
6 xrsmulgzz nA*n𝑠*A=n𝑒A
7 3 5 6 syl2anc A+nn𝑠*A=n𝑒A
8 3 zred A+nn
9 rpre A+A
10 9 adantr A+nA
11 rexmul nAn𝑒A=nA
12 remulcl nAnA
13 11 12 eqeltrd nAn𝑒A
14 8 10 13 syl2anc A+nn𝑒A
15 7 14 eqeltrd A+nn𝑠*A
16 ltpnf n𝑠*An𝑠*A<+∞
17 15 16 syl A+nn𝑠*A<+∞
18 17 ralrimiva A+nn𝑠*A<+∞
19 xrsex 𝑠*V
20 pnfxr +∞*
21 xrsbas *=Base𝑠*
22 xrs0 0=0𝑠*
23 eqid 𝑠*=𝑠*
24 xrslt <=<𝑠*
25 21 22 23 24 isinftm 𝑠*VA*+∞*A𝑠*+∞0<Ann𝑠*A<+∞
26 19 20 25 mp3an13 A*A𝑠*+∞0<Ann𝑠*A<+∞
27 4 26 syl A+A𝑠*+∞0<Ann𝑠*A<+∞
28 1 18 27 mpbir2and A+A𝑠*+∞