Theorem 0red 8327

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

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

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 8273  ax-addrcl 8276  ax-rnegex 8288

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  8755  add20  8802  subge0  8803  lesub0  8807  addgt0d  8849  sublt0d  8899  gt0add  8902  apreap  8916  gt0ap0  8955  ap0gt0  8969  lt0ap0  8977  prodgt0  9183  prodge0  9185  lt2msq1  9216  lediv12a  9225  ledivp1  9234  squeeze0  9235  mulle0r  9275  indfdc  9299  nn2ge  9338  0mnnnnn0  9597  elnn0z  9659  nn0negleid  9715  rpgecl  10085  ge0p1rp  10088  ledivge1le  10129  mul2lt0rlt0  10162  mul2lt0rgt0  10163  mul2lt0np  10166  iccf1o  10409  elfz1b  10499  elfz0fzfz0  10535  fz0fzelfz0  10536  fzo1fzo0n0  10597  elfzo0z  10598  fzofzim  10602  elfzodifsumelfzo  10621  btwnzge0  10737  modqid  10788  mulqaddmodid  10803  mulp1mod1  10804  modqltm1p1mod  10815  addmodlteq  10837  expgt1  11016  ltexp2a  11030  leexp2a  11031  expnbnd  11103  expnlbnd2  11105  zzlesq  11148  nn0ltexp2  11149  expcanlem  11155  expcan  11156  bcm1n  11209  ssenneg  11282  sshashneg  11283  iswrdiz  11313  ccat2s1fvwd  11417  swrdswrdlem  11478  swrdswrd  11479  sq01  11662  resqrexlemcalc3  11784  resqrexlemnm  11786  resqrexlemgt0  11788  sqrtgt0  11802  abs00ap  11830  leabs  11842  ltabs  11855  abslt  11856  absle  11857  absgt0ap  11867  rpmaxcl  11991  nn0maxcl  11993  rpmincl  12006  mul0inf  12009  reccn2ap  12081  climge0  12093  fsumrecl  12170  isumlessdc  12265  divcnv  12266  expcnvre  12272  absltap  12278  geolim2  12281  georeclim  12282  geoisumr  12287  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  cvgratnnlemabsle  12296  mertenslem2  12305  cos12dec  12537  p1modz1  12563  dvdslelemd  12612  oddge22np1  12650  divalglemnn  12687  divalglemeuneg  12692  bitsfzolem  12723  bitsinv1lem  12730  lcmgcdlem  12857  dvdsnprmd  12905  isprm5lem  12921  sqrt2irraplemnn  12959  sqrt2irrap  12960  qnumgt0  12978  qexpz  13133  4sqlem6  13164  ballotfilemonn  13223  ballotfilemfc0  13234  ballotfilemfcc  13235  znnen  13291  ennnfoneleminc  13304  exmidunben  13319  mulcncflem  15710  hovercncf  15749  hovera  15750  hoverb  15751  hoverlt1  15752  hovergt0  15753  ivthdichlem  15754  dich0  15755  cosz12  15884  cos02pilt1  15955  ioocosf1o  15958  rplogcl  15984  logdivlt  15999  logdivle  16000  cxplt  16024  cxple  16025  ltexp2  16049  mersenne  16117  lgsdilem  16158  gausslemma2dlem1a  16189  lgseisen  16205  lgsquadlem1  16208  lgsquadlem2  16209  dichmul0orlem1  16765  dichmul0orlem5  16769  dichmul0orlem6  16770  refeq  17085  trilpolemeq1  17101  trilpolemlt1  17102  ltlenmkv  17132