Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pnfinf Structured version   Visualization version   Unicode version

Theorem pnfinf 28512
 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.)
Assertion
Ref Expression
pnfinf <<<

Proof of Theorem pnfinf
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rpgt0 11320 . 2
2 nnz 10966 . . . . . . 7
32adantl 468 . . . . . 6
4 rpxr 11316 . . . . . . 7
54adantr 467 . . . . . 6
6 xrsmulgzz 28452 . . . . . 6 .g
73, 5, 6syl2anc 667 . . . . 5 .g
83zred 11047 . . . . . 6
9 rpre 11315 . . . . . . 7
109adantr 467 . . . . . 6
11 rexmul 11564 . . . . . . 7
12 remulcl 9629 . . . . . . 7
1311, 12eqeltrd 2531 . . . . . 6
148, 10, 13syl2anc 667 . . . . 5
157, 14eqeltrd 2531 . . . 4 .g
16 ltpnf 11429 . . . 4 .g .g
1715, 16syl 17 . . 3 .g
1817ralrimiva 2804 . 2 .g
19 xrsex 18995 . . . 4
20 pnfxr 11419 . . . 4
21 xrsbas 18996 . . . . 5
22 xrs0 28449 . . . . 5
23 eqid 2453 . . . . 5 .g .g
24 xrslt 28450 . . . . 5
2521, 22, 23, 24isinftm 28510 . . . 4 <<< .g
2619, 20, 25mp3an13 1357 . . 3 <<< .g
274, 26syl 17 . 2 <<< .g
281, 18, 27mpbir2and 934 1 <<<
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1446   wcel 1889  wral 2739  cvv 3047   class class class wbr 4405  cfv 5585  (class class class)co 6295  cr 9543  cc0 9544   cmul 9549   cpnf 9677  cxr 9679   clt 9680  cn 10616  cz 10944  crp 11309  cxmu 11415  cxrs 15410  .gcmg 16684  <<
 Copyright terms: Public domain W3C validator