Theorem resubcl 11629

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 11297	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11297	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11613	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 608	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11628	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11290	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 605	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2861	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  (class class class)co 7424  ℂcc 11205  ℝcr 11206   + caddc 11210   − cmin 11548   -cneg 11549

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  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 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-er 8724  df-en 8981  df-dom 8982  df-sdom 8983  df-pnf 11352  df-mnf 11353  df-ltxr 11355  df-sub 11550  df-neg 11551

This theorem is used by:  peano2rem  11632  resubcld  11751  ltaddsub  11797  leaddsub  11799  posdif  11816  lt2sub  11821  le2sub  11822  mulsuble0b  12196  cju  12323  elz2  12718  rpnnen1lem5  13116  difrp  13167  qbtwnre  13336  iooshf  13564  iccshftl  13626  lincmb01cmp  13633  uzsubsubfz  13687  difelfzle  13782  fzonmapblen  13850  eluzgtdifelfzo  13869  subfzo0  13935  fracle1  13950  fldiv  14007  modcl  14020  2submod  14082  modsubdir  14090  modfzo0difsn  14093  expubnd  14328  absdiflt  15494  absdifle  15495  elicc4abs  15496  abssubge0  15504  abs2difabs  15511  rddif  15517  absrdbnd  15518  climsup  15846  flo1  16032  supcvg  16034  refallfaccl  16194  resin4p  16315  recos4p  16316  cos01bnd  16363  cos01gt0  16368  pythagtriplem12  17013  pythagtriplem14  17015  pythagtriplem16  17017  fldivp1  17084  prmreclem6  17108  cshwshashlem2  17283  bl2ioo  25120  ioo2bl  25121  ioo2blex  25122  blssioo  25123  blcvx  25126  reconnlem2  25156  opnreen  25160  iirev  25259  iihalf2  25263  iccpnfhmeo  25275  iccvolcl  25897  ioovolcl  25900  ismbf3d  25984  itgrecl  26127  cmvth  26320  dvle  26336  dvcvx  26349  dvfsumge  26351  aalioulem3  26670  aaliou  26674  aaliou3lem9  26686  abelthlem2  26768  abelthlem7  26774  abelth2  26778  sincosq1sgn  26836  sincosq2sgn  26837  sincosq3sgn  26838  sincosq4sgn  26839  tangtx  26843  sinq12gt0  26845  cosq14gt0  26848  cosq14ge0  26849  cosne0  26866  sinord  26871  resinf1o  26873  tanregt0  26876  efif1olem2  26880  relogdiv  26930  logneg2  26952  logdivlti  26957  logcnlem4  26982  logccv  27000  cxpaddlelem  27088  loglesqrt  27098  ang180lem2  27147  acoscos  27230  acosbnd  27237  acosrecl  27240  atanlogaddlem  27250  atans2  27268  leibpi  27279  divsqrtsumo1  27320  cvxcl  27321  scvxcvx  27322  jensenlem2  27324  amgmlem  27326  harmonicbnd4  27347  zetacvg  27351  ftalem5  27413  basellem9  27425  mumullem2  27516  ppiub  27540  chtub  27548  bposlem1  27620  bposlem6  27625  bposlem9  27628  gausslemma2dlem1a  27701  chtppilim  27811  chto1ub  27812  rplogsumlem2  27821  rpvmasumlem  27823  dchrisum0flblem1  27844  dchrisum0re  27849  log2sumbnd  27880  selberglem2  27882  pntrmax  27900  pntpbnd2  27923  pntlem3  27945  brbtwn2  29492  colinearalglem4  29496  eleesub  29498  eleesubd  29499  axsegconlem2  29505  ax5seglem2  29516  ax5seglem3  29518  axpaschlem  29527  axpasch  29528  axcontlem2  29552  crctcshwlkn0lem3  30410  crctcshwlkn0lem7  30414  eucrctshift  30853  xlt2addrd  33401  signshf  35267  resconn  36101  sinccvglem  36527  fz0n  36592  dnibndlem4  37443  dnibndlem6  37445  dnibndlem7  37446  dnibndlem9  37448  dnibndlem10  37449  knoppndvlem15  37488  sin2h  38642  tan2h  38644  poimir  38680  mblfinlem3  38686  mblfinlem4  38687  itg2addnclem  38698  itg2addnclem3  38700  ftc1anclem5  38724  ftc1anclem6  38725  ftc1anclem7  38726  dvasin  38731  geomcau  38802  bfp  38867  ismrer1  38881  iccbnd  38883  jm2.17a  44076  acongeq  44099  jm3.1lem2  44134  areaquad  44327  lptre2pt  46758  dvnmul  47061  stoweidlem59  47177  fourierdlem42  47267  hoidmvlelem2  47714  smfmullem1  47909  ltsubsubaddltsub  48479  zm1nn  48480  nn0resubcl  48486  subsubelfzo0  48505  bgoldbtbndlem2  49012  ply1mulgsumlem2  49607  ltsubaddb  49734  ltsubsubb  49735  ltsubadd2b  49736  line2  49972