Theorem 0red 8170

Description: 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
0red	|- ( ph -> 0 e. RR )

Proof of Theorem 0red

Step	Hyp	Ref	Expression
1		0re 8169	. 2 |- 0 e. RR
2	1	a1i 9	1 |- ( ph -> 0 e. RR )

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 8021   0cc0 8022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8116  ax-addrcl 8119  ax-rnegex 8131

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-ral 2513  df-rex 2514

This theorem is referenced by:  gt0ne0  8597  add20  8644  subge0  8645  lesub0  8649  addgt0d  8691  sublt0d  8740  gt0add  8743  apreap  8757  gt0ap0  8796  ap0gt0  8810  lt0ap0  8818  prodgt0  9022  prodge0  9024  lt2msq1  9055  lediv12a  9064  ledivp1  9073  squeeze0  9074  mulle0r  9114  nn2ge  9166  0mnnnnn0  9424  elnn0z  9482  nn0negleid  9538  rpgecl  9907  ge0p1rp  9910  ledivge1le  9951  mul2lt0rlt0  9984  mul2lt0rgt0  9985  mul2lt0np  9988  iccf1o  10229  elfz1b  10315  elfz0fzfz0  10351  fz0fzelfz0  10352  fzo1fzo0n0  10412  elfzo0z  10413  fzofzim  10417  elfzodifsumelfzo  10436  btwnzge0  10550  modqid  10601  mulqaddmodid  10616  mulp1mod1  10617  modqltm1p1mod  10628  addmodlteq  10650  expgt1  10829  ltexp2a  10843  leexp2a  10844  expnbnd  10915  expnlbnd2  10917  zzlesq  10960  nn0ltexp2  10961  expcanlem  10967  expcan  10968  iswrdiz  11110  ccat2s1fvwd  11214  swrdswrdlem  11275  swrdswrd  11276  resqrexlemcalc3  11567  resqrexlemnm  11569  resqrexlemgt0  11571  sqrtgt0  11585  abs00ap  11613  leabs  11625  ltabs  11638  abslt  11639  absle  11640  absgt0ap  11650  rpmaxcl  11774  nn0maxcl  11776  rpmincl  11789  mul0inf  11792  reccn2ap  11864  climge0  11876  fsumrecl  11952  isumlessdc  12047  divcnv  12048  expcnvre  12054  absltap  12060  geolim2  12063  georeclim  12064  geoisumr  12069  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemabsle  12078  mertenslem2  12087  cos12dec  12319  p1modz1  12345  dvdslelemd  12394  oddge22np1  12432  divalglemnn  12469  divalglemeuneg  12474  bitsfzolem  12505  bitsinv1lem  12512  lcmgcdlem  12639  dvdsnprmd  12687  isprm5lem  12703  sqrt2irraplemnn  12741  sqrt2irrap  12742  qnumgt0  12760  qexpz  12915  4sqlem6  12946  znnen  13009  ennnfoneleminc  13022  exmidunben  13037  mulcncflem  15321  hovercncf  15360  hovera  15361  hoverb  15362  hoverlt1  15363  hovergt0  15364  ivthdichlem  15365  dich0  15366  cosz12  15494  cos02pilt1  15565  ioocosf1o  15568  rplogcl  15593  cxplt  15630  cxple  15631  ltexp2  15655  mersenne  15711  lgsdilem  15746  gausslemma2dlem1a  15777  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  refeq  16568  trilpolemeq1  16580  trilpolemlt1  16581  ltlenmkv  16610