Theorem resubcl 11449

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 11119	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11119	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11433	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 602	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11448	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11112	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 599	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2840	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027  ℝcr 11028   + caddc 11032   − cmin 11368  -cneg 11369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-po 5526  df-so 5527  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-neg 11371

This theorem is referenced by:  peano2rem  11452  resubcld  11569  ltaddsub  11615  leaddsub  11617  posdif  11634  lt2sub  11639  le2sub  11640  mulsuble0b  12019  cju  12146  elz2  12533  rpnnen1lem5  12922  difrp  12973  qbtwnre  13142  iooshf  13370  iccshftl  13432  lincmb01cmp  13439  uzsubsubfz  13491  difelfzle  13586  fzonmapblen  13654  eluzgtdifelfzo  13673  subfzo0  13738  fracle1  13753  fldiv  13810  modcl  13823  2submod  13885  modsubdir  13893  modfzo0difsn  13896  expubnd  14131  absdiflt  15271  absdifle  15272  elicc4abs  15273  abssubge0  15281  abs2difabs  15288  rddif  15294  absrdbnd  15295  climsup  15623  flo1  15810  supcvg  15812  refallfaccl  15974  resin4p  16096  recos4p  16097  cos01bnd  16144  cos01gt0  16149  pythagtriplem12  16788  pythagtriplem14  16790  pythagtriplem16  16792  fldivp1  16859  prmreclem6  16883  cshwshashlem2  17058  bl2ioo  24775  ioo2bl  24776  ioo2blex  24777  blssioo  24778  blcvx  24781  reconnlem2  24811  opnreen  24815  iirev  24914  iihalf2  24918  iccpnfhmeo  24930  iccvolcl  25552  ioovolcl  25555  ismbf3d  25639  itgrecl  25783  cmvth  25976  dvle  25992  dvcvx  26005  dvfsumge  26007  aalioulem3  26318  aaliou  26322  aaliou3lem9  26334  abelthlem2  26415  abelthlem7  26421  abelth2  26425  sincosq1sgn  26480  sincosq2sgn  26481  sincosq3sgn  26482  sincosq4sgn  26483  tangtx  26487  sinq12gt0  26489  cosq14gt0  26492  cosq14ge0  26493  cosne0  26511  sinord  26516  resinf1o  26518  tanregt0  26521  efif1olem2  26525  relogdiv  26575  logneg2  26597  logdivlti  26602  logcnlem4  26627  logccv  26645  cxpaddlelem  26733  loglesqrt  26743  ang180lem2  26792  acoscos  26875  acosbnd  26882  acosrecl  26885  atanlogaddlem  26895  atans2  26913  leibpi  26924  divsqrtsumo1  26965  cvxcl  26966  scvxcvx  26967  jensenlem2  26969  amgmlem  26971  harmonicbnd4  26992  zetacvg  26996  ftalem5  27058  basellem9  27070  mumullem2  27161  ppiub  27185  chtub  27193  bposlem1  27265  bposlem6  27270  bposlem9  27273  gausslemma2dlem1a  27346  chtppilim  27456  chto1ub  27457  rplogsumlem2  27466  rpvmasumlem  27468  dchrisum0flblem1  27489  dchrisum0re  27494  log2sumbnd  27525  selberglem2  27527  pntrmax  27545  pntpbnd2  27568  pntlem3  27590  brbtwn2  28992  colinearalglem4  28996  eleesub  28998  eleesubd  28999  axsegconlem2  29005  ax5seglem2  29016  ax5seglem3  29018  axpaschlem  29027  axpasch  29028  axcontlem2  29052  crctcshwlkn0lem3  29898  crctcshwlkn0lem7  29902  eucrctshift  30331  xlt2addrd  32851  signshf  34772  resconn  35474  sinccvglem  35900  fz0n  35959  dnibndlem4  36787  dnibndlem6  36789  dnibndlem7  36790  dnibndlem9  36792  dnibndlem10  36793  knoppndvlem15  36832  sin2h  37977  tan2h  37979  poimir  38020  mblfinlem3  38026  mblfinlem4  38027  itg2addnclem  38038  itg2addnclem3  38040  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anclem7  38066  dvasin  38071  geomcau  38126  bfp  38191  ismrer1  38205  iccbnd  38207  jm2.17a  43405  acongeq  43428  jm3.1lem2  43463  areaquad  43661  lptre2pt  46083  dvnmul  46386  stoweidlem59  46502  fourierdlem42  46592  hoidmvlelem2  47039  smfmullem1  47234  ltsubsubaddltsub  47764  zm1nn  47765  nn0resubcl  47771  subsubelfzo0  47790  bgoldbtbndlem2  48297  ply1mulgsumlem2  48878  ltsubaddb  49005  ltsubsubb  49006  ltsubadd2b  49007  line2  49243