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  8719  add20  8766  subge0  8767  lesub0  8771  addgt0d  8813  sublt0d  8862  gt0add  8865  apreap  8879  gt0ap0  8918  ap0gt0  8932  lt0ap0  8940  prodgt0  9146  prodge0  9148  lt2msq1  9179  lediv12a  9188  ledivp1  9197  squeeze0  9198  mulle0r  9238  nn2ge  9290  0mnnnnn0  9548  elnn0z  9610  nn0negleid  9666  rpgecl  10036  ge0p1rp  10039  ledivge1le  10080  mul2lt0rlt0  10113  mul2lt0rgt0  10114  mul2lt0np  10117  iccf1o  10360  elfz1b  10449  elfz0fzfz0  10485  fz0fzelfz0  10486  fzo1fzo0n0  10547  elfzo0z  10548  fzofzim  10552  elfzodifsumelfzo  10571  btwnzge0  10687  modqid  10738  mulqaddmodid  10753  mulp1mod1  10754  modqltm1p1mod  10765  addmodlteq  10787  expgt1  10966  ltexp2a  10980  leexp2a  10981  expnbnd  11053  expnlbnd2  11055  zzlesq  11098  nn0ltexp2  11099  expcanlem  11105  expcan  11106  bcm1n  11159  ssenneg  11232  sshashneg  11233  iswrdiz  11259  ccat2s1fvwd  11363  swrdswrdlem  11424  swrdswrd  11425  sq01  11608  resqrexlemcalc3  11730  resqrexlemnm  11732  resqrexlemgt0  11734  sqrtgt0  11748  abs00ap  11776  leabs  11788  ltabs  11801  abslt  11802  absle  11803  absgt0ap  11813  rpmaxcl  11937  nn0maxcl  11939  rpmincl  11952  mul0inf  11955  reccn2ap  12027  climge0  12039  fsumrecl  12116  isumlessdc  12211  divcnv  12212  expcnvre  12218  absltap  12224  geolim2  12227  georeclim  12228  geoisumr  12233  cvgratnnlemnexp  12239  cvgratnnlemmn  12240  cvgratnnlemabsle  12242  mertenslem2  12251  cos12dec  12483  p1modz1  12509  dvdslelemd  12558  oddge22np1  12596  divalglemnn  12633  divalglemeuneg  12638  bitsfzolem  12669  bitsinv1lem  12676  lcmgcdlem  12803  dvdsnprmd  12851  isprm5lem  12867  sqrt2irraplemnn  12905  sqrt2irrap  12906  qnumgt0  12924  qexpz  13079  4sqlem6  13110  ballotfilemonn  13169  ballotfilemfc0  13180  ballotfilemfcc  13181  znnen  13237  ennnfoneleminc  13250  exmidunben  13265  mulcncflem  15602  hovercncf  15641  hovera  15642  hoverb  15643  hoverlt1  15644  hovergt0  15645  ivthdichlem  15646  dich0  15647  cosz12  15775  cos02pilt1  15846  ioocosf1o  15849  rplogcl  15874  cxplt  15911  cxple  15912  ltexp2  15936  mersenne  15995  lgsdilem  16030  gausslemma2dlem1a  16061  lgseisen  16077  lgsquadlem1  16080  lgsquadlem2  16081  dichmul0orlem1  16637  dichmul0orlem5  16641  dichmul0orlem6  16642  refeq  16948  trilpolemeq1  16964  trilpolemlt1  16965  ltlenmkv  16995