Theorem 0red 7914

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

Syntax hints:   -> wi 4   e. wcel 2141   RRcr 7766   0cc0 7767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1re 7861  ax-addrcl 7864  ax-rnegex 7876

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-cleq 2163  df-clel 2166  df-ral 2453  df-rex 2454

This theorem is referenced by:  gt0ne0  8339  add20  8386  subge0  8387  lesub0  8391  addgt0d  8433  sublt0d  8482  gt0add  8485  apreap  8499  gt0ap0  8538  ap0gt0  8552  lt0ap0  8560  prodgt0  8761  prodge0  8763  lt2msq1  8794  lediv12a  8803  ledivp1  8812  squeeze0  8813  mulle0r  8853  nn2ge  8904  0mnnnnn0  9160  elnn0z  9218  nn0negleid  9273  rpgecl  9632  ge0p1rp  9635  ledivge1le  9676  mul2lt0rlt0  9709  mul2lt0rgt0  9710  mul2lt0np  9713  iccf1o  9954  elfz1b  10039  elfz0fzfz0  10075  fz0fzelfz0  10076  fzo1fzo0n0  10132  elfzo0z  10133  fzofzim  10137  elfzodifsumelfzo  10150  btwnzge0  10249  modqid  10298  mulqaddmodid  10313  mulp1mod1  10314  modqltm1p1mod  10325  addmodlteq  10347  expgt1  10507  ltexp2a  10521  leexp2a  10522  expnbnd  10592  expnlbnd2  10594  nn0ltexp2  10637  expcanlem  10642  expcan  10643  resqrexlemcalc3  10973  resqrexlemnm  10975  resqrexlemgt0  10977  sqrtgt0  10991  abs00ap  11019  leabs  11031  ltabs  11044  abslt  11045  absle  11046  absgt0ap  11056  rpmaxcl  11180  rpmincl  11194  mul0inf  11197  reccn2ap  11269  climge0  11281  fsumrecl  11357  isumlessdc  11452  divcnv  11453  expcnvre  11459  absltap  11465  geolim2  11468  georeclim  11469  geoisumr  11474  cvgratnnlemnexp  11480  cvgratnnlemmn  11481  cvgratnnlemabsle  11483  mertenslem2  11492  cos12dec  11723  p1modz1  11749  dvdslelemd  11796  oddge22np1  11833  divalglemnn  11870  divalglemeuneg  11875  lcmgcdlem  12024  dvdsnprmd  12072  isprm5lem  12088  sqrt2irraplemnn  12126  sqrt2irrap  12127  qnumgt0  12145  qexpz  12297  4sqlem6  12328  znnen  12346  ennnfoneleminc  12359  exmidunben  12374  mulcncflem  13349  cosz12  13460  cos02pilt1  13531  ioocosf1o  13534  rplogcl  13559  cxplt  13595  cxple  13596  ltexp2  13619  lgsdilem  13687  refeq  14025  trilpolemeq1  14037  trilpolemlt1  14038