Theorem resubcl 10936

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 10613	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 10613	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 10920	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 597	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 10935	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 10606	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 594	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2914	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  (class class class)co 7142  ℂcc 10521  ℝcr 10522   + caddc 10526   − cmin 10856  -cneg 10857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-po 5460  df-so 5461  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-pnf 10663  df-mnf 10664  df-ltxr 10666  df-sub 10858  df-neg 10859

This theorem is referenced by:  peano2rem  10939  resubcld  11054  ltaddsub  11100  leaddsub  11102  posdif  11119  lt2sub  11124  le2sub  11125  mulsuble0b  11498  cju  11620  elz2  11986  rpnnen1lem5  12367  difrp  12414  qbtwnre  12579  iooshf  12802  iccshftl  12863  lincmb01cmp  12870  uzsubsubfz  12919  difelfzle  13010  fzonmapblen  13073  eluzgtdifelfzo  13089  subfzo0  13149  fracle1  13163  fldiv  13218  modcl  13231  2submod  13290  modsubdir  13298  modfzo0difsn  13301  expubnd  13531  absdiflt  14662  absdifle  14663  elicc4abs  14664  abssubge0  14672  abs2difabs  14679  rddif  14685  absrdbnd  14686  climsup  15011  flo1  15194  supcvg  15196  refallfaccl  15357  resin4p  15476  recos4p  15477  cos01bnd  15524  cos01gt0  15529  pythagtriplem12  16146  pythagtriplem14  16148  pythagtriplem16  16150  fldivp1  16216  prmreclem6  16240  cshwshashlem2  16413  bl2ioo  23383  ioo2bl  23384  ioo2blex  23385  blssioo  23386  blcvx  23389  reconnlem2  23418  opnreen  23422  iirev  23516  iihalf2  23520  iccpnfhmeo  23532  iccvolcl  24151  ioovolcl  24154  ismbf3d  24238  itgrecl  24381  cmvth  24573  dvle  24589  dvcvx  24602  dvfsumge  24604  aalioulem3  24909  aaliou  24913  aaliou3lem9  24925  abelthlem2  25006  abelthlem7  25012  abelth2  25016  sincosq1sgn  25070  sincosq2sgn  25071  sincosq3sgn  25072  sincosq4sgn  25073  tangtx  25077  sinq12gt0  25079  cosq14gt0  25082  cosq14ge0  25083  cosne0  25100  sinord  25104  resinf1o  25106  tanregt0  25109  efif1olem2  25113  relogdiv  25162  logneg2  25184  logdivlti  25189  logcnlem4  25214  logccv  25232  cxpaddlelem  25318  loglesqrt  25325  ang180lem2  25374  acoscos  25457  acosbnd  25464  acosrecl  25467  atanlogaddlem  25477  atans2  25495  leibpi  25506  divsqrtsumo1  25547  cvxcl  25548  scvxcvx  25549  jensenlem2  25551  amgmlem  25553  harmonicbnd4  25574  zetacvg  25578  ftalem5  25640  basellem9  25652  mumullem2  25743  ppiub  25766  chtub  25774  bposlem1  25846  bposlem6  25851  bposlem9  25854  gausslemma2dlem1a  25927  chtppilim  26037  chto1ub  26038  rplogsumlem2  26047  rpvmasumlem  26049  dchrisum0flblem1  26070  dchrisum0re  26075  log2sumbnd  26106  selberglem2  26108  pntrmax  26126  pntpbnd2  26149  pntlem3  26171  brbtwn2  26677  colinearalglem4  26681  eleesub  26683  eleesubd  26684  axsegconlem2  26690  ax5seglem2  26701  ax5seglem3  26703  axpaschlem  26712  axpasch  26713  axcontlem2  26737  crctcshwlkn0lem3  27576  crctcshwlkn0lem7  27580  eucrctshift  28006  xlt2addrd  30468  signshf  31865  resconn  32500  sinccvglem  32922  fz0n  32969  dnibndlem4  33827  dnibndlem6  33829  dnibndlem7  33830  dnibndlem9  33832  dnibndlem10  33833  knoppndvlem15  33872  sin2h  34916  tan2h  34918  poimir  34959  mblfinlem3  34965  mblfinlem4  34966  itg2addnclem  34977  itg2addnclem3  34979  ftc1anclem5  35003  ftc1anclem6  35004  ftc1anclem7  35005  dvasin  35010  geomcau  35066  bfp  35134  ismrer1  35148  iccbnd  35150  jm2.17a  39649  acongeq  39672  jm3.1lem2  39707  areaquad  39914  lptre2pt  42011  dvnmul  42318  stoweidlem59  42434  fourierdlem42  42524  hoidmvlelem2  42968  smfmullem1  43156  ltsubsubaddltsub  43591  zm1nn  43592  nn0resubcl  43598  subsubelfzo0  43616  bgoldbtbndlem2  44056  ply1mulgsumlem2  44526  ltsubaddb  44654  ltsubsubb  44655  ltsubadd2b  44656  line2  44824