Theorem resubcl 11457

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 11128	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11128	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11441	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 597	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11456	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11121	. . 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 7368  ℂcc 11036  ℝcr 11037   + caddc 11041   − cmin 11376  -cneg 11377

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

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 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-sub 11378  df-neg 11379

This theorem is referenced by:  peano2rem  11460  resubcld  11577  ltaddsub  11623  leaddsub  11625  posdif  11642  lt2sub  11647  le2sub  11648  mulsuble0b  12026  cju  12153  elz2  12518  rpnnen1lem5  12906  difrp  12957  qbtwnre  13126  iooshf  13354  iccshftl  13416  lincmb01cmp  13423  uzsubsubfz  13474  difelfzle  13569  fzonmapblen  13636  eluzgtdifelfzo  13655  subfzo0  13720  fracle1  13735  fldiv  13792  modcl  13805  2submod  13867  modsubdir  13875  modfzo0difsn  13878  expubnd  14113  absdiflt  15253  absdifle  15254  elicc4abs  15255  abssubge0  15263  abs2difabs  15270  rddif  15276  absrdbnd  15277  climsup  15605  flo1  15789  supcvg  15791  refallfaccl  15953  resin4p  16075  recos4p  16076  cos01bnd  16123  cos01gt0  16128  pythagtriplem12  16766  pythagtriplem14  16768  pythagtriplem16  16770  fldivp1  16837  prmreclem6  16861  cshwshashlem2  17036  bl2ioo  24748  ioo2bl  24749  ioo2blex  24750  blssioo  24751  blcvx  24754  reconnlem2  24784  opnreen  24788  iirev  24891  iihalf2  24896  iccpnfhmeo  24911  iccvolcl  25536  ioovolcl  25539  ismbf3d  25623  itgrecl  25767  cmvth  25963  cmvthOLD  25964  dvle  25980  dvcvx  25993  dvfsumge  25996  aalioulem3  26310  aaliou  26314  aaliou3lem9  26326  abelthlem2  26410  abelthlem7  26416  abelth2  26420  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  tangtx  26482  sinq12gt0  26484  cosq14gt0  26487  cosq14ge0  26488  cosne0  26506  sinord  26511  resinf1o  26513  tanregt0  26516  efif1olem2  26520  relogdiv  26570  logneg2  26592  logdivlti  26597  logcnlem4  26622  logccv  26640  cxpaddlelem  26729  loglesqrt  26739  ang180lem2  26788  acoscos  26871  acosbnd  26878  acosrecl  26881  atanlogaddlem  26891  atans2  26909  leibpi  26920  divsqrtsumo1  26962  cvxcl  26963  scvxcvx  26964  jensenlem2  26966  amgmlem  26968  harmonicbnd4  26989  zetacvg  26993  ftalem5  27055  basellem9  27067  mumullem2  27158  ppiub  27183  chtub  27191  bposlem1  27263  bposlem6  27268  bposlem9  27271  gausslemma2dlem1a  27344  chtppilim  27454  chto1ub  27455  rplogsumlem2  27464  rpvmasumlem  27466  dchrisum0flblem1  27487  dchrisum0re  27492  log2sumbnd  27523  selberglem2  27525  pntrmax  27543  pntpbnd2  27566  pntlem3  27588  brbtwn2  28990  colinearalglem4  28994  eleesub  28996  eleesubd  28997  axsegconlem2  29003  ax5seglem2  29014  ax5seglem3  29016  axpaschlem  29025  axpasch  29026  axcontlem2  29050  crctcshwlkn0lem3  29897  crctcshwlkn0lem7  29901  eucrctshift  30330  xlt2addrd  32850  signshf  34766  resconn  35462  sinccvglem  35888  fz0n  35947  dnibndlem4  36703  dnibndlem6  36705  dnibndlem7  36706  dnibndlem9  36708  dnibndlem10  36709  knoppndvlem15  36748  sin2h  37861  tan2h  37863  poimir  37904  mblfinlem3  37910  mblfinlem4  37911  itg2addnclem  37922  itg2addnclem3  37924  ftc1anclem5  37948  ftc1anclem6  37949  ftc1anclem7  37950  dvasin  37955  geomcau  38010  bfp  38075  ismrer1  38089  iccbnd  38091  jm2.17a  43317  acongeq  43340  jm3.1lem2  43375  areaquad  43573  lptre2pt  45998  dvnmul  46301  stoweidlem59  46417  fourierdlem42  46507  hoidmvlelem2  46954  smfmullem1  47149  ltsubsubaddltsub  47661  zm1nn  47662  nn0resubcl  47668  subsubelfzo0  47686  bgoldbtbndlem2  48166  ply1mulgsumlem2  48747  ltsubaddb  48874  ltsubsubb  48875  ltsubadd2b  48876  line2  49112