Theorem 0xr 11286

Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)

Assertion

Ref	Expression
0xr	⊢ 0 ∈ ℝ*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 11283	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11241	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3976	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2099  ℝcr 11132  0cc0 11133  ℝ^*cxr 11272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-1cn 11191  ax-addrcl 11194  ax-rnegex 11204  ax-cnre 11206

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rex 3067  df-v 3472  df-un 3950  df-in 3952  df-ss 3962  df-xr 11277

This theorem is referenced by:  0lepnf  13139  ge0gtmnf  13178  max0sub  13202  xlt0neg1  13225  xlt0neg2  13226  xle0neg1  13227  xle0neg2  13228  xaddf  13230  xaddrid  13247  xaddlid  13248  xnn0xadd0  13253  xaddge0  13264  xsubge0  13267  xposdif  13268  xmullem  13270  xmullem2  13271  xmul01  13273  xmul02  13274  xmulneg1  13275  xmulf  13278  xmulpnf1  13280  xmulasslem2  13288  xmulge0  13290  xmulasslem  13291  xlemul1a  13294  xadddi  13301  xadddi2  13303  dfrp2  13400  ioopos  13428  ioorebas  13455  xrge0neqmnf  13456  elxrge0  13461  0e0iccpnf  13463  xov1plusxeqvd  13502  xnn0xrge0  13510  ico01fl0  13811  rpsup  13858  addmodid  13911  hashgt0  14374  hashle00  14386  hashgt0elex  14387  hashgt23el  14410  sgn0  15063  sgnp  15064  sgnn  15068  fprodge0  15964  ef01bndlem  16155  sin01bnd  16156  cos01bnd  16157  cos1bnd  16158  sinltx  16160  sin01gt0  16161  cos01gt0  16162  sin02gt0  16163  sincos1sgn  16164  sincos2sgn  16165  halfleoddlt  16333  xrsmgm  21328  leordtval2  23110  pnfnei  23118  mnfnei  23119  psmetge0  24212  isxmet2d  24227  xmetge0  24244  xmetgt0  24258  prdsdsf  24267  prdsxmetlem  24268  xpsdsval  24281  blgt0  24299  xblss2ps  24301  xblss2  24302  xbln0  24314  prdsbl  24394  stdbdxmet  24418  stdbdmopn  24421  metustto  24456  metustid  24457  metustexhalf  24459  cfilucfil  24462  blval2  24465  metuel2  24468  nmoge0  24632  nmo0  24646  cnblcld  24685  blssioo  24705  blcvx  24708  xrsxmet  24719  metdsf  24758  metds0  24760  metdseq0  24764  metnrmlem1a  24768  iccpnfcnv  24863  iccpnfhmeo  24864  xrhmeo  24865  pcoass  24945  iscfil2  25188  ovolmge0  25400  ovolge0  25404  ovolf  25405  ovolssnul  25410  ovolctb  25413  ovoliunnul  25430  ovolicopnf  25447  voliunlem3  25475  volsup  25479  ioorf  25496  volivth  25530  vitalilem4  25534  vitalilem5  25535  itg2ge0  25659  itg2const2  25665  itg2seq  25666  itg2monolem1  25674  itg2monolem2  25675  itg2monolem3  25676  itg2gt0  25684  dvne0  25938  mdegle0  26007  ply1remlem  26093  ply1rem  26094  idomrootle  26101  plypf1  26140  aaliou3lem2  26272  aaliou3lem3  26273  taylfvallem1  26285  taylfval  26287  tayl0  26290  radcnvcl  26347  radcnvle  26350  pserulm  26352  psercnlem1  26356  pilem2  26383  sinhalfpilem  26392  sincosq1lem  26426  sincosq1sgn  26427  sincosq2sgn  26428  tangtx  26434  tanabsge  26435  sinq12gt0  26436  cosq14gt0  26439  sincos4thpi  26442  pige3ALT  26448  cos02pilt1  26454  cosq34lt1  26455  cosordlem  26458  cos0pilt1  26460  tanord1  26465  tanord  26466  efifo  26475  argimgt0  26540  argimlt0  26541  logccv  26591  loglesqrt  26687  atantan  26849  rlimcnp  26891  rlimcnp2  26892  scvxcvx  26912  basellem1  27007  dchrisum0lem2a  27444  pntibndlem1  27516  pntibnd  27520  pntlemc  27522  pntlem3  27536  abvcxp  27542  padicabvf  27558  padicabvcxp  27559  ostth2  27564  ttgcontlem1  28689  elntg2  28790  nmooge0  30571  nmoo0  30595  nmlnogt0  30601  nmopge0  31715  nmopgt0  31716  nmfnge0  31731  nmop0  31790  nmfn0  31791  xraddge02  32521  xlt2addrd  32523  xrge0infss  32525  elxrge02  32650  xrs0  32728  xrge00  32737  xrge0addass  32741  xrge0addgt0  32742  xrge0adddir  32743  fsumrp0cl  32746  ply1unit  33250  metider  33490  unitssxrge0  33496  xrge0iifcnv  33529  xrge0iifcv  33530  xrge0iifiso  33531  xrge0iifhom  33533  xrge0mulc1cn  33537  pnfneige0  33547  lmxrge0  33548  esumgsum  33659  esumnul  33662  esum0  33663  esumle  33672  esumlef  33676  esumcst  33677  esumsnf  33678  esumpr2  33681  esumpinfval  33687  esumpinfsum  33691  esumpcvgval  33692  esumpmono  33693  hashf2  33698  esumcvg  33700  measle0  33822  voliune  33843  volfiniune  33844  ddemeas  33850  aean  33858  oms0  33912  prob01  34028  probmeasb  34045  dstfrvclim1  34092  sgncl  34153  sgn3da  34156  signsply0  34178  chtvalz  34256  hgt750lemf  34280  cvmliftlem10  34899  cvmliftlem13  34901  sinccvglem  35271  dnizeq0  35945  iccioo01  36801  sin2h  37078  tan2h  37080  broucube  37122  mblfinlem2  37126  ovoliunnfl  37130  voliunnfl  37132  volsupnfl  37133  mbfposadd  37135  itg2addnclem2  37140  itg2gt0cn  37143  ftc1anclem5  37165  ftc1anclem8  37168  dvasin  37172  areacirc  37181  rrnequiv  37303  dvrelog2b  41532  aks6d1c5lem3  41603  aks6d1c6lem1  41637  acos1half  42088  imo72b2  43593  absfico  44582  xadd0ge  44693  xrge0nemnfd  44705  xralrple2  44727  xrpnf  44859  pnfel0pnf  44904  ge0xrre  44907  sqrlearg  44929  fsumge0cl  44952  limsup10ex  45152  liminf10ex  45153  sinaover2ne0  45247  itgsin0pilem1  45329  iblsplit  45345  stoweidlem46  45425  fourierdlem43  45529  fourierdlem44  45530  fourierdlem60  45545  fourierdlem61  45546  fourierdlem87  45572  fourierdlem103  45588  fourierdlem104  45589  fourierdlem111  45596  sqwvfourb  45608  fourierswlem  45609  fouriersw  45610  etransclem23  45636  salexct2  45718  fge0npnf  45746  fge0iccico  45749  gsumge0cl  45750  sge0z  45754  sge00  45755  sge0sn  45758  sge0tsms  45759  sge0cl  45760  sge0f1o  45761  sge0ge0  45763  sge0repnf  45765  sge0fsum  45766  sge0pr  45773  sge0ssre  45776  sge0prle  45780  sge0p1  45793  sge0iunmptlemre  45794  sge0rpcpnf  45800  sge0rernmpt  45801  sge0isum  45806  sge0ad2en  45810  sge0xaddlem2  45813  sge0uzfsumgt  45823  sge0seq  45825  sge0reuz  45826  voliunsge0lem  45851  meage0  45854  meassre  45856  meale0eq0  45857  meaiuninclem  45859  omessre  45889  omeiunltfirp  45898  carageniuncllem2  45901  carageniuncl  45902  omege0  45912  omess0  45913  hoiprodcl  45926  ovnlerp  45941  ovnf  45942  ovn0lem  45944  ovnsubaddlem1  45949  hoiprodcl3  45959  hoidmvcl  45961  hoidmv1lelem3  45972  hoidmvlelem5  45978  ovnhoilem1  45980  ovolval5lem1  46031  pimrecltneg  46103  mod42tp1mod8  46933  eenglngeehlnmlem1  47801  eenglngeehlnmlem2  47802  rrxsphere  47812  itscnhlinecirc02p  47849  iooii  47927  io1ii  47930  sepfsepc  47937  seppcld  47939

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »