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  8755  add20  8802  subge0  8803  lesub0  8807  addgt0d  8849  sublt0d  8898  gt0add  8901  apreap  8915  gt0ap0  8954  ap0gt0  8968  lt0ap0  8976  prodgt0  9182  prodge0  9184  lt2msq1  9215  lediv12a  9224  ledivp1  9233  squeeze0  9234  mulle0r  9274  indfdc  9298  nn2ge  9337  0mnnnnn0  9595  elnn0z  9657  nn0negleid  9713  rpgecl  10083  ge0p1rp  10086  ledivge1le  10127  mul2lt0rlt0  10160  mul2lt0rgt0  10161  mul2lt0np  10164  iccf1o  10407  elfz1b  10497  elfz0fzfz0  10533  fz0fzelfz0  10534  fzo1fzo0n0  10595  elfzo0z  10596  fzofzim  10600  elfzodifsumelfzo  10619  btwnzge0  10735  modqid  10786  mulqaddmodid  10801  mulp1mod1  10802  modqltm1p1mod  10813  addmodlteq  10835  expgt1  11014  ltexp2a  11028  leexp2a  11029  expnbnd  11101  expnlbnd2  11103  zzlesq  11146  nn0ltexp2  11147  expcanlem  11153  expcan  11154  bcm1n  11207  ssenneg  11280  sshashneg  11281  iswrdiz  11311  ccat2s1fvwd  11415  swrdswrdlem  11476  swrdswrd  11477  sq01  11660  resqrexlemcalc3  11782  resqrexlemnm  11784  resqrexlemgt0  11786  sqrtgt0  11800  abs00ap  11828  leabs  11840  ltabs  11853  abslt  11854  absle  11855  absgt0ap  11865  rpmaxcl  11989  nn0maxcl  11991  rpmincl  12004  mul0inf  12007  reccn2ap  12079  climge0  12091  fsumrecl  12168  isumlessdc  12263  divcnv  12264  expcnvre  12270  absltap  12276  geolim2  12279  georeclim  12280  geoisumr  12285  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  cvgratnnlemabsle  12294  mertenslem2  12303  cos12dec  12535  p1modz1  12561  dvdslelemd  12610  oddge22np1  12648  divalglemnn  12685  divalglemeuneg  12690  bitsfzolem  12721  bitsinv1lem  12728  lcmgcdlem  12855  dvdsnprmd  12903  isprm5lem  12919  sqrt2irraplemnn  12957  sqrt2irrap  12958  qnumgt0  12976  qexpz  13131  4sqlem6  13162  ballotfilemonn  13221  ballotfilemfc0  13232  ballotfilemfcc  13233  znnen  13289  ennnfoneleminc  13302  exmidunben  13317  mulcncflem  15708  hovercncf  15747  hovera  15748  hoverb  15749  hoverlt1  15750  hovergt0  15751  ivthdichlem  15752  dich0  15753  cosz12  15881  cos02pilt1  15952  ioocosf1o  15955  rplogcl  15980  cxplt  16018  cxple  16019  ltexp2  16043  mersenne  16111  lgsdilem  16146  gausslemma2dlem1a  16177  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  dichmul0orlem1  16753  dichmul0orlem5  16757  dichmul0orlem6  16758  refeq  17073  trilpolemeq1  17089  trilpolemlt1  17090  ltlenmkv  17120