Theorem 0red 8027

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 8026	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 9	1 ⊢ (𝜑 → 0 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2167  ℝcr 7878  0cc0 7879

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7973  ax-addrcl 7976  ax-rnegex 7988

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-cleq 2189  df-clel 2192  df-ral 2480  df-rex 2481

This theorem is referenced by:  gt0ne0  8454  add20  8501  subge0  8502  lesub0  8506  addgt0d  8548  sublt0d  8597  gt0add  8600  apreap  8614  gt0ap0  8653  ap0gt0  8667  lt0ap0  8675  prodgt0  8879  prodge0  8881  lt2msq1  8912  lediv12a  8921  ledivp1  8930  squeeze0  8931  mulle0r  8971  nn2ge  9023  0mnnnnn0  9281  elnn0z  9339  nn0negleid  9394  rpgecl  9757  ge0p1rp  9760  ledivge1le  9801  mul2lt0rlt0  9834  mul2lt0rgt0  9835  mul2lt0np  9838  iccf1o  10079  elfz1b  10165  elfz0fzfz0  10201  fz0fzelfz0  10202  fzo1fzo0n0  10259  elfzo0z  10260  fzofzim  10264  elfzodifsumelfzo  10277  btwnzge0  10390  modqid  10441  mulqaddmodid  10456  mulp1mod1  10457  modqltm1p1mod  10468  addmodlteq  10490  expgt1  10669  ltexp2a  10683  leexp2a  10684  expnbnd  10755  expnlbnd2  10757  zzlesq  10800  nn0ltexp2  10801  expcanlem  10807  expcan  10808  iswrdiz  10942  resqrexlemcalc3  11181  resqrexlemnm  11183  resqrexlemgt0  11185  sqrtgt0  11199  abs00ap  11227  leabs  11239  ltabs  11252  abslt  11253  absle  11254  absgt0ap  11264  rpmaxcl  11388  nn0maxcl  11390  rpmincl  11403  mul0inf  11406  reccn2ap  11478  climge0  11490  fsumrecl  11566  isumlessdc  11661  divcnv  11662  expcnvre  11668  absltap  11674  geolim2  11677  georeclim  11678  geoisumr  11683  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemabsle  11692  mertenslem2  11701  cos12dec  11933  p1modz1  11959  dvdslelemd  12008  oddge22np1  12046  divalglemnn  12083  divalglemeuneg  12088  bitsfzolem  12118  lcmgcdlem  12245  dvdsnprmd  12293  isprm5lem  12309  sqrt2irraplemnn  12347  sqrt2irrap  12348  qnumgt0  12366  qexpz  12521  4sqlem6  12552  znnen  12615  ennnfoneleminc  12628  exmidunben  12643  mulcncflem  14843  hovercncf  14882  hovera  14883  hoverb  14884  hoverlt1  14885  hovergt0  14886  ivthdichlem  14887  dich0  14888  cosz12  15016  cos02pilt1  15087  ioocosf1o  15090  rplogcl  15115  cxplt  15152  cxple  15153  ltexp2  15177  mersenne  15233  lgsdilem  15268  gausslemma2dlem1a  15299  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  refeq  15672  trilpolemeq1  15684  trilpolemlt1  15685  ltlenmkv  15714