Theorem resubcl 11387

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 11063	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11063	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11371	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11386	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11056	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2838	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105  (class class class)co 7338  ℂcc 10971  ℝcr 10972   + caddc 10976   − cmin 11307  -cneg 11308

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-br 5094  df-opab 5156  df-mpt 5177  df-id 5519  df-po 5533  df-so 5534  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-er 8570  df-en 8806  df-dom 8807  df-sdom 8808  df-pnf 11113  df-mnf 11114  df-ltxr 11116  df-sub 11309  df-neg 11310

This theorem is referenced by:  peano2rem  11390  resubcld  11505  ltaddsub  11551  leaddsub  11553  posdif  11570  lt2sub  11575  le2sub  11576  mulsuble0b  11949  cju  12071  elz2  12439  rpnnen1lem5  12823  difrp  12870  qbtwnre  13035  iooshf  13260  iccshftl  13322  lincmb01cmp  13329  uzsubsubfz  13380  difelfzle  13471  fzonmapblen  13535  eluzgtdifelfzo  13551  subfzo0  13611  fracle1  13625  fldiv  13682  modcl  13695  2submod  13754  modsubdir  13762  modfzo0difsn  13765  expubnd  13997  absdiflt  15129  absdifle  15130  elicc4abs  15131  abssubge0  15139  abs2difabs  15146  rddif  15152  absrdbnd  15153  climsup  15481  flo1  15666  supcvg  15668  refallfaccl  15828  resin4p  15947  recos4p  15948  cos01bnd  15995  cos01gt0  16000  pythagtriplem12  16625  pythagtriplem14  16627  pythagtriplem16  16629  fldivp1  16696  prmreclem6  16720  cshwshashlem2  16896  bl2ioo  24062  ioo2bl  24063  ioo2blex  24064  blssioo  24065  blcvx  24068  reconnlem2  24097  opnreen  24101  iirev  24199  iihalf2  24203  iccpnfhmeo  24215  iccvolcl  24838  ioovolcl  24841  ismbf3d  24925  itgrecl  25069  cmvth  25262  dvle  25278  dvcvx  25291  dvfsumge  25293  aalioulem3  25601  aaliou  25605  aaliou3lem9  25617  abelthlem2  25698  abelthlem7  25704  abelth2  25708  sincosq1sgn  25762  sincosq2sgn  25763  sincosq3sgn  25764  sincosq4sgn  25765  tangtx  25769  sinq12gt0  25771  cosq14gt0  25774  cosq14ge0  25775  cosne0  25792  sinord  25797  resinf1o  25799  tanregt0  25802  efif1olem2  25806  relogdiv  25855  logneg2  25877  logdivlti  25882  logcnlem4  25907  logccv  25925  cxpaddlelem  26011  loglesqrt  26018  ang180lem2  26067  acoscos  26150  acosbnd  26157  acosrecl  26160  atanlogaddlem  26170  atans2  26188  leibpi  26199  divsqrtsumo1  26240  cvxcl  26241  scvxcvx  26242  jensenlem2  26244  amgmlem  26246  harmonicbnd4  26267  zetacvg  26271  ftalem5  26333  basellem9  26345  mumullem2  26436  ppiub  26459  chtub  26467  bposlem1  26539  bposlem6  26544  bposlem9  26547  gausslemma2dlem1a  26620  chtppilim  26730  chto1ub  26731  rplogsumlem2  26740  rpvmasumlem  26742  dchrisum0flblem1  26763  dchrisum0re  26768  log2sumbnd  26799  selberglem2  26801  pntrmax  26819  pntpbnd2  26842  pntlem3  26864  brbtwn2  27563  colinearalglem4  27567  eleesub  27569  eleesubd  27570  axsegconlem2  27576  ax5seglem2  27587  ax5seglem3  27589  axpaschlem  27598  axpasch  27599  axcontlem2  27623  crctcshwlkn0lem3  28466  crctcshwlkn0lem7  28470  eucrctshift  28896  xlt2addrd  31368  signshf  32867  resconn  33507  sinccvglem  33929  fz0n  33988  dnibndlem4  34800  dnibndlem6  34802  dnibndlem7  34803  dnibndlem9  34805  dnibndlem10  34806  knoppndvlem15  34845  sin2h  35923  tan2h  35925  poimir  35966  mblfinlem3  35972  mblfinlem4  35973  itg2addnclem  35984  itg2addnclem3  35986  ftc1anclem5  36010  ftc1anclem6  36011  ftc1anclem7  36012  dvasin  36017  geomcau  36073  bfp  36138  ismrer1  36152  iccbnd  36154  jm2.17a  41096  acongeq  41119  jm3.1lem2  41154  areaquad  41362  lptre2pt  43569  dvnmul  43872  stoweidlem59  43988  fourierdlem42  44078  hoidmvlelem2  44523  smfmullem1  44718  ltsubsubaddltsub  45211  zm1nn  45212  nn0resubcl  45218  subsubelfzo0  45236  bgoldbtbndlem2  45676  ply1mulgsumlem2  46146  ltsubaddb  46273  ltsubsubb  46274  ltsubadd2b  46275  line2  46516