Theorem resubcl 11452

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 11122	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11122	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11436	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 597	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11451	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11115	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 594	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2838	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030  ℝcr 11031   + caddc 11035   − cmin 11371  -cneg 11372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-ltxr 11178  df-sub 11373  df-neg 11374

This theorem is referenced by:  peano2rem  11455  resubcld  11572  ltaddsub  11618  leaddsub  11620  posdif  11637  lt2sub  11642  le2sub  11643  mulsuble0b  12022  cju  12149  elz2  12536  rpnnen1lem5  12925  difrp  12976  qbtwnre  13145  iooshf  13373  iccshftl  13435  lincmb01cmp  13442  uzsubsubfz  13494  difelfzle  13589  fzonmapblen  13657  eluzgtdifelfzo  13676  subfzo0  13741  fracle1  13756  fldiv  13813  modcl  13826  2submod  13888  modsubdir  13896  modfzo0difsn  13899  expubnd  14134  absdiflt  15274  absdifle  15275  elicc4abs  15276  abssubge0  15284  abs2difabs  15291  rddif  15297  absrdbnd  15298  climsup  15626  flo1  15813  supcvg  15815  refallfaccl  15977  resin4p  16099  recos4p  16100  cos01bnd  16147  cos01gt0  16152  pythagtriplem12  16791  pythagtriplem14  16793  pythagtriplem16  16795  fldivp1  16862  prmreclem6  16886  cshwshashlem2  17061  bl2ioo  24770  ioo2bl  24771  ioo2blex  24772  blssioo  24773  blcvx  24776  reconnlem2  24806  opnreen  24810  iirev  24909  iihalf2  24913  iccpnfhmeo  24925  iccvolcl  25547  ioovolcl  25550  ismbf3d  25634  itgrecl  25778  cmvth  25971  dvle  25987  dvcvx  26000  dvfsumge  26002  aalioulem3  26314  aaliou  26318  aaliou3lem9  26330  abelthlem2  26413  abelthlem7  26419  abelth2  26423  sincosq1sgn  26478  sincosq2sgn  26479  sincosq3sgn  26480  sincosq4sgn  26481  tangtx  26485  sinq12gt0  26487  cosq14gt0  26490  cosq14ge0  26491  cosne0  26509  sinord  26514  resinf1o  26516  tanregt0  26519  efif1olem2  26523  relogdiv  26573  logneg2  26595  logdivlti  26600  logcnlem4  26625  logccv  26643  cxpaddlelem  26731  loglesqrt  26741  ang180lem2  26790  acoscos  26873  acosbnd  26880  acosrecl  26883  atanlogaddlem  26893  atans2  26911  leibpi  26922  divsqrtsumo1  26964  cvxcl  26965  scvxcvx  26966  jensenlem2  26968  amgmlem  26970  harmonicbnd4  26991  zetacvg  26995  ftalem5  27057  basellem9  27069  mumullem2  27160  ppiub  27184  chtub  27192  bposlem1  27264  bposlem6  27269  bposlem9  27272  gausslemma2dlem1a  27345  chtppilim  27455  chto1ub  27456  rplogsumlem2  27465  rpvmasumlem  27467  dchrisum0flblem1  27488  dchrisum0re  27493  log2sumbnd  27524  selberglem2  27526  pntrmax  27544  pntpbnd2  27567  pntlem3  27589  brbtwn2  28991  colinearalglem4  28995  eleesub  28997  eleesubd  28998  axsegconlem2  29004  ax5seglem2  29015  ax5seglem3  29017  axpaschlem  29026  axpasch  29027  axcontlem2  29051  crctcshwlkn0lem3  29898  crctcshwlkn0lem7  29902  eucrctshift  30331  xlt2addrd  32850  signshf  34751  resconn  35447  sinccvglem  35873  fz0n  35932  dnibndlem4  36760  dnibndlem6  36762  dnibndlem7  36763  dnibndlem9  36765  dnibndlem10  36766  knoppndvlem15  36805  sin2h  37948  tan2h  37950  poimir  37991  mblfinlem3  37997  mblfinlem4  37998  itg2addnclem  38009  itg2addnclem3  38011  ftc1anclem5  38035  ftc1anclem6  38036  ftc1anclem7  38037  dvasin  38042  geomcau  38097  bfp  38162  ismrer1  38176  iccbnd  38178  jm2.17a  43409  acongeq  43432  jm3.1lem2  43467  areaquad  43665  lptre2pt  46089  dvnmul  46392  stoweidlem59  46508  fourierdlem42  46598  hoidmvlelem2  47045  smfmullem1  47240  ltsubsubaddltsub  47764  zm1nn  47765  nn0resubcl  47771  subsubelfzo0  47790  bgoldbtbndlem2  48297  ply1mulgsumlem2  48878  ltsubaddb  49005  ltsubsubb  49006  ltsubadd2b  49007  line2  49243