HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem xrre 9378
Description: A way of proving that an extended real is real.
Assertion
Ref Expression
xrre

Proof of Theorem xrre
StepHypRef Expression
1 simprl 711 . 2
2 ltpnf 9350 . . . . . 6
32adantl 445 . . . . 5
4 rexr 8187 . . . . . 6
5 pnfxr 9344 . . . . . . 7
6 xrlelttr 9371 . . . . . . 7
75, 6mp3an3 1229 . . . . . 6
84, 7sylan2 453 . . . . 5
93, 8mpan2d 650 . . . 4
109imp 414 . . 3
1110adantrl 690 . 2
12 xrrebnd 9377 . . 3
1312ad2antrr 700 . 2
141, 11, 13mpbir2and 848 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 174   wa 357   wcel 1533   class class class wbr 3591  cr 8060   cle 8174   cpnf 8175   cmnf 8176  cxr 8177   clt 8178
This theorem is referenced by:  supxrre  9430  infmxrre  9438  caucvglem  10483  pcgcd1  11127  tgioo  14377  ovollecl  14670  ovolunlem1a  14683  ovoliunlem1  14689  ioombl1lem2  14744  itg2lecl  14921  itg2monolem2  14934  dvferm1lem  15129  radcnvle  15511  psercnlem1  15516  nmobndi  16691  ubthlem3  16789  nmophmi  17950  bdophsi  18015  bdopcoi  18017
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049  ax-cnex 8116  ax-resscn 8117  ax-pre-lttri 8134  ax-pre-lttrn 8135
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-tru 1264  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-nel 2210  df-ral 2303  df-rex 2304  df-rab 2306  df-v 2502  df-sbc 2669  df-csb 2751  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-op 3277  df-uni 3435  df-br 3592  df-opab 3645  df-id 3848  df-po 3853  df-so 3854  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-mpt 5461  df-er 6076  df-en 6249  df-dom 6250  df-sdom 6251  df-pnf 8179  df-mnf 8180  df-xr 8181  df-ltxr 8182  df-le 8183
Copyright terms: Public domain