Theorem 0red 8328

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8179   0cc0 8180

This proof depends on 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 8274  ax-addrcl 8277  ax-rnegex 8289

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

This theorem is used by:  gt0ne0  8757  add20  8804  subge0  8805  lesub0  8809  addgt0d  8851  sublt0d  8901  gt0add  8904  apreap  8918  gt0ap0  8957  ap0gt0  8971  lt0ap0  8979  prodgt0  9185  prodge0  9187  lt2msq1  9218  lediv12a  9227  ledivp1  9236  squeeze0  9237  mulle0r  9277  indfdc  9301  nn2ge  9340  0mnnnnn0  9600  elnn0z  9662  nn0negleid  9718  rpgecl  10094  ge0p1rp  10097  ledivge1le  10138  mul2lt0rlt0  10171  mul2lt0rgt0  10172  mul2lt0np  10175  iccf1o  10418  elfz1b  10508  elfz0fzfz0  10544  fz0fzelfz0  10545  fzo1fzo0n0  10606  elfzo0z  10607  fzofzim  10611  elfzodifsumelfzo  10630  btwnzge0  10750  modqid  10801  mulqaddmodid  10816  mulp1mod1  10817  modqltm1p1mod  10828  addmodlteq  10850  expgt1  11029  ltexp2a  11043  leexp2a  11044  expnbnd  11116  expnlbnd2  11118  zzlesq  11161  nn0ltexp2  11163  expcanlem  11169  expcan  11170  bcm1n  11223  ssenneg  11296  sshashneg  11297  iswrdiz  11327  ccat2s1fvwd  11431  swrdswrdlem  11492  swrdswrd  11493  sq01  11676  resqrexlemcalc3  11798  resqrexlemnm  11800  resqrexlemgt0  11802  sqrtgt0  11816  abs00ap  11844  leabs  11856  ltabs  11870  abslt  11871  absle  11872  absgt0ap  11882  rpmaxcl  12006  nn0maxcl  12008  rpmincl  12022  mul0inf  12026  reccn2ap  12098  climge0  12110  fsumrecl  12187  isumlessdc  12282  divcnv  12283  expcnvre  12289  absltap  12295  geolim2  12298  georeclim  12299  geoisumr  12304  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  cvgratnnlemabsle  12313  mertenslem2  12322  cos12dec  12554  p1modz1  12580  dvdslelemd  12629  oddge22np1  12667  divalglemnn  12704  divalglemeuneg  12709  bitsfzolem  12740  bitsinv1lem  12747  lcmgcdlem  12874  dvdsnprmd  12922  isprm5lem  12939  sqrt2irraplemnn  12978  sqrt2irrap  12979  qnumgt0  12997  sqrtrirr  13008  qexpz  13154  4sqlem6  13185  ballotfilemonn  13273  ballotfilemfc0  13284  ballotfilemfcc  13285  znnen  13341  ennnfoneleminc  13354  exmidunben  13369  mulcncflem  15799  hovercncf  15838  hovera  15839  hoverb  15840  hoverlt1  15841  hovergt0  15842  ivthdichlem  15843  dich0  15844  cosz12  15973  cos02pilt1  16044  ioocosf1o  16047  rplogcl  16073  logdivlt  16088  logdivle  16089  cxplt  16113  cxple  16114  ltexp2  16138  ppiqfi  16203  chtqwordi  16224  ppiqwordi  16229  chtqrpcl  16240  ppiqltx  16242  mersenne  16258  bposlem1  16272  lgsdilem  16312  gausslemma2dlem1a  16343  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  dichmul0orlem1  16919  dichmul0orlem5  16923  dichmul0orlem6  16924  refeq  17239  trilpolemeq1  17256  trilpolemlt1  17257  ltlenmkv  17287