Theorem 0red 7900

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℝcr 7752  0cc0 7753

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1re 7847  ax-addrcl 7850  ax-rnegex 7862

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-cleq 2158  df-clel 2161  df-ral 2449  df-rex 2450

This theorem is referenced by:  gt0ne0  8325  add20  8372  subge0  8373  lesub0  8377  addgt0d  8419  sublt0d  8468  gt0add  8471  apreap  8485  gt0ap0  8524  ap0gt0  8538  lt0ap0  8546  prodgt0  8747  prodge0  8749  lt2msq1  8780  lediv12a  8789  ledivp1  8798  squeeze0  8799  mulle0r  8839  nn2ge  8890  0mnnnnn0  9146  elnn0z  9204  nn0negleid  9259  rpgecl  9618  ge0p1rp  9621  ledivge1le  9662  mul2lt0rlt0  9695  mul2lt0rgt0  9696  mul2lt0np  9699  iccf1o  9940  elfz1b  10025  elfz0fzfz0  10061  fz0fzelfz0  10062  fzo1fzo0n0  10118  elfzo0z  10119  fzofzim  10123  elfzodifsumelfzo  10136  btwnzge0  10235  modqid  10284  mulqaddmodid  10299  mulp1mod1  10300  modqltm1p1mod  10311  addmodlteq  10333  expgt1  10493  ltexp2a  10507  leexp2a  10508  expnbnd  10578  expnlbnd2  10580  nn0ltexp2  10623  expcanlem  10628  expcan  10629  resqrexlemcalc3  10958  resqrexlemnm  10960  resqrexlemgt0  10962  sqrtgt0  10976  abs00ap  11004  leabs  11016  ltabs  11029  abslt  11030  absle  11031  absgt0ap  11041  rpmaxcl  11165  rpmincl  11179  mul0inf  11182  reccn2ap  11254  climge0  11266  fsumrecl  11342  isumlessdc  11437  divcnv  11438  expcnvre  11444  absltap  11450  geolim2  11453  georeclim  11454  geoisumr  11459  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemabsle  11468  mertenslem2  11477  cos12dec  11708  p1modz1  11734  dvdslelemd  11781  oddge22np1  11818  divalglemnn  11855  divalglemeuneg  11860  lcmgcdlem  12009  dvdsnprmd  12057  isprm5lem  12073  sqrt2irraplemnn  12111  sqrt2irrap  12112  qnumgt0  12130  qexpz  12282  4sqlem6  12313  znnen  12331  ennnfoneleminc  12344  exmidunben  12359  mulcncflem  13230  cosz12  13341  cos02pilt1  13412  ioocosf1o  13415  rplogcl  13440  cxplt  13476  cxple  13477  ltexp2  13500  lgsdilem  13568  refeq  13907  trilpolemeq1  13919  trilpolemlt1  13920