Theorem 0red 8163

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8014  0cc0 8015

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 8109  ax-addrcl 8112  ax-rnegex 8124

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  8590  add20  8637  subge0  8638  lesub0  8642  addgt0d  8684  sublt0d  8733  gt0add  8736  apreap  8750  gt0ap0  8789  ap0gt0  8803  lt0ap0  8811  prodgt0  9015  prodge0  9017  lt2msq1  9048  lediv12a  9057  ledivp1  9066  squeeze0  9067  mulle0r  9107  nn2ge  9159  0mnnnnn0  9417  elnn0z  9475  nn0negleid  9531  rpgecl  9895  ge0p1rp  9898  ledivge1le  9939  mul2lt0rlt0  9972  mul2lt0rgt0  9973  mul2lt0np  9976  iccf1o  10217  elfz1b  10303  elfz0fzfz0  10339  fz0fzelfz0  10340  fzo1fzo0n0  10400  elfzo0z  10401  fzofzim  10405  elfzodifsumelfzo  10424  btwnzge0  10537  modqid  10588  mulqaddmodid  10603  mulp1mod1  10604  modqltm1p1mod  10615  addmodlteq  10637  expgt1  10816  ltexp2a  10830  leexp2a  10831  expnbnd  10902  expnlbnd2  10904  zzlesq  10947  nn0ltexp2  10948  expcanlem  10954  expcan  10955  iswrdiz  11096  swrdswrdlem  11257  swrdswrd  11258  resqrexlemcalc3  11548  resqrexlemnm  11550  resqrexlemgt0  11552  sqrtgt0  11566  abs00ap  11594  leabs  11606  ltabs  11619  abslt  11620  absle  11621  absgt0ap  11631  rpmaxcl  11755  nn0maxcl  11757  rpmincl  11770  mul0inf  11773  reccn2ap  11845  climge0  11857  fsumrecl  11933  isumlessdc  12028  divcnv  12029  expcnvre  12035  absltap  12041  geolim2  12044  georeclim  12045  geoisumr  12050  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  cvgratnnlemabsle  12059  mertenslem2  12068  cos12dec  12300  p1modz1  12326  dvdslelemd  12375  oddge22np1  12413  divalglemnn  12450  divalglemeuneg  12455  bitsfzolem  12486  bitsinv1lem  12493  lcmgcdlem  12620  dvdsnprmd  12668  isprm5lem  12684  sqrt2irraplemnn  12722  sqrt2irrap  12723  qnumgt0  12741  qexpz  12896  4sqlem6  12927  znnen  12990  ennnfoneleminc  13003  exmidunben  13018  mulcncflem  15302  hovercncf  15341  hovera  15342  hoverb  15343  hoverlt1  15344  hovergt0  15345  ivthdichlem  15346  dich0  15347  cosz12  15475  cos02pilt1  15546  ioocosf1o  15549  rplogcl  15574  cxplt  15611  cxple  15612  ltexp2  15636  mersenne  15692  lgsdilem  15727  gausslemma2dlem1a  15758  lgseisen  15774  lgsquadlem1  15777  lgsquadlem2  15778  refeq  16510  trilpolemeq1  16522  trilpolemlt1  16523  ltlenmkv  16552