Theorem 0red 8135

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 7986  0cc0 7987

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8081  ax-addrcl 8084  ax-rnegex 8096

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-ral 2513  df-rex 2514

This theorem is referenced by:  gt0ne0  8562  add20  8609  subge0  8610  lesub0  8614  addgt0d  8656  sublt0d  8705  gt0add  8708  apreap  8722  gt0ap0  8761  ap0gt0  8775  lt0ap0  8783  prodgt0  8987  prodge0  8989  lt2msq1  9020  lediv12a  9029  ledivp1  9038  squeeze0  9039  mulle0r  9079  nn2ge  9131  0mnnnnn0  9389  elnn0z  9447  nn0negleid  9503  rpgecl  9866  ge0p1rp  9869  ledivge1le  9910  mul2lt0rlt0  9943  mul2lt0rgt0  9944  mul2lt0np  9947  iccf1o  10188  elfz1b  10274  elfz0fzfz0  10310  fz0fzelfz0  10311  fzo1fzo0n0  10371  elfzo0z  10372  fzofzim  10376  elfzodifsumelfzo  10394  btwnzge0  10507  modqid  10558  mulqaddmodid  10573  mulp1mod1  10574  modqltm1p1mod  10585  addmodlteq  10607  expgt1  10786  ltexp2a  10800  leexp2a  10801  expnbnd  10872  expnlbnd2  10874  zzlesq  10917  nn0ltexp2  10918  expcanlem  10924  expcan  10925  iswrdiz  11065  swrdswrdlem  11222  swrdswrd  11223  resqrexlemcalc3  11513  resqrexlemnm  11515  resqrexlemgt0  11517  sqrtgt0  11531  abs00ap  11559  leabs  11571  ltabs  11584  abslt  11585  absle  11586  absgt0ap  11596  rpmaxcl  11720  nn0maxcl  11722  rpmincl  11735  mul0inf  11738  reccn2ap  11810  climge0  11822  fsumrecl  11898  isumlessdc  11993  divcnv  11994  expcnvre  12000  absltap  12006  geolim2  12009  georeclim  12010  geoisumr  12015  cvgratnnlemnexp  12021  cvgratnnlemmn  12022  cvgratnnlemabsle  12024  mertenslem2  12033  cos12dec  12265  p1modz1  12291  dvdslelemd  12340  oddge22np1  12378  divalglemnn  12415  divalglemeuneg  12420  bitsfzolem  12451  bitsinv1lem  12458  lcmgcdlem  12585  dvdsnprmd  12633  isprm5lem  12649  sqrt2irraplemnn  12687  sqrt2irrap  12688  qnumgt0  12706  qexpz  12861  4sqlem6  12892  znnen  12955  ennnfoneleminc  12968  exmidunben  12983  mulcncflem  15266  hovercncf  15305  hovera  15306  hoverb  15307  hoverlt1  15308  hovergt0  15309  ivthdichlem  15310  dich0  15311  cosz12  15439  cos02pilt1  15510  ioocosf1o  15513  rplogcl  15538  cxplt  15575  cxple  15576  ltexp2  15600  mersenne  15656  lgsdilem  15691  gausslemma2dlem1a  15722  lgseisen  15738  lgsquadlem1  15741  lgsquadlem2  15742  refeq  16327  trilpolemeq1  16339  trilpolemlt1  16340  ltlenmkv  16369