Theorem 0red 8275

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

Syntax hints:   -> wi 4   e. wcel 2203   RRcr 8126   0cc0 8127

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-1re 8221  ax-addrcl 8224  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2225  df-clel 2228  df-ral 2525  df-rex 2526

This theorem is referenced by:  gt0ne0  8701  add20  8748  subge0  8749  lesub0  8753  addgt0d  8795  sublt0d  8844  gt0add  8847  apreap  8861  gt0ap0  8900  ap0gt0  8914  lt0ap0  8922  prodgt0  9126  prodge0  9128  lt2msq1  9159  lediv12a  9168  ledivp1  9177  squeeze0  9178  mulle0r  9218  nn2ge  9270  0mnnnnn0  9528  elnn0z  9590  nn0negleid  9646  rpgecl  10015  ge0p1rp  10018  ledivge1le  10059  mul2lt0rlt0  10092  mul2lt0rgt0  10093  mul2lt0np  10096  iccf1o  10338  elfz1b  10424  elfz0fzfz0  10460  fz0fzelfz0  10461  fzo1fzo0n0  10522  elfzo0z  10523  fzofzim  10527  elfzodifsumelfzo  10546  btwnzge0  10660  modqid  10711  mulqaddmodid  10726  mulp1mod1  10727  modqltm1p1mod  10738  addmodlteq  10760  expgt1  10939  ltexp2a  10953  leexp2a  10954  expnbnd  11025  expnlbnd2  11027  zzlesq  11070  nn0ltexp2  11071  expcanlem  11077  expcan  11078  bcm1n  11131  ssenneg  11204  sshashneg  11205  iswrdiz  11231  ccat2s1fvwd  11335  swrdswrdlem  11396  swrdswrd  11397  resqrexlemcalc3  11701  resqrexlemnm  11703  resqrexlemgt0  11705  sqrtgt0  11719  abs00ap  11747  leabs  11759  ltabs  11772  abslt  11773  absle  11774  absgt0ap  11784  rpmaxcl  11908  nn0maxcl  11910  rpmincl  11923  mul0inf  11926  reccn2ap  11998  climge0  12010  fsumrecl  12087  isumlessdc  12182  divcnv  12183  expcnvre  12189  absltap  12195  geolim2  12198  georeclim  12199  geoisumr  12204  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratnnlemabsle  12213  mertenslem2  12222  cos12dec  12454  p1modz1  12480  dvdslelemd  12529  oddge22np1  12567  divalglemnn  12604  divalglemeuneg  12609  bitsfzolem  12640  bitsinv1lem  12647  lcmgcdlem  12774  dvdsnprmd  12822  isprm5lem  12838  sqrt2irraplemnn  12876  sqrt2irrap  12877  qnumgt0  12895  qexpz  13050  4sqlem6  13081  ballotfilemonn  13140  znnen  13149  ennnfoneleminc  13162  exmidunben  13177  mulcncflem  15472  hovercncf  15511  hovera  15512  hoverb  15513  hoverlt1  15514  hovergt0  15515  ivthdichlem  15516  dich0  15517  cosz12  15645  cos02pilt1  15716  ioocosf1o  15719  rplogcl  15744  cxplt  15781  cxple  15782  ltexp2  15806  mersenne  15865  lgsdilem  15900  gausslemma2dlem1a  15931  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  refeq  16808  trilpolemeq1  16824  trilpolemlt1  16825  ltlenmkv  16856