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

Theorem resubcl 10196
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 9882 . . 3 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2 recn 9882 . . 3 (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3 negsub 10180 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴𝐵))
41, 2, 3syl2an 492 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴𝐵))
5 renegcl 10195 . . 3 (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6 readdcl 9875 . . 3 ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
75, 6sylan2 489 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
84, 7eqeltrrd 2688 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  (class class class)co 6527  cc 9790  cr 9791   + caddc 9795  cmin 10117  -cneg 10118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-ltxr 9935  df-sub 10119  df-neg 10120
This theorem is referenced by:  peano2rem  10199  resubcld  10309  ltaddsub  10351  leaddsub  10353  posdif  10370  lt2sub  10375  le2sub  10376  mulsuble0b  10744  cju  10863  elz2  11227  rpnnen1lem5  11650  rpnnen1lem5OLD  11656  difrp  11700  qbtwnre  11863  iooshf  12079  iccshftl  12135  lincmb01cmp  12142  uzsubsubfz  12189  difelfzle  12276  fzonmapblen  12336  eluzgtdifelfzo  12352  subfzo0  12407  fracle1  12421  fldiv  12476  modcl  12489  2submod  12548  modsubdir  12556  modfzo0difsn  12559  expubnd  12738  absdiflt  13851  absdifle  13852  elicc4abs  13853  abssubge0  13861  abs2difabs  13868  rddif  13874  absrdbnd  13875  climsup  14194  flo1  14371  supcvg  14373  refallfaccl  14534  resin4p  14653  recos4p  14654  cos01bnd  14701  cos01gt0  14706  pythagtriplem12  15315  pythagtriplem14  15317  pythagtriplem16  15319  fldivp1  15385  prmreclem6  15409  cshwshashlem2  15587  bl2ioo  22335  ioo2bl  22336  ioo2blex  22337  blssioo  22338  blcvx  22341  reconnlem2  22370  opnreen  22374  iirev  22467  iihalf2  22471  iccpnfhmeo  22483  iccvolcl  23059  ioovolcl  23061  ismbf3d  23144  itgrecl  23287  cmvth  23475  dvle  23491  dvcvx  23504  dvfsumge  23506  aalioulem3  23810  aaliou  23814  aaliou3lem9  23826  abelthlem2  23907  abelthlem7  23913  abelth2  23917  sincosq1sgn  23971  sincosq2sgn  23972  sincosq3sgn  23973  sincosq4sgn  23974  tangtx  23978  sinq12gt0  23980  cosq14gt0  23983  cosq14ge0  23984  cosne0  23997  sinord  24001  resinf1o  24003  tanregt0  24006  efif1olem2  24010  relogdiv  24060  logneg2  24082  logdivlti  24087  logcnlem4  24108  logccv  24126  cxpaddlelem  24209  loglesqrt  24216  ang180lem2  24257  acoscos  24337  acosbnd  24344  acosrecl  24347  atanlogaddlem  24357  atans2  24375  leibpi  24386  divsqrtsumo1  24427  cvxcl  24428  scvxcvx  24429  jensenlem2  24431  amgmlem  24433  harmonicbnd4  24454  zetacvg  24458  ftalem5  24520  basellem9  24532  mumullem2  24623  ppiub  24646  chtub  24654  bposlem1  24726  bposlem6  24731  bposlem9  24734  gausslemma2dlem1a  24807  chtppilim  24881  chto1ub  24882  rplogsumlem2  24891  rpvmasumlem  24893  dchrisum0flblem1  24914  dchrisum0re  24919  log2sumbnd  24950  selberglem2  24952  pntrmax  24970  pntpbnd2  24993  pntlem3  25015  brbtwn2  25503  colinearalglem4  25507  eleesub  25509  eleesubd  25510  axsegconlem2  25516  ax5seglem2  25527  ax5seglem3  25529  axpaschlem  25538  axpasch  25539  axcontlem2  25563  xlt2addrd  28719  signshf  29797  rescon  30288  sinccvglem  30626  fz0n  30675  dnibndlem4  31447  dnibndlem6  31449  dnibndlem7  31450  dnibndlem9  31452  dnibndlem10  31453  knoppndvlem15  31493  sin2h  32365  tan2h  32367  poimir  32408  mblfinlem3  32414  mblfinlem4  32415  itg2addnclem  32427  itg2addnclem3  32429  ftc1anclem5  32455  ftc1anclem6  32456  ftc1anclem7  32457  dvasin  32462  geomcau  32521  bfp  32589  ismrer1  32603  iccbnd  32605  rmspecsqrtnqOLD  36285  jm2.17a  36341  acongeq  36364  jm3.1lem2  36399  areaquad  36617  lptre2pt  38504  dvnmul  38630  stoweidlem59  38749  fourierdlem42  38839  hoidmvlelem2  39283  smfmullem1  39473  bgoldbtbndlem2  40020  ltsubsubaddltsub  40167  zm1nn  40168  nn0resubcl  40169  subsubelfzo0  40179  crctcsh1wlkn0lem3  41010  crctcsh1wlkn0lem7  41014  eucrctshift  41406  ply1mulgsumlem2  41964  ltsubaddb  42093  ltsubsubb  42094  ltsubadd2b  42095
  Copyright terms: Public domain W3C validator