Theorem resubcld 8550

Description: Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
renegcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
resubcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
resubcld	⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Proof of Theorem resubcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		resubcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		resubcl 8433	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6013  ℝcr 8021   − cmin 8340

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-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-setind 4633  ax-resscn 8114  ax-1cn 8115  ax-icn 8117  ax-addcl 8118  ax-addrcl 8119  ax-mulcl 8120  ax-addcom 8122  ax-addass 8124  ax-distr 8126  ax-i2m1 8127  ax-0id 8130  ax-rnegex 8131  ax-cnre 8133

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-sub 8342  df-neg 8343

This theorem is referenced by:  ltsubadd  8602  lesubadd  8604  ltaddsub  8606  leaddsub  8608  lesub1  8626  lesub2  8627  ltsub1  8628  ltsub2  8629  lt2sub  8630  le2sub  8631  rereim  8756  ltmul1a  8761  cru  8772  lemul1a  9028  ztri3or  9512  lincmb01cmp  10228  iccf1o  10229  rebtwn2z  10504  qbtwnrelemcalc  10505  qbtwnre  10506  intfracq  10572  modqval  10576  modqlt  10585  modqsubdir  10645  ser3le  10789  expnbnd  10915  crre  11408  remullem  11422  recvguniqlem  11545  resqrexlemover  11561  resqrexlemcalc2  11566  resqrexlemcalc3  11567  resqrexlemnmsq  11568  resqrexlemnm  11569  resqrexlemcvg  11570  resqrexlemglsq  11573  resqrexlemga  11574  fzomaxdiflem  11663  caubnd2  11668  amgm2  11669  icodiamlt  11731  qdenre  11753  maxabslemab  11757  maxabslemlub  11758  maxltsup  11769  bdtrilem  11790  bdtri  11791  mulcn2  11863  reccn2ap  11864  climle  11885  climsqz  11886  climsqz2  11887  climcvg1nlem  11900  fsumle  12014  cvgratnnlembern  12074  cvgratnnlemsumlt  12079  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratnn  12082  efltim  12249  sin01bnd  12308  sin01gt0  12313  cos12dec  12319  bitscmp  12509  bitsinv1lem  12512  uzwodc  12598  pythagtriplem12  12838  pythagtriplem14  12840  4sqlem15  12968  blss2ps  15120  blss2  15121  blssps  15141  blss  15142  maxcncf  15329  mincncf  15330  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthreinc  15359  dvcjbr  15422  reeff1oleme  15486  efltlemlt  15488  sin0pilem1  15495  tangtx  15552  cosordlem  15563  cosq34lt1  15564  gausslemma2dlem1a  15777  lgsquadlem1  15796  cvgcmp2nlemabs  16572  iooref1o  16574  trilpolemlt1  16581  trirec0  16584  apdifflemf  16586  neap0mkv  16609