Theorem resubcl 11517

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 11185	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11185	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11501	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 607	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11516	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11178	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 604	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2864	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093  ℝcr 11094   + caddc 11098   − cmin 11436  -cneg 11437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-ltxr 11243  df-sub 11438  df-neg 11439

This theorem is referenced by:  peano2rem  11520  resubcld  11637  ltaddsub  11683  leaddsub  11685  posdif  11702  lt2sub  11707  le2sub  11708  mulsuble0b  12082  cju  12209  elz2  12604  rpnnen1lem5  13000  difrp  13051  qbtwnre  13220  iooshf  13448  iccshftl  13510  lincmb01cmp  13517  uzsubsubfz  13570  difelfzle  13665  fzonmapblen  13733  eluzgtdifelfzo  13752  subfzo0  13817  fracle1  13832  fldiv  13889  modcl  13902  2submod  13964  modsubdir  13972  modfzo0difsn  13975  expubnd  14210  absdiflt  15365  absdifle  15366  elicc4abs  15367  abssubge0  15375  abs2difabs  15382  rddif  15388  absrdbnd  15389  climsup  15717  flo1  15904  supcvg  15906  refallfaccl  16068  resin4p  16189  recos4p  16190  cos01bnd  16237  cos01gt0  16242  pythagtriplem12  16881  pythagtriplem14  16883  pythagtriplem16  16885  fldivp1  16952  prmreclem6  16976  cshwshashlem2  17151  bl2ioo  24949  ioo2bl  24950  ioo2blex  24951  blssioo  24952  blcvx  24955  reconnlem2  24985  opnreen  24989  iirev  25088  iihalf2  25092  iccpnfhmeo  25104  iccvolcl  25726  ioovolcl  25729  ismbf3d  25813  itgrecl  25957  cmvth  26150  dvle  26166  dvcvx  26179  dvfsumge  26181  aalioulem3  26497  aaliou  26501  aaliou3lem9  26513  abelthlem2  26595  abelthlem7  26601  abelth2  26605  sincosq1sgn  26663  sincosq2sgn  26664  sincosq3sgn  26665  sincosq4sgn  26666  tangtx  26670  sinq12gt0  26672  cosq14gt0  26675  cosq14ge0  26676  cosne0  26694  sinord  26699  resinf1o  26701  tanregt0  26704  efif1olem2  26708  relogdiv  26758  logneg2  26780  logdivlti  26785  logcnlem4  26810  logccv  26828  cxpaddlelem  26916  loglesqrt  26926  ang180lem2  26975  acoscos  27058  acosbnd  27065  acosrecl  27068  atanlogaddlem  27078  atans2  27096  leibpi  27107  divsqrtsumo1  27148  cvxcl  27149  scvxcvx  27150  jensenlem2  27152  amgmlem  27154  harmonicbnd4  27175  zetacvg  27179  ftalem5  27241  basellem9  27253  mumullem2  27344  ppiub  27368  chtub  27376  bposlem1  27448  bposlem6  27453  bposlem9  27456  gausslemma2dlem1a  27529  chtppilim  27639  chto1ub  27640  rplogsumlem2  27649  rpvmasumlem  27651  dchrisum0flblem1  27672  dchrisum0re  27677  log2sumbnd  27708  selberglem2  27710  pntrmax  27728  pntpbnd2  27751  pntlem3  27773  brbtwn2  29255  colinearalglem4  29259  eleesub  29261  eleesubd  29262  axsegconlem2  29268  ax5seglem2  29279  ax5seglem3  29281  axpaschlem  29290  axpasch  29291  axcontlem2  29315  crctcshwlkn0lem3  30161  crctcshwlkn0lem7  30165  eucrctshift  30594  xlt2addrd  33104  signshf  34975  resconn  35738  sinccvglem  36164  fz0n  36223  dnibndlem4  37070  dnibndlem6  37072  dnibndlem7  37073  dnibndlem9  37075  dnibndlem10  37076  knoppndvlem15  37115  sin2h  38261  tan2h  38263  poimir  38304  mblfinlem3  38310  mblfinlem4  38311  itg2addnclem  38322  itg2addnclem3  38324  ftc1anclem5  38348  ftc1anclem6  38349  ftc1anclem7  38350  dvasin  38355  geomcau  38410  bfp  38475  ismrer1  38489  iccbnd  38491  jm2.17a  43687  acongeq  43710  jm3.1lem2  43745  areaquad  43943  lptre2pt  46354  dvnmul  46657  stoweidlem59  46773  fourierdlem42  46863  hoidmvlelem2  47310  smfmullem1  47505  ltsubsubaddltsub  48038  zm1nn  48039  nn0resubcl  48045  subsubelfzo0  48064  bgoldbtbndlem2  48571  ply1mulgsumlem2  49167  ltsubaddb  49294  ltsubsubb  49295  ltsubadd2b  49296  line2  49532