MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resubcl Structured version   Visualization version   GIF version

Theorem resubcl 10939
Description: Closure law for subtraction of reals. (Contributed by NM, 20-Jan-1997.)
Assertion
Ref Expression
resubcl ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)

Proof of Theorem resubcl
StepHypRef Expression
1 recn 10616 . . 3 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2 recn 10616 . . 3 (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3 negsub 10923 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴𝐵))
41, 2, 3syl2an 595 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴𝐵))
5 renegcl 10938 . . 3 (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6 readdcl 10609 . . 3 ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
75, 6sylan2 592 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
84, 7eqeltrrd 2914 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10524  cr 10525   + caddc 10529  cmin 10859  -cneg 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-ltxr 10669  df-sub 10861  df-neg 10862
This theorem is referenced by:  peano2rem  10942  resubcld  11057  ltaddsub  11103  leaddsub  11105  posdif  11122  lt2sub  11127  le2sub  11128  mulsuble0b  11501  cju  11623  elz2  11988  rpnnen1lem5  12370  difrp  12417  qbtwnre  12582  iooshf  12805  iccshftl  12864  lincmb01cmp  12871  uzsubsubfz  12919  difelfzle  13010  fzonmapblen  13073  eluzgtdifelfzo  13089  subfzo0  13149  fracle1  13163  fldiv  13218  modcl  13231  2submod  13290  modsubdir  13298  modfzo0difsn  13301  expubnd  13531  absdiflt  14667  absdifle  14668  elicc4abs  14669  abssubge0  14677  abs2difabs  14684  rddif  14690  absrdbnd  14691  climsup  15016  flo1  15199  supcvg  15201  refallfaccl  15362  resin4p  15481  recos4p  15482  cos01bnd  15529  cos01gt0  15534  pythagtriplem12  16153  pythagtriplem14  16155  pythagtriplem16  16157  fldivp1  16223  prmreclem6  16247  cshwshashlem2  16420  bl2ioo  23329  ioo2bl  23330  ioo2blex  23331  blssioo  23332  blcvx  23335  reconnlem2  23364  opnreen  23368  iirev  23462  iihalf2  23466  iccpnfhmeo  23478  iccvolcl  24097  ioovolcl  24100  ismbf3d  24184  itgrecl  24327  cmvth  24517  dvle  24533  dvcvx  24546  dvfsumge  24548  aalioulem3  24852  aaliou  24856  aaliou3lem9  24868  abelthlem2  24949  abelthlem7  24955  abelth2  24959  sincosq1sgn  25013  sincosq2sgn  25014  sincosq3sgn  25015  sincosq4sgn  25016  tangtx  25020  sinq12gt0  25022  cosq14gt0  25025  cosq14ge0  25026  cosne0  25041  sinord  25045  resinf1o  25047  tanregt0  25050  efif1olem2  25054  relogdiv  25103  logneg2  25125  logdivlti  25130  logcnlem4  25155  logccv  25173  cxpaddlelem  25259  loglesqrt  25266  ang180lem2  25315  acoscos  25398  acosbnd  25405  acosrecl  25408  atanlogaddlem  25418  atans2  25436  leibpi  25448  divsqrtsumo1  25489  cvxcl  25490  scvxcvx  25491  jensenlem2  25493  amgmlem  25495  harmonicbnd4  25516  zetacvg  25520  ftalem5  25582  basellem9  25594  mumullem2  25685  ppiub  25708  chtub  25716  bposlem1  25788  bposlem6  25793  bposlem9  25796  gausslemma2dlem1a  25869  chtppilim  25979  chto1ub  25980  rplogsumlem2  25989  rpvmasumlem  25991  dchrisum0flblem1  26012  dchrisum0re  26017  log2sumbnd  26048  selberglem2  26050  pntrmax  26068  pntpbnd2  26091  pntlem3  26113  brbtwn2  26619  colinearalglem4  26623  eleesub  26625  eleesubd  26626  axsegconlem2  26632  ax5seglem2  26643  ax5seglem3  26645  axpaschlem  26654  axpasch  26655  axcontlem2  26679  crctcshwlkn0lem3  27518  crctcshwlkn0lem7  27522  eucrctshift  27950  xlt2addrd  30409  signshf  31758  resconn  32391  sinccvglem  32813  fz0n  32860  dnibndlem4  33718  dnibndlem6  33720  dnibndlem7  33721  dnibndlem9  33723  dnibndlem10  33724  knoppndvlem15  33763  sin2h  34764  tan2h  34766  poimir  34807  mblfinlem3  34813  mblfinlem4  34814  itg2addnclem  34825  itg2addnclem3  34827  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  dvasin  34860  geomcau  34917  bfp  34985  ismrer1  34999  iccbnd  35001  jm2.17a  39437  acongeq  39460  jm3.1lem2  39495  areaquad  39703  lptre2pt  41801  dvnmul  42108  stoweidlem59  42225  fourierdlem42  42315  hoidmvlelem2  42759  smfmullem1  42947  ltsubsubaddltsub  43382  zm1nn  43383  nn0resubcl  43389  subsubelfzo0  43407  bgoldbtbndlem2  43818  ply1mulgsumlem2  44339  ltsubaddb  44467  ltsubsubb  44468  ltsubadd2b  44469  line2  44637
  Copyright terms: Public domain W3C validator