Theorem 0red 8180

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8031   0cc0 8032

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-cleq 2224  df-clel 2227  df-ral 2515  df-rex 2516

This theorem is referenced by:  gt0ne0  8607  add20  8654  subge0  8655  lesub0  8659  addgt0d  8701  sublt0d  8750  gt0add  8753  apreap  8767  gt0ap0  8806  ap0gt0  8820  lt0ap0  8828  prodgt0  9032  prodge0  9034  lt2msq1  9065  lediv12a  9074  ledivp1  9083  squeeze0  9084  mulle0r  9124  nn2ge  9176  0mnnnnn0  9434  elnn0z  9492  nn0negleid  9548  rpgecl  9917  ge0p1rp  9920  ledivge1le  9961  mul2lt0rlt0  9994  mul2lt0rgt0  9995  mul2lt0np  9998  iccf1o  10239  elfz1b  10325  elfz0fzfz0  10361  fz0fzelfz0  10362  fzo1fzo0n0  10423  elfzo0z  10424  fzofzim  10428  elfzodifsumelfzo  10447  btwnzge0  10561  modqid  10612  mulqaddmodid  10627  mulp1mod1  10628  modqltm1p1mod  10639  addmodlteq  10661  expgt1  10840  ltexp2a  10854  leexp2a  10855  expnbnd  10926  expnlbnd2  10928  zzlesq  10971  nn0ltexp2  10972  expcanlem  10978  expcan  10979  iswrdiz  11124  ccat2s1fvwd  11228  swrdswrdlem  11289  swrdswrd  11290  resqrexlemcalc3  11594  resqrexlemnm  11596  resqrexlemgt0  11598  sqrtgt0  11612  abs00ap  11640  leabs  11652  ltabs  11665  abslt  11666  absle  11667  absgt0ap  11677  rpmaxcl  11801  nn0maxcl  11803  rpmincl  11816  mul0inf  11819  reccn2ap  11891  climge0  11903  fsumrecl  11980  isumlessdc  12075  divcnv  12076  expcnvre  12082  absltap  12088  geolim2  12091  georeclim  12092  geoisumr  12097  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  cvgratnnlemabsle  12106  mertenslem2  12115  cos12dec  12347  p1modz1  12373  dvdslelemd  12422  oddge22np1  12460  divalglemnn  12497  divalglemeuneg  12502  bitsfzolem  12533  bitsinv1lem  12540  lcmgcdlem  12667  dvdsnprmd  12715  isprm5lem  12731  sqrt2irraplemnn  12769  sqrt2irrap  12770  qnumgt0  12788  qexpz  12943  4sqlem6  12974  znnen  13037  ennnfoneleminc  13050  exmidunben  13065  mulcncflem  15350  hovercncf  15389  hovera  15390  hoverb  15391  hoverlt1  15392  hovergt0  15393  ivthdichlem  15394  dich0  15395  cosz12  15523  cos02pilt1  15594  ioocosf1o  15597  rplogcl  15622  cxplt  15659  cxple  15660  ltexp2  15684  mersenne  15740  lgsdilem  15775  gausslemma2dlem1a  15806  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  refeq  16683  trilpolemeq1  16695  trilpolemlt1  16696  ltlenmkv  16726