Theorem resubcl 11428

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 11099	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11099	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11412	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11427	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11092	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2829	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007  ℝcr 11008   + caddc 11012   − cmin 11347  -cneg 11348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-sub 11349  df-neg 11350

This theorem is referenced by:  peano2rem  11431  resubcld  11548  ltaddsub  11594  leaddsub  11596  posdif  11613  lt2sub  11618  le2sub  11619  mulsuble0b  11997  cju  12124  elz2  12489  rpnnen1lem5  12882  difrp  12933  qbtwnre  13101  iooshf  13329  iccshftl  13391  lincmb01cmp  13398  uzsubsubfz  13449  difelfzle  13544  fzonmapblen  13611  eluzgtdifelfzo  13630  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  24678  ioo2bl  24679  ioo2blex  24680  blssioo  24681  blcvx  24684  reconnlem2  24714  opnreen  24718  iirev  24821  iihalf2  24826  iccpnfhmeo  24841  iccvolcl  25466  ioovolcl  25469  ismbf3d  25553  itgrecl  25697  cmvth  25893  cmvthOLD  25894  dvle  25910  dvcvx  25923  dvfsumge  25926  aalioulem3  26240  aaliou  26244  aaliou3lem9  26256  abelthlem2  26340  abelthlem7  26346  abelth2  26350  sincosq1sgn  26405  sincosq2sgn  26406  sincosq3sgn  26407  sincosq4sgn  26408  tangtx  26412  sinq12gt0  26414  cosq14gt0  26417  cosq14ge0  26418  cosne0  26436  sinord  26441  resinf1o  26443  tanregt0  26446  efif1olem2  26450  relogdiv  26500  logneg2  26522  logdivlti  26527  logcnlem4  26552  logccv  26570  cxpaddlelem  26659  loglesqrt  26669  ang180lem2  26718  acoscos  26801  acosbnd  26808  acosrecl  26811  atanlogaddlem  26821  atans2  26839  leibpi  26850  divsqrtsumo1  26892  cvxcl  26893  scvxcvx  26894  jensenlem2  26896  amgmlem  26898  harmonicbnd4  26919  zetacvg  26923  ftalem5  26985  basellem9  26997  mumullem2  27088  ppiub  27113  chtub  27121  bposlem1  27193  bposlem6  27198  bposlem9  27201  gausslemma2dlem1a  27274  chtppilim  27384  chto1ub  27385  rplogsumlem2  27394  rpvmasumlem  27396  dchrisum0flblem1  27417  dchrisum0re  27422  log2sumbnd  27453  selberglem2  27455  pntrmax  27473  pntpbnd2  27496  pntlem3  27518  brbtwn2  28850  colinearalglem4  28854  eleesub  28856  eleesubd  28857  axsegconlem2  28863  ax5seglem2  28874  ax5seglem3  28876  axpaschlem  28885  axpasch  28886  axcontlem2  28910  crctcshwlkn0lem3  29757  crctcshwlkn0lem7  29761  eucrctshift  30187  xlt2addrd  32702  signshf  34556  resconn  35219  sinccvglem  35645  fz0n  35704  dnibndlem4  36455  dnibndlem6  36457  dnibndlem7  36458  dnibndlem9  36460  dnibndlem10  36461  knoppndvlem15  36500  sin2h  37590  tan2h  37592  poimir  37633  mblfinlem3  37639  mblfinlem4  37640  itg2addnclem  37651  itg2addnclem3  37653  ftc1anclem5  37677  ftc1anclem6  37678  ftc1anclem7  37679  dvasin  37684  geomcau  37739  bfp  37804  ismrer1  37818  iccbnd  37820  jm2.17a  42933  acongeq  42956  jm3.1lem2  42991  areaquad  43189  lptre2pt  45621  dvnmul  45924  stoweidlem59  46040  fourierdlem42  46130  hoidmvlelem2  46577  smfmullem1  46772  ltsubsubaddltsub  47285  zm1nn  47286  nn0resubcl  47292  subsubelfzo0  47310  bgoldbtbndlem2  47790  ply1mulgsumlem2  48372  ltsubaddb  48499  ltsubsubb  48500  ltsubadd2b  48501  line2  48737