Theorem 0red 7767

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

Syntax hints:   -> wi 4   e. wcel 1480   RRcr 7619   0cc0 7620

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 2121  ax-1re 7714  ax-addrcl 7717  ax-rnegex 7729

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-cleq 2132  df-clel 2135  df-ral 2421  df-rex 2422

This theorem is referenced by:  gt0ne0  8189  add20  8236  subge0  8237  lesub0  8241  addgt0d  8283  sublt0d  8332  gt0add  8335  apreap  8349  gt0ap0  8388  ap0gt0  8402  lt0ap0  8410  prodgt0  8610  prodge0  8612  lt2msq1  8643  lediv12a  8652  ledivp1  8661  squeeze0  8662  mulle0r  8702  nn2ge  8753  0mnnnnn0  9009  elnn0z  9067  rpgecl  9470  ge0p1rp  9473  ledivge1le  9513  mul2lt0rlt0  9546  mul2lt0rgt0  9547  mul2lt0np  9550  iccf1o  9787  elfz1b  9870  elfz0fzfz0  9903  fz0fzelfz0  9904  fzo1fzo0n0  9960  elfzo0z  9961  fzofzim  9965  elfzodifsumelfzo  9978  btwnzge0  10073  modqid  10122  mulqaddmodid  10137  mulp1mod1  10138  modqltm1p1mod  10149  addmodlteq  10171  expgt1  10331  ltexp2a  10345  leexp2a  10346  expnbnd  10415  expnlbnd2  10417  expcanlem  10462  expcan  10463  resqrexlemcalc3  10788  resqrexlemnm  10790  resqrexlemgt0  10792  sqrtgt0  10806  abs00ap  10834  leabs  10846  ltabs  10859  abslt  10860  absle  10861  absgt0ap  10871  rpmaxcl  10995  rpmincl  11009  mul0inf  11012  reccn2ap  11082  climge0  11094  fsumrecl  11170  isumlessdc  11265  divcnv  11266  expcnvre  11272  absltap  11278  geolim2  11281  georeclim  11282  geoisumr  11287  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratnnlemabsle  11296  mertenslem2  11305  cos12dec  11474  dvdslelemd  11541  oddge22np1  11578  divalglemnn  11615  divalglemeuneg  11620  lcmgcdlem  11758  dvdsnprmd  11806  sqrt2irraplemnn  11857  sqrt2irrap  11858  qnumgt0  11876  znnen  11911  ennnfoneleminc  11924  exmidunben  11939  mulcncflem  12759  cosz12  12861  cos02pilt1  12932  refeq  13223  trilpolemeq1  13233  trilpolemlt1  13234