Theorem 0red 7468

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

Syntax hints:   → wi 4   ∈ wcel 1438  ℝcr 7328  0cc0 7329

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-1re 7418  ax-addrcl 7421  ax-rnegex 7433

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-cleq 2081  df-clel 2084  df-ral 2364  df-rex 2365

This theorem is referenced by:  gt0ne0  7884  add20  7931  subge0  7932  lesub0  7936  addgt0d  7974  sublt0d  8023  gt0add  8026  apreap  8040  gt0ap0  8078  ap0gt0  8091  prodgt0  8285  prodge0  8287  lt2msq1  8318  lediv12a  8327  ledivp1  8336  squeeze0  8337  mulle0r  8377  nn2ge  8426  0mnnnnn0  8675  elnn0z  8733  rpgecl  9131  ge0p1rp  9134  ledivge1le  9172  iccf1o  9390  elfz1b  9471  elfz0fzfz0  9502  fz0fzelfz0  9503  fzo1fzo0n0  9559  elfzo0z  9560  fzofzim  9564  elfzodifsumelfzo  9577  btwnzge0  9672  modqid  9721  mulqaddmodid  9736  mulp1mod1  9737  modqltm1p1mod  9748  addmodlteq  9770  expgt1  9958  ltexp2a  9972  leexp2a  9973  expnbnd  10042  expnlbnd2  10044  expcanlem  10089  expcan  10090  resqrexlemcalc3  10414  resqrexlemnm  10416  resqrexlemgt0  10418  sqrtgt0  10432  abs00ap  10460  leabs  10472  ltabs  10485  abslt  10486  absle  10487  absgt0ap  10497  climge0  10677  fsumrecl  10758  divcnv  10852  expcnvre  10858  absltap  10864  geolim2  10867  georeclim  10868  geoisumr  10873  cvgratnnlemnexp  10879  cvgratnnlemmn  10880  cvgratnnlemabsle  10882  dvdslelemd  10937  oddge22np1  10974  divalglemnn  11011  divalglemeuneg  11016  lcmgcdlem  11152  dvdsnprmd  11200  sqrt2irraplemnn  11250  sqrt2irrap  11251  qnumgt0  11269  znnen  11304