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  9668  nn0negleid  9724  rpgecl  10100  ge0p1rp  10103  ledivge1le  10144  mul2lt0rlt0  10177  mul2lt0rgt0  10178  mul2lt0np  10181  iccf1o  10424  elfz1b  10514  elfz0fzfz0  10550  fz0fzelfz0  10551  fzo1fzo0n0  10612  elfzo0z  10613  fzofzim  10617  elfzodifsumelfzo  10636  btwnzge0  10756  modqid  10807  mulqaddmodid  10822  mulp1mod1  10823  modqltm1p1mod  10834  addmodlteq  10856  expgt1  11035  ltexp2a  11049  leexp2a  11050  expnbnd  11122  expnlbnd2  11124  zzlesq  11167  nn0ltexp2  11169  expcanlem  11175  expcan  11176  bcm1n  11229  ssenneg  11302  sshashneg  11303  iswrdiz  11333  ccat2s1fvwd  11437  swrdswrdlem  11498  swrdswrd  11499  sq01  11682  resqrexlemcalc3  11804  resqrexlemnm  11806  resqrexlemgt0  11808  sqrtgt0  11822  abs00ap  11850  leabs  11862  ltabs  11876  abslt  11877  absle  11878  absgt0ap  11888  rpmaxcl  12012  nn0maxcl  12014  rpmincl  12028  mul0inf  12032  reccn2ap  12104  climge0  12116  fsumrecl  12193  isumlessdc  12288  divcnv  12289  expcnvre  12295  absltap  12301  geolim2  12304  georeclim  12305  geoisumr  12310  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemabsle  12319  mertenslem2  12328  cos12dec  12560  p1modz1  12586  dvdslelemd  12635  oddge22np1  12673  divalglemnn  12710  divalglemeuneg  12715  bitsfzolem  12746  bitsinv1lem  12753  lcmgcdlem  12880  dvdsnprmd  12928  isprm5lem  12945  sqrt2irraplemnn  12984  sqrt2irrap  12985  qnumgt0  13003  sqrtrirr  13014  qexpz  13160  4sqlem6  13191  ballotfilemonn  13279  ballotfilemfc0  13290  ballotfilemfcc  13291  znnen  13347  ennnfoneleminc  13360  exmidunben  13375  mulcncflem  15833  hovercncf  15872  hovera  15873  hoverb  15874  hoverlt1  15875  hovergt0  15876  ivthdichlem  15877  dich0  15878  cosz12  16007  cos02pilt1  16079  ioocosf1o  16082  rplogcl  16109  logdivlt  16124  logdivle  16125  cxplt  16151  cxple  16152  ltexp2  16177  ppiqfi  16242  chtqwordi  16263  ppiqwordi  16268  chtqrpcl  16279  ppiqltx  16281  mersenne  16297  bposlem1  16311  lgsdilem  16351  gausslemma2dlem1a  16382  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  dichmul0orlem1  16958  dichmul0orlem5  16962  dichmul0orlem6  16963  refeq  17279  trilpolemeq1  17296  trilpolemlt1  17297  ltlenmkv  17327