Theorem resubcl 11622

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 11290	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11290	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11606	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 608	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11621	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11283	. . 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 7420  ℂcc 11198  ℝcr 11199   + caddc 11203   − cmin 11541   -cneg 11542

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 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

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 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-sub 11543  df-neg 11544

This theorem is used by:  peano2rem  11625  resubcld  11744  ltaddsub  11790  leaddsub  11792  posdif  11809  lt2sub  11814  le2sub  11815  mulsuble0b  12189  cju  12316  elz2  12711  rpnnen1lem5  13109  difrp  13160  qbtwnre  13329  iooshf  13557  iccshftl  13619  lincmb01cmp  13626  uzsubsubfz  13680  difelfzle  13775  fzonmapblen  13843  eluzgtdifelfzo  13862  subfzo0  13928  fracle1  13943  fldiv  14000  modcl  14013  2submod  14075  modsubdir  14083  modfzo0difsn  14086  expubnd  14321  absdiflt  15485  absdifle  15486  elicc4abs  15487  abssubge0  15495  abs2difabs  15502  rddif  15508  absrdbnd  15509  climsup  15837  flo1  16023  supcvg  16025  refallfaccl  16185  resin4p  16306  recos4p  16307  cos01bnd  16354  cos01gt0  16359  pythagtriplem12  17004  pythagtriplem14  17006  pythagtriplem16  17008  fldivp1  17075  prmreclem6  17099  cshwshashlem2  17274  bl2ioo  25111  ioo2bl  25112  ioo2blex  25113  blssioo  25114  blcvx  25117  reconnlem2  25147  opnreen  25151  iirev  25250  iihalf2  25254  iccpnfhmeo  25266  iccvolcl  25888  ioovolcl  25891  ismbf3d  25975  itgrecl  26118  cmvth  26311  dvle  26327  dvcvx  26340  dvfsumge  26342  aalioulem3  26661  aaliou  26665  aaliou3lem9  26677  abelthlem2  26759  abelthlem7  26765  abelth2  26769  sincosq1sgn  26827  sincosq2sgn  26828  sincosq3sgn  26829  sincosq4sgn  26830  tangtx  26834  sinq12gt0  26836  cosq14gt0  26839  cosq14ge0  26840  cosne0  26857  sinord  26862  resinf1o  26864  tanregt0  26867  efif1olem2  26871  relogdiv  26921  logneg2  26943  logdivlti  26948  logcnlem4  26973  logccv  26991  cxpaddlelem  27079  loglesqrt  27089  ang180lem2  27138  acoscos  27221  acosbnd  27228  acosrecl  27231  atanlogaddlem  27241  atans2  27259  leibpi  27270  divsqrtsumo1  27311  cvxcl  27312  scvxcvx  27313  jensenlem2  27315  amgmlem  27317  harmonicbnd4  27338  zetacvg  27342  ftalem5  27404  basellem9  27416  mumullem2  27507  ppiub  27531  chtub  27539  bposlem1  27611  bposlem6  27616  bposlem9  27619  gausslemma2dlem1a  27692  chtppilim  27802  chto1ub  27803  rplogsumlem2  27812  rpvmasumlem  27814  dchrisum0flblem1  27835  dchrisum0re  27840  log2sumbnd  27871  selberglem2  27873  pntrmax  27891  pntpbnd2  27914  pntlem3  27936  brbtwn2  29483  colinearalglem4  29487  eleesub  29489  eleesubd  29490  axsegconlem2  29496  ax5seglem2  29507  ax5seglem3  29509  axpaschlem  29518  axpasch  29519  axcontlem2  29543  crctcshwlkn0lem3  30401  crctcshwlkn0lem7  30405  eucrctshift  30844  xlt2addrd  33351  signshf  35217  resconn  36011  sinccvglem  36437  fz0n  36496  dnibndlem4  37347  dnibndlem6  37349  dnibndlem7  37350  dnibndlem9  37352  dnibndlem10  37353  knoppndvlem15  37392  sin2h  38534  tan2h  38536  poimir  38572  mblfinlem3  38578  mblfinlem4  38579  itg2addnclem  38590  itg2addnclem3  38592  ftc1anclem5  38616  ftc1anclem6  38617  ftc1anclem7  38618  dvasin  38623  geomcau  38694  bfp  38759  ismrer1  38773  iccbnd  38775  jm2.17a  43967  acongeq  43990  jm3.1lem2  44025  areaquad  44218  lptre2pt  46650  dvnmul  46953  stoweidlem59  47069  fourierdlem42  47159  hoidmvlelem2  47606  smfmullem1  47801  ltsubsubaddltsub  48371  zm1nn  48372  nn0resubcl  48378  subsubelfzo0  48397  bgoldbtbndlem2  48904  ply1mulgsumlem2  49499  ltsubaddb  49626  ltsubsubb  49627  ltsubadd2b  49628  line2  49864