Theorem 0red 8108

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

Syntax hints:   -> wi 4   e. wcel 2178   RRcr 7959   0cc0 7960

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-1re 8054  ax-addrcl 8057  ax-rnegex 8069

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-cleq 2200  df-clel 2203  df-ral 2491  df-rex 2492

This theorem is referenced by:  gt0ne0  8535  add20  8582  subge0  8583  lesub0  8587  addgt0d  8629  sublt0d  8678  gt0add  8681  apreap  8695  gt0ap0  8734  ap0gt0  8748  lt0ap0  8756  prodgt0  8960  prodge0  8962  lt2msq1  8993  lediv12a  9002  ledivp1  9011  squeeze0  9012  mulle0r  9052  nn2ge  9104  0mnnnnn0  9362  elnn0z  9420  nn0negleid  9476  rpgecl  9839  ge0p1rp  9842  ledivge1le  9883  mul2lt0rlt0  9916  mul2lt0rgt0  9917  mul2lt0np  9920  iccf1o  10161  elfz1b  10247  elfz0fzfz0  10283  fz0fzelfz0  10284  fzo1fzo0n0  10344  elfzo0z  10345  fzofzim  10349  elfzodifsumelfzo  10367  btwnzge0  10480  modqid  10531  mulqaddmodid  10546  mulp1mod1  10547  modqltm1p1mod  10558  addmodlteq  10580  expgt1  10759  ltexp2a  10773  leexp2a  10774  expnbnd  10845  expnlbnd2  10847  zzlesq  10890  nn0ltexp2  10891  expcanlem  10897  expcan  10898  iswrdiz  11038  swrdswrdlem  11195  swrdswrd  11196  resqrexlemcalc3  11442  resqrexlemnm  11444  resqrexlemgt0  11446  sqrtgt0  11460  abs00ap  11488  leabs  11500  ltabs  11513  abslt  11514  absle  11515  absgt0ap  11525  rpmaxcl  11649  nn0maxcl  11651  rpmincl  11664  mul0inf  11667  reccn2ap  11739  climge0  11751  fsumrecl  11827  isumlessdc  11922  divcnv  11923  expcnvre  11929  absltap  11935  geolim2  11938  georeclim  11939  geoisumr  11944  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  cvgratnnlemabsle  11953  mertenslem2  11962  cos12dec  12194  p1modz1  12220  dvdslelemd  12269  oddge22np1  12307  divalglemnn  12344  divalglemeuneg  12349  bitsfzolem  12380  bitsinv1lem  12387  lcmgcdlem  12514  dvdsnprmd  12562  isprm5lem  12578  sqrt2irraplemnn  12616  sqrt2irrap  12617  qnumgt0  12635  qexpz  12790  4sqlem6  12821  znnen  12884  ennnfoneleminc  12897  exmidunben  12912  mulcncflem  15194  hovercncf  15233  hovera  15234  hoverb  15235  hoverlt1  15236  hovergt0  15237  ivthdichlem  15238  dich0  15239  cosz12  15367  cos02pilt1  15438  ioocosf1o  15441  rplogcl  15466  cxplt  15503  cxple  15504  ltexp2  15528  mersenne  15584  lgsdilem  15619  gausslemma2dlem1a  15650  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  refeq  16169  trilpolemeq1  16181  trilpolemlt1  16182  ltlenmkv  16211