Theorem 0red 8173

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8024  0cc0 8025

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8119  ax-addrcl 8122  ax-rnegex 8134

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-ral 2513  df-rex 2514

This theorem is referenced by:  gt0ne0  8600  add20  8647  subge0  8648  lesub0  8652  addgt0d  8694  sublt0d  8743  gt0add  8746  apreap  8760  gt0ap0  8799  ap0gt0  8813  lt0ap0  8821  prodgt0  9025  prodge0  9027  lt2msq1  9058  lediv12a  9067  ledivp1  9076  squeeze0  9077  mulle0r  9117  nn2ge  9169  0mnnnnn0  9427  elnn0z  9485  nn0negleid  9541  rpgecl  9910  ge0p1rp  9913  ledivge1le  9954  mul2lt0rlt0  9987  mul2lt0rgt0  9988  mul2lt0np  9991  iccf1o  10232  elfz1b  10318  elfz0fzfz0  10354  fz0fzelfz0  10355  fzo1fzo0n0  10415  elfzo0z  10416  fzofzim  10420  elfzodifsumelfzo  10439  btwnzge0  10553  modqid  10604  mulqaddmodid  10619  mulp1mod1  10620  modqltm1p1mod  10631  addmodlteq  10653  expgt1  10832  ltexp2a  10846  leexp2a  10847  expnbnd  10918  expnlbnd2  10920  zzlesq  10963  nn0ltexp2  10964  expcanlem  10970  expcan  10971  iswrdiz  11113  ccat2s1fvwd  11217  swrdswrdlem  11278  swrdswrd  11279  resqrexlemcalc3  11570  resqrexlemnm  11572  resqrexlemgt0  11574  sqrtgt0  11588  abs00ap  11616  leabs  11628  ltabs  11641  abslt  11642  absle  11643  absgt0ap  11653  rpmaxcl  11777  nn0maxcl  11779  rpmincl  11792  mul0inf  11795  reccn2ap  11867  climge0  11879  fsumrecl  11955  isumlessdc  12050  divcnv  12051  expcnvre  12057  absltap  12063  geolim2  12066  georeclim  12067  geoisumr  12072  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  cvgratnnlemabsle  12081  mertenslem2  12090  cos12dec  12322  p1modz1  12348  dvdslelemd  12397  oddge22np1  12435  divalglemnn  12472  divalglemeuneg  12477  bitsfzolem  12508  bitsinv1lem  12515  lcmgcdlem  12642  dvdsnprmd  12690  isprm5lem  12706  sqrt2irraplemnn  12744  sqrt2irrap  12745  qnumgt0  12763  qexpz  12918  4sqlem6  12949  znnen  13012  ennnfoneleminc  13025  exmidunben  13040  mulcncflem  15324  hovercncf  15363  hovera  15364  hoverb  15365  hoverlt1  15366  hovergt0  15367  ivthdichlem  15368  dich0  15369  cosz12  15497  cos02pilt1  15568  ioocosf1o  15571  rplogcl  15596  cxplt  15633  cxple  15634  ltexp2  15658  mersenne  15714  lgsdilem  15749  gausslemma2dlem1a  15780  lgseisen  15796  lgsquadlem1  15799  lgsquadlem2  15800  refeq  16582  trilpolemeq1  16594  trilpolemlt1  16595  ltlenmkv  16624