Theorem 0red 8317

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 8316	. 2 |- 0 e. RR
2	1	a1i 9	1 |- ( ph -> 0 e. RR )

Syntax hints:   -> wi 4   e. wcel 2209   RRcr 8168   0cc0 8169

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8263  ax-addrcl 8266  ax-rnegex 8278

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-ral 2533  df-rex 2534

This theorem is referenced by:  gt0ne0  8745  add20  8792  subge0  8793  lesub0  8797  addgt0d  8839  sublt0d  8888  gt0add  8891  apreap  8905  gt0ap0  8944  ap0gt0  8958  lt0ap0  8966  prodgt0  9172  prodge0  9174  lt2msq1  9205  lediv12a  9214  ledivp1  9223  squeeze0  9224  mulle0r  9264  nn2ge  9316  0mnnnnn0  9574  elnn0z  9636  nn0negleid  9692  rpgecl  10062  ge0p1rp  10065  ledivge1le  10106  mul2lt0rlt0  10139  mul2lt0rgt0  10140  mul2lt0np  10143  iccf1o  10386  elfz1b  10475  elfz0fzfz0  10511  fz0fzelfz0  10512  fzo1fzo0n0  10573  elfzo0z  10574  fzofzim  10578  elfzodifsumelfzo  10597  btwnzge0  10713  modqid  10764  mulqaddmodid  10779  mulp1mod1  10780  modqltm1p1mod  10791  addmodlteq  10813  expgt1  10992  ltexp2a  11006  leexp2a  11007  expnbnd  11079  expnlbnd2  11081  zzlesq  11124  nn0ltexp2  11125  expcanlem  11131  expcan  11132  bcm1n  11185  ssenneg  11258  sshashneg  11259  iswrdiz  11289  ccat2s1fvwd  11393  swrdswrdlem  11454  swrdswrd  11455  sq01  11638  resqrexlemcalc3  11760  resqrexlemnm  11762  resqrexlemgt0  11764  sqrtgt0  11778  abs00ap  11806  leabs  11818  ltabs  11831  abslt  11832  absle  11833  absgt0ap  11843  rpmaxcl  11967  nn0maxcl  11969  rpmincl  11982  mul0inf  11985  reccn2ap  12057  climge0  12069  fsumrecl  12146  isumlessdc  12241  divcnv  12242  expcnvre  12248  absltap  12254  geolim2  12257  georeclim  12258  geoisumr  12263  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratnnlemabsle  12272  mertenslem2  12281  cos12dec  12513  p1modz1  12539  dvdslelemd  12588  oddge22np1  12626  divalglemnn  12663  divalglemeuneg  12668  bitsfzolem  12699  bitsinv1lem  12706  lcmgcdlem  12833  dvdsnprmd  12881  isprm5lem  12897  sqrt2irraplemnn  12935  sqrt2irrap  12936  qnumgt0  12954  qexpz  13109  4sqlem6  13140  ballotfilemonn  13199  ballotfilemfc0  13210  ballotfilemfcc  13211  znnen  13267  ennnfoneleminc  13280  exmidunben  13295  mulcncflem  15631  hovercncf  15670  hovera  15671  hoverb  15672  hoverlt1  15673  hovergt0  15674  ivthdichlem  15675  dich0  15676  cosz12  15804  cos02pilt1  15875  ioocosf1o  15878  rplogcl  15903  cxplt  15941  cxple  15942  ltexp2  15966  mersenne  16025  lgsdilem  16060  gausslemma2dlem1a  16091  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  dichmul0orlem1  16667  dichmul0orlem5  16671  dichmul0orlem6  16672  refeq  16978  trilpolemeq1  16994  trilpolemlt1  16995  ltlenmkv  17025