Theorem resubcl 11443

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 11114	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11114	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11427	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11442	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11107	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2835	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  (class class class)co 7356  ℂcc 11022  ℝcr 11023   + caddc 11027   − cmin 11362  -cneg 11363

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-ltxr 11169  df-sub 11364  df-neg 11365

This theorem is referenced by:  peano2rem  11446  resubcld  11563  ltaddsub  11609  leaddsub  11611  posdif  11628  lt2sub  11633  le2sub  11634  mulsuble0b  12012  cju  12139  elz2  12504  rpnnen1lem5  12892  difrp  12943  qbtwnre  13112  iooshf  13340  iccshftl  13402  lincmb01cmp  13409  uzsubsubfz  13460  difelfzle  13555  fzonmapblen  13622  eluzgtdifelfzo  13641  subfzo0  13706  fracle1  13721  fldiv  13778  modcl  13791  2submod  13853  modsubdir  13861  modfzo0difsn  13864  expubnd  14099  absdiflt  15239  absdifle  15240  elicc4abs  15241  abssubge0  15249  abs2difabs  15256  rddif  15262  absrdbnd  15263  climsup  15591  flo1  15775  supcvg  15777  refallfaccl  15939  resin4p  16061  recos4p  16062  cos01bnd  16109  cos01gt0  16114  pythagtriplem12  16752  pythagtriplem14  16754  pythagtriplem16  16756  fldivp1  16823  prmreclem6  16847  cshwshashlem2  17022  bl2ioo  24734  ioo2bl  24735  ioo2blex  24736  blssioo  24737  blcvx  24740  reconnlem2  24770  opnreen  24774  iirev  24877  iihalf2  24882  iccpnfhmeo  24897  iccvolcl  25522  ioovolcl  25525  ismbf3d  25609  itgrecl  25753  cmvth  25949  cmvthOLD  25950  dvle  25966  dvcvx  25979  dvfsumge  25982  aalioulem3  26296  aaliou  26300  aaliou3lem9  26312  abelthlem2  26396  abelthlem7  26402  abelth2  26406  sincosq1sgn  26461  sincosq2sgn  26462  sincosq3sgn  26463  sincosq4sgn  26464  tangtx  26468  sinq12gt0  26470  cosq14gt0  26473  cosq14ge0  26474  cosne0  26492  sinord  26497  resinf1o  26499  tanregt0  26502  efif1olem2  26506  relogdiv  26556  logneg2  26578  logdivlti  26583  logcnlem4  26608  logccv  26626  cxpaddlelem  26715  loglesqrt  26725  ang180lem2  26774  acoscos  26857  acosbnd  26864  acosrecl  26867  atanlogaddlem  26877  atans2  26895  leibpi  26906  divsqrtsumo1  26948  cvxcl  26949  scvxcvx  26950  jensenlem2  26952  amgmlem  26954  harmonicbnd4  26975  zetacvg  26979  ftalem5  27041  basellem9  27053  mumullem2  27144  ppiub  27169  chtub  27177  bposlem1  27249  bposlem6  27254  bposlem9  27257  gausslemma2dlem1a  27330  chtppilim  27440  chto1ub  27441  rplogsumlem2  27450  rpvmasumlem  27452  dchrisum0flblem1  27473  dchrisum0re  27478  log2sumbnd  27509  selberglem2  27511  pntrmax  27529  pntpbnd2  27552  pntlem3  27574  brbtwn2  28927  colinearalglem4  28931  eleesub  28933  eleesubd  28934  axsegconlem2  28940  ax5seglem2  28951  ax5seglem3  28953  axpaschlem  28962  axpasch  28963  axcontlem2  28987  crctcshwlkn0lem3  29834  crctcshwlkn0lem7  29838  eucrctshift  30267  xlt2addrd  32788  signshf  34694  resconn  35389  sinccvglem  35815  fz0n  35874  dnibndlem4  36624  dnibndlem6  36626  dnibndlem7  36627  dnibndlem9  36629  dnibndlem10  36630  knoppndvlem15  36669  sin2h  37750  tan2h  37752  poimir  37793  mblfinlem3  37799  mblfinlem4  37800  itg2addnclem  37811  itg2addnclem3  37813  ftc1anclem5  37837  ftc1anclem6  37838  ftc1anclem7  37839  dvasin  37844  geomcau  37899  bfp  37964  ismrer1  37978  iccbnd  37980  jm2.17a  43144  acongeq  43167  jm3.1lem2  43202  areaquad  43400  lptre2pt  45826  dvnmul  46129  stoweidlem59  46245  fourierdlem42  46335  hoidmvlelem2  46782  smfmullem1  46977  ltsubsubaddltsub  47489  zm1nn  47490  nn0resubcl  47496  subsubelfzo0  47514  bgoldbtbndlem2  47994  ply1mulgsumlem2  48575  ltsubaddb  48702  ltsubsubb  48703  ltsubadd2b  48704  line2  48940