Theorem resubcl 11528

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 11202	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11202	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11512	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 594	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11527	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11195	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 591	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2832	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110  ℝcr 11111   + caddc 11115   − cmin 11448  -cneg 11449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-ltxr 11257  df-sub 11450  df-neg 11451

This theorem is referenced by:  peano2rem  11531  resubcld  11646  ltaddsub  11692  leaddsub  11694  posdif  11711  lt2sub  11716  le2sub  11717  mulsuble0b  12090  cju  12212  elz2  12580  rpnnen1lem5  12969  difrp  13016  qbtwnre  13182  iooshf  13407  iccshftl  13469  lincmb01cmp  13476  uzsubsubfz  13527  difelfzle  13618  fzonmapblen  13682  eluzgtdifelfzo  13698  subfzo0  13758  fracle1  13772  fldiv  13829  modcl  13842  2submod  13901  modsubdir  13909  modfzo0difsn  13912  expubnd  14146  absdiflt  15268  absdifle  15269  elicc4abs  15270  abssubge0  15278  abs2difabs  15285  rddif  15291  absrdbnd  15292  climsup  15620  flo1  15804  supcvg  15806  refallfaccl  15966  resin4p  16085  recos4p  16086  cos01bnd  16133  cos01gt0  16138  pythagtriplem12  16763  pythagtriplem14  16765  pythagtriplem16  16767  fldivp1  16834  prmreclem6  16858  cshwshashlem2  17034  bl2ioo  24528  ioo2bl  24529  ioo2blex  24530  blssioo  24531  blcvx  24534  reconnlem2  24563  opnreen  24567  iirev  24670  iihalf2  24675  iccpnfhmeo  24690  iccvolcl  25316  ioovolcl  25319  ismbf3d  25403  itgrecl  25547  cmvth  25743  dvle  25759  dvcvx  25772  dvfsumge  25774  aalioulem3  26083  aaliou  26087  aaliou3lem9  26099  abelthlem2  26180  abelthlem7  26186  abelth2  26190  sincosq1sgn  26244  sincosq2sgn  26245  sincosq3sgn  26246  sincosq4sgn  26247  tangtx  26251  sinq12gt0  26253  cosq14gt0  26256  cosq14ge0  26257  cosne0  26274  sinord  26279  resinf1o  26281  tanregt0  26284  efif1olem2  26288  relogdiv  26337  logneg2  26359  logdivlti  26364  logcnlem4  26389  logccv  26407  cxpaddlelem  26495  loglesqrt  26502  ang180lem2  26551  acoscos  26634  acosbnd  26641  acosrecl  26644  atanlogaddlem  26654  atans2  26672  leibpi  26683  divsqrtsumo1  26724  cvxcl  26725  scvxcvx  26726  jensenlem2  26728  amgmlem  26730  harmonicbnd4  26751  zetacvg  26755  ftalem5  26817  basellem9  26829  mumullem2  26920  ppiub  26943  chtub  26951  bposlem1  27023  bposlem6  27028  bposlem9  27031  gausslemma2dlem1a  27104  chtppilim  27214  chto1ub  27215  rplogsumlem2  27224  rpvmasumlem  27226  dchrisum0flblem1  27247  dchrisum0re  27252  log2sumbnd  27283  selberglem2  27285  pntrmax  27303  pntpbnd2  27326  pntlem3  27348  brbtwn2  28430  colinearalglem4  28434  eleesub  28436  eleesubd  28437  axsegconlem2  28443  ax5seglem2  28454  ax5seglem3  28456  axpaschlem  28465  axpasch  28466  axcontlem2  28490  crctcshwlkn0lem3  29333  crctcshwlkn0lem7  29337  eucrctshift  29763  xlt2addrd  32238  signshf  33897  resconn  34535  sinccvglem  34955  fz0n  35004  gg-cmvth  35466  dnibndlem4  35660  dnibndlem6  35662  dnibndlem7  35663  dnibndlem9  35665  dnibndlem10  35666  knoppndvlem15  35705  sin2h  36781  tan2h  36783  poimir  36824  mblfinlem3  36830  mblfinlem4  36831  itg2addnclem  36842  itg2addnclem3  36844  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  dvasin  36875  geomcau  36930  bfp  36995  ismrer1  37009  iccbnd  37011  jm2.17a  42001  acongeq  42024  jm3.1lem2  42059  areaquad  42267  lptre2pt  44654  dvnmul  44957  stoweidlem59  45073  fourierdlem42  45163  hoidmvlelem2  45610  smfmullem1  45805  ltsubsubaddltsub  46307  zm1nn  46308  nn0resubcl  46314  subsubelfzo0  46332  bgoldbtbndlem2  46772  ply1mulgsumlem2  47155  ltsubaddb  47282  ltsubsubb  47283  ltsubadd2b  47284  line2  47525