Theorem resubcl 10687

Description: Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)

Assertion

Ref	Expression
resubcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Proof of Theorem resubcl

Step	Hyp	Ref	Expression
1		recn 10362	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 10362	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 10671	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 589	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 10686	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 10355	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 586	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2859	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2106  (class class class)co 6922  ℂcc 10270  ℝcr 10271   + caddc 10275   − cmin 10606  -cneg 10607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-ltxr 10416  df-sub 10608  df-neg 10609

This theorem is referenced by:  peano2rem  10690  resubcld  10803  ltaddsub  10849  leaddsub  10851  posdif  10868  lt2sub  10873  le2sub  10874  mulsuble0b  11249  cju  11370  elz2  11745  rpnnen1lem5  12128  difrp  12177  qbtwnre  12342  iooshf  12564  iccshftl  12625  lincmb01cmp  12632  uzsubsubfz  12680  difelfzle  12771  fzonmapblen  12833  eluzgtdifelfzo  12849  subfzo0  12909  fracle1  12923  fldiv  12978  modcl  12991  2submod  13050  modsubdir  13058  modfzo0difsn  13061  expubnd  13239  absdiflt  14464  absdifle  14465  elicc4abs  14466  abssubge0  14474  abs2difabs  14481  rddif  14487  absrdbnd  14488  climsup  14808  flo1  14990  supcvg  14992  refallfaccl  15151  resin4p  15270  recos4p  15271  cos01bnd  15318  cos01gt0  15323  pythagtriplem12  15935  pythagtriplem14  15937  pythagtriplem16  15939  fldivp1  16005  prmreclem6  16029  cshwshashlem2  16202  bl2ioo  23003  ioo2bl  23004  ioo2blex  23005  blssioo  23006  blcvx  23009  reconnlem2  23038  opnreen  23042  iirev  23136  iihalf2  23140  iccpnfhmeo  23152  iccvolcl  23771  ioovolcl  23774  ismbf3d  23858  itgrecl  24001  cmvth  24191  dvle  24207  dvcvx  24220  dvfsumge  24222  aalioulem3  24526  aaliou  24530  aaliou3lem9  24542  abelthlem2  24623  abelthlem7  24629  abelth2  24633  sincosq1sgn  24688  sincosq2sgn  24689  sincosq3sgn  24690  sincosq4sgn  24691  tangtx  24695  sinq12gt0  24697  cosq14gt0  24700  cosq14ge0  24701  cosne0  24714  sinord  24718  resinf1o  24720  tanregt0  24723  efif1olem2  24727  relogdiv  24776  logneg2  24798  logdivlti  24803  logcnlem4  24828  logccv  24846  cxpaddlelem  24932  loglesqrt  24939  ang180lem2  24988  acoscos  25071  acosbnd  25078  acosrecl  25081  atanlogaddlem  25091  atans2  25109  leibpi  25121  divsqrtsumo1  25162  cvxcl  25163  scvxcvx  25164  jensenlem2  25166  amgmlem  25168  harmonicbnd4  25189  zetacvg  25193  ftalem5  25255  basellem9  25267  mumullem2  25358  ppiub  25381  chtub  25389  bposlem1  25461  bposlem6  25466  bposlem9  25469  gausslemma2dlem1a  25542  chtppilim  25616  chto1ub  25617  rplogsumlem2  25626  rpvmasumlem  25628  dchrisum0flblem1  25649  dchrisum0re  25654  log2sumbnd  25685  selberglem2  25687  pntrmax  25705  pntpbnd2  25728  pntlem3  25750  brbtwn2  26254  colinearalglem4  26258  eleesub  26260  eleesubd  26261  axsegconlem2  26267  ax5seglem2  26278  ax5seglem3  26280  axpaschlem  26289  axpasch  26290  axcontlem2  26314  crctcshwlkn0lem3  27161  crctcshwlkn0lem7  27165  eucrctshift  27661  xlt2addrd  30102  signshf  31281  resconn  31841  sinccvglem  32177  fz0n  32224  dnibndlem4  33068  dnibndlem6  33070  dnibndlem7  33071  dnibndlem9  33073  dnibndlem10  33074  knoppndvlem15  33113  sin2h  34018  tan2h  34020  poimir  34062  mblfinlem3  34068  mblfinlem4  34069  itg2addnclem  34080  itg2addnclem3  34082  ftc1anclem5  34108  ftc1anclem6  34109  ftc1anclem7  34110  dvasin  34115  geomcau  34173  bfp  34241  ismrer1  34255  iccbnd  34257  jm2.17a  38478  acongeq  38501  jm3.1lem2  38536  areaquad  38752  lptre2pt  40772  dvnmul  41078  stoweidlem59  41195  fourierdlem42  41285  hoidmvlelem2  41729  smfmullem1  41917  ltsubsubaddltsub  42335  zm1nn  42336  nn0resubcl  42342  subsubelfzo0  42360  bgoldbtbndlem2  42711  ply1mulgsumlem2  43182  ltsubaddb  43311  ltsubsubb  43312  ltsubadd2b  43313  line2  43480