Theorem 0red 8147

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

Syntax hints:   -> wi 4   e. wcel 2200   RRcr 7998   0cc0 7999

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8093  ax-addrcl 8096  ax-rnegex 8108

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-ral 2513  df-rex 2514

This theorem is referenced by:  gt0ne0  8574  add20  8621  subge0  8622  lesub0  8626  addgt0d  8668  sublt0d  8717  gt0add  8720  apreap  8734  gt0ap0  8773  ap0gt0  8787  lt0ap0  8795  prodgt0  8999  prodge0  9001  lt2msq1  9032  lediv12a  9041  ledivp1  9050  squeeze0  9051  mulle0r  9091  nn2ge  9143  0mnnnnn0  9401  elnn0z  9459  nn0negleid  9515  rpgecl  9878  ge0p1rp  9881  ledivge1le  9922  mul2lt0rlt0  9955  mul2lt0rgt0  9956  mul2lt0np  9959  iccf1o  10200  elfz1b  10286  elfz0fzfz0  10322  fz0fzelfz0  10323  fzo1fzo0n0  10383  elfzo0z  10384  fzofzim  10388  elfzodifsumelfzo  10407  btwnzge0  10520  modqid  10571  mulqaddmodid  10586  mulp1mod1  10587  modqltm1p1mod  10598  addmodlteq  10620  expgt1  10799  ltexp2a  10813  leexp2a  10814  expnbnd  10885  expnlbnd2  10887  zzlesq  10930  nn0ltexp2  10931  expcanlem  10937  expcan  10938  iswrdiz  11078  swrdswrdlem  11236  swrdswrd  11237  resqrexlemcalc3  11527  resqrexlemnm  11529  resqrexlemgt0  11531  sqrtgt0  11545  abs00ap  11573  leabs  11585  ltabs  11598  abslt  11599  absle  11600  absgt0ap  11610  rpmaxcl  11734  nn0maxcl  11736  rpmincl  11749  mul0inf  11752  reccn2ap  11824  climge0  11836  fsumrecl  11912  isumlessdc  12007  divcnv  12008  expcnvre  12014  absltap  12020  geolim2  12023  georeclim  12024  geoisumr  12029  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratnnlemabsle  12038  mertenslem2  12047  cos12dec  12279  p1modz1  12305  dvdslelemd  12354  oddge22np1  12392  divalglemnn  12429  divalglemeuneg  12434  bitsfzolem  12465  bitsinv1lem  12472  lcmgcdlem  12599  dvdsnprmd  12647  isprm5lem  12663  sqrt2irraplemnn  12701  sqrt2irrap  12702  qnumgt0  12720  qexpz  12875  4sqlem6  12906  znnen  12969  ennnfoneleminc  12982  exmidunben  12997  mulcncflem  15281  hovercncf  15320  hovera  15321  hoverb  15322  hoverlt1  15323  hovergt0  15324  ivthdichlem  15325  dich0  15326  cosz12  15454  cos02pilt1  15525  ioocosf1o  15528  rplogcl  15553  cxplt  15590  cxple  15591  ltexp2  15615  mersenne  15671  lgsdilem  15706  gausslemma2dlem1a  15737  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  refeq  16396  trilpolemeq1  16408  trilpolemlt1  16409  ltlenmkv  16438