Theorem resubcl 11495

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 11163	. . 3 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2		recn 11163	. . 3 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
3		negsub 11479	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
4	1, 2, 3	syl2an 605	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) = (𝐴 − 𝐵))
5		renegcl 11494	. . 3 ⊢ (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
6		readdcl 11156	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
7	5, 6	sylan2 602	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + -𝐵) ∈ ℝ)
8	4, 7	eqeltrrd 2863	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071  ℝcr 11072   + caddc 11076   − cmin 11414  -cneg 11415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-ltxr 11221  df-sub 11416  df-neg 11417

This theorem is referenced by:  peano2rem  11498  resubcld  11615  ltaddsub  11661  leaddsub  11663  posdif  11680  lt2sub  11685  le2sub  11686  mulsuble0b  12064  cju  12191  elz2  12586  rpnnen1lem5  12982  difrp  13033  qbtwnre  13202  iooshf  13430  iccshftl  13492  lincmb01cmp  13499  uzsubsubfz  13551  difelfzle  13646  fzonmapblen  13714  eluzgtdifelfzo  13733  subfzo0  13798  fracle1  13813  fldiv  13870  modcl  13883  2submod  13945  modsubdir  13953  modfzo0difsn  13956  expubnd  14191  absdiflt  15345  absdifle  15346  elicc4abs  15347  abssubge0  15355  abs2difabs  15362  rddif  15368  absrdbnd  15369  climsup  15697  flo1  15884  supcvg  15886  refallfaccl  16048  resin4p  16170  recos4p  16171  cos01bnd  16218  cos01gt0  16223  pythagtriplem12  16862  pythagtriplem14  16864  pythagtriplem16  16866  fldivp1  16933  prmreclem6  16957  cshwshashlem2  17132  bl2ioo  24849  ioo2bl  24850  ioo2blex  24851  blssioo  24852  blcvx  24855  reconnlem2  24885  opnreen  24889  iirev  24988  iihalf2  24992  iccpnfhmeo  25004  iccvolcl  25626  ioovolcl  25629  ismbf3d  25713  itgrecl  25857  cmvth  26050  dvle  26066  dvcvx  26079  dvfsumge  26081  aalioulem3  26395  aaliou  26399  aaliou3lem9  26411  abelthlem2  26492  abelthlem7  26498  abelth2  26502  sincosq1sgn  26560  sincosq2sgn  26561  sincosq3sgn  26562  sincosq4sgn  26563  tangtx  26567  sinq12gt0  26569  cosq14gt0  26572  cosq14ge0  26573  cosne0  26591  sinord  26596  resinf1o  26598  tanregt0  26601  efif1olem2  26605  relogdiv  26655  logneg2  26677  logdivlti  26682  logcnlem4  26707  logccv  26725  cxpaddlelem  26813  loglesqrt  26823  ang180lem2  26872  acoscos  26955  acosbnd  26962  acosrecl  26965  atanlogaddlem  26975  atans2  26993  leibpi  27004  divsqrtsumo1  27045  cvxcl  27046  scvxcvx  27047  jensenlem2  27049  amgmlem  27051  harmonicbnd4  27072  zetacvg  27076  ftalem5  27138  basellem9  27150  mumullem2  27241  ppiub  27265  chtub  27273  bposlem1  27345  bposlem6  27350  bposlem9  27353  gausslemma2dlem1a  27426  chtppilim  27536  chto1ub  27537  rplogsumlem2  27546  rpvmasumlem  27548  dchrisum0flblem1  27569  dchrisum0re  27574  log2sumbnd  27605  selberglem2  27607  pntrmax  27625  pntpbnd2  27648  pntlem3  27670  brbtwn2  29103  colinearalglem4  29107  eleesub  29109  eleesubd  29110  axsegconlem2  29116  ax5seglem2  29127  ax5seglem3  29129  axpaschlem  29138  axpasch  29139  axcontlem2  29163  crctcshwlkn0lem3  30009  crctcshwlkn0lem7  30013  eucrctshift  30442  xlt2addrd  32958  signshf  34879  resconn  35593  sinccvglem  36019  fz0n  36078  dnibndlem4  36916  dnibndlem6  36918  dnibndlem7  36919  dnibndlem9  36921  dnibndlem10  36922  knoppndvlem15  36961  sin2h  38106  tan2h  38108  poimir  38149  mblfinlem3  38155  mblfinlem4  38156  itg2addnclem  38167  itg2addnclem3  38169  ftc1anclem5  38193  ftc1anclem6  38194  ftc1anclem7  38195  dvasin  38200  geomcau  38255  bfp  38320  ismrer1  38334  iccbnd  38336  jm2.17a  43534  acongeq  43557  jm3.1lem2  43592  areaquad  43790  lptre2pt  46211  dvnmul  46514  stoweidlem59  46630  fourierdlem42  46720  hoidmvlelem2  47167  smfmullem1  47362  ltsubsubaddltsub  47892  zm1nn  47893  nn0resubcl  47899  subsubelfzo0  47918  bgoldbtbndlem2  48425  ply1mulgsumlem2  49006  ltsubaddb  49133  ltsubsubb  49134  ltsubadd2b  49135  line2  49371