Theorem 0red 7896

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

Syntax hints:   -> wi 4   e. wcel 2136   RRcr 7748   0cc0 7749

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1re 7843  ax-addrcl 7846  ax-rnegex 7858

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-cleq 2158  df-clel 2161  df-ral 2448  df-rex 2449

This theorem is referenced by:  gt0ne0  8321  add20  8368  subge0  8369  lesub0  8373  addgt0d  8415  sublt0d  8464  gt0add  8467  apreap  8481  gt0ap0  8520  ap0gt0  8534  lt0ap0  8542  prodgt0  8743  prodge0  8745  lt2msq1  8776  lediv12a  8785  ledivp1  8794  squeeze0  8795  mulle0r  8835  nn2ge  8886  0mnnnnn0  9142  elnn0z  9200  nn0negleid  9255  rpgecl  9614  ge0p1rp  9617  ledivge1le  9658  mul2lt0rlt0  9691  mul2lt0rgt0  9692  mul2lt0np  9695  iccf1o  9936  elfz1b  10021  elfz0fzfz0  10057  fz0fzelfz0  10058  fzo1fzo0n0  10114  elfzo0z  10115  fzofzim  10119  elfzodifsumelfzo  10132  btwnzge0  10231  modqid  10280  mulqaddmodid  10295  mulp1mod1  10296  modqltm1p1mod  10307  addmodlteq  10329  expgt1  10489  ltexp2a  10503  leexp2a  10504  expnbnd  10574  expnlbnd2  10576  nn0ltexp2  10619  expcanlem  10624  expcan  10625  resqrexlemcalc3  10954  resqrexlemnm  10956  resqrexlemgt0  10958  sqrtgt0  10972  abs00ap  11000  leabs  11012  ltabs  11025  abslt  11026  absle  11027  absgt0ap  11037  rpmaxcl  11161  rpmincl  11175  mul0inf  11178  reccn2ap  11250  climge0  11262  fsumrecl  11338  isumlessdc  11433  divcnv  11434  expcnvre  11440  absltap  11446  geolim2  11449  georeclim  11450  geoisumr  11455  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratnnlemabsle  11464  mertenslem2  11473  cos12dec  11704  p1modz1  11730  dvdslelemd  11777  oddge22np1  11814  divalglemnn  11851  divalglemeuneg  11856  lcmgcdlem  12005  dvdsnprmd  12053  isprm5lem  12069  sqrt2irraplemnn  12107  sqrt2irrap  12108  qnumgt0  12126  qexpz  12278  4sqlem6  12309  znnen  12327  ennnfoneleminc  12340  exmidunben  12355  mulcncflem  13190  cosz12  13301  cos02pilt1  13372  ioocosf1o  13375  rplogcl  13400  cxplt  13436  cxple  13437  ltexp2  13460  lgsdilem  13528  refeq  13867  trilpolemeq1  13879  trilpolemlt1  13880