Theorem resubcl 11574

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 11248	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11248	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11558	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 594	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11573	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11241	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 591	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2827	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2099  (class class class)co 7424  ℂcc 11156  ℝcr 11157   + caddc 11161   − cmin 11494  -cneg 11495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11300  df-mnf 11301  df-ltxr 11303  df-sub 11496  df-neg 11497

This theorem is referenced by:  peano2rem  11577  resubcld  11692  ltaddsub  11738  leaddsub  11740  posdif  11757  lt2sub  11762  le2sub  11763  mulsuble0b  12138  cju  12260  elz2  12628  rpnnen1lem5  13017  difrp  13066  qbtwnre  13232  iooshf  13457  iccshftl  13519  lincmb01cmp  13526  uzsubsubfz  13577  difelfzle  13668  fzonmapblen  13732  eluzgtdifelfzo  13748  subfzo0  13809  fracle1  13823  fldiv  13880  modcl  13893  2submod  13952  modsubdir  13960  modfzo0difsn  13963  expubnd  14196  absdiflt  15322  absdifle  15323  elicc4abs  15324  abssubge0  15332  abs2difabs  15339  rddif  15345  absrdbnd  15346  climsup  15674  flo1  15858  supcvg  15860  refallfaccl  16020  resin4p  16140  recos4p  16141  cos01bnd  16188  cos01gt0  16193  pythagtriplem12  16828  pythagtriplem14  16830  pythagtriplem16  16832  fldivp1  16899  prmreclem6  16923  cshwshashlem2  17099  bl2ioo  24799  ioo2bl  24800  ioo2blex  24801  blssioo  24802  blcvx  24805  reconnlem2  24834  opnreen  24838  iirev  24941  iihalf2  24946  iccpnfhmeo  24961  iccvolcl  25587  ioovolcl  25590  ismbf3d  25674  itgrecl  25818  cmvth  26014  cmvthOLD  26015  dvle  26031  dvcvx  26044  dvfsumge  26047  aalioulem3  26362  aaliou  26366  aaliou3lem9  26378  abelthlem2  26462  abelthlem7  26468  abelth2  26472  sincosq1sgn  26526  sincosq2sgn  26527  sincosq3sgn  26528  sincosq4sgn  26529  tangtx  26533  sinq12gt0  26535  cosq14gt0  26538  cosq14ge0  26539  cosne0  26556  sinord  26561  resinf1o  26563  tanregt0  26566  efif1olem2  26570  relogdiv  26620  logneg2  26642  logdivlti  26647  logcnlem4  26672  logccv  26690  cxpaddlelem  26779  loglesqrt  26789  ang180lem2  26838  acoscos  26921  acosbnd  26928  acosrecl  26931  atanlogaddlem  26941  atans2  26959  leibpi  26970  divsqrtsumo1  27012  cvxcl  27013  scvxcvx  27014  jensenlem2  27016  amgmlem  27018  harmonicbnd4  27039  zetacvg  27043  ftalem5  27105  basellem9  27117  mumullem2  27208  ppiub  27233  chtub  27241  bposlem1  27313  bposlem6  27318  bposlem9  27321  gausslemma2dlem1a  27394  chtppilim  27504  chto1ub  27505  rplogsumlem2  27514  rpvmasumlem  27516  dchrisum0flblem1  27537  dchrisum0re  27542  log2sumbnd  27573  selberglem2  27575  pntrmax  27593  pntpbnd2  27616  pntlem3  27638  brbtwn2  28839  colinearalglem4  28843  eleesub  28845  eleesubd  28846  axsegconlem2  28852  ax5seglem2  28863  ax5seglem3  28865  axpaschlem  28874  axpasch  28875  axcontlem2  28899  crctcshwlkn0lem3  29746  crctcshwlkn0lem7  29750  eucrctshift  30176  xlt2addrd  32662  signshf  34434  resconn  35074  sinccvglem  35500  fz0n  35553  dnibndlem4  36184  dnibndlem6  36186  dnibndlem7  36187  dnibndlem9  36189  dnibndlem10  36190  knoppndvlem15  36229  sin2h  37311  tan2h  37313  poimir  37354  mblfinlem3  37360  mblfinlem4  37361  itg2addnclem  37372  itg2addnclem3  37374  ftc1anclem5  37398  ftc1anclem6  37399  ftc1anclem7  37400  dvasin  37405  geomcau  37460  bfp  37525  ismrer1  37539  iccbnd  37541  jm2.17a  42618  acongeq  42641  jm3.1lem2  42676  areaquad  42881  lptre2pt  45261  dvnmul  45564  stoweidlem59  45680  fourierdlem42  45770  hoidmvlelem2  46217  smfmullem1  46412  ltsubsubaddltsub  46914  zm1nn  46915  nn0resubcl  46921  subsubelfzo0  46939  bgoldbtbndlem2  47378  ply1mulgsumlem2  47770  ltsubaddb  47897  ltsubsubb  47898  ltsubadd2b  47899  line2  48140