Theorem 0red 8155

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℝcr 8006  0cc0 8007

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 8101  ax-addrcl 8104  ax-rnegex 8116

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  8582  add20  8629  subge0  8630  lesub0  8634  addgt0d  8676  sublt0d  8725  gt0add  8728  apreap  8742  gt0ap0  8781  ap0gt0  8795  lt0ap0  8803  prodgt0  9007  prodge0  9009  lt2msq1  9040  lediv12a  9049  ledivp1  9058  squeeze0  9059  mulle0r  9099  nn2ge  9151  0mnnnnn0  9409  elnn0z  9467  nn0negleid  9523  rpgecl  9886  ge0p1rp  9889  ledivge1le  9930  mul2lt0rlt0  9963  mul2lt0rgt0  9964  mul2lt0np  9967  iccf1o  10208  elfz1b  10294  elfz0fzfz0  10330  fz0fzelfz0  10331  fzo1fzo0n0  10391  elfzo0z  10392  fzofzim  10396  elfzodifsumelfzo  10415  btwnzge0  10528  modqid  10579  mulqaddmodid  10594  mulp1mod1  10595  modqltm1p1mod  10606  addmodlteq  10628  expgt1  10807  ltexp2a  10821  leexp2a  10822  expnbnd  10893  expnlbnd2  10895  zzlesq  10938  nn0ltexp2  10939  expcanlem  10945  expcan  10946  iswrdiz  11086  swrdswrdlem  11244  swrdswrd  11245  resqrexlemcalc3  11535  resqrexlemnm  11537  resqrexlemgt0  11539  sqrtgt0  11553  abs00ap  11581  leabs  11593  ltabs  11606  abslt  11607  absle  11608  absgt0ap  11618  rpmaxcl  11742  nn0maxcl  11744  rpmincl  11757  mul0inf  11760  reccn2ap  11832  climge0  11844  fsumrecl  11920  isumlessdc  12015  divcnv  12016  expcnvre  12022  absltap  12028  geolim2  12031  georeclim  12032  geoisumr  12037  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  cvgratnnlemabsle  12046  mertenslem2  12055  cos12dec  12287  p1modz1  12313  dvdslelemd  12362  oddge22np1  12400  divalglemnn  12437  divalglemeuneg  12442  bitsfzolem  12473  bitsinv1lem  12480  lcmgcdlem  12607  dvdsnprmd  12655  isprm5lem  12671  sqrt2irraplemnn  12709  sqrt2irrap  12710  qnumgt0  12728  qexpz  12883  4sqlem6  12914  znnen  12977  ennnfoneleminc  12990  exmidunben  13005  mulcncflem  15289  hovercncf  15328  hovera  15329  hoverb  15330  hoverlt1  15331  hovergt0  15332  ivthdichlem  15333  dich0  15334  cosz12  15462  cos02pilt1  15533  ioocosf1o  15536  rplogcl  15561  cxplt  15598  cxple  15599  ltexp2  15623  mersenne  15679  lgsdilem  15714  gausslemma2dlem1a  15745  lgseisen  15761  lgsquadlem1  15764  lgsquadlem2  15765  refeq  16426  trilpolemeq1  16438  trilpolemlt1  16439  ltlenmkv  16468