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

Theorem resubcl 11466
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 11142 . . 3 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2 recn 11142 . . 3 (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3 negsub 11450 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴𝐵))
41, 2, 3syl2an 597 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴𝐵))
5 renegcl 11465 . . 3 (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6 readdcl 11135 . . 3 ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
75, 6sylan2 594 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
84, 7eqeltrrd 2839 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  (class class class)co 7358  cc 11050  cr 11051   + caddc 11055  cmin 11386  -cneg 11387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-ltxr 11195  df-sub 11388  df-neg 11389
This theorem is referenced by:  peano2rem  11469  resubcld  11584  ltaddsub  11630  leaddsub  11632  posdif  11649  lt2sub  11654  le2sub  11655  mulsuble0b  12028  cju  12150  elz2  12518  rpnnen1lem5  12907  difrp  12954  qbtwnre  13119  iooshf  13344  iccshftl  13406  lincmb01cmp  13413  uzsubsubfz  13464  difelfzle  13555  fzonmapblen  13619  eluzgtdifelfzo  13635  subfzo0  13695  fracle1  13709  fldiv  13766  modcl  13779  2submod  13838  modsubdir  13846  modfzo0difsn  13849  expubnd  14083  absdiflt  15203  absdifle  15204  elicc4abs  15205  abssubge0  15213  abs2difabs  15220  rddif  15226  absrdbnd  15227  climsup  15555  flo1  15740  supcvg  15742  refallfaccl  15902  resin4p  16021  recos4p  16022  cos01bnd  16069  cos01gt0  16074  pythagtriplem12  16699  pythagtriplem14  16701  pythagtriplem16  16703  fldivp1  16770  prmreclem6  16794  cshwshashlem2  16970  bl2ioo  24158  ioo2bl  24159  ioo2blex  24160  blssioo  24161  blcvx  24164  reconnlem2  24193  opnreen  24197  iirev  24295  iihalf2  24299  iccpnfhmeo  24311  iccvolcl  24934  ioovolcl  24937  ismbf3d  25021  itgrecl  25165  cmvth  25358  dvle  25374  dvcvx  25387  dvfsumge  25389  aalioulem3  25697  aaliou  25701  aaliou3lem9  25713  abelthlem2  25794  abelthlem7  25800  abelth2  25804  sincosq1sgn  25858  sincosq2sgn  25859  sincosq3sgn  25860  sincosq4sgn  25861  tangtx  25865  sinq12gt0  25867  cosq14gt0  25870  cosq14ge0  25871  cosne0  25888  sinord  25893  resinf1o  25895  tanregt0  25898  efif1olem2  25902  relogdiv  25951  logneg2  25973  logdivlti  25978  logcnlem4  26003  logccv  26021  cxpaddlelem  26107  loglesqrt  26114  ang180lem2  26163  acoscos  26246  acosbnd  26253  acosrecl  26256  atanlogaddlem  26266  atans2  26284  leibpi  26295  divsqrtsumo1  26336  cvxcl  26337  scvxcvx  26338  jensenlem2  26340  amgmlem  26342  harmonicbnd4  26363  zetacvg  26367  ftalem5  26429  basellem9  26441  mumullem2  26532  ppiub  26555  chtub  26563  bposlem1  26635  bposlem6  26640  bposlem9  26643  gausslemma2dlem1a  26716  chtppilim  26826  chto1ub  26827  rplogsumlem2  26836  rpvmasumlem  26838  dchrisum0flblem1  26859  dchrisum0re  26864  log2sumbnd  26895  selberglem2  26897  pntrmax  26915  pntpbnd2  26938  pntlem3  26960  brbtwn2  27857  colinearalglem4  27861  eleesub  27863  eleesubd  27864  axsegconlem2  27870  ax5seglem2  27881  ax5seglem3  27883  axpaschlem  27892  axpasch  27893  axcontlem2  27917  crctcshwlkn0lem3  28760  crctcshwlkn0lem7  28764  eucrctshift  29190  xlt2addrd  31666  signshf  33203  resconn  33843  sinccvglem  34263  fz0n  34306  dnibndlem4  34947  dnibndlem6  34949  dnibndlem7  34950  dnibndlem9  34952  dnibndlem10  34953  knoppndvlem15  34992  sin2h  36071  tan2h  36073  poimir  36114  mblfinlem3  36120  mblfinlem4  36121  itg2addnclem  36132  itg2addnclem3  36134  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  dvasin  36165  geomcau  36221  bfp  36286  ismrer1  36300  iccbnd  36302  jm2.17a  41287  acongeq  41310  jm3.1lem2  41345  areaquad  41553  lptre2pt  43888  dvnmul  44191  stoweidlem59  44307  fourierdlem42  44397  hoidmvlelem2  44844  smfmullem1  45039  ltsubsubaddltsub  45540  zm1nn  45541  nn0resubcl  45547  subsubelfzo0  45565  bgoldbtbndlem2  46005  ply1mulgsumlem2  46475  ltsubaddb  46602  ltsubsubb  46603  ltsubadd2b  46604  line2  46845
  Copyright terms: Public domain W3C validator