Theorem 0red 8333

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8184   0cc0 8185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8279  ax-addrcl 8282  ax-rnegex 8294

This proof depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-ral 2533  df-rex 2534

This theorem is used by:  gt0ne0  8762  add20  8809  subge0  8810  lesub0  8814  addgt0d  8856  sublt0d  8906  gt0add  8909  apreap  8923  gt0ap0  8962  ap0gt0  8976  lt0ap0  8984  prodgt0  9190  prodge0  9192  lt2msq1  9223  lediv12a  9232  ledivp1  9241  squeeze0  9242  mulle0r  9282  indfdc  9307  nn2ge  9346  0mnnnnn0  9606  elnn0z  9666  nn0negleid  9722  rpgecl  10099  ge0p1rp  10102  ledivge1le  10143  mul2lt0rlt0  10176  mul2lt0rgt0  10177  mul2lt0np  10180  iccf1o  10423  elfz1b  10513  elfz0fzfz0  10549  fz0fzelfz0  10550  fzo1fzo0n0  10611  elfzo0z  10612  fzofzim  10616  elfzodifsumelfzo  10635  btwnzge0  10755  modqid  10806  mulqaddmodid  10821  mulp1mod1  10822  modqltm1p1mod  10833  addmodlteq  10855  expgt1  11034  ltexp2a  11048  leexp2a  11049  expnbnd  11121  expnlbnd2  11123  zzlesq  11166  nn0ltexp2  11168  expcanlem  11174  expcan  11175  bcm1n  11228  ssenneg  11301  sshashneg  11302  iswrdiz  11332  ccat2s1fvwd  11436  swrdswrdlem  11497  swrdswrd  11498  sq01  11681  resqrexlemcalc3  11803  resqrexlemnm  11805  resqrexlemgt0  11807  sqrtgt0  11821  abs00ap  11849  leabs  11861  ltabs  11875  abslt  11876  absle  11877  absgt0ap  11887  rpmaxcl  12011  nn0maxcl  12013  rpmincl  12027  mul0inf  12031  reccn2ap  12103  climge0  12115  fsumrecl  12192  isumlessdc  12287  divcnv  12288  expcnvre  12294  absltap  12300  geolim2  12303  georeclim  12304  geoisumr  12309  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemabsle  12318  mertenslem2  12327  cos12dec  12559  p1modz1  12585  dvdslelemd  12634  oddge22np1  12672  divalglemnn  12709  divalglemeuneg  12714  bitsfzolem  12745  bitsinv1lem  12752  lcmgcdlem  12879  dvdsnprmd  12927  isprm5lem  12944  sqrt2irraplemnn  12983  sqrt2irrap  12984  qnumgt0  13002  sqrtrirr  13013  qexpz  13159  4sqlem6  13190  ballotfilemonn  13278  ballotfilemfc0  13289  ballotfilemfcc  13290  znnen  13346  ennnfoneleminc  13359  exmidunben  13374  mulcncflem  15850  hovercncf  15889  hovera  15890  hoverb  15891  hoverlt1  15892  hovergt0  15893  ivthdichlem  15894  dich0  15895  cosz12  16024  cos02pilt1  16096  ioocosf1o  16099  rplogcl  16126  logdivlt  16141  logdivle  16142  cxplt  16168  cxple  16169  ltexp2  16194  ppiqfi  16259  chtqwordi  16280  ppiqwordi  16285  chtqrpcl  16296  ppiqltx  16298  mersenne  16314  bposlem1  16328  lgsdilem  16368  gausslemma2dlem1a  16399  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  dichmul0orlem1  16975  dichmul0orlem5  16979  dichmul0orlem6  16980  refeq  17296  trilpolemeq1  17313  trilpolemlt1  17314  ltlenmkv  17344