Theorem resubcl 11445

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 11116	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11116	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11429	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11444	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11109	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2837	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  ℝcr 11025   + caddc 11029   − cmin 11364  -cneg 11365

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171  df-sub 11366  df-neg 11367

This theorem is referenced by:  peano2rem  11448  resubcld  11565  ltaddsub  11611  leaddsub  11613  posdif  11630  lt2sub  11635  le2sub  11636  mulsuble0b  12014  cju  12141  elz2  12506  rpnnen1lem5  12894  difrp  12945  qbtwnre  13114  iooshf  13342  iccshftl  13404  lincmb01cmp  13411  uzsubsubfz  13462  difelfzle  13557  fzonmapblen  13624  eluzgtdifelfzo  13643  subfzo0  13708  fracle1  13723  fldiv  13780  modcl  13793  2submod  13855  modsubdir  13863  modfzo0difsn  13866  expubnd  14101  absdiflt  15241  absdifle  15242  elicc4abs  15243  abssubge0  15251  abs2difabs  15258  rddif  15264  absrdbnd  15265  climsup  15593  flo1  15777  supcvg  15779  refallfaccl  15941  resin4p  16063  recos4p  16064  cos01bnd  16111  cos01gt0  16116  pythagtriplem12  16754  pythagtriplem14  16756  pythagtriplem16  16758  fldivp1  16825  prmreclem6  16849  cshwshashlem2  17024  bl2ioo  24736  ioo2bl  24737  ioo2blex  24738  blssioo  24739  blcvx  24742  reconnlem2  24772  opnreen  24776  iirev  24879  iihalf2  24884  iccpnfhmeo  24899  iccvolcl  25524  ioovolcl  25527  ismbf3d  25611  itgrecl  25755  cmvth  25951  cmvthOLD  25952  dvle  25968  dvcvx  25981  dvfsumge  25984  aalioulem3  26298  aaliou  26302  aaliou3lem9  26314  abelthlem2  26398  abelthlem7  26404  abelth2  26408  sincosq1sgn  26463  sincosq2sgn  26464  sincosq3sgn  26465  sincosq4sgn  26466  tangtx  26470  sinq12gt0  26472  cosq14gt0  26475  cosq14ge0  26476  cosne0  26494  sinord  26499  resinf1o  26501  tanregt0  26504  efif1olem2  26508  relogdiv  26558  logneg2  26580  logdivlti  26585  logcnlem4  26610  logccv  26628  cxpaddlelem  26717  loglesqrt  26727  ang180lem2  26776  acoscos  26859  acosbnd  26866  acosrecl  26869  atanlogaddlem  26879  atans2  26897  leibpi  26908  divsqrtsumo1  26950  cvxcl  26951  scvxcvx  26952  jensenlem2  26954  amgmlem  26956  harmonicbnd4  26977  zetacvg  26981  ftalem5  27043  basellem9  27055  mumullem2  27146  ppiub  27171  chtub  27179  bposlem1  27251  bposlem6  27256  bposlem9  27259  gausslemma2dlem1a  27332  chtppilim  27442  chto1ub  27443  rplogsumlem2  27452  rpvmasumlem  27454  dchrisum0flblem1  27475  dchrisum0re  27480  log2sumbnd  27511  selberglem2  27513  pntrmax  27531  pntpbnd2  27554  pntlem3  27576  brbtwn2  28978  colinearalglem4  28982  eleesub  28984  eleesubd  28985  axsegconlem2  28991  ax5seglem2  29002  ax5seglem3  29004  axpaschlem  29013  axpasch  29014  axcontlem2  29038  crctcshwlkn0lem3  29885  crctcshwlkn0lem7  29889  eucrctshift  30318  xlt2addrd  32839  signshf  34745  resconn  35440  sinccvglem  35866  fz0n  35925  dnibndlem4  36681  dnibndlem6  36683  dnibndlem7  36684  dnibndlem9  36686  dnibndlem10  36687  knoppndvlem15  36726  sin2h  37811  tan2h  37813  poimir  37854  mblfinlem3  37860  mblfinlem4  37861  itg2addnclem  37872  itg2addnclem3  37874  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  dvasin  37905  geomcau  37960  bfp  38025  ismrer1  38039  iccbnd  38041  jm2.17a  43202  acongeq  43225  jm3.1lem2  43260  areaquad  43458  lptre2pt  45884  dvnmul  46187  stoweidlem59  46303  fourierdlem42  46393  hoidmvlelem2  46840  smfmullem1  47035  ltsubsubaddltsub  47547  zm1nn  47548  nn0resubcl  47554  subsubelfzo0  47572  bgoldbtbndlem2  48052  ply1mulgsumlem2  48633  ltsubaddb  48760  ltsubsubb  48761  ltsubadd2b  48762  line2  48998