Theorem 0red 8073

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

Syntax hints:   -> wi 4   e. wcel 2176   RRcr 7924   0cc0 7925

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-1re 8019  ax-addrcl 8022  ax-rnegex 8034

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-cleq 2198  df-clel 2201  df-ral 2489  df-rex 2490

This theorem is referenced by:  gt0ne0  8500  add20  8547  subge0  8548  lesub0  8552  addgt0d  8594  sublt0d  8643  gt0add  8646  apreap  8660  gt0ap0  8699  ap0gt0  8713  lt0ap0  8721  prodgt0  8925  prodge0  8927  lt2msq1  8958  lediv12a  8967  ledivp1  8976  squeeze0  8977  mulle0r  9017  nn2ge  9069  0mnnnnn0  9327  elnn0z  9385  nn0negleid  9441  rpgecl  9804  ge0p1rp  9807  ledivge1le  9848  mul2lt0rlt0  9881  mul2lt0rgt0  9882  mul2lt0np  9885  iccf1o  10126  elfz1b  10212  elfz0fzfz0  10248  fz0fzelfz0  10249  fzo1fzo0n0  10307  elfzo0z  10308  fzofzim  10312  elfzodifsumelfzo  10330  btwnzge0  10443  modqid  10494  mulqaddmodid  10509  mulp1mod1  10510  modqltm1p1mod  10521  addmodlteq  10543  expgt1  10722  ltexp2a  10736  leexp2a  10737  expnbnd  10808  expnlbnd2  10810  zzlesq  10853  nn0ltexp2  10854  expcanlem  10860  expcan  10861  iswrdiz  11001  resqrexlemcalc3  11327  resqrexlemnm  11329  resqrexlemgt0  11331  sqrtgt0  11345  abs00ap  11373  leabs  11385  ltabs  11398  abslt  11399  absle  11400  absgt0ap  11410  rpmaxcl  11534  nn0maxcl  11536  rpmincl  11549  mul0inf  11552  reccn2ap  11624  climge0  11636  fsumrecl  11712  isumlessdc  11807  divcnv  11808  expcnvre  11814  absltap  11820  geolim2  11823  georeclim  11824  geoisumr  11829  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  cvgratnnlemabsle  11838  mertenslem2  11847  cos12dec  12079  p1modz1  12105  dvdslelemd  12154  oddge22np1  12192  divalglemnn  12229  divalglemeuneg  12234  bitsfzolem  12265  bitsinv1lem  12272  lcmgcdlem  12399  dvdsnprmd  12447  isprm5lem  12463  sqrt2irraplemnn  12501  sqrt2irrap  12502  qnumgt0  12520  qexpz  12675  4sqlem6  12706  znnen  12769  ennnfoneleminc  12782  exmidunben  12797  mulcncflem  15079  hovercncf  15118  hovera  15119  hoverb  15120  hoverlt1  15121  hovergt0  15122  ivthdichlem  15123  dich0  15124  cosz12  15252  cos02pilt1  15323  ioocosf1o  15326  rplogcl  15351  cxplt  15388  cxple  15389  ltexp2  15413  mersenne  15469  lgsdilem  15504  gausslemma2dlem1a  15535  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  refeq  15967  trilpolemeq1  15979  trilpolemlt1  15980  ltlenmkv  16009