Theorem resubcld 8488

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

Syntax hints:   → wi 4   ∈ wcel 2178  (class class class)co 5967  ℝcr 7959   − cmin 8278

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-setind 4603  ax-resscn 8052  ax-1cn 8053  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-addcom 8060  ax-addass 8062  ax-distr 8064  ax-i2m1 8065  ax-0id 8068  ax-rnegex 8069  ax-cnre 8071

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-ral 2491  df-rex 2492  df-reu 2493  df-rab 2495  df-v 2778  df-sbc 3006  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-iota 5251  df-fun 5292  df-fv 5298  df-riota 5922  df-ov 5970  df-oprab 5971  df-mpo 5972  df-sub 8280  df-neg 8281

This theorem is referenced by:  ltsubadd  8540  lesubadd  8542  ltaddsub  8544  leaddsub  8546  lesub1  8564  lesub2  8565  ltsub1  8566  ltsub2  8567  lt2sub  8568  le2sub  8569  rereim  8694  ltmul1a  8699  cru  8710  lemul1a  8966  ztri3or  9450  lincmb01cmp  10160  iccf1o  10161  rebtwn2z  10434  qbtwnrelemcalc  10435  qbtwnre  10436  intfracq  10502  modqval  10506  modqlt  10515  modqsubdir  10575  ser3le  10719  expnbnd  10845  crre  11283  remullem  11297  recvguniqlem  11420  resqrexlemover  11436  resqrexlemcalc2  11441  resqrexlemcalc3  11442  resqrexlemnmsq  11443  resqrexlemnm  11444  resqrexlemcvg  11445  resqrexlemglsq  11448  resqrexlemga  11449  fzomaxdiflem  11538  caubnd2  11543  amgm2  11544  icodiamlt  11606  qdenre  11628  maxabslemab  11632  maxabslemlub  11633  maxltsup  11644  bdtrilem  11665  bdtri  11666  mulcn2  11738  reccn2ap  11739  climle  11760  climsqz  11761  climsqz2  11762  climcvg1nlem  11775  fsumle  11889  cvgratnnlembern  11949  cvgratnnlemsumlt  11954  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratnn  11957  efltim  12124  sin01bnd  12183  sin01gt0  12188  cos12dec  12194  bitscmp  12384  bitsinv1lem  12387  uzwodc  12473  pythagtriplem12  12713  pythagtriplem14  12715  4sqlem15  12843  blss2ps  14993  blss2  14994  blssps  15014  blss  15015  maxcncf  15202  mincncf  15203  ivthinclemlopn  15223  ivthinclemuopn  15225  ivthreinc  15232  dvcjbr  15295  reeff1oleme  15359  efltlemlt  15361  sin0pilem1  15368  tangtx  15425  cosordlem  15436  cosq34lt1  15437  gausslemma2dlem1a  15650  lgsquadlem1  15669  cvgcmp2nlemabs  16173  iooref1o  16175  trilpolemlt1  16182  trirec0  16185  apdifflemf  16187  neap0mkv  16210