Theorem 0red 8291

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

Syntax hints:   -> wi 4   e. wcel 2205   RRcr 8142   0cc0 8143

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2227  df-clel 2230  df-ral 2527  df-rex 2528

This theorem is referenced by:  gt0ne0  8718  add20  8765  subge0  8766  lesub0  8770  addgt0d  8812  sublt0d  8861  gt0add  8864  apreap  8878  gt0ap0  8917  ap0gt0  8931  lt0ap0  8939  prodgt0  9143  prodge0  9145  lt2msq1  9176  lediv12a  9185  ledivp1  9194  squeeze0  9195  mulle0r  9235  nn2ge  9287  0mnnnnn0  9545  elnn0z  9607  nn0negleid  9663  rpgecl  10033  ge0p1rp  10036  ledivge1le  10077  mul2lt0rlt0  10110  mul2lt0rgt0  10111  mul2lt0np  10114  iccf1o  10357  elfz1b  10446  elfz0fzfz0  10482  fz0fzelfz0  10483  fzo1fzo0n0  10544  elfzo0z  10545  fzofzim  10549  elfzodifsumelfzo  10568  btwnzge0  10684  modqid  10735  mulqaddmodid  10750  mulp1mod1  10751  modqltm1p1mod  10762  addmodlteq  10784  expgt1  10963  ltexp2a  10977  leexp2a  10978  expnbnd  11050  expnlbnd2  11052  zzlesq  11095  nn0ltexp2  11096  expcanlem  11102  expcan  11103  bcm1n  11156  ssenneg  11229  sshashneg  11230  iswrdiz  11256  ccat2s1fvwd  11360  swrdswrdlem  11421  swrdswrd  11422  resqrexlemcalc3  11726  resqrexlemnm  11728  resqrexlemgt0  11730  sqrtgt0  11744  abs00ap  11772  leabs  11784  ltabs  11797  abslt  11798  absle  11799  absgt0ap  11809  rpmaxcl  11933  nn0maxcl  11935  rpmincl  11948  mul0inf  11951  reccn2ap  12023  climge0  12035  fsumrecl  12112  isumlessdc  12207  divcnv  12208  expcnvre  12214  absltap  12220  geolim2  12223  georeclim  12224  geoisumr  12229  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemabsle  12238  mertenslem2  12247  cos12dec  12479  p1modz1  12505  dvdslelemd  12554  oddge22np1  12592  divalglemnn  12629  divalglemeuneg  12634  bitsfzolem  12665  bitsinv1lem  12672  lcmgcdlem  12799  dvdsnprmd  12847  isprm5lem  12863  sqrt2irraplemnn  12901  sqrt2irrap  12902  qnumgt0  12920  qexpz  13075  4sqlem6  13106  ballotfilemonn  13165  ballotfilemfc0  13176  ballotfilemfcc  13177  znnen  13233  ennnfoneleminc  13246  exmidunben  13261  mulcncflem  15598  hovercncf  15637  hovera  15638  hoverb  15639  hoverlt1  15640  hovergt0  15641  ivthdichlem  15642  dich0  15643  cosz12  15771  cos02pilt1  15842  ioocosf1o  15845  rplogcl  15870  cxplt  15907  cxple  15908  ltexp2  15932  mersenne  15991  lgsdilem  16026  gausslemma2dlem1a  16057  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  refeq  16934  trilpolemeq1  16950  trilpolemlt1  16951  ltlenmkv  16982