Theorem 0red 8086

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℝcr 7937  0cc0 7938

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-1re 8032  ax-addrcl 8035  ax-rnegex 8047

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-cleq 2199  df-clel 2202  df-ral 2490  df-rex 2491

This theorem is referenced by:  gt0ne0  8513  add20  8560  subge0  8561  lesub0  8565  addgt0d  8607  sublt0d  8656  gt0add  8659  apreap  8673  gt0ap0  8712  ap0gt0  8726  lt0ap0  8734  prodgt0  8938  prodge0  8940  lt2msq1  8971  lediv12a  8980  ledivp1  8989  squeeze0  8990  mulle0r  9030  nn2ge  9082  0mnnnnn0  9340  elnn0z  9398  nn0negleid  9454  rpgecl  9817  ge0p1rp  9820  ledivge1le  9861  mul2lt0rlt0  9894  mul2lt0rgt0  9895  mul2lt0np  9898  iccf1o  10139  elfz1b  10225  elfz0fzfz0  10261  fz0fzelfz0  10262  fzo1fzo0n0  10320  elfzo0z  10321  fzofzim  10325  elfzodifsumelfzo  10343  btwnzge0  10456  modqid  10507  mulqaddmodid  10522  mulp1mod1  10523  modqltm1p1mod  10534  addmodlteq  10556  expgt1  10735  ltexp2a  10749  leexp2a  10750  expnbnd  10821  expnlbnd2  10823  zzlesq  10866  nn0ltexp2  10867  expcanlem  10873  expcan  10874  iswrdiz  11014  swrdswrdlem  11169  swrdswrd  11170  resqrexlemcalc3  11377  resqrexlemnm  11379  resqrexlemgt0  11381  sqrtgt0  11395  abs00ap  11423  leabs  11435  ltabs  11448  abslt  11449  absle  11450  absgt0ap  11460  rpmaxcl  11584  nn0maxcl  11586  rpmincl  11599  mul0inf  11602  reccn2ap  11674  climge0  11686  fsumrecl  11762  isumlessdc  11857  divcnv  11858  expcnvre  11864  absltap  11870  geolim2  11873  georeclim  11874  geoisumr  11879  cvgratnnlemnexp  11885  cvgratnnlemmn  11886  cvgratnnlemabsle  11888  mertenslem2  11897  cos12dec  12129  p1modz1  12155  dvdslelemd  12204  oddge22np1  12242  divalglemnn  12279  divalglemeuneg  12284  bitsfzolem  12315  bitsinv1lem  12322  lcmgcdlem  12449  dvdsnprmd  12497  isprm5lem  12513  sqrt2irraplemnn  12551  sqrt2irrap  12552  qnumgt0  12570  qexpz  12725  4sqlem6  12756  znnen  12819  ennnfoneleminc  12832  exmidunben  12847  mulcncflem  15129  hovercncf  15168  hovera  15169  hoverb  15170  hoverlt1  15171  hovergt0  15172  ivthdichlem  15173  dich0  15174  cosz12  15302  cos02pilt1  15373  ioocosf1o  15376  rplogcl  15401  cxplt  15438  cxple  15439  ltexp2  15463  mersenne  15519  lgsdilem  15554  gausslemma2dlem1a  15585  lgseisen  15601  lgsquadlem1  15604  lgsquadlem2  15605  refeq  16082  trilpolemeq1  16094  trilpolemlt1  16095  ltlenmkv  16124