Theorem resubcl 11615

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 11283	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11283	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11599	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 608	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11614	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11276	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 605	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2862	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  (class class class)co 7418  ℂcc 11191  ℝcr 11192   + caddc 11196   − cmin 11534  -cneg 11535

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341  df-sub 11536  df-neg 11537

This theorem is used by:  peano2rem  11618  resubcld  11737  ltaddsub  11783  leaddsub  11785  posdif  11802  lt2sub  11807  le2sub  11808  mulsuble0b  12182  cju  12309  elz2  12704  rpnnen1lem5  13102  difrp  13153  qbtwnre  13322  iooshf  13550  iccshftl  13612  lincmb01cmp  13619  uzsubsubfz  13673  difelfzle  13768  fzonmapblen  13836  eluzgtdifelfzo  13855  subfzo0  13921  fracle1  13936  fldiv  13993  modcl  14006  2submod  14068  modsubdir  14076  modfzo0difsn  14079  expubnd  14314  absdiflt  15478  absdifle  15479  elicc4abs  15480  abssubge0  15488  abs2difabs  15495  rddif  15501  absrdbnd  15502  climsup  15830  flo1  16016  supcvg  16018  refallfaccl  16178  resin4p  16299  recos4p  16300  cos01bnd  16347  cos01gt0  16352  pythagtriplem12  16997  pythagtriplem14  16999  pythagtriplem16  17001  fldivp1  17068  prmreclem6  17092  cshwshashlem2  17267  bl2ioo  25104  ioo2bl  25105  ioo2blex  25106  blssioo  25107  blcvx  25110  reconnlem2  25140  opnreen  25144  iirev  25243  iihalf2  25247  iccpnfhmeo  25259  iccvolcl  25881  ioovolcl  25884  ismbf3d  25968  itgrecl  26111  cmvth  26304  dvle  26320  dvcvx  26333  dvfsumge  26335  aalioulem3  26654  aaliou  26658  aaliou3lem9  26670  abelthlem2  26752  abelthlem7  26758  abelth2  26762  sincosq1sgn  26820  sincosq2sgn  26821  sincosq3sgn  26822  sincosq4sgn  26823  tangtx  26827  sinq12gt0  26829  cosq14gt0  26832  cosq14ge0  26833  cosne0  26850  sinord  26855  resinf1o  26857  tanregt0  26860  efif1olem2  26864  relogdiv  26914  logneg2  26936  logdivlti  26941  logcnlem4  26966  logccv  26984  cxpaddlelem  27072  loglesqrt  27082  ang180lem2  27131  acoscos  27214  acosbnd  27221  acosrecl  27224  atanlogaddlem  27234  atans2  27252  leibpi  27263  divsqrtsumo1  27304  cvxcl  27305  scvxcvx  27306  jensenlem2  27308  amgmlem  27310  harmonicbnd4  27331  zetacvg  27335  ftalem5  27397  basellem9  27409  mumullem2  27500  ppiub  27524  chtub  27532  bposlem1  27604  bposlem6  27609  bposlem9  27612  gausslemma2dlem1a  27685  chtppilim  27795  chto1ub  27796  rplogsumlem2  27805  rpvmasumlem  27807  dchrisum0flblem1  27828  dchrisum0re  27833  log2sumbnd  27864  selberglem2  27866  pntrmax  27884  pntpbnd2  27907  pntlem3  27929  brbtwn2  29476  colinearalglem4  29480  eleesub  29482  eleesubd  29483  axsegconlem2  29489  ax5seglem2  29500  ax5seglem3  29502  axpaschlem  29511  axpasch  29512  axcontlem2  29536  crctcshwlkn0lem3  30394  crctcshwlkn0lem7  30398  eucrctshift  30837  xlt2addrd  33344  signshf  35210  resconn  35990  sinccvglem  36416  fz0n  36475  dnibndlem4  37327  dnibndlem6  37329  dnibndlem7  37330  dnibndlem9  37332  dnibndlem10  37333  knoppndvlem15  37372  sin2h  38513  tan2h  38515  poimir  38551  mblfinlem3  38557  mblfinlem4  38558  itg2addnclem  38569  itg2addnclem3  38571  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  dvasin  38602  geomcau  38673  bfp  38738  ismrer1  38752  iccbnd  38754  jm2.17a  43946  acongeq  43969  jm3.1lem2  44004  areaquad  44202  lptre2pt  46619  dvnmul  46922  stoweidlem59  47038  fourierdlem42  47128  hoidmvlelem2  47575  smfmullem1  47770  ltsubsubaddltsub  48340  zm1nn  48341  nn0resubcl  48347  subsubelfzo0  48366  bgoldbtbndlem2  48873  ply1mulgsumlem2  49468  ltsubaddb  49595  ltsubsubb  49596  ltsubadd2b  49597  line2  49833