Theorem 0red 8020

Description: 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
0red	⊢ (𝜑 → 0 ∈ ℝ)

Proof of Theorem 0red

Step	Hyp	Ref	Expression
1		0re 8019	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 9	1 ⊢ (𝜑 → 0 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2164  ℝcr 7871  0cc0 7872

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1re 7966  ax-addrcl 7969  ax-rnegex 7981

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-cleq 2186  df-clel 2189  df-ral 2477  df-rex 2478

This theorem is referenced by:  gt0ne0  8446  add20  8493  subge0  8494  lesub0  8498  addgt0d  8540  sublt0d  8589  gt0add  8592  apreap  8606  gt0ap0  8645  ap0gt0  8659  lt0ap0  8667  prodgt0  8871  prodge0  8873  lt2msq1  8904  lediv12a  8913  ledivp1  8922  squeeze0  8923  mulle0r  8963  nn2ge  9015  0mnnnnn0  9272  elnn0z  9330  nn0negleid  9385  rpgecl  9748  ge0p1rp  9751  ledivge1le  9792  mul2lt0rlt0  9825  mul2lt0rgt0  9826  mul2lt0np  9829  iccf1o  10070  elfz1b  10156  elfz0fzfz0  10192  fz0fzelfz0  10193  fzo1fzo0n0  10250  elfzo0z  10251  fzofzim  10255  elfzodifsumelfzo  10268  btwnzge0  10369  modqid  10420  mulqaddmodid  10435  mulp1mod1  10436  modqltm1p1mod  10447  addmodlteq  10469  expgt1  10648  ltexp2a  10662  leexp2a  10663  expnbnd  10734  expnlbnd2  10736  zzlesq  10779  nn0ltexp2  10780  expcanlem  10786  expcan  10787  iswrdiz  10921  resqrexlemcalc3  11160  resqrexlemnm  11162  resqrexlemgt0  11164  sqrtgt0  11178  abs00ap  11206  leabs  11218  ltabs  11231  abslt  11232  absle  11233  absgt0ap  11243  rpmaxcl  11367  rpmincl  11381  mul0inf  11384  reccn2ap  11456  climge0  11468  fsumrecl  11544  isumlessdc  11639  divcnv  11640  expcnvre  11646  absltap  11652  geolim2  11655  georeclim  11656  geoisumr  11661  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemabsle  11670  mertenslem2  11679  cos12dec  11911  p1modz1  11937  dvdslelemd  11985  oddge22np1  12022  divalglemnn  12059  divalglemeuneg  12064  lcmgcdlem  12215  dvdsnprmd  12263  isprm5lem  12279  sqrt2irraplemnn  12317  sqrt2irrap  12318  qnumgt0  12336  qexpz  12490  4sqlem6  12521  znnen  12555  ennnfoneleminc  12568  exmidunben  12583  mulcncflem  14761  hovercncf  14800  hovera  14801  hoverb  14802  hoverlt1  14803  hovergt0  14804  ivthdichlem  14805  dich0  14806  cosz12  14915  cos02pilt1  14986  ioocosf1o  14989  rplogcl  15014  cxplt  15050  cxple  15051  ltexp2  15074  lgsdilem  15143  gausslemma2dlem1a  15174  lgseisen  15190  lgsquadlem1  15191  refeq  15518  trilpolemeq1  15530  trilpolemlt1  15531  ltlenmkv  15560