Theorem 0red 7760

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

Syntax hints:   -> wi 4   e. wcel 1480   RRcr 7612   0cc0 7613

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-1re 7707  ax-addrcl 7710  ax-rnegex 7722

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-cleq 2130  df-clel 2133  df-ral 2419  df-rex 2420

This theorem is referenced by:  gt0ne0  8182  add20  8229  subge0  8230  lesub0  8234  addgt0d  8276  sublt0d  8325  gt0add  8328  apreap  8342  gt0ap0  8381  ap0gt0  8395  lt0ap0  8403  prodgt0  8603  prodge0  8605  lt2msq1  8636  lediv12a  8645  ledivp1  8654  squeeze0  8655  mulle0r  8695  nn2ge  8746  0mnnnnn0  9002  elnn0z  9060  rpgecl  9463  ge0p1rp  9466  ledivge1le  9506  mul2lt0rlt0  9539  mul2lt0rgt0  9540  mul2lt0np  9543  iccf1o  9780  elfz1b  9863  elfz0fzfz0  9896  fz0fzelfz0  9897  fzo1fzo0n0  9953  elfzo0z  9954  fzofzim  9958  elfzodifsumelfzo  9971  btwnzge0  10066  modqid  10115  mulqaddmodid  10130  mulp1mod1  10131  modqltm1p1mod  10142  addmodlteq  10164  expgt1  10324  ltexp2a  10338  leexp2a  10339  expnbnd  10408  expnlbnd2  10410  expcanlem  10455  expcan  10456  resqrexlemcalc3  10781  resqrexlemnm  10783  resqrexlemgt0  10785  sqrtgt0  10799  abs00ap  10827  leabs  10839  ltabs  10852  abslt  10853  absle  10854  absgt0ap  10864  rpmaxcl  10988  rpmincl  11002  mul0inf  11005  reccn2ap  11075  climge0  11087  fsumrecl  11163  isumlessdc  11258  divcnv  11259  expcnvre  11265  absltap  11271  geolim2  11274  georeclim  11275  geoisumr  11280  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  cvgratnnlemabsle  11289  mertenslem2  11298  cos12dec  11463  dvdslelemd  11530  oddge22np1  11567  divalglemnn  11604  divalglemeuneg  11609  lcmgcdlem  11747  dvdsnprmd  11795  sqrt2irraplemnn  11846  sqrt2irrap  11847  qnumgt0  11865  znnen  11900  ennnfoneleminc  11913  exmidunben  11928  mulcncflem  12748  cosz12  12850  cos02pilt1  12921  refeq  13212  trilpolemeq1  13222  trilpolemlt1  13223