Theorem 0red 7958

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℝcr 7810  0cc0 7811

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7905  ax-addrcl 7908  ax-rnegex 7920

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-cleq 2170  df-clel 2173  df-ral 2460  df-rex 2461

This theorem is referenced by:  gt0ne0  8384  add20  8431  subge0  8432  lesub0  8436  addgt0d  8478  sublt0d  8527  gt0add  8530  apreap  8544  gt0ap0  8583  ap0gt0  8597  lt0ap0  8605  prodgt0  8809  prodge0  8811  lt2msq1  8842  lediv12a  8851  ledivp1  8860  squeeze0  8861  mulle0r  8901  nn2ge  8952  0mnnnnn0  9208  elnn0z  9266  nn0negleid  9321  rpgecl  9682  ge0p1rp  9685  ledivge1le  9726  mul2lt0rlt0  9759  mul2lt0rgt0  9760  mul2lt0np  9763  iccf1o  10004  elfz1b  10090  elfz0fzfz0  10126  fz0fzelfz0  10127  fzo1fzo0n0  10183  elfzo0z  10184  fzofzim  10188  elfzodifsumelfzo  10201  btwnzge0  10300  modqid  10349  mulqaddmodid  10364  mulp1mod1  10365  modqltm1p1mod  10376  addmodlteq  10398  expgt1  10558  ltexp2a  10572  leexp2a  10573  expnbnd  10644  expnlbnd2  10646  nn0ltexp2  10689  expcanlem  10695  expcan  10696  resqrexlemcalc3  11025  resqrexlemnm  11027  resqrexlemgt0  11029  sqrtgt0  11043  abs00ap  11071  leabs  11083  ltabs  11096  abslt  11097  absle  11098  absgt0ap  11108  rpmaxcl  11232  rpmincl  11246  mul0inf  11249  reccn2ap  11321  climge0  11333  fsumrecl  11409  isumlessdc  11504  divcnv  11505  expcnvre  11511  absltap  11517  geolim2  11520  georeclim  11521  geoisumr  11526  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratnnlemabsle  11535  mertenslem2  11544  cos12dec  11775  p1modz1  11801  dvdslelemd  11849  oddge22np1  11886  divalglemnn  11923  divalglemeuneg  11928  lcmgcdlem  12077  dvdsnprmd  12125  isprm5lem  12141  sqrt2irraplemnn  12179  sqrt2irrap  12180  qnumgt0  12198  qexpz  12350  4sqlem6  12381  znnen  12399  ennnfoneleminc  12412  exmidunben  12427  mulcncflem  14093  cosz12  14204  cos02pilt1  14275  ioocosf1o  14278  rplogcl  14303  cxplt  14339  cxple  14340  ltexp2  14363  lgsdilem  14431  refeq  14779  trilpolemeq1  14791  trilpolemlt1  14792  ltlenmkv  14820