MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0red Unicode version

Theorem 0red 9379
Description: is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
0red

Proof of Theorem 0red
StepHypRef Expression
1 0re 9378 . 2
21a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1756   cr 9273  0cc0 9274
This theorem is referenced by:  gt0ne0  9796  add20  9843  subge0  9844  lesub0  9848  mulge0  9849  msqgt0  9852  msqge0  9853  addgt0d  9906  prodgt0  10166  prodge0  10168  lt2msq1  10207  supmul1  10287  supmul  10290  0mnnnnn0  10604  rpgecl  11008  ge0p1rp  11011  max0sub  11158  iccf1o  11421  xov1plusxeqvd  11423  elfz0fzfz0  11477  fz0fzelfz0  11478  elfz1b  11519  fzo1fzo0n0  11580  elfzo0z  11581  fzofzim  11585  elfzodifsumelfzo  11596  ssfzoulel  11613  elfznelfzo  11622  modltm1p1mod  11743  expgt1  11894  ltexp2a  11907  expcan  11908  ltexp2  11909  leexp2  11910  leexp2a  11911  expnlbnd2  11987  discr  11993  brfi1uzind  12211  ccatsymb  12273  swrdnd  12318  swrdvalodm2  12325  swrdswrdlem  12345  swrdswrd  12346  swrdccatin2  12370  swrdccatin12lem3  12373  repswswrd  12414  swrd2lsw  12544  2swrd2eqwrdeq  12545  leabs  12780  max0add  12791  absgt0  12804  rlimrege0  13049  iseraltlem2  13152  fsumrecl  13203  o1fsum  13268  cvgcmp  13271  cvgcmpce  13273  geomulcvg  13328  mertenslem2  13337  rpnnen2lem4  13492  moddvds  13534  bitsfzolem  13622  bitsinv1lem  13629  sadcaddlem  13645  qnumgt0  13820  modprm0  13865  qexpz  13955  prmreclem4  13972  4sqlem6  13996  gzrngunit  17858  regsumsupp  18032  prdsmet  19925  metustexhalf  20119  nlmvscnlem2  20246  nlmvscnlem1  20247  nmo0  20294  evth  20511  lebnumlem1  20513  lebnumii  20518  htpycc  20532  pcohtpylem  20571  pcoass  20576  pcorevlem  20578  nmoleub2lem3  20650  ipcnlem2  20736  ipcnlem1  20737  rrxcph  20876  rrxmetlem  20886  rrxmet  20887  rrxdstprj1  20888  ehlbase  20890  minveclem3b  20895  minveclem6  20901  pjthlem1  20904  ovolicopnf  20987  ioorcl2  21032  volivth  21067  mbfposr  21110  i1fmulc  21161  itg1mulc  21162  itg1ge0a  21169  mbfi1flim  21181  itg2split  21207  itg2monolem1  21208  itg2monolem3  21210  itg2mono  21211  itgge0  21268  dvlip  21445  dvlipcn  21446  dveq0  21452  dv11cn  21453  dvlt0  21457  dvfsumge  21474  dgradd2  21715  plydivlem3  21741  mtest  21849  radcnvlem1  21858  radcnv0  21861  radcnvlt1  21863  radcnvle  21865  pserulm  21867  pserdvlem1  21872  pserdv  21874  abelthlem2  21877  abelthlem7  21883  pilem2  21897  coseq00topi  21944  tanabsge  21948  tanord1  21973  tanord  21974  logne0  22031  rplogcl  22033  logdivle  22051  logcnlem3  22069  logcnlem4  22070  dvloglem  22073  logtayl  22085  abscxp2  22118  cxplt  22119  cxple  22120  cxple2a  22124  cxpcn3lem  22165  abscxpbnd  22171  chordthmlem5  22211  asinlem3  22246  atanre  22260  atanlogaddlem  22288  atanlogadd  22289  atanlogsublem  22290  atantan  22298  atans2  22306  cxp2limlem  22349  cxp2lim  22350  cxploglim2  22352  divsqrsumlem  22353  jensenlem2  22361  harmonicubnd  22383  fsumharmonic  22385  ftalem1  22390  ftalem2  22391  ftalem5  22394  vmacl  22436  chtwordi  22474  ppiwordi  22480  chtrpcl  22493  fsumfldivdiaglem  22509  fsumvma2  22533  chpval2  22537  chpchtsum  22538  chpub  22539  logfacbnd3  22542  logexprlim  22544  mersenne  22546  lgslem4  22618  lgsdilem  22641  lgsne0  22652  lgseisen  22672  lgsquadlem1  22673  lgsquadlem2  22674  chebbnd1lem2  22699  chebbnd1lem3  22700  chebbnd1  22701  chtppilimlem1  22702  chtppilimlem2  22703  chtppilim  22704  chebbnd2  22706  chto1lb  22707  chpchtlim  22708  chpo1ub  22709  dchrisumlema  22717  dchrisumlem2  22719  dchrisumlem3  22720  dchrmusumlema  22722  dchrvmasumlem2  22727  dchrvmasumiflem1  22730  dchrisum0flblem1  22737  dchrisum0flblem2  22738  dchrisum0re  22742  dchrisum0lema  22743  dchrisum0  22749  dirith2  22757  mulog2sumlem1  22763  vmalogdivsum2  22767  log2sumbnd  22773  selberg2lem  22779  chpdifbndlem1  22782  chpdifbndlem2  22783  chpdifbnd  22784  selberg3lem1  22786  pntrmax  22793  pntrsumo1  22794  pntrlog2bndlem4  22809  pntrlog2bndlem5  22810  pntpbnd1a  22814  pntpbnd1  22815  pntpbnd2  22816  pntlemg  22827  pntlemj  22832  pntlemk  22835  pntlem3  22838  pntleml  22840  pnt2  22842  pnt  22843  ostth2lem1  22847  padicabv  22859  padicabvcxp  22861  ostth2lem3  22864  ostth2lem4  22865  ostth3  22867  nvnencycllem  23497  minvecolem5  24250  minvecolem6  24251  htthlem  24287  pjhthlem1  24762  eulerpartlemgc  26714  stoweidlem1  29767  stoweidlem7  29773  stoweidlem11  29777  stoweidlem25  29791  stoweidlem26  29792  stoweidlem34  29800  stoweidlem36  29802  stoweidlem41  29807  stoweidlem42  29808  stoweidlem44  29810  stoweidlem45  29811  frgraogt3nreg  30684  friendshipgt3  30685  bj-pinftynminfty  32450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089
  Copyright terms: Public domain W3C validator