Theorem 0red 7791

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

Syntax hints:   → wi 4   ∈ wcel 1481  ℝcr 7643  0cc0 7644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-1re 7738  ax-addrcl 7741  ax-rnegex 7753

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-cleq 2133  df-clel 2136  df-ral 2422  df-rex 2423

This theorem is referenced by:  gt0ne0  8213  add20  8260  subge0  8261  lesub0  8265  addgt0d  8307  sublt0d  8356  gt0add  8359  apreap  8373  gt0ap0  8412  ap0gt0  8426  lt0ap0  8434  prodgt0  8634  prodge0  8636  lt2msq1  8667  lediv12a  8676  ledivp1  8685  squeeze0  8686  mulle0r  8726  nn2ge  8777  0mnnnnn0  9033  elnn0z  9091  rpgecl  9499  ge0p1rp  9502  ledivge1le  9543  mul2lt0rlt0  9576  mul2lt0rgt0  9577  mul2lt0np  9580  iccf1o  9817  elfz1b  9901  elfz0fzfz0  9934  fz0fzelfz0  9935  fzo1fzo0n0  9991  elfzo0z  9992  fzofzim  9996  elfzodifsumelfzo  10009  btwnzge0  10104  modqid  10153  mulqaddmodid  10168  mulp1mod1  10169  modqltm1p1mod  10180  addmodlteq  10202  expgt1  10362  ltexp2a  10376  leexp2a  10377  expnbnd  10446  expnlbnd2  10448  expcanlem  10493  expcan  10494  resqrexlemcalc3  10820  resqrexlemnm  10822  resqrexlemgt0  10824  sqrtgt0  10838  abs00ap  10866  leabs  10878  ltabs  10891  abslt  10892  absle  10893  absgt0ap  10903  rpmaxcl  11027  rpmincl  11041  mul0inf  11044  reccn2ap  11114  climge0  11126  fsumrecl  11202  isumlessdc  11297  divcnv  11298  expcnvre  11304  absltap  11310  geolim2  11313  georeclim  11314  geoisumr  11319  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratnnlemabsle  11328  mertenslem2  11337  cos12dec  11510  dvdslelemd  11577  oddge22np1  11614  divalglemnn  11651  divalglemeuneg  11656  lcmgcdlem  11794  dvdsnprmd  11842  sqrt2irraplemnn  11893  sqrt2irrap  11894  qnumgt0  11912  znnen  11947  ennnfoneleminc  11960  exmidunben  11975  mulcncflem  12798  cosz12  12909  cos02pilt1  12980  ioocosf1o  12983  rplogcl  13008  cxplt  13044  cxple  13045  refeq  13398  trilpolemeq1  13408  trilpolemlt1  13409