Theorem 0red 8046

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℝcr 7897  0cc0 7898

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 7992  ax-addrcl 7995  ax-rnegex 8007

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  8473  add20  8520  subge0  8521  lesub0  8525  addgt0d  8567  sublt0d  8616  gt0add  8619  apreap  8633  gt0ap0  8672  ap0gt0  8686  lt0ap0  8694  prodgt0  8898  prodge0  8900  lt2msq1  8931  lediv12a  8940  ledivp1  8949  squeeze0  8950  mulle0r  8990  nn2ge  9042  0mnnnnn0  9300  elnn0z  9358  nn0negleid  9413  rpgecl  9776  ge0p1rp  9779  ledivge1le  9820  mul2lt0rlt0  9853  mul2lt0rgt0  9854  mul2lt0np  9857  iccf1o  10098  elfz1b  10184  elfz0fzfz0  10220  fz0fzelfz0  10221  fzo1fzo0n0  10278  elfzo0z  10279  fzofzim  10283  elfzodifsumelfzo  10296  btwnzge0  10409  modqid  10460  mulqaddmodid  10475  mulp1mod1  10476  modqltm1p1mod  10487  addmodlteq  10509  expgt1  10688  ltexp2a  10702  leexp2a  10703  expnbnd  10774  expnlbnd2  10776  zzlesq  10819  nn0ltexp2  10820  expcanlem  10826  expcan  10827  iswrdiz  10961  resqrexlemcalc3  11200  resqrexlemnm  11202  resqrexlemgt0  11204  sqrtgt0  11218  abs00ap  11246  leabs  11258  ltabs  11271  abslt  11272  absle  11273  absgt0ap  11283  rpmaxcl  11407  nn0maxcl  11409  rpmincl  11422  mul0inf  11425  reccn2ap  11497  climge0  11509  fsumrecl  11585  isumlessdc  11680  divcnv  11681  expcnvre  11687  absltap  11693  geolim2  11696  georeclim  11697  geoisumr  11702  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  cvgratnnlemabsle  11711  mertenslem2  11720  cos12dec  11952  p1modz1  11978  dvdslelemd  12027  oddge22np1  12065  divalglemnn  12102  divalglemeuneg  12107  bitsfzolem  12138  bitsinv1lem  12145  lcmgcdlem  12272  dvdsnprmd  12320  isprm5lem  12336  sqrt2irraplemnn  12374  sqrt2irrap  12375  qnumgt0  12393  qexpz  12548  4sqlem6  12579  znnen  12642  ennnfoneleminc  12655  exmidunben  12670  mulcncflem  14951  hovercncf  14990  hovera  14991  hoverb  14992  hoverlt1  14993  hovergt0  14994  ivthdichlem  14995  dich0  14996  cosz12  15124  cos02pilt1  15195  ioocosf1o  15198  rplogcl  15223  cxplt  15260  cxple  15261  ltexp2  15285  mersenne  15341  lgsdilem  15376  gausslemma2dlem1a  15407  lgseisen  15423  lgsquadlem1  15426  lgsquadlem2  15427  refeq  15785  trilpolemeq1  15797  trilpolemlt1  15798  ltlenmkv  15827