Theorem resubcld 8698

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 8580	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2209  (class class class)co 6075  ℝcr 8168   − cmin 8487

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306  ax-pr 4341  ax-setind 4679  ax-resscn 8261  ax-1cn 8262  ax-icn 8264  ax-addcl 8265  ax-addrcl 8266  ax-mulcl 8267  ax-addcom 8269  ax-addass 8271  ax-distr 8273  ax-i2m1 8274  ax-0id 8277  ax-rnegex 8278  ax-cnre 8280

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-opab 4188  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-iota 5332  df-fun 5374  df-fv 5380  df-riota 6028  df-ov 6078  df-oprab 6079  df-mpo 6080  df-sub 8489  df-neg 8490

This theorem is referenced by:  ltsubadd  8750  lesubadd  8752  ltaddsub  8754  leaddsub  8756  lesub1  8774  lesub2  8775  ltsub1  8776  ltsub2  8777  lt2sub  8778  le2sub  8779  rereim  8904  ltmul1a  8909  cru  8920  lemul1a  9178  ztri3or  9666  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  rebtwn2z  10667  qbtwnrelemcalc  10668  qbtwnre  10669  intfracq  10735  modqval  10739  modqlt  10748  modqsubdir  10808  ser3le  10952  resq01  11073  expnbnd  11079  bcm1n  11185  crre  11600  remullem  11614  recvguniqlem  11738  resqrexlemover  11754  resqrexlemcalc2  11759  resqrexlemcalc3  11760  resqrexlemnmsq  11761  resqrexlemnm  11762  resqrexlemcvg  11763  resqrexlemglsq  11766  resqrexlemga  11767  fzomaxdiflem  11856  caubnd2  11861  amgm2  11862  icodiamlt  11924  qdenre  11946  maxabslemab  11950  maxabslemlub  11951  maxltsup  11962  bdtrilem  11983  bdtri  11984  mulcn2  12056  reccn2ap  12057  climle  12078  climsqz  12079  climsqz2  12080  climcvg1nlem  12093  fsumle  12208  cvgratnnlembern  12268  cvgratnnlemsumlt  12273  cvgratnnlemfm  12274  cvgratnnlemrate  12275  cvgratnn  12276  efltim  12443  sin01bnd  12502  sin01gt0  12507  cos12dec  12513  bitscmp  12703  bitsinv1lem  12706  uzwodc  12792  pythagtriplem12  13032  pythagtriplem14  13034  4sqlem15  13162  ballotfilemfrcn0  13251  gzsumshift  14126  blss2ps  15430  blss2  15431  blssps  15451  blss  15452  maxcncf  15639  mincncf  15640  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthreinc  15669  dvcjbr  15732  reeff1oleme  15796  efltlemlt  15798  sin0pilem1  15805  tangtx  15862  cosordlem  15873  cosq34lt1  15874  pellexlem2  16006  gausslemma2dlem1a  16091  lgsquadlem1  16110  repiecelem  16979  cvgcmp2nlemabs  16986  iooref1o  16988  trilpolemlt1  16995  trirec0  16998  apdifflemf  17000  qdiff  17003  neap0mkv  17024