Theorem 0red 8334

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

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

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 8280  ax-addrcl 8283  ax-rnegex 8295

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  8763  add20  8810  subge0  8811  lesub0  8815  addgt0d  8857  sublt0d  8907  gt0add  8910  apreap  8924  gt0ap0  8963  ap0gt0  8977  lt0ap0  8985  prodgt0  9191  prodge0  9193  lt2msq1  9224  lediv12a  9233  ledivp1  9242  squeeze0  9243  mulle0r  9283  indfdc  9308  nn2ge  9347  0mnnnnn0  9607  elnn0z  9669  nn0negleid  9725  rpgecl  10101  ge0p1rp  10104  ledivge1le  10145  mul2lt0rlt0  10178  mul2lt0rgt0  10179  mul2lt0np  10182  iccf1o  10425  elfz1b  10515  elfz0fzfz0  10551  fz0fzelfz0  10552  fzo1fzo0n0  10613  elfzo0z  10614  fzofzim  10618  elfzodifsumelfzo  10637  btwnzge0  10757  modqid  10808  mulqaddmodid  10823  mulp1mod1  10824  modqltm1p1mod  10835  addmodlteq  10857  expgt1  11036  ltexp2a  11050  leexp2a  11051  expnbnd  11123  expnlbnd2  11125  zzlesq  11168  nn0ltexp2  11170  expcanlem  11176  expcan  11177  bcm1n  11230  ssenneg  11303  sshashneg  11304  iswrdiz  11334  ccat2s1fvwd  11438  swrdswrdlem  11499  swrdswrd  11500  sq01  11683  resqrexlemcalc3  11805  resqrexlemnm  11807  resqrexlemgt0  11809  sqrtgt0  11823  abs00ap  11851  leabs  11863  ltabs  11877  abslt  11878  absle  11879  absgt0ap  11889  rpmaxcl  12013  nn0maxcl  12015  rpmincl  12029  mul0inf  12033  reccn2ap  12105  climge0  12117  fsumrecl  12194  isumlessdc  12289  divcnv  12290  expcnvre  12296  absltap  12302  geolim2  12305  georeclim  12306  geoisumr  12311  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  cvgratnnlemabsle  12320  mertenslem2  12329  cos12dec  12561  p1modz1  12587  dvdslelemd  12636  oddge22np1  12674  divalglemnn  12711  divalglemeuneg  12716  bitsfzolem  12747  bitsinv1lem  12754  lcmgcdlem  12881  dvdsnprmd  12929  isprm5lem  12946  sqrt2irraplemnn  12985  sqrt2irrap  12986  qnumgt0  13004  sqrtrirr  13015  qexpz  13161  4sqlem6  13192  ballotfilemonn  13280  ballotfilemfc0  13291  ballotfilemfcc  13292  znnen  13348  ennnfoneleminc  13361  exmidunben  13376  mulcncflem  15845  hovercncf  15884  hovera  15885  hoverb  15886  hoverlt1  15887  hovergt0  15888  ivthdichlem  15889  dich0  15890  cosz12  16019  cos02pilt1  16091  ioocosf1o  16094  rplogcl  16121  logdivlt  16136  logdivle  16137  cxplt  16163  cxple  16164  ltexp2  16189  ppiqfi  16254  chtqwordi  16275  ppiqwordi  16280  chtqrpcl  16291  ppiqltx  16293  mersenne  16309  bposlem1  16323  lgsdilem  16363  gausslemma2dlem1a  16394  lgseisen  16410  lgsquadlem1  16413  lgsquadlem2  16414  dichmul0orlem1  16970  dichmul0orlem5  16974  dichmul0orlem6  16975  refeq  17291  trilpolemeq1  17308  trilpolemlt1  17309  ltlenmkv  17339