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  24656  ioo2bl  24657  ioo2blex  24658  blssioo  24659  blcvx  24662  reconnlem2  24692  opnreen  24696  iirev  24799  iihalf2  24804  iccpnfhmeo  24819  iccvolcl  25444  ioovolcl  25447  ismbf3d  25531  itgrecl  25675  cmvth  25871  cmvthOLD  25872  dvle  25888  dvcvx  25901  dvfsumge  25904  aalioulem3  26218  aaliou  26222  aaliou3lem9  26234  abelthlem2  26318  abelthlem7  26324  abelth2  26328  sincosq1sgn  26383  sincosq2sgn  26384  sincosq3sgn  26385  sincosq4sgn  26386  tangtx  26390  sinq12gt0  26392  cosq14gt0  26395  cosq14ge0  26396  cosne0  26414  sinord  26419  resinf1o  26421  tanregt0  26424  efif1olem2  26428  relogdiv  26478  logneg2  26500  logdivlti  26505  logcnlem4  26530  logccv  26548  cxpaddlelem  26637  loglesqrt  26647  ang180lem2  26696  acoscos  26779  acosbnd  26786  acosrecl  26789  atanlogaddlem  26799  atans2  26817  leibpi  26828  divsqrtsumo1  26870  cvxcl  26871  scvxcvx  26872  jensenlem2  26874  amgmlem  26876  harmonicbnd4  26897  zetacvg  26901  ftalem5  26963  basellem9  26975  mumullem2  27066  ppiub  27091  chtub  27099  bposlem1  27171  bposlem6  27176  bposlem9  27179  gausslemma2dlem1a  27252  chtppilim  27362  chto1ub  27363  rplogsumlem2  27372  rpvmasumlem  27374  dchrisum0flblem1  27395  dchrisum0re  27400  log2sumbnd  27431  selberglem2  27433  pntrmax  27451  pntpbnd2  27474  pntlem3  27496  brbtwn2  28808  colinearalglem4  28812  eleesub  28814  eleesubd  28815  axsegconlem2  28821  ax5seglem2  28832  ax5seglem3  28834  axpaschlem  28843  axpasch  28844  axcontlem2  28868  crctcshwlkn0lem3  29715  crctcshwlkn0lem7  29719  eucrctshift  30145  xlt2addrd  32655  signshf  34552  resconn  35206  sinccvglem  35632  fz0n  35691  dnibndlem4  36442  dnibndlem6  36444  dnibndlem7  36445  dnibndlem9  36447  dnibndlem10  36448  knoppndvlem15  36487  sin2h  37577  tan2h  37579  poimir  37620  mblfinlem3  37626  mblfinlem4  37627  itg2addnclem  37638  itg2addnclem3  37640  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anclem7  37666  dvasin  37671  geomcau  37726  bfp  37791  ismrer1  37805  iccbnd  37807  jm2.17a  42922  acongeq  42945  jm3.1lem2  42980  areaquad  43178  lptre2pt  45611  dvnmul  45914  stoweidlem59  46030  fourierdlem42  46120  hoidmvlelem2  46567  smfmullem1  46762  ltsubsubaddltsub  47275  zm1nn  47276  nn0resubcl  47282  subsubelfzo0  47300  bgoldbtbndlem2  47780  ply1mulgsumlem2  48349  ltsubaddb  48476  ltsubsubb  48477  ltsubadd2b  48478  line2  48714