Theorem 0red 7988

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

Syntax hints:   -> wi 4   e. wcel 2160   RRcr 7840   0cc0 7841

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-1re 7935  ax-addrcl 7938  ax-rnegex 7950

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-cleq 2182  df-clel 2185  df-ral 2473  df-rex 2474

This theorem is referenced by:  gt0ne0  8414  add20  8461  subge0  8462  lesub0  8466  addgt0d  8508  sublt0d  8557  gt0add  8560  apreap  8574  gt0ap0  8613  ap0gt0  8627  lt0ap0  8635  prodgt0  8839  prodge0  8841  lt2msq1  8872  lediv12a  8881  ledivp1  8890  squeeze0  8891  mulle0r  8931  nn2ge  8982  0mnnnnn0  9238  elnn0z  9296  nn0negleid  9351  rpgecl  9712  ge0p1rp  9715  ledivge1le  9756  mul2lt0rlt0  9789  mul2lt0rgt0  9790  mul2lt0np  9793  iccf1o  10034  elfz1b  10120  elfz0fzfz0  10156  fz0fzelfz0  10157  fzo1fzo0n0  10213  elfzo0z  10214  fzofzim  10218  elfzodifsumelfzo  10231  btwnzge0  10331  modqid  10380  mulqaddmodid  10395  mulp1mod1  10396  modqltm1p1mod  10407  addmodlteq  10429  expgt1  10589  ltexp2a  10603  leexp2a  10604  expnbnd  10675  expnlbnd2  10677  zzlesq  10720  nn0ltexp2  10721  expcanlem  10727  expcan  10728  resqrexlemcalc3  11057  resqrexlemnm  11059  resqrexlemgt0  11061  sqrtgt0  11075  abs00ap  11103  leabs  11115  ltabs  11128  abslt  11129  absle  11130  absgt0ap  11140  rpmaxcl  11264  rpmincl  11278  mul0inf  11281  reccn2ap  11353  climge0  11365  fsumrecl  11441  isumlessdc  11536  divcnv  11537  expcnvre  11543  absltap  11549  geolim2  11552  georeclim  11553  geoisumr  11558  cvgratnnlemnexp  11564  cvgratnnlemmn  11565  cvgratnnlemabsle  11567  mertenslem2  11576  cos12dec  11807  p1modz1  11833  dvdslelemd  11881  oddge22np1  11918  divalglemnn  11955  divalglemeuneg  11960  lcmgcdlem  12109  dvdsnprmd  12157  isprm5lem  12173  sqrt2irraplemnn  12211  sqrt2irrap  12212  qnumgt0  12230  qexpz  12384  4sqlem6  12415  znnen  12449  ennnfoneleminc  12462  exmidunben  12477  mulcncflem  14547  cosz12  14658  cos02pilt1  14729  ioocosf1o  14732  rplogcl  14757  cxplt  14793  cxple  14794  ltexp2  14817  lgsdilem  14886  refeq  15235  trilpolemeq1  15247  trilpolemlt1  15248  ltlenmkv  15277