Theorem resubcl 11546

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 11214	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11214	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11530	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 608	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11545	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11207	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 605	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2861	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  (class class class)co 7413  ℂcc 11122  ℝcr 11123   + caddc 11127   − cmin 11465  -cneg 11466

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-ltxr 11272  df-sub 11467  df-neg 11468

This theorem is used by:  peano2rem  11549  resubcld  11666  ltaddsub  11712  leaddsub  11714  posdif  11731  lt2sub  11736  le2sub  11737  mulsuble0b  12111  cju  12238  elz2  12633  rpnnen1lem5  13031  difrp  13082  qbtwnre  13251  iooshf  13479  iccshftl  13541  lincmb01cmp  13548  uzsubsubfz  13601  difelfzle  13696  fzonmapblen  13764  eluzgtdifelfzo  13783  subfzo0  13849  fracle1  13864  fldiv  13921  modcl  13934  2submod  13996  modsubdir  14004  modfzo0difsn  14007  expubnd  14242  absdiflt  15405  absdifle  15406  elicc4abs  15407  abssubge0  15415  abs2difabs  15422  rddif  15428  absrdbnd  15429  climsup  15757  flo1  15943  supcvg  15945  refallfaccl  16105  resin4p  16226  recos4p  16227  cos01bnd  16274  cos01gt0  16279  pythagtriplem12  16918  pythagtriplem14  16920  pythagtriplem16  16922  fldivp1  16989  prmreclem6  17013  cshwshashlem2  17188  bl2ioo  25018  ioo2bl  25019  ioo2blex  25020  blssioo  25021  blcvx  25024  reconnlem2  25054  opnreen  25058  iirev  25157  iihalf2  25161  iccpnfhmeo  25173  iccvolcl  25795  ioovolcl  25798  ismbf3d  25882  itgrecl  26025  cmvth  26218  dvle  26234  dvcvx  26247  dvfsumge  26249  aalioulem3  26570  aaliou  26574  aaliou3lem9  26586  abelthlem2  26668  abelthlem7  26674  abelth2  26678  sincosq1sgn  26736  sincosq2sgn  26737  sincosq3sgn  26738  sincosq4sgn  26739  tangtx  26743  sinq12gt0  26745  cosq14gt0  26748  cosq14ge0  26749  cosne0  26766  sinord  26771  resinf1o  26773  tanregt0  26776  efif1olem2  26780  relogdiv  26830  logneg2  26852  logdivlti  26857  logcnlem4  26882  logccv  26900  cxpaddlelem  26988  loglesqrt  26998  ang180lem2  27047  acoscos  27130  acosbnd  27137  acosrecl  27140  atanlogaddlem  27150  atans2  27168  leibpi  27179  divsqrtsumo1  27220  cvxcl  27221  scvxcvx  27222  jensenlem2  27224  amgmlem  27226  harmonicbnd4  27247  zetacvg  27251  ftalem5  27313  basellem9  27325  mumullem2  27416  ppiub  27440  chtub  27448  bposlem1  27520  bposlem6  27525  bposlem9  27528  gausslemma2dlem1a  27601  chtppilim  27711  chto1ub  27712  rplogsumlem2  27721  rpvmasumlem  27723  dchrisum0flblem1  27744  dchrisum0re  27749  log2sumbnd  27780  selberglem2  27782  pntrmax  27800  pntpbnd2  27823  pntlem3  27845  brbtwn2  29362  colinearalglem4  29366  eleesub  29368  eleesubd  29369  axsegconlem2  29375  ax5seglem2  29386  ax5seglem3  29388  axpaschlem  29397  axpasch  29398  axcontlem2  29422  crctcshwlkn0lem3  30280  crctcshwlkn0lem7  30284  eucrctshift  30723  xlt2addrd  33230  signshf  35096  resconn  35825  sinccvglem  36251  fz0n  36310  dnibndlem4  37178  dnibndlem6  37180  dnibndlem7  37181  dnibndlem9  37183  dnibndlem10  37184  knoppndvlem15  37223  sin2h  38364  tan2h  38366  poimir  38402  mblfinlem3  38408  mblfinlem4  38409  itg2addnclem  38420  itg2addnclem3  38422  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  dvasin  38453  geomcau  38509  bfp  38574  ismrer1  38588  iccbnd  38590  jm2.17a  43801  acongeq  43824  jm3.1lem2  43859  areaquad  44057  lptre2pt  46468  dvnmul  46771  stoweidlem59  46887  fourierdlem42  46977  hoidmvlelem2  47424  smfmullem1  47619  ltsubsubaddltsub  48189  zm1nn  48190  nn0resubcl  48196  subsubelfzo0  48215  bgoldbtbndlem2  48722  ply1mulgsumlem2  49317  ltsubaddb  49444  ltsubsubb  49445  ltsubadd2b  49446  line2  49682