Theorem 0red 7586

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

Syntax hints:   -> wi 4   e. wcel 1445   RRcr 7446   0cc0 7447

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-1re 7536  ax-addrcl 7539  ax-rnegex 7551

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-cleq 2088  df-clel 2091  df-ral 2375  df-rex 2376

This theorem is referenced by:  gt0ne0  8002  add20  8049  subge0  8050  lesub0  8054  addgt0d  8095  sublt0d  8144  gt0add  8147  apreap  8161  gt0ap0  8199  ap0gt0  8212  prodgt0  8410  prodge0  8412  lt2msq1  8443  lediv12a  8452  ledivp1  8461  squeeze0  8462  mulle0r  8502  nn2ge  8553  0mnnnnn0  8803  elnn0z  8861  rpgecl  9261  ge0p1rp  9264  ledivge1le  9302  iccf1o  9570  elfz1b  9653  elfz0fzfz0  9686  fz0fzelfz0  9687  fzo1fzo0n0  9743  elfzo0z  9744  fzofzim  9748  elfzodifsumelfzo  9761  btwnzge0  9856  modqid  9905  mulqaddmodid  9920  mulp1mod1  9921  modqltm1p1mod  9932  addmodlteq  9954  expgt1  10124  ltexp2a  10138  leexp2a  10139  expnbnd  10208  expnlbnd2  10210  expcanlem  10255  expcan  10256  resqrexlemcalc3  10580  resqrexlemnm  10582  resqrexlemgt0  10584  sqrtgt0  10598  abs00ap  10626  leabs  10638  ltabs  10651  abslt  10652  absle  10653  absgt0ap  10663  rpmincl  10800  reccn2ap  10872  climge0  10884  fsumrecl  10960  isumlessdc  11055  divcnv  11056  expcnvre  11062  absltap  11068  geolim2  11071  georeclim  11072  geoisumr  11077  cvgratnnlemnexp  11083  cvgratnnlemmn  11084  cvgratnnlemabsle  11086  mertenslem2  11095  dvdslelemd  11287  oddge22np1  11324  divalglemnn  11361  divalglemeuneg  11366  lcmgcdlem  11502  dvdsnprmd  11550  sqrt2irraplemnn  11600  sqrt2irrap  11601  qnumgt0  11619  znnen  11654  mulcncflem  12369