Theorem resubcld 8056

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

Syntax hints:   → wi 4   ∈ wcel 1461  (class class class)co 5726  ℝcr 7540   − cmin 7850

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089  ax-setind 4410  ax-resscn 7631  ax-1cn 7632  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-addcom 7639  ax-addass 7641  ax-distr 7643  ax-i2m1 7644  ax-0id 7647  ax-rnegex 7648  ax-cnre 7650

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-ral 2393  df-rex 2394  df-reu 2395  df-rab 2397  df-v 2657  df-sbc 2877  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-id 4173  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-iota 5044  df-fun 5081  df-fv 5087  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-sub 7852  df-neg 7853

This theorem is referenced by:  ltsubadd  8107  lesubadd  8109  ltaddsub  8111  leaddsub  8113  lesub1  8131  lesub2  8132  ltsub1  8133  ltsub2  8134  lt2sub  8135  le2sub  8136  rereim  8260  ltmul1a  8265  cru  8276  lemul1a  8520  ztri3or  8995  lincmb01cmp  9673  iccf1o  9674  rebtwn2z  9919  qbtwnrelemcalc  9920  qbtwnre  9921  intfracq  9980  modqval  9984  modqlt  9993  modqsubdir  10053  ser3le  10178  expnbnd  10302  crre  10516  remullem  10530  recvguniqlem  10652  resqrexlemover  10668  resqrexlemcalc2  10673  resqrexlemcalc3  10674  resqrexlemnmsq  10675  resqrexlemnm  10676  resqrexlemcvg  10677  resqrexlemglsq  10680  resqrexlemga  10681  fzomaxdiflem  10770  caubnd2  10775  amgm2  10776  icodiamlt  10838  qdenre  10860  maxabslemab  10864  maxabslemlub  10865  maxltsup  10876  bdtrilem  10896  bdtri  10897  mulcn2  10967  reccn2ap  10968  climle  10989  climsqz  10990  climsqz2  10991  climcvg1nlem  11004  fsumle  11118  cvgratnnlembern  11178  cvgratnnlemsumlt  11183  cvgratnnlemfm  11184  cvgratnnlemrate  11185  cvgratnn  11186  efltim  11249  sin01bnd  11309  sin01gt0  11313  blss2ps  12389  blss2  12390  blssps  12410  blss  12411  cvgcmp2nlemabs  12908  trilpolemlt1  12915