Theorem resubcl 11552

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 11224	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11224	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11536	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11551	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11217	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2836	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132  ℝcr 11133   + caddc 11137   − cmin 11471  -cneg 11472

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 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-ltxr 11279  df-sub 11473  df-neg 11474

This theorem is referenced by:  peano2rem  11555  resubcld  11670  ltaddsub  11716  leaddsub  11718  posdif  11735  lt2sub  11740  le2sub  11741  mulsuble0b  12119  cju  12241  elz2  12611  rpnnen1lem5  13002  difrp  13052  qbtwnre  13220  iooshf  13448  iccshftl  13510  lincmb01cmp  13517  uzsubsubfz  13568  difelfzle  13663  fzonmapblen  13730  eluzgtdifelfzo  13748  subfzo0  13810  fracle1  13825  fldiv  13882  modcl  13895  2submod  13955  modsubdir  13963  modfzo0difsn  13966  expubnd  14201  absdiflt  15341  absdifle  15342  elicc4abs  15343  abssubge0  15351  abs2difabs  15358  rddif  15364  absrdbnd  15365  climsup  15691  flo1  15875  supcvg  15877  refallfaccl  16039  resin4p  16161  recos4p  16162  cos01bnd  16209  cos01gt0  16214  pythagtriplem12  16851  pythagtriplem14  16853  pythagtriplem16  16855  fldivp1  16922  prmreclem6  16946  cshwshashlem2  17121  bl2ioo  24736  ioo2bl  24737  ioo2blex  24738  blssioo  24739  blcvx  24742  reconnlem2  24772  opnreen  24776  iirev  24879  iihalf2  24884  iccpnfhmeo  24899  iccvolcl  25525  ioovolcl  25528  ismbf3d  25612  itgrecl  25756  cmvth  25952  cmvthOLD  25953  dvle  25969  dvcvx  25982  dvfsumge  25985  aalioulem3  26299  aaliou  26303  aaliou3lem9  26315  abelthlem2  26399  abelthlem7  26405  abelth2  26409  sincosq1sgn  26464  sincosq2sgn  26465  sincosq3sgn  26466  sincosq4sgn  26467  tangtx  26471  sinq12gt0  26473  cosq14gt0  26476  cosq14ge0  26477  cosne0  26495  sinord  26500  resinf1o  26502  tanregt0  26505  efif1olem2  26509  relogdiv  26559  logneg2  26581  logdivlti  26586  logcnlem4  26611  logccv  26629  cxpaddlelem  26718  loglesqrt  26728  ang180lem2  26777  acoscos  26860  acosbnd  26867  acosrecl  26870  atanlogaddlem  26880  atans2  26898  leibpi  26909  divsqrtsumo1  26951  cvxcl  26952  scvxcvx  26953  jensenlem2  26955  amgmlem  26957  harmonicbnd4  26978  zetacvg  26982  ftalem5  27044  basellem9  27056  mumullem2  27147  ppiub  27172  chtub  27180  bposlem1  27252  bposlem6  27257  bposlem9  27260  gausslemma2dlem1a  27333  chtppilim  27443  chto1ub  27444  rplogsumlem2  27453  rpvmasumlem  27455  dchrisum0flblem1  27476  dchrisum0re  27481  log2sumbnd  27512  selberglem2  27514  pntrmax  27532  pntpbnd2  27555  pntlem3  27577  brbtwn2  28889  colinearalglem4  28893  eleesub  28895  eleesubd  28896  axsegconlem2  28902  ax5seglem2  28913  ax5seglem3  28915  axpaschlem  28924  axpasch  28925  axcontlem2  28949  crctcshwlkn0lem3  29799  crctcshwlkn0lem7  29803  eucrctshift  30229  xlt2addrd  32741  signshf  34625  resconn  35273  sinccvglem  35699  fz0n  35753  dnibndlem4  36504  dnibndlem6  36506  dnibndlem7  36507  dnibndlem9  36509  dnibndlem10  36510  knoppndvlem15  36549  sin2h  37639  tan2h  37641  poimir  37682  mblfinlem3  37688  mblfinlem4  37689  itg2addnclem  37700  itg2addnclem3  37702  ftc1anclem5  37726  ftc1anclem6  37727  ftc1anclem7  37728  dvasin  37733  geomcau  37788  bfp  37853  ismrer1  37867  iccbnd  37869  jm2.17a  42959  acongeq  42982  jm3.1lem2  43017  areaquad  43215  lptre2pt  45649  dvnmul  45952  stoweidlem59  46068  fourierdlem42  46158  hoidmvlelem2  46605  smfmullem1  46800  ltsubsubaddltsub  47310  zm1nn  47311  nn0resubcl  47317  subsubelfzo0  47335  bgoldbtbndlem2  47800  ply1mulgsumlem2  48343  ltsubaddb  48470  ltsubsubb  48471  ltsubadd2b  48472  line2  48712