Theorem 0red 8179

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8030   0cc0 8031

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8125  ax-addrcl 8128  ax-rnegex 8140

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-cleq 2224  df-clel 2227  df-ral 2515  df-rex 2516

This theorem is referenced by:  gt0ne0  8606  add20  8653  subge0  8654  lesub0  8658  addgt0d  8700  sublt0d  8749  gt0add  8752  apreap  8766  gt0ap0  8805  ap0gt0  8819  lt0ap0  8827  prodgt0  9031  prodge0  9033  lt2msq1  9064  lediv12a  9073  ledivp1  9082  squeeze0  9083  mulle0r  9123  nn2ge  9175  0mnnnnn0  9433  elnn0z  9491  nn0negleid  9547  rpgecl  9916  ge0p1rp  9919  ledivge1le  9960  mul2lt0rlt0  9993  mul2lt0rgt0  9994  mul2lt0np  9997  iccf1o  10238  elfz1b  10324  elfz0fzfz0  10360  fz0fzelfz0  10361  fzo1fzo0n0  10421  elfzo0z  10422  fzofzim  10426  elfzodifsumelfzo  10445  btwnzge0  10559  modqid  10610  mulqaddmodid  10625  mulp1mod1  10626  modqltm1p1mod  10637  addmodlteq  10659  expgt1  10838  ltexp2a  10852  leexp2a  10853  expnbnd  10924  expnlbnd2  10926  zzlesq  10969  nn0ltexp2  10970  expcanlem  10976  expcan  10977  iswrdiz  11119  ccat2s1fvwd  11223  swrdswrdlem  11284  swrdswrd  11285  resqrexlemcalc3  11576  resqrexlemnm  11578  resqrexlemgt0  11580  sqrtgt0  11594  abs00ap  11622  leabs  11634  ltabs  11647  abslt  11648  absle  11649  absgt0ap  11659  rpmaxcl  11783  nn0maxcl  11785  rpmincl  11798  mul0inf  11801  reccn2ap  11873  climge0  11885  fsumrecl  11961  isumlessdc  12056  divcnv  12057  expcnvre  12063  absltap  12069  geolim2  12072  georeclim  12073  geoisumr  12078  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemabsle  12087  mertenslem2  12096  cos12dec  12328  p1modz1  12354  dvdslelemd  12403  oddge22np1  12441  divalglemnn  12478  divalglemeuneg  12483  bitsfzolem  12514  bitsinv1lem  12521  lcmgcdlem  12648  dvdsnprmd  12696  isprm5lem  12712  sqrt2irraplemnn  12750  sqrt2irrap  12751  qnumgt0  12769  qexpz  12924  4sqlem6  12955  znnen  13018  ennnfoneleminc  13031  exmidunben  13046  mulcncflem  15330  hovercncf  15369  hovera  15370  hoverb  15371  hoverlt1  15372  hovergt0  15373  ivthdichlem  15374  dich0  15375  cosz12  15503  cos02pilt1  15574  ioocosf1o  15577  rplogcl  15602  cxplt  15639  cxple  15640  ltexp2  15664  mersenne  15720  lgsdilem  15755  gausslemma2dlem1a  15786  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  refeq  16632  trilpolemeq1  16644  trilpolemlt1  16645  ltlenmkv  16674