Theorem 0red 8044

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

Syntax hints:   -> wi 4   e. wcel 2167   RRcr 7895   0cc0 7896

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7990  ax-addrcl 7993  ax-rnegex 8005

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-cleq 2189  df-clel 2192  df-ral 2480  df-rex 2481

This theorem is referenced by:  gt0ne0  8471  add20  8518  subge0  8519  lesub0  8523  addgt0d  8565  sublt0d  8614  gt0add  8617  apreap  8631  gt0ap0  8670  ap0gt0  8684  lt0ap0  8692  prodgt0  8896  prodge0  8898  lt2msq1  8929  lediv12a  8938  ledivp1  8947  squeeze0  8948  mulle0r  8988  nn2ge  9040  0mnnnnn0  9298  elnn0z  9356  nn0negleid  9411  rpgecl  9774  ge0p1rp  9777  ledivge1le  9818  mul2lt0rlt0  9851  mul2lt0rgt0  9852  mul2lt0np  9855  iccf1o  10096  elfz1b  10182  elfz0fzfz0  10218  fz0fzelfz0  10219  fzo1fzo0n0  10276  elfzo0z  10277  fzofzim  10281  elfzodifsumelfzo  10294  btwnzge0  10407  modqid  10458  mulqaddmodid  10473  mulp1mod1  10474  modqltm1p1mod  10485  addmodlteq  10507  expgt1  10686  ltexp2a  10700  leexp2a  10701  expnbnd  10772  expnlbnd2  10774  zzlesq  10817  nn0ltexp2  10818  expcanlem  10824  expcan  10825  iswrdiz  10959  resqrexlemcalc3  11198  resqrexlemnm  11200  resqrexlemgt0  11202  sqrtgt0  11216  abs00ap  11244  leabs  11256  ltabs  11269  abslt  11270  absle  11271  absgt0ap  11281  rpmaxcl  11405  nn0maxcl  11407  rpmincl  11420  mul0inf  11423  reccn2ap  11495  climge0  11507  fsumrecl  11583  isumlessdc  11678  divcnv  11679  expcnvre  11685  absltap  11691  geolim2  11694  georeclim  11695  geoisumr  11700  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemabsle  11709  mertenslem2  11718  cos12dec  11950  p1modz1  11976  dvdslelemd  12025  oddge22np1  12063  divalglemnn  12100  divalglemeuneg  12105  bitsfzolem  12136  bitsinv1lem  12143  lcmgcdlem  12270  dvdsnprmd  12318  isprm5lem  12334  sqrt2irraplemnn  12372  sqrt2irrap  12373  qnumgt0  12391  qexpz  12546  4sqlem6  12577  znnen  12640  ennnfoneleminc  12653  exmidunben  12668  mulcncflem  14927  hovercncf  14966  hovera  14967  hoverb  14968  hoverlt1  14969  hovergt0  14970  ivthdichlem  14971  dich0  14972  cosz12  15100  cos02pilt1  15171  ioocosf1o  15174  rplogcl  15199  cxplt  15236  cxple  15237  ltexp2  15261  mersenne  15317  lgsdilem  15352  gausslemma2dlem1a  15383  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  refeq  15759  trilpolemeq1  15771  trilpolemlt1  15772  ltlenmkv  15801