Theorem resubcl 11537

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 11205	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11205	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11521	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 608	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11536	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11198	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 605	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2866	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  (class class class)co 7419  ℂcc 11113  ℝcr 11114   + caddc 11118   − cmin 11456  -cneg 11457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11172  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-mulcom 11179  ax-addass 11180  ax-mulass 11181  ax-distr 11182  ax-i2m1 11183  ax-1ne0 11184  ax-1rid 11185  ax-rnegex 11186  ax-rrecex 11187  ax-cnre 11188  ax-pre-lttri 11189  ax-pre-lttrn 11190  ax-pre-ltadd 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-ltxr 11263  df-sub 11458  df-neg 11459

This theorem is used by:  peano2rem  11540  resubcld  11657  ltaddsub  11703  leaddsub  11705  posdif  11722  lt2sub  11727  le2sub  11728  mulsuble0b  12102  cju  12229  elz2  12624  rpnnen1lem5  13021  difrp  13072  qbtwnre  13241  iooshf  13469  iccshftl  13531  lincmb01cmp  13538  uzsubsubfz  13591  difelfzle  13686  fzonmapblen  13754  eluzgtdifelfzo  13773  subfzo0  13839  fracle1  13854  fldiv  13911  modcl  13924  2submod  13986  modsubdir  13994  modfzo0difsn  13997  expubnd  14232  absdiflt  15393  absdifle  15394  elicc4abs  15395  abssubge0  15403  abs2difabs  15410  rddif  15416  absrdbnd  15417  climsup  15745  flo1  15931  supcvg  15933  refallfaccl  16095  resin4p  16216  recos4p  16217  cos01bnd  16264  cos01gt0  16269  pythagtriplem12  16908  pythagtriplem14  16910  pythagtriplem16  16912  fldivp1  16979  prmreclem6  17003  cshwshashlem2  17178  bl2ioo  25000  ioo2bl  25001  ioo2blex  25002  blssioo  25003  blcvx  25006  reconnlem2  25036  opnreen  25040  iirev  25139  iihalf2  25143  iccpnfhmeo  25155  iccvolcl  25777  ioovolcl  25780  ismbf3d  25864  itgrecl  26008  cmvth  26201  dvle  26217  dvcvx  26230  dvfsumge  26232  aalioulem3  26548  aaliou  26552  aaliou3lem9  26564  abelthlem2  26646  abelthlem7  26652  abelth2  26656  sincosq1sgn  26714  sincosq2sgn  26715  sincosq3sgn  26716  sincosq4sgn  26717  tangtx  26721  sinq12gt0  26723  cosq14gt0  26726  cosq14ge0  26727  cosne0  26745  sinord  26750  resinf1o  26752  tanregt0  26755  efif1olem2  26759  relogdiv  26809  logneg2  26831  logdivlti  26836  logcnlem4  26861  logccv  26879  cxpaddlelem  26967  loglesqrt  26977  ang180lem2  27026  acoscos  27109  acosbnd  27116  acosrecl  27119  atanlogaddlem  27129  atans2  27147  leibpi  27158  divsqrtsumo1  27199  cvxcl  27200  scvxcvx  27201  jensenlem2  27203  amgmlem  27205  harmonicbnd4  27226  zetacvg  27230  ftalem5  27292  basellem9  27304  mumullem2  27395  ppiub  27419  chtub  27427  bposlem1  27499  bposlem6  27504  bposlem9  27507  gausslemma2dlem1a  27580  chtppilim  27690  chto1ub  27691  rplogsumlem2  27700  rpvmasumlem  27702  dchrisum0flblem1  27723  dchrisum0re  27728  log2sumbnd  27759  selberglem2  27761  pntrmax  27779  pntpbnd2  27802  pntlem3  27824  brbtwn2  29310  colinearalglem4  29314  eleesub  29316  eleesubd  29317  axsegconlem2  29323  ax5seglem2  29334  ax5seglem3  29336  axpaschlem  29345  axpasch  29346  axcontlem2  29370  crctcshwlkn0lem3  30228  crctcshwlkn0lem7  30232  eucrctshift  30665  xlt2addrd  33174  signshf  35040  resconn  35775  sinccvglem  36201  fz0n  36260  dnibndlem4  37127  dnibndlem6  37129  dnibndlem7  37130  dnibndlem9  37132  dnibndlem10  37133  knoppndvlem15  37172  sin2h  38318  tan2h  38320  poimir  38361  mblfinlem3  38367  mblfinlem4  38368  itg2addnclem  38379  itg2addnclem3  38381  ftc1anclem5  38405  ftc1anclem6  38406  ftc1anclem7  38407  dvasin  38412  geomcau  38468  bfp  38533  ismrer1  38547  iccbnd  38549  jm2.17a  43745  acongeq  43768  jm3.1lem2  43803  areaquad  44001  lptre2pt  46412  dvnmul  46715  stoweidlem59  46831  fourierdlem42  46921  hoidmvlelem2  47368  smfmullem1  47563  ltsubsubaddltsub  48096  zm1nn  48097  nn0resubcl  48103  subsubelfzo0  48122  bgoldbtbndlem2  48629  ply1mulgsumlem2  49224  ltsubaddb  49351  ltsubsubb  49352  ltsubadd2b  49353  line2  49589