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  9667  nn0negleid  9723  rpgecl  10100  ge0p1rp  10103  ledivge1le  10144  mul2lt0rlt0  10177  mul2lt0rgt0  10178  mul2lt0np  10181  iccf1o  10424  elfz1b  10514  elfz0fzfz0  10550  fz0fzelfz0  10551  fzo1fzo0n0  10612  elfzo0z  10613  fzofzim  10617  elfzodifsumelfzo  10636  btwnzge0  10756  modqid  10807  mulqaddmodid  10822  mulp1mod1  10823  modqltm1p1mod  10834  addmodlteq  10856  expgt1  11035  ltexp2a  11049  leexp2a  11050  expnbnd  11122  expnlbnd2  11124  zzlesq  11167  nn0ltexp2  11169  expcanlem  11175  expcan  11176  bcm1n  11229  ssenneg  11302  sshashneg  11303  iswrdiz  11333  ccat2s1fvwd  11437  swrdswrdlem  11498  swrdswrd  11499  sq01  11682  resqrexlemcalc3  11804  resqrexlemnm  11806  resqrexlemgt0  11808  sqrtgt0  11822  abs00ap  11850  leabs  11862  ltabs  11876  abslt  11877  absle  11878  absgt0ap  11888  rpmaxcl  12012  nn0maxcl  12014  rpmincl  12028  mul0inf  12032  reccn2ap  12104  climge0  12116  fsumrecl  12193  isumlessdc  12288  divcnv  12289  expcnvre  12295  absltap  12301  geolim2  12304  georeclim  12305  geoisumr  12310  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  cvgratnnlemabsle  12319  mertenslem2  12328  cos12dec  12560  p1modz1  12586  dvdslelemd  12635  oddge22np1  12673  divalglemnn  12710  divalglemeuneg  12715  bitsfzolem  12746  bitsinv1lem  12753  lcmgcdlem  12880  dvdsnprmd  12928  isprm5lem  12945  sqrt2irraplemnn  12984  sqrt2irrap  12985  qnumgt0  13003  sqrtrirr  13014  qexpz  13160  4sqlem6  13191  ballotfilemonn  13279  ballotfilemfc0  13290  ballotfilemfcc  13291  znnen  13347  ennnfoneleminc  13360  exmidunben  13375  mulcncflem  15866  hovercncf  15905  hovera  15906  hoverb  15907  hoverlt1  15908  hovergt0  15909  ivthdichlem  15910  dich0  15911  cosz12  16040  cos02pilt1  16112  ioocosf1o  16115  rplogcl  16142  logdivlt  16157  logdivle  16158  cxplt  16184  cxple  16185  ltexp2  16210  ppiqfi  16275  chtqwordi  16296  ppiqwordi  16301  chtqrpcl  16312  ppiqltx  16314  mersenne  16330  bposlem1  16344  lgsdilem  16384  gausslemma2dlem1a  16415  lgseisen  16431  lgsquadlem1  16434  lgsquadlem2  16435  dichmul0orlem1  16991  dichmul0orlem5  16995  dichmul0orlem6  16996  refeq  17312  trilpolemeq1  17329  trilpolemlt1  17330  ltlenmkv  17360