Theorem resubcl 11520

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 11196	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11196	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11504	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11519	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11189	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2834	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  (class class class)co 7405  ℂcc 11104  ℝcr 11105   + caddc 11109   − cmin 11440  -cneg 11441

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442  df-neg 11443

This theorem is referenced by:  peano2rem  11523  resubcld  11638  ltaddsub  11684  leaddsub  11686  posdif  11703  lt2sub  11708  le2sub  11709  mulsuble0b  12082  cju  12204  elz2  12572  rpnnen1lem5  12961  difrp  13008  qbtwnre  13174  iooshf  13399  iccshftl  13461  lincmb01cmp  13468  uzsubsubfz  13519  difelfzle  13610  fzonmapblen  13674  eluzgtdifelfzo  13690  subfzo0  13750  fracle1  13764  fldiv  13821  modcl  13834  2submod  13893  modsubdir  13901  modfzo0difsn  13904  expubnd  14138  absdiflt  15260  absdifle  15261  elicc4abs  15262  abssubge0  15270  abs2difabs  15277  rddif  15283  absrdbnd  15284  climsup  15612  flo1  15796  supcvg  15798  refallfaccl  15958  resin4p  16077  recos4p  16078  cos01bnd  16125  cos01gt0  16130  pythagtriplem12  16755  pythagtriplem14  16757  pythagtriplem16  16759  fldivp1  16826  prmreclem6  16850  cshwshashlem2  17026  bl2ioo  24299  ioo2bl  24300  ioo2blex  24301  blssioo  24302  blcvx  24305  reconnlem2  24334  opnreen  24338  iirev  24436  iihalf2  24440  iccpnfhmeo  24452  iccvolcl  25075  ioovolcl  25078  ismbf3d  25162  itgrecl  25306  cmvth  25499  dvle  25515  dvcvx  25528  dvfsumge  25530  aalioulem3  25838  aaliou  25842  aaliou3lem9  25854  abelthlem2  25935  abelthlem7  25941  abelth2  25945  sincosq1sgn  25999  sincosq2sgn  26000  sincosq3sgn  26001  sincosq4sgn  26002  tangtx  26006  sinq12gt0  26008  cosq14gt0  26011  cosq14ge0  26012  cosne0  26029  sinord  26034  resinf1o  26036  tanregt0  26039  efif1olem2  26043  relogdiv  26092  logneg2  26114  logdivlti  26119  logcnlem4  26144  logccv  26162  cxpaddlelem  26248  loglesqrt  26255  ang180lem2  26304  acoscos  26387  acosbnd  26394  acosrecl  26397  atanlogaddlem  26407  atans2  26425  leibpi  26436  divsqrtsumo1  26477  cvxcl  26478  scvxcvx  26479  jensenlem2  26481  amgmlem  26483  harmonicbnd4  26504  zetacvg  26508  ftalem5  26570  basellem9  26582  mumullem2  26673  ppiub  26696  chtub  26704  bposlem1  26776  bposlem6  26781  bposlem9  26784  gausslemma2dlem1a  26857  chtppilim  26967  chto1ub  26968  rplogsumlem2  26977  rpvmasumlem  26979  dchrisum0flblem1  27000  dchrisum0re  27005  log2sumbnd  27036  selberglem2  27038  pntrmax  27056  pntpbnd2  27079  pntlem3  27101  brbtwn2  28152  colinearalglem4  28156  eleesub  28158  eleesubd  28159  axsegconlem2  28165  ax5seglem2  28176  ax5seglem3  28178  axpaschlem  28187  axpasch  28188  axcontlem2  28212  crctcshwlkn0lem3  29055  crctcshwlkn0lem7  29059  eucrctshift  29485  xlt2addrd  31958  signshf  33587  resconn  34225  sinccvglem  34645  fz0n  34688  gg-cmvth  35169  dnibndlem4  35345  dnibndlem6  35347  dnibndlem7  35348  dnibndlem9  35350  dnibndlem10  35351  knoppndvlem15  35390  sin2h  36466  tan2h  36468  poimir  36509  mblfinlem3  36515  mblfinlem4  36516  itg2addnclem  36527  itg2addnclem3  36529  ftc1anclem5  36553  ftc1anclem6  36554  ftc1anclem7  36555  dvasin  36560  geomcau  36615  bfp  36680  ismrer1  36694  iccbnd  36696  jm2.17a  41684  acongeq  41707  jm3.1lem2  41742  areaquad  41950  lptre2pt  44342  dvnmul  44645  stoweidlem59  44761  fourierdlem42  44851  hoidmvlelem2  45298  smfmullem1  45493  ltsubsubaddltsub  45995  zm1nn  45996  nn0resubcl  46002  subsubelfzo0  46020  bgoldbtbndlem2  46460  ply1mulgsumlem2  47021  ltsubaddb  47148  ltsubsubb  47149  ltsubadd2b  47150  line2  47391