Theorem 0red 8291

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8142  0cc0 8143

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2227  df-clel 2230  df-ral 2527  df-rex 2528

This theorem is referenced by:  gt0ne0  8718  add20  8765  subge0  8766  lesub0  8770  addgt0d  8812  sublt0d  8861  gt0add  8864  apreap  8878  gt0ap0  8917  ap0gt0  8931  lt0ap0  8939  prodgt0  9143  prodge0  9145  lt2msq1  9176  lediv12a  9185  ledivp1  9194  squeeze0  9195  mulle0r  9235  nn2ge  9287  0mnnnnn0  9545  elnn0z  9607  nn0negleid  9663  rpgecl  10033  ge0p1rp  10036  ledivge1le  10077  mul2lt0rlt0  10110  mul2lt0rgt0  10111  mul2lt0np  10114  iccf1o  10357  elfz1b  10446  elfz0fzfz0  10482  fz0fzelfz0  10483  fzo1fzo0n0  10544  elfzo0z  10545  fzofzim  10549  elfzodifsumelfzo  10568  btwnzge0  10684  modqid  10735  mulqaddmodid  10750  mulp1mod1  10751  modqltm1p1mod  10762  addmodlteq  10784  expgt1  10963  ltexp2a  10977  leexp2a  10978  expnbnd  11050  expnlbnd2  11052  zzlesq  11095  nn0ltexp2  11096  expcanlem  11102  expcan  11103  bcm1n  11156  ssenneg  11229  sshashneg  11230  iswrdiz  11256  ccat2s1fvwd  11360  swrdswrdlem  11421  swrdswrd  11422  resqrexlemcalc3  11726  resqrexlemnm  11728  resqrexlemgt0  11730  sqrtgt0  11744  abs00ap  11772  leabs  11784  ltabs  11797  abslt  11798  absle  11799  absgt0ap  11809  rpmaxcl  11933  nn0maxcl  11935  rpmincl  11948  mul0inf  11951  reccn2ap  12023  climge0  12035  fsumrecl  12112  isumlessdc  12207  divcnv  12208  expcnvre  12214  absltap  12220  geolim2  12223  georeclim  12224  geoisumr  12229  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemabsle  12238  mertenslem2  12247  cos12dec  12479  p1modz1  12505  dvdslelemd  12554  oddge22np1  12592  divalglemnn  12629  divalglemeuneg  12634  bitsfzolem  12665  bitsinv1lem  12672  lcmgcdlem  12799  dvdsnprmd  12847  isprm5lem  12863  sqrt2irraplemnn  12901  sqrt2irrap  12902  qnumgt0  12920  qexpz  13075  4sqlem6  13106  ballotfilemonn  13165  ballotfilemfc0  13176  ballotfilemfcc  13177  znnen  13233  ennnfoneleminc  13246  exmidunben  13261  mulcncflem  15584  hovercncf  15623  hovera  15624  hoverb  15625  hoverlt1  15626  hovergt0  15627  ivthdichlem  15628  dich0  15629  cosz12  15757  cos02pilt1  15828  ioocosf1o  15831  rplogcl  15856  cxplt  15893  cxple  15894  ltexp2  15918  mersenne  15977  lgsdilem  16012  gausslemma2dlem1a  16043  lgseisen  16059  lgsquadlem1  16062  lgsquadlem2  16063  refeq  16920  trilpolemeq1  16936  trilpolemlt1  16937  ltlenmkv  16968