Theorem resubcld 11744

Description: Closure law for subtraction of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
renegcld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
resubcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
resubcld	⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

Proof of Theorem resubcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		resubcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		resubcl 11622	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 − 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199   − cmin 11541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-sub 11543  df-neg 11544

This theorem is used by:  ltsubadd  11786  lesubadd  11788  lesub1  11810  lesub2  11811  ltsub1  11812  ltsub2  11813  lt2sub  11814  le2sub  11815  ltmul1a  12166  supaddc  12284  cru  12312  ge2halflem1  13237  qbtwnre  13329  lincmb01cmp  13626  iccf1o  13627  xov1plusxeqvd  13629  intfracq  13999  fldiv  14000  modlt  14020  modsubdir  14083  modsumfzodifsn  14087  serle  14200  expmulnbnd  14379  discr  14384  fzsdom2  14573  cshwidxmod  14954  sgnsub  15259  crre  15281  remullem  15295  01sqrexlem7  15415  absrdbnd  15509  fzomaxdiflem  15510  caubnd2  15525  amgm2  15537  icodiamlt  15605  bhmafibid1  15635  mulcn2  15763  reccn2  15764  rlimo1  15784  climle  15807  climsqz  15808  climsqz2  15809  rlimle  15815  isercolllem1  15832  climsup  15837  caucvgrlem  15840  caucvgrlem2  15842  iseraltlem2  15850  iseraltlem3  15851  iseralt  15852  fsumle  15966  cvgcmp  15983  cvgcmpce  15985  bpoly4  16225  eflt  16285  resinhcl  16324  tanhlt1  16328  sin01bnd  16353  sin01gt0  16358  moddvds  16433  bitscmp  16608  bitsinv1lem  16611  smueqlem  16660  modprm0  16983  pcbc  17078  4sqlem15  17137  blss2ps  24722  blss2  24723  blssps  24743  blss  24744  nm2dif  24944  nlmvscnlem2  25004  nrginvrcnlem  25010  iccntr  25141  icccmplem2  25143  metdstri  25171  cnllycmp  25277  evth  25280  lebnumii  25287  ipcnlem2  25565  cncmet  25643  rrxds  25714  rrxmval  25726  rrxmet  25729  rrxdstprj1  25730  rrxdsfi  25732  ehl1eudis  25741  ehl2eudis  25743  minveclem3b  25749  minveclem4  25753  ivthlem2  25773  ivthlem3  25774  ovollb2lem  25809  ovoliunlem1  25823  ovolscalem1  25834  ovolicc1  25837  ovolicc2lem4  25841  ovolicc2  25843  ovolicc  25844  voliunlem2  25872  ovolioo  25889  ioorcl2  25893  uniioovol  25900  uniioombllem2  25904  uniioombllem3a  25905  uniioombllem3  25906  uniioombllem4  25907  uniioombllem6  25909  opnmbllem  25922  volcn  25927  vitalilem2  25930  ismbf3d  25975  mbfaddlem  25981  i1fadd  26016  itg1addlem4  26020  mbfi1fseqlem6  26041  itg2seq  26063  itg2split  26070  itg2cnlem2  26083  itg2cn  26084  itgrevallem1  26115  dvcjbr  26269  dvferm1lem  26304  dvferm2lem  26306  cmvth  26311  mvth  26312  dvlip  26313  dvlip2  26315  c1liplem1  26316  dvgt0  26324  dvlt0  26325  dvge0  26326  dvle  26327  dvivthlem1  26328  lhop1lem  26333  lhop  26336  dvcnvrelem1  26337  dvcnvrelem2  26338  dvcnvre  26339  dvcvx  26340  dvfsumle  26341  dvfsumge  26342  dvfsumrlimf  26345  dvfsumlem2  26347  dvfsumlem3  26348  dvfsumlem4  26349  dvfsum2  26354  ftc1a  26357  ftc1lem4  26359  coe1mul3  26417  ply1divex  26455  plydivex  26618  aalioulem2  26660  aalioulem3  26661  aalioulem4  26662  aalioulem5  26663  aalioulem6  26664  aaliou3lem7  26676  taylthlem2  26701  mtest  26731  pilem2  26779  tangtx  26834  cosordlem  26858  efif1olem2  26871  logcnlem3  26972  logcnlem4  26973  isosctrlem2  27147  chordthmlem2  27161  chordthmlem4  27163  heron  27166  atanlogsublem  27243  atantan  27251  birthdaylem3  27281  logdifbnd  27321  emcllem1  27323  emcllem2  27324  emcllem5  27327  emcllem6  27328  harmonicbnd4  27338  fsumharmonic  27339  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamucov  27365  relgamcl  27389  ftalem2  27401  ftalem5  27404  chpub  27547  logfaclbnd  27549  logfacbnd3  27550  logexprlim  27552  bposlem1  27611  bposlem9  27619  gausslemma2dlem1a  27692  lgseisenlem1  27702  lgsquadlem1  27707  2sqmod  27763  chtppilimlem1  27800  vmadivsum  27809  vmadivsumb  27810  rplogsumlem1  27811  rplogsumlem2  27812  rpvmasumlem  27814  dchrisumlem2  27817  dchrisum0re  27840  rplogsum  27854  mulogsumlem  27858  mulog2sumlem1  27861  vmalogdivsum2  27865  vmalogdivsum  27866  2vmadivsumlem  27867  log2sumbnd  27871  selbergb  27876  selberg2lem  27877  selberg2b  27879  chpdifbndlem1  27880  selberg3lem1  27884  selberg3lem2  27885  selberg3  27886  selberg4lem1  27887  selberg4  27888  pntrf  27890  pntrmax  27891  pntrsumo1  27892  selberg3r  27896  selberg4r  27897  selberg34r  27898  pntrlog2bndlem1  27904  pntrlog2bndlem2  27905  pntrlog2bndlem3  27906  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntrlog2bndlem6  27910  pntrlog2bnd  27911  pntpbnd1a  27912  pntpbnd2  27914  pntibndlem2  27918  pntlemg  27925  pntlemn  27927  pntlemj  27930  pntlemf  27932  pntlemo  27934  pntlem3  27936  pntleml  27938  ttgcontlem1  29462  eqeelen  29482  brbtwn2  29483  colinearalg  29488  axcgrid  29494  axsegconlem1  29495  axsegconlem3  29497  axsegconlem8  29502  axsegconlem9  29503  axsegconlem10  29504  ax5seglem3a  29508  ax5seg  29516  axpaschlem  29518  axcontlem8  29549  nbusgrvtxm1  29960  crctcshwlkn0lem3  30401  crctcshwlkn0lem5  30403  crctcsh  30413  clwlkclwwlklem2fv2  30587  clwlkclwwlklem2a4  30588  clwlkclwwlklem2a  30589  nvabs  31274  dipcj  31316  minvecolem4  31482  lt2addrd  33342  xlt2addrd  33351  fzsplit3  33385  bcm1n  33387  ply1degltel  34126  ply1degltlss  34128  iconstr  34398  constrresqrtcl  34409  cos9thpiminplylem1  34414  submateqlem1  34439  cnre2csqlem  34542  tpr2rico  34544  dya2ub  34902  dya2icoseg  34909  ballotlemfcc  35126  ballotlemfrcn0  35162  signslema  35191  ftc2re  35227  subfacval3  35954  dnibndlem8  37351  dnibndlem10  37353  dnibndlem11  37354  dnibndlem12  37355  dnicn  37358  knoppcnlem4  37362  unblimceq0  37373  unbdqndv2lem2  37376  knoppndvlem11  37388  knoppndvlem14  37391  knoppndvlem15  37392  knoppndvlem17  37394  knoppndvlem20  37397  irrdifflemf  38246  qdiff  38248  poimirlem29  38567  broucube  38572  opnmbllem0  38574  mblfinlem3  38577  mblfinlem4  38578  itg2addnclem  38589  itg2addnclem3  38591  itg2gt0cn  38593  ftc1cnnclem  38609  areacirclem1  38626  areacirclem2  38627  areacirclem4  38629  areacirclem5  38630  areacirc  38631  cntotbnd  38730  rrnmet  38763  rrndstprj1  38764  rrndstprj2  38765  lcmineqlem23  43101  intlewftc  43111  aks4d1p1p2  43120  aks4d1p1p4  43121  dvle2  43122  aks4d1p1  43126  primrootlekpowne0  43155  hashscontpow1  43171  aks6d1c2  43180  aks6d1c5lem2  43188  sticksstones10  43205  sticksstones12a  43207  sticksstones12  43208  aks6d1c6lem3  43222  bcled  43228  bcle2d  43229  unitscyglem2  43246  unitscyglem4  43248  readdrcl2d  43332  frlmvscadiccat  43573  fltnlta  43674  3cubeslem2  43695  3cubeslem4  43699  irrapxlem2  43829  irrapxlem3  43830  irrapxlem4  43831  irrapxlem5  43832  pellexlem2  43836  pellexlem6  43840  pell1qrgaplem  43879  rmspecsqrtnq  43912  rmspecfund  43915  rmspecpos  43922  jm2.24nn  43965  jm2.17c  43968  fzmaxdif  43987  acongeq  43989  modabsdifz  43992  jm3.1lem2  44024  areaquad  44217  sqrtcvallem2  44636  sqrtcvallem3  44637  sqrtcval  44640  imo72b2lem0  45164  cvgdvgrat  45296  hashnzfzclim  45305  binomcxplemdvbinom  45336  oddfl  46293  lefldiveq  46307  fperiodmul  46319  fzdifsuc2  46325  suprltrp  46339  supxrgere  46344  supxrgelem  46348  suplesup  46350  infleinflem2  46381  infleinf  46382  xrralrecnnge  46400  iccshift  46529  iooshift  46533  iooiinicc  46553  fmul01lt1lem2  46596  climinf  46617  sumnnodd  46641  ltmod  46647  lptre2pt  46649  climleltrp  46685  limsupgtlem  46786  liminflimsupclim  46816  fperdvper  46928  dvbdfbdioolem1  46937  dvbdfbdioolem2  46938  dvbdfbdioo  46939  ioodvbdlimc1lem1  46940  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnmul  46952  iblspltprt  46982  itgspltprt  46988  itgiccshift  46989  itgperiod  46990  itgsbtaddcnst  46991  sublevolico  46993  stoweidlem1  47010  stoweidlem11  47020  stoweidlem12  47021  stoweidlem13  47022  stoweidlem14  47023  stoweidlem23  47032  stoweidlem24  47033  stoweidlem25  47034  stoweidlem26  47035  stoweidlem34  47043  stoweidlem40  47049  stoweidlem41  47050  stoweidlem42  47051  stoweidlem45  47054  stoweidlem60  47069  stoweidlem62  47071  wallispilem3  47076  wallispilem4  47077  wallispi  47079  wallispi2lem1  47080  stirlinglem5  47087  stirlinglem11  47093  stirlinglem12  47094  dirkercncflem1  47112  fourierdlem4  47120  fourierdlem6  47122  fourierdlem7  47123  fourierdlem9  47125  fourierdlem13  47129  fourierdlem14  47130  fourierdlem15  47131  fourierdlem19  47135  fourierdlem26  47142  fourierdlem35  47151  fourierdlem39  47155  fourierdlem40  47156  fourierdlem41  47157  fourierdlem42  47158  fourierdlem48  47163  fourierdlem49  47164  fourierdlem50  47165  fourierdlem51  47166  fourierdlem56  47171  fourierdlem57  47172  fourierdlem59  47174  fourierdlem60  47175  fourierdlem61  47176  fourierdlem63  47178  fourierdlem64  47179  fourierdlem65  47180  fourierdlem66  47181  fourierdlem68  47183  fourierdlem71  47186  fourierdlem72  47187  fourierdlem73  47188  fourierdlem74  47189  fourierdlem75  47190  fourierdlem76  47191  fourierdlem78  47193  fourierdlem79  47194  fourierdlem81  47196  fourierdlem82  47197  fourierdlem83  47198  fourierdlem84  47199  fourierdlem88  47203  fourierdlem89  47204  fourierdlem90  47205  fourierdlem91  47206  fourierdlem92  47207  fourierdlem93  47208  fourierdlem95  47210  fourierdlem97  47212  fourierdlem101  47216  fourierdlem103  47218  fourierdlem104  47219  fourierdlem107  47222  fourierdlem109  47224  fourierdlem111  47226  fouriersw  47240  elaa2lem  47242  etransclem23  47266  rrxtopnfi  47296  rrndistlt  47299  ioorrnopnlem  47313  ioorrnopnxrlem  47315  sge0gtfsumgt  47452  iundjiun  47469  volicorecl  47555  hoiprodcl  47556  hoiprodcl3  47589  volicore  47590  hoidmvcl  47591  hoidmv1lelem2  47601  hoidmv1lelem3  47602  hoidmv1le  47603  hoidmvlelem1  47604  hoidmvlelem2  47605  hoiqssbllem1  47631  hoiqssbllem2  47632  hoiqssbllem3  47633  hspmbllem1  47635  ovolval5lem1  47661  ovolval5lem2  47662  iunhoiioolem  47684  iccvonmbllem  47687  vonicclem1  47692  preimageiingt  47729  salpreimagtge  47734  smfaddlem1  47772  smflimlem4  47783  smfmullem1  47800  smfmullem2  47801  smfmullem3  47802  ltsubsubaddltsub  48370  2elfz2melfz  48387  2tceilhalfelfzo1  48405  flmrecm1  48412  requad01  48718  requad1  48719  requad2  48720  bgoldbtbndlem2  48903  bgoldbtbndlem3  48904  bgoldbtbndlem4  48905  bgoldbtbnd  48906  gpgedgvtx0  49158  gpgedgvtx1  49159  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx13starlem2  49169  ply1mulgsumlem2  49498  nnpw2pmod  49694  dignn0flhalflem1  49726  affinecomb1  49813  rrxlinesc  49846  rrxlinec  49847  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  rrx2vlinest  49852  rrx2linest2  49855  2sphere  49860  line2  49863  itsclc0lem2  49868  itsclc0lem3  49869  itscnhlc0yqe  49870  itsclc0yqsollem2  49874  itsclc0yqsol  49875  itscnhlc0xyqsol  49876  itsclinecirc0  49884  itsclinecirc0b  49885  itsclinecirc0in  49886  itsclquadb  49887  2itscp  49892  itscnhlinecirc02plem1  49893  itscnhlinecirc02p  49896  inlinecirc02plem  49897  crosspcle1d  50954  crosspcle2d  50955  crosspcle3d  50956  crossp3d  50966  amgmwlem  50986