Theorem 0red 8328

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℝcr 8179  0cc0 8180

This proof depends on 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 8274  ax-addrcl 8277  ax-rnegex 8289

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

This theorem is used by:  gt0ne0  8757  add20  8804  subge0  8805  lesub0  8809  addgt0d  8851  sublt0d  8901  gt0add  8904  apreap  8918  gt0ap0  8957  ap0gt0  8971  lt0ap0  8979  prodgt0  9185  prodge0  9187  lt2msq1  9218  lediv12a  9227  ledivp1  9236  squeeze0  9237  mulle0r  9277  indfdc  9301  nn2ge  9340  0mnnnnn0  9600  elnn0z  9662  nn0negleid  9718  rpgecl  10094  ge0p1rp  10097  ledivge1le  10138  mul2lt0rlt0  10171  mul2lt0rgt0  10172  mul2lt0np  10175  iccf1o  10418  elfz1b  10508  elfz0fzfz0  10544  fz0fzelfz0  10545  fzo1fzo0n0  10606  elfzo0z  10607  fzofzim  10611  elfzodifsumelfzo  10630  btwnzge0  10749  modqid  10800  mulqaddmodid  10815  mulp1mod1  10816  modqltm1p1mod  10827  addmodlteq  10849  expgt1  11028  ltexp2a  11042  leexp2a  11043  expnbnd  11115  expnlbnd2  11117  zzlesq  11160  nn0ltexp2  11162  expcanlem  11168  expcan  11169  bcm1n  11222  ssenneg  11295  sshashneg  11296  iswrdiz  11326  ccat2s1fvwd  11430  swrdswrdlem  11491  swrdswrd  11492  sq01  11675  resqrexlemcalc3  11797  resqrexlemnm  11799  resqrexlemgt0  11801  sqrtgt0  11815  abs00ap  11843  leabs  11855  ltabs  11869  abslt  11870  absle  11871  absgt0ap  11881  rpmaxcl  12005  nn0maxcl  12007  rpmincl  12021  mul0inf  12025  reccn2ap  12097  climge0  12109  fsumrecl  12186  isumlessdc  12281  divcnv  12282  expcnvre  12288  absltap  12294  geolim2  12297  georeclim  12298  geoisumr  12303  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  cvgratnnlemabsle  12312  mertenslem2  12321  cos12dec  12553  p1modz1  12579  dvdslelemd  12628  oddge22np1  12666  divalglemnn  12703  divalglemeuneg  12708  bitsfzolem  12739  bitsinv1lem  12746  lcmgcdlem  12873  dvdsnprmd  12921  isprm5lem  12938  sqrt2irraplemnn  12977  sqrt2irrap  12978  qnumgt0  12996  sqrtrirr  13007  qexpz  13153  4sqlem6  13184  ballotfilemonn  13272  ballotfilemfc0  13283  ballotfilemfcc  13284  znnen  13340  ennnfoneleminc  13353  exmidunben  13368  mulcncflem  15760  hovercncf  15799  hovera  15800  hoverb  15801  hoverlt1  15802  hovergt0  15803  ivthdichlem  15804  dich0  15805  cosz12  15934  cos02pilt1  16005  ioocosf1o  16008  rplogcl  16034  logdivlt  16049  logdivle  16050  cxplt  16074  cxple  16075  ltexp2  16099  ppiqfi  16164  chtqwordi  16185  ppiqwordi  16190  chtqrpcl  16201  ppiqltx  16203  mersenne  16219  bposlem1  16233  lgsdilem  16268  gausslemma2dlem1a  16299  lgseisen  16315  lgsquadlem1  16318  lgsquadlem2  16319  dichmul0orlem1  16875  dichmul0orlem5  16879  dichmul0orlem6  16880  refeq  17195  trilpolemeq1  17211  trilpolemlt1  17212  ltlenmkv  17242