Theorem resubcld 10458

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

Hypotheses

Ref	Expression
renegcld.1	|- ( ph -> A e. RR )
resubcld.2	|- ( ph -> B e. RR )

Assertion

Ref	Expression
resubcld	|- ( ph -> ( A - B ) e. RR )

Proof of Theorem resubcld

Step	Hyp	Ref	Expression
1		renegcld.1	. 2 |- ( ph -> A e. RR )
2		resubcld.2	. 2 |- ( ph -> B e. RR )
3		resubcl 10345	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> ( A - B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 1990  (class class class)co 6650   RRcr 9935   - cmin 10266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-ltxr 10079  df-sub 10268  df-neg 10269

This theorem is referenced by:  ltsubadd  10498  lesubadd  10500  lesub1  10522  lesub2  10523  ltsub1  10524  ltsub2  10525  lt2sub  10526  le2sub  10527  ltmul1a  10872  supaddc  10990  cru  11012  qbtwnre  12030  lincmb01cmp  12315  iccf1o  12316  xov1plusxeqvd  12318  intfracq  12658  fldiv  12659  modlt  12679  modsubdir  12739  modsumfzodifsn  12743  serle  12856  expmulnbnd  12996  discr  13001  fzsdom2  13215  cshwidxmod  13549  crre  13854  remullem  13868  sqrlem7  13989  absrdbnd  14081  fzomaxdiflem  14082  caubnd2  14097  amgm2  14109  icodiamlt  14174  mulcn2  14326  reccn2  14327  rlimo1  14347  climle  14370  climsqz  14371  climsqz2  14372  rlimle  14378  isercolllem1  14395  climsup  14400  caucvgrlem  14403  caucvgrlem2  14405  iseraltlem2  14413  iseraltlem3  14414  iseralt  14415  fsumle  14531  cvgcmp  14548  cvgcmpce  14550  bpoly4  14790  eflt  14847  resinhcl  14886  tanhlt1  14890  sin01bnd  14915  sin01gt0  14920  moddvds  14991  bitscmp  15160  bitsinv1lem  15163  smueqlem  15212  modprm0  15510  pcbc  15604  4sqlem15  15663  blss2ps  22208  blss2  22209  blssps  22229  blss  22230  nm2dif  22429  nlmvscnlem2  22489  nrginvrcnlem  22495  iccntr  22624  icccmplem2  22626  metdstri  22654  cnllycmp  22755  evth  22758  lebnumii  22765  ipcnlem2  23043  cncmet  23119  rrxds  23181  rrxmval  23188  rrxmet  23191  rrxdstprj1  23192  minveclem3b  23199  minveclem4  23203  ivthlem2  23221  ivthlem3  23222  ovollb2lem  23256  ovoliunlem1  23270  ovolscalem1  23281  ovolicc1  23284  ovolicc2lem4  23288  ovolicc2  23290  ovolicc  23291  voliunlem2  23319  ovolioo  23336  ioorcl2  23340  uniioovol  23347  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem6  23356  opnmbllem  23369  volcn  23374  vitalilem2  23378  ismbf3d  23421  mbfaddlem  23427  i1fadd  23462  itg1addlem4  23466  mbfi1fseqlem6  23487  itg2seq  23509  itg2split  23516  itg2cnlem2  23529  itg2cn  23530  itgrevallem1  23561  dvcjbr  23712  dvferm1lem  23747  dvferm2lem  23749  cmvth  23754  mvth  23755  dvlip  23756  dvlip2  23758  c1liplem1  23759  dvgt0  23767  dvlt0  23768  dvge0  23769  dvle  23770  dvivthlem1  23771  lhop1lem  23776  lhop  23779  dvcnvrelem1  23780  dvcnvrelem2  23781  dvcnvre  23782  dvcvx  23783  dvfsumle  23784  dvfsumge  23785  dvfsumrlimf  23788  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsum2  23797  ftc1a  23800  ftc1lem4  23802  coe1mul3  23859  ply1divex  23896  plydivex  24052  aalioulem2  24088  aalioulem3  24089  aalioulem4  24090  aalioulem5  24091  aalioulem6  24092  aaliou3lem7  24104  taylthlem2  24128  mtest  24158  pilem2  24206  tangtx  24257  cosordlem  24277  efif1olem2  24289  logcnlem3  24390  logcnlem4  24391  isosctrlem2  24549  chordthmlem2  24560  chordthmlem4  24562  heron  24565  atanlogsublem  24642  atantan  24650  birthdaylem3  24680  logdifbnd  24720  emcllem1  24722  emcllem2  24723  emcllem5  24726  emcllem6  24727  harmonicbnd4  24737  fsumharmonic  24738  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamucov  24764  relgamcl  24788  ftalem2  24800  ftalem5  24803  chpub  24945  logfaclbnd  24947  logfacbnd3  24948  logexprlim  24950  bposlem1  25009  bposlem9  25017  gausslemma2dlem1a  25090  lgseisenlem1  25100  lgsquadlem1  25105  chtppilimlem1  25162  vmadivsum  25171  vmadivsumb  25172  rplogsumlem1  25173  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlem2  25179  dchrisum0re  25202  rplogsum  25216  mulogsumlem  25220  mulog2sumlem1  25223  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  log2sumbnd  25233  selbergb  25238  selberg2lem  25239  selberg2b  25241  chpdifbndlem1  25242  selberg3lem1  25246  selberg3lem2  25247  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrf  25252  pntrmax  25253  pntrsumo1  25254  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd2  25276  pntibndlem2  25280  pntlemg  25287  pntlemn  25289  pntlemj  25292  pntlemf  25294  pntlemo  25296  pntlem3  25298  pntleml  25300  ttgcontlem1  25765  eqeelen  25784  brbtwn2  25785  colinearalg  25790  axcgrid  25796  axsegconlem1  25797  axsegconlem3  25799  axsegconlem8  25804  axsegconlem9  25805  axsegconlem10  25806  ax5seglem3a  25810  ax5seg  25818  axpaschlem  25820  axcontlem8  25851  nbusgrvtxm1  26281  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  crctcsh  26716  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  nvabs  27527  dipcj  27569  minvecolem4  27736  lt2addrd  29516  xlt2addrd  29523  fzsplit3  29553  bcm1n  29554  bhmafibid1  29644  2sqmod  29648  submateqlem1  29873  cnre2csqlem  29956  tpr2rico  29958  dya2ub  30332  dya2icoseg  30339  ballotlemfcc  30555  ballotlemfrcn0  30591  sgnsub  30606  signslema  30639  ftc2re  30676  subfacval3  31171  dnibndlem8  32475  dnibndlem10  32477  dnibndlem11  32478  dnibndlem12  32479  dnicn  32482  knoppcnlem4  32486  unblimceq0  32498  unbdqndv2lem2  32501  knoppndvlem11  32513  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem20  32522  poimirlem29  33438  broucube  33443  opnmbllem0  33445  mblfinlem3  33448  mblfinlem4  33449  itg2addnclem  33461  itg2addnclem3  33463  itg2gt0cn  33465  ftc1cnnclem  33483  areacirclem1  33500  areacirclem2  33501  areacirclem4  33503  areacirclem5  33504  areacirc  33505  cntotbnd  33595  rrnmet  33628  rrndstprj1  33629  rrndstprj2  33630  irrapxlem2  37387  irrapxlem3  37388  irrapxlem4  37389  irrapxlem5  37390  pellexlem2  37394  pellexlem6  37398  pell1qrgaplem  37437  rmspecsqrtnq  37470  rmspecfund  37474  rmspecpos  37481  jm2.24nn  37526  jm2.17c  37529  fzmaxdif  37548  acongeq  37550  modabsdifz  37553  jm3.1lem2  37585  areaquad  37802  imo72b2lem0  38465  cvgdvgrat  38512  hashnzfzclim  38521  binomcxplemdvbinom  38552  oddfl  39489  lefldiveq  39505  fperiodmul  39518  fzdifsuc2  39525  suprltrp  39544  supxrgere  39549  supxrgelem  39553  suplesup  39555  infleinflem2  39587  infleinf  39588  xrralrecnnge  39613  iccshift  39744  iooshift  39748  iooiinicc  39769  fmul01lt1lem2  39817  climinf  39838  sumnnodd  39862  ltmod  39870  lptre2pt  39872  climleltrp  39908  limsupgtlem  40009  liminflimsupclim  40039  fperdvper  40133  dvbdfbdioolem1  40143  dvbdfbdioolem2  40144  dvbdfbdioo  40145  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmul  40158  iblspltprt  40189  itgspltprt  40195  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  sublevolico  40201  stoweidlem1  40218  stoweidlem11  40228  stoweidlem12  40229  stoweidlem13  40230  stoweidlem14  40231  stoweidlem23  40240  stoweidlem24  40241  stoweidlem25  40242  stoweidlem26  40243  stoweidlem34  40251  stoweidlem40  40257  stoweidlem41  40258  stoweidlem42  40259  stoweidlem45  40262  stoweidlem60  40277  stoweidlem62  40279  wallispilem3  40284  wallispilem4  40285  wallispi  40287  wallispi2lem1  40288  stirlinglem5  40295  stirlinglem11  40301  stirlinglem12  40302  dirkercncflem1  40320  fourierdlem4  40328  fourierdlem6  40330  fourierdlem7  40331  fourierdlem9  40333  fourierdlem13  40337  fourierdlem14  40338  fourierdlem15  40339  fourierdlem19  40343  fourierdlem26  40350  fourierdlem35  40359  fourierdlem39  40363  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem56  40379  fourierdlem57  40380  fourierdlem59  40382  fourierdlem60  40383  fourierdlem61  40384  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem66  40389  fourierdlem68  40391  fourierdlem71  40394  fourierdlem72  40395  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem83  40406  fourierdlem84  40407  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem93  40416  fourierdlem95  40418  fourierdlem97  40420  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem107  40430  fourierdlem109  40432  fourierdlem111  40434  fouriersw  40448  elaa2lem  40450  etransclem23  40474  rrxdsfi  40505  rrxtopnfi  40506  rrndistlt  40510  ioorrnopnlem  40524  ioorrnopnxrlem  40526  sge0gtfsumgt  40660  iundjiun  40677  volicorecl  40760  hoiprodcl  40761  hoiprodcl3  40794  volicore  40795  hoidmvcl  40796  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoiqssbllem1  40836  hoiqssbllem2  40837  hoiqssbllem3  40838  hspmbllem1  40840  ovolval5lem1  40866  ovolval5lem2  40867  iunhoiioolem  40889  iccvonmbllem  40892  vonicclem1  40897  preimageiingt  40930  salpreimagtge  40934  smfaddlem1  40971  smflimlem4  40982  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  ltsubsubaddltsub  41315  2elfz2melfz  41328  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  ply1mulgsumlem2  42175  difmodm1lt  42317  nnpw2pmod  42377  dignn0flhalflem1  42409  amgmwlem  42548