Theorem resubcl 11462

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 11134	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11134	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11446	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11461	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11127	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 593	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2829	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042  ℝcr 11043   + caddc 11047   − cmin 11381  -cneg 11382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-ltxr 11189  df-sub 11383  df-neg 11384

This theorem is referenced by:  peano2rem  11465  resubcld  11582  ltaddsub  11628  leaddsub  11630  posdif  11647  lt2sub  11652  le2sub  11653  mulsuble0b  12031  cju  12158  elz2  12523  rpnnen1lem5  12916  difrp  12967  qbtwnre  13135  iooshf  13363  iccshftl  13425  lincmb01cmp  13432  uzsubsubfz  13483  difelfzle  13578  fzonmapblen  13645  eluzgtdifelfzo  13664  subfzo0  13726  fracle1  13741  fldiv  13798  modcl  13811  2submod  13873  modsubdir  13881  modfzo0difsn  13884  expubnd  14119  absdiflt  15260  absdifle  15261  elicc4abs  15262  abssubge0  15270  abs2difabs  15277  rddif  15283  absrdbnd  15284  climsup  15612  flo1  15796  supcvg  15798  refallfaccl  15960  resin4p  16082  recos4p  16083  cos01bnd  16130  cos01gt0  16135  pythagtriplem12  16773  pythagtriplem14  16775  pythagtriplem16  16777  fldivp1  16844  prmreclem6  16868  cshwshashlem2  17043  bl2ioo  24713  ioo2bl  24714  ioo2blex  24715  blssioo  24716  blcvx  24719  reconnlem2  24749  opnreen  24753  iirev  24856  iihalf2  24861  iccpnfhmeo  24876  iccvolcl  25501  ioovolcl  25504  ismbf3d  25588  itgrecl  25732  cmvth  25928  cmvthOLD  25929  dvle  25945  dvcvx  25958  dvfsumge  25961  aalioulem3  26275  aaliou  26279  aaliou3lem9  26291  abelthlem2  26375  abelthlem7  26381  abelth2  26385  sincosq1sgn  26440  sincosq2sgn  26441  sincosq3sgn  26442  sincosq4sgn  26443  tangtx  26447  sinq12gt0  26449  cosq14gt0  26452  cosq14ge0  26453  cosne0  26471  sinord  26476  resinf1o  26478  tanregt0  26481  efif1olem2  26485  relogdiv  26535  logneg2  26557  logdivlti  26562  logcnlem4  26587  logccv  26605  cxpaddlelem  26694  loglesqrt  26704  ang180lem2  26753  acoscos  26836  acosbnd  26843  acosrecl  26846  atanlogaddlem  26856  atans2  26874  leibpi  26885  divsqrtsumo1  26927  cvxcl  26928  scvxcvx  26929  jensenlem2  26931  amgmlem  26933  harmonicbnd4  26954  zetacvg  26958  ftalem5  27020  basellem9  27032  mumullem2  27123  ppiub  27148  chtub  27156  bposlem1  27228  bposlem6  27233  bposlem9  27236  gausslemma2dlem1a  27309  chtppilim  27419  chto1ub  27420  rplogsumlem2  27429  rpvmasumlem  27431  dchrisum0flblem1  27452  dchrisum0re  27457  log2sumbnd  27488  selberglem2  27490  pntrmax  27508  pntpbnd2  27531  pntlem3  27553  brbtwn2  28885  colinearalglem4  28889  eleesub  28891  eleesubd  28892  axsegconlem2  28898  ax5seglem2  28909  ax5seglem3  28911  axpaschlem  28920  axpasch  28921  axcontlem2  28945  crctcshwlkn0lem3  29792  crctcshwlkn0lem7  29796  eucrctshift  30222  xlt2addrd  32732  signshf  34572  resconn  35226  sinccvglem  35652  fz0n  35711  dnibndlem4  36462  dnibndlem6  36464  dnibndlem7  36465  dnibndlem9  36467  dnibndlem10  36468  knoppndvlem15  36507  sin2h  37597  tan2h  37599  poimir  37640  mblfinlem3  37646  mblfinlem4  37647  itg2addnclem  37658  itg2addnclem3  37660  ftc1anclem5  37684  ftc1anclem6  37685  ftc1anclem7  37686  dvasin  37691  geomcau  37746  bfp  37811  ismrer1  37825  iccbnd  37827  jm2.17a  42942  acongeq  42965  jm3.1lem2  43000  areaquad  43198  lptre2pt  45631  dvnmul  45934  stoweidlem59  46050  fourierdlem42  46140  hoidmvlelem2  46587  smfmullem1  46782  ltsubsubaddltsub  47295  zm1nn  47296  nn0resubcl  47302  subsubelfzo0  47320  bgoldbtbndlem2  47800  ply1mulgsumlem2  48369  ltsubaddb  48496  ltsubsubb  48497  ltsubadd2b  48498  line2  48734