Theorem 0red 8327

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 8326	. 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 8178   0cc0 8179

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 8273  ax-addrcl 8276  ax-rnegex 8288

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  8756  add20  8803  subge0  8804  lesub0  8808  addgt0d  8850  sublt0d  8900  gt0add  8903  apreap  8917  gt0ap0  8956  ap0gt0  8970  lt0ap0  8978  prodgt0  9184  prodge0  9186  lt2msq1  9217  lediv12a  9226  ledivp1  9235  squeeze0  9236  mulle0r  9276  indfdc  9300  nn2ge  9339  0mnnnnn0  9599  elnn0z  9661  nn0negleid  9717  rpgecl  10093  ge0p1rp  10096  ledivge1le  10137  mul2lt0rlt0  10170  mul2lt0rgt0  10171  mul2lt0np  10174  iccf1o  10417  elfz1b  10507  elfz0fzfz0  10543  fz0fzelfz0  10544  fzo1fzo0n0  10605  elfzo0z  10606  fzofzim  10610  elfzodifsumelfzo  10629  btwnzge0  10748  modqid  10799  mulqaddmodid  10814  mulp1mod1  10815  modqltm1p1mod  10826  addmodlteq  10848  expgt1  11027  ltexp2a  11041  leexp2a  11042  expnbnd  11114  expnlbnd2  11116  zzlesq  11159  nn0ltexp2  11161  expcanlem  11167  expcan  11168  bcm1n  11221  ssenneg  11294  sshashneg  11295  iswrdiz  11325  ccat2s1fvwd  11429  swrdswrdlem  11490  swrdswrd  11491  sq01  11674  resqrexlemcalc3  11796  resqrexlemnm  11798  resqrexlemgt0  11800  sqrtgt0  11814  abs00ap  11842  leabs  11854  ltabs  11868  abslt  11869  absle  11870  absgt0ap  11880  rpmaxcl  12004  nn0maxcl  12006  rpmincl  12019  mul0inf  12023  reccn2ap  12095  climge0  12107  fsumrecl  12184  isumlessdc  12279  divcnv  12280  expcnvre  12286  absltap  12292  geolim2  12295  georeclim  12296  geoisumr  12301  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemabsle  12310  mertenslem2  12319  cos12dec  12551  p1modz1  12577  dvdslelemd  12626  oddge22np1  12664  divalglemnn  12701  divalglemeuneg  12706  bitsfzolem  12737  bitsinv1lem  12744  lcmgcdlem  12871  dvdsnprmd  12919  isprm5lem  12936  sqrt2irraplemnn  12975  sqrt2irrap  12976  qnumgt0  12994  sqrtrirr  13005  qexpz  13151  4sqlem6  13182  ballotfilemonn  13270  ballotfilemfc0  13281  ballotfilemfcc  13282  znnen  13338  ennnfoneleminc  13351  exmidunben  13366  mulcncflem  15757  hovercncf  15796  hovera  15797  hoverb  15798  hoverlt1  15799  hovergt0  15800  ivthdichlem  15801  dich0  15802  cosz12  15931  cos02pilt1  16002  ioocosf1o  16005  rplogcl  16031  logdivlt  16046  logdivle  16047  cxplt  16071  cxple  16072  ltexp2  16096  ppiqfi  16158  ppiqwordi  16174  ppiqltx  16183  mersenne  16195  bposlem1  16209  lgsdilem  16244  gausslemma2dlem1a  16275  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  dichmul0orlem1  16851  dichmul0orlem5  16855  dichmul0orlem6  16856  refeq  17171  trilpolemeq1  17187  trilpolemlt1  17188  ltlenmkv  17218