Theorem 0red 8223

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℝcr 8074  0cc0 8075

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1re 8169  ax-addrcl 8172  ax-rnegex 8184

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2224  df-clel 2227  df-ral 2516  df-rex 2517

This theorem is referenced by:  gt0ne0  8650  add20  8697  subge0  8698  lesub0  8702  addgt0d  8744  sublt0d  8793  gt0add  8796  apreap  8810  gt0ap0  8849  ap0gt0  8863  lt0ap0  8871  prodgt0  9075  prodge0  9077  lt2msq1  9108  lediv12a  9117  ledivp1  9126  squeeze0  9127  mulle0r  9167  nn2ge  9219  0mnnnnn0  9477  elnn0z  9535  nn0negleid  9591  rpgecl  9960  ge0p1rp  9963  ledivge1le  10004  mul2lt0rlt0  10037  mul2lt0rgt0  10038  mul2lt0np  10041  iccf1o  10282  elfz1b  10368  elfz0fzfz0  10404  fz0fzelfz0  10405  fzo1fzo0n0  10466  elfzo0z  10467  fzofzim  10471  elfzodifsumelfzo  10490  btwnzge0  10604  modqid  10655  mulqaddmodid  10670  mulp1mod1  10671  modqltm1p1mod  10682  addmodlteq  10704  expgt1  10883  ltexp2a  10897  leexp2a  10898  expnbnd  10969  expnlbnd2  10971  zzlesq  11014  nn0ltexp2  11015  expcanlem  11021  expcan  11022  iswrdiz  11167  ccat2s1fvwd  11271  swrdswrdlem  11332  swrdswrd  11333  resqrexlemcalc3  11637  resqrexlemnm  11639  resqrexlemgt0  11641  sqrtgt0  11655  abs00ap  11683  leabs  11695  ltabs  11708  abslt  11709  absle  11710  absgt0ap  11720  rpmaxcl  11844  nn0maxcl  11846  rpmincl  11859  mul0inf  11862  reccn2ap  11934  climge0  11946  fsumrecl  12023  isumlessdc  12118  divcnv  12119  expcnvre  12125  absltap  12131  geolim2  12134  georeclim  12135  geoisumr  12140  cvgratnnlemnexp  12146  cvgratnnlemmn  12147  cvgratnnlemabsle  12149  mertenslem2  12158  cos12dec  12390  p1modz1  12416  dvdslelemd  12465  oddge22np1  12503  divalglemnn  12540  divalglemeuneg  12545  bitsfzolem  12576  bitsinv1lem  12583  lcmgcdlem  12710  dvdsnprmd  12758  isprm5lem  12774  sqrt2irraplemnn  12812  sqrt2irrap  12813  qnumgt0  12831  qexpz  12986  4sqlem6  13017  znnen  13080  ennnfoneleminc  13093  exmidunben  13108  mulcncflem  15398  hovercncf  15437  hovera  15438  hoverb  15439  hoverlt1  15440  hovergt0  15441  ivthdichlem  15442  dich0  15443  cosz12  15571  cos02pilt1  15642  ioocosf1o  15645  rplogcl  15670  cxplt  15707  cxple  15708  ltexp2  15732  mersenne  15791  lgsdilem  15826  gausslemma2dlem1a  15857  lgseisen  15873  lgsquadlem1  15876  lgsquadlem2  15877  refeq  16736  trilpolemeq1  16752  trilpolemlt1  16753  ltlenmkv  16783