Theorem 0red 8321

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℝcr 8172  0cc0 8173

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8267  ax-addrcl 8270  ax-rnegex 8282

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-ral 2533  df-rex 2534

This theorem is referenced by:  gt0ne0  8749  add20  8796  subge0  8797  lesub0  8801  addgt0d  8843  sublt0d  8892  gt0add  8895  apreap  8909  gt0ap0  8948  ap0gt0  8962  lt0ap0  8970  prodgt0  9176  prodge0  9178  lt2msq1  9209  lediv12a  9218  ledivp1  9227  squeeze0  9228  mulle0r  9268  nn2ge  9320  0mnnnnn0  9578  elnn0z  9640  nn0negleid  9696  rpgecl  10066  ge0p1rp  10069  ledivge1le  10110  mul2lt0rlt0  10143  mul2lt0rgt0  10144  mul2lt0np  10147  iccf1o  10390  elfz1b  10480  elfz0fzfz0  10516  fz0fzelfz0  10517  fzo1fzo0n0  10578  elfzo0z  10579  fzofzim  10583  elfzodifsumelfzo  10602  btwnzge0  10718  modqid  10769  mulqaddmodid  10784  mulp1mod1  10785  modqltm1p1mod  10796  addmodlteq  10818  expgt1  10997  ltexp2a  11011  leexp2a  11012  expnbnd  11084  expnlbnd2  11086  zzlesq  11129  nn0ltexp2  11130  expcanlem  11136  expcan  11137  bcm1n  11190  ssenneg  11263  sshashneg  11264  iswrdiz  11294  ccat2s1fvwd  11398  swrdswrdlem  11459  swrdswrd  11460  sq01  11643  resqrexlemcalc3  11765  resqrexlemnm  11767  resqrexlemgt0  11769  sqrtgt0  11783  abs00ap  11811  leabs  11823  ltabs  11836  abslt  11837  absle  11838  absgt0ap  11848  rpmaxcl  11972  nn0maxcl  11974  rpmincl  11987  mul0inf  11990  reccn2ap  12062  climge0  12074  fsumrecl  12151  isumlessdc  12246  divcnv  12247  expcnvre  12253  absltap  12259  geolim2  12262  georeclim  12263  geoisumr  12268  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  cvgratnnlemabsle  12277  mertenslem2  12286  cos12dec  12518  p1modz1  12544  dvdslelemd  12593  oddge22np1  12631  divalglemnn  12668  divalglemeuneg  12673  bitsfzolem  12704  bitsinv1lem  12711  lcmgcdlem  12838  dvdsnprmd  12886  isprm5lem  12902  sqrt2irraplemnn  12940  sqrt2irrap  12941  qnumgt0  12959  qexpz  13114  4sqlem6  13145  ballotfilemonn  13204  ballotfilemfc0  13215  ballotfilemfcc  13216  znnen  13272  ennnfoneleminc  13285  exmidunben  13300  mulcncflem  15691  hovercncf  15730  hovera  15731  hoverb  15732  hoverlt1  15733  hovergt0  15734  ivthdichlem  15735  dich0  15736  cosz12  15864  cos02pilt1  15935  ioocosf1o  15938  rplogcl  15963  cxplt  16001  cxple  16002  ltexp2  16026  mersenne  16094  lgsdilem  16129  gausslemma2dlem1a  16160  lgseisen  16176  lgsquadlem1  16179  lgsquadlem2  16180  dichmul0orlem1  16736  dichmul0orlem5  16740  dichmul0orlem6  16741  refeq  17047  trilpolemeq1  17063  trilpolemlt1  17064  ltlenmkv  17094