Theorem resubcl 11521

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 11189	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11189	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11505	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 607	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11520	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11182	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 604	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2870	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  (class class class)co 7411  ℂcc 11097  ℝcr 11098   + caddc 11102   − cmin 11440  -cneg 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-ltxr 11247  df-sub 11442  df-neg 11443

This theorem is referenced by:  peano2rem  11524  resubcld  11641  ltaddsub  11687  leaddsub  11689  posdif  11706  lt2sub  11711  le2sub  11712  mulsuble0b  12086  cju  12213  elz2  12608  rpnnen1lem5  13004  difrp  13055  qbtwnre  13224  iooshf  13452  iccshftl  13514  lincmb01cmp  13521  uzsubsubfz  13573  difelfzle  13668  fzonmapblen  13736  eluzgtdifelfzo  13755  subfzo0  13820  fracle1  13835  fldiv  13892  modcl  13905  2submod  13967  modsubdir  13975  modfzo0difsn  13978  expubnd  14213  absdiflt  15368  absdifle  15369  elicc4abs  15370  abssubge0  15378  abs2difabs  15385  rddif  15391  absrdbnd  15392  climsup  15720  flo1  15907  supcvg  15909  refallfaccl  16071  resin4p  16193  recos4p  16194  cos01bnd  16241  cos01gt0  16246  pythagtriplem12  16885  pythagtriplem14  16887  pythagtriplem16  16889  fldivp1  16956  prmreclem6  16980  cshwshashlem2  17155  bl2ioo  24917  ioo2bl  24918  ioo2blex  24919  blssioo  24920  blcvx  24923  reconnlem2  24953  opnreen  24957  iirev  25056  iihalf2  25060  iccpnfhmeo  25072  iccvolcl  25694  ioovolcl  25697  ismbf3d  25781  itgrecl  25925  cmvth  26118  dvle  26134  dvcvx  26147  dvfsumge  26149  aalioulem3  26463  aaliou  26467  aaliou3lem9  26479  abelthlem2  26560  abelthlem7  26566  abelth2  26570  sincosq1sgn  26628  sincosq2sgn  26629  sincosq3sgn  26630  sincosq4sgn  26631  tangtx  26635  sinq12gt0  26637  cosq14gt0  26640  cosq14ge0  26641  cosne0  26659  sinord  26664  resinf1o  26666  tanregt0  26669  efif1olem2  26673  relogdiv  26723  logneg2  26745  logdivlti  26750  logcnlem4  26775  logccv  26793  cxpaddlelem  26881  loglesqrt  26891  ang180lem2  26940  acoscos  27023  acosbnd  27030  acosrecl  27033  atanlogaddlem  27043  atans2  27061  leibpi  27072  divsqrtsumo1  27113  cvxcl  27114  scvxcvx  27115  jensenlem2  27117  amgmlem  27119  harmonicbnd4  27140  zetacvg  27144  ftalem5  27206  basellem9  27218  mumullem2  27309  ppiub  27333  chtub  27341  bposlem1  27413  bposlem6  27418  bposlem9  27421  gausslemma2dlem1a  27494  chtppilim  27604  chto1ub  27605  rplogsumlem2  27614  rpvmasumlem  27616  dchrisum0flblem1  27637  dchrisum0re  27642  log2sumbnd  27673  selberglem2  27675  pntrmax  27693  pntpbnd2  27716  pntlem3  27738  brbtwn2  29195  colinearalglem4  29199  eleesub  29201  eleesubd  29202  axsegconlem2  29208  ax5seglem2  29219  ax5seglem3  29221  axpaschlem  29230  axpasch  29231  axcontlem2  29255  crctcshwlkn0lem3  30101  crctcshwlkn0lem7  30105  eucrctshift  30534  xlt2addrd  33044  signshf  34919  resconn  35636  sinccvglem  36062  fz0n  36121  dnibndlem4  36958  dnibndlem6  36960  dnibndlem7  36961  dnibndlem9  36963  dnibndlem10  36964  knoppndvlem15  37003  sin2h  38148  tan2h  38150  poimir  38191  mblfinlem3  38197  mblfinlem4  38198  itg2addnclem  38209  itg2addnclem3  38211  ftc1anclem5  38235  ftc1anclem6  38236  ftc1anclem7  38237  dvasin  38242  geomcau  38297  bfp  38362  ismrer1  38376  iccbnd  38378  jm2.17a  43578  acongeq  43601  jm3.1lem2  43636  areaquad  43834  lptre2pt  46245  dvnmul  46548  stoweidlem59  46664  fourierdlem42  46754  hoidmvlelem2  47201  smfmullem1  47396  ltsubsubaddltsub  47926  zm1nn  47927  nn0resubcl  47933  subsubelfzo0  47952  bgoldbtbndlem2  48459  ply1mulgsumlem2  49051  ltsubaddb  49178  ltsubsubb  49179  ltsubadd2b  49180  line2  49416