Theorem resubcl 11425

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 11096	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11096	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11409	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11424	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11089	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2832	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  ℝcr 11005   + caddc 11009   − cmin 11344  -cneg 11345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-ltxr 11151  df-sub 11346  df-neg 11347

This theorem is referenced by:  peano2rem  11428  resubcld  11545  ltaddsub  11591  leaddsub  11593  posdif  11610  lt2sub  11615  le2sub  11616  mulsuble0b  11994  cju  12121  elz2  12486  rpnnen1lem5  12879  difrp  12930  qbtwnre  13098  iooshf  13326  iccshftl  13388  lincmb01cmp  13395  uzsubsubfz  13446  difelfzle  13541  fzonmapblen  13608  eluzgtdifelfzo  13627  subfzo0  13692  fracle1  13707  fldiv  13764  modcl  13777  2submod  13839  modsubdir  13847  modfzo0difsn  13850  expubnd  14085  absdiflt  15225  absdifle  15226  elicc4abs  15227  abssubge0  15235  abs2difabs  15242  rddif  15248  absrdbnd  15249  climsup  15577  flo1  15761  supcvg  15763  refallfaccl  15925  resin4p  16047  recos4p  16048  cos01bnd  16095  cos01gt0  16100  pythagtriplem12  16738  pythagtriplem14  16740  pythagtriplem16  16742  fldivp1  16809  prmreclem6  16833  cshwshashlem2  17008  bl2ioo  24707  ioo2bl  24708  ioo2blex  24709  blssioo  24710  blcvx  24713  reconnlem2  24743  opnreen  24747  iirev  24850  iihalf2  24855  iccpnfhmeo  24870  iccvolcl  25495  ioovolcl  25498  ismbf3d  25582  itgrecl  25726  cmvth  25922  cmvthOLD  25923  dvle  25939  dvcvx  25952  dvfsumge  25955  aalioulem3  26269  aaliou  26273  aaliou3lem9  26285  abelthlem2  26369  abelthlem7  26375  abelth2  26379  sincosq1sgn  26434  sincosq2sgn  26435  sincosq3sgn  26436  sincosq4sgn  26437  tangtx  26441  sinq12gt0  26443  cosq14gt0  26446  cosq14ge0  26447  cosne0  26465  sinord  26470  resinf1o  26472  tanregt0  26475  efif1olem2  26479  relogdiv  26529  logneg2  26551  logdivlti  26556  logcnlem4  26581  logccv  26599  cxpaddlelem  26688  loglesqrt  26698  ang180lem2  26747  acoscos  26830  acosbnd  26837  acosrecl  26840  atanlogaddlem  26850  atans2  26868  leibpi  26879  divsqrtsumo1  26921  cvxcl  26922  scvxcvx  26923  jensenlem2  26925  amgmlem  26927  harmonicbnd4  26948  zetacvg  26952  ftalem5  27014  basellem9  27026  mumullem2  27117  ppiub  27142  chtub  27150  bposlem1  27222  bposlem6  27227  bposlem9  27230  gausslemma2dlem1a  27303  chtppilim  27413  chto1ub  27414  rplogsumlem2  27423  rpvmasumlem  27425  dchrisum0flblem1  27446  dchrisum0re  27451  log2sumbnd  27482  selberglem2  27484  pntrmax  27502  pntpbnd2  27525  pntlem3  27547  brbtwn2  28883  colinearalglem4  28887  eleesub  28889  eleesubd  28890  axsegconlem2  28896  ax5seglem2  28907  ax5seglem3  28909  axpaschlem  28918  axpasch  28919  axcontlem2  28943  crctcshwlkn0lem3  29790  crctcshwlkn0lem7  29794  eucrctshift  30223  xlt2addrd  32742  signshf  34601  resconn  35290  sinccvglem  35716  fz0n  35775  dnibndlem4  36523  dnibndlem6  36525  dnibndlem7  36526  dnibndlem9  36528  dnibndlem10  36529  knoppndvlem15  36568  sin2h  37658  tan2h  37660  poimir  37701  mblfinlem3  37707  mblfinlem4  37708  itg2addnclem  37719  itg2addnclem3  37721  ftc1anclem5  37745  ftc1anclem6  37746  ftc1anclem7  37747  dvasin  37752  geomcau  37807  bfp  37872  ismrer1  37886  iccbnd  37888  jm2.17a  43001  acongeq  43024  jm3.1lem2  43059  areaquad  43257  lptre2pt  45686  dvnmul  45989  stoweidlem59  46105  fourierdlem42  46195  hoidmvlelem2  46642  smfmullem1  46837  ltsubsubaddltsub  47340  zm1nn  47341  nn0resubcl  47347  subsubelfzo0  47365  bgoldbtbndlem2  47845  ply1mulgsumlem2  48427  ltsubaddb  48554  ltsubsubb  48555  ltsubadd2b  48556  line2  48792