Theorem subcld 10392

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

Hypotheses

Ref	Expression
negidd.1	|- ( ph -> A e. CC )
pncand.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
subcld	|- ( ph -> ( A - B ) e. CC )

Proof of Theorem subcld

Step	Hyp	Ref	Expression
1		negidd.1	. 2 |- ( ph -> A e. CC )
2		pncand.2	. 2 |- ( ph -> B e. CC )
3		subcl 10280	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
4	1, 2, 3	syl2anc 693	1 |- ( ph -> ( A - B ) e. CC )

Syntax hints:   -> wi 4   e. wcel 1990  (class class class)co 6650   CCcc 9934   - 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

This theorem is referenced by:  pnpncand  10452  subdir2d  10488  muleqadd  10671  modmuladdnn0  12714  hashfz  13214  hashfzo  13216  hashf1lem2  13240  hashf1  13241  ccatswrd  13456  crre  13854  remim  13857  remullem  13868  abs3lem  14078  caubnd2  14097  rlimuni  14281  climuni  14283  rlimcld2  14309  rlimrege0  14310  rlimrecl  14311  mulcn2  14326  reccn2  14327  cn1lem  14328  o1sub  14346  rlimo1  14347  o1dif  14360  rlimsqzlem  14379  caucvgrlem2  14405  iseralt  14415  fsumparts  14538  cvgcmpce  14550  incexclem  14568  arisum2  14593  geoserg  14598  geo2sum2  14605  fallfacfwd  14767  binomfallfaclem2  14771  bpolycl  14783  bpoly3  14789  bpoly4  14790  fsumcube  14791  sinf  14854  tanval2  14863  tanval3  14864  sinneg  14876  efival  14882  sinhval  14884  bitsinv1lem  15163  bitsres  15195  pythagtriplem1  15521  pythagtriplem14  15533  pythagtriplem17  15536  dvdsprmpweqle  15590  4sqlem5  15646  mul4sqlem  15657  4sqlem17  15665  vdwlem5  15689  vdwlem6  15690  vdwlem8  15692  blcvx  22601  recld2  22617  addcnlem  22667  cnllycmp  22755  cphipval2  23040  4cphipval2  23041  cphipval  23042  ipcnlem2  23043  rrxmval  23188  rrxmetlem  23190  pjthlem1  23208  ovollb2lem  23256  itgcnlem  23556  dvlem  23660  dvconst  23680  dvid  23681  dvcnp2  23683  dvaddbr  23701  dvmulbr  23702  dvcobr  23709  dvcjbr  23712  dvrec  23718  dvmptim  23733  dvcnvlem  23739  dveflem  23742  dvsincos  23744  cmvth  23754  dvlip  23756  dvlipcn  23757  c1liplem1  23759  dveq0  23763  dv11cn  23764  dvle  23770  lhop1lem  23776  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem2  23790  dvfsumrlim  23794  dvfsumrlim2  23795  ftc1lem4  23802  ftc1lem5  23803  ftc2  23807  dgrcolem2  24030  plydiveu  24053  aaliou2b  24096  taylfvallem1  24111  taylply2  24122  dvtaylp  24124  dvntaylp  24125  taylthlem1  24127  taylthlem2  24128  ulmbdd  24152  ulmcn  24153  ulmdvlem1  24154  mtest  24158  iblulm  24161  itgulm  24162  abelthlem9  24194  ptolemy  24248  tangtx  24257  sineq0  24273  efeq1  24275  efif1olem4  24291  tanarg  24365  logcnlem3  24390  logcnlem4  24391  advlogexp  24401  efopn  24404  cxpcn3lem  24488  cxpeq  24498  ang180lem4  24542  ang180lem5  24543  ang180  24544  isosctrlem2  24549  isosctrlem3  24550  isosctr  24551  ssscongptld  24552  affineequiv  24553  affineequiv2  24554  angpieqvdlem  24555  angpieqvdlem2  24556  angpined  24557  angpieqvd  24558  chordthmlem  24559  chordthmlem2  24560  chordthmlem3  24561  chordthmlem4  24562  chordthmlem5  24563  heron  24565  quad2  24566  quad  24567  dcubic1lem  24570  dcubic  24573  mcubic  24574  cubic2  24575  cubic  24576  dquartlem1  24578  dquartlem2  24579  dquart  24580  quart1cl  24581  quart1lem  24582  quart1  24583  quartlem2  24585  quartlem4  24587  quart  24588  atanf  24607  sinasin  24616  asinsin  24619  atanneg  24634  atancj  24637  efiatan  24639  atanlogsub  24643  efiatan2  24644  2efiatan  24645  atanbndlem  24652  dvatan  24662  atantayl  24664  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamgulm2  24762  lgamucov  24764  lgamcvg2  24781  gamcvg  24782  gamcvg2lem  24785  ftalem2  24800  logfacrlim  24949  logexprlim  24950  lgsdirprm  25056  gausslemma2dlem1a  25090  gausslemma2dlem4  25094  vmadivsum  25171  rpvmasumlem  25176  dchrisumlem2  25179  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  rpvmasum2  25201  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  rplogsum  25216  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  mulog2sumlem1  25223  mulog2sumlem2  25224  mulog2sumlem3  25225  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  selberglem1  25234  selberglem2  25235  selberg2lem  25239  selberg2  25240  selberg3lem1  25246  selberg4lem1  25249  selberg4  25250  pntrsumo1  25254  selberg3r  25258  selberg34r  25260  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntibndlem2  25280  pntlemf  25294  pntlemo  25296  ttgcontlem1  25765  brbtwn2  25785  colinearalglem1  25786  colinearalglem2  25787  colinearalg  25790  axsegconlem1  25797  ax5seglem2  25809  ax5seglem6  25814  ax5seglem9  25817  axlowdimlem17  25838  axcontlem7  25850  axcontlem8  25851  clwlkclwwlk  26903  numclwlk3lem3  27206  numclwwlkovf2exlem1  27211  numclwlk1lem2fo  27228  smcnlem  27552  ipval2  27562  4ipval2  27563  dipcj  27569  pjhthlem1  28250  lt2addrd  29516  bcm1n  29554  bhmafibid2  29645  2sqmod  29648  sqsscirc2  29955  signslema  30639  circlemeth  30718  logdivsqrle  30728  subfaclim  31170  divcnvlin  31618  iprodgam  31628  dnicld1  32462  dnibndlem2  32469  dnibndlem3  32470  dnibndlem6  32473  dnibndlem9  32476  dnibndlem10  32477  dnibndlem11  32478  unblimceq0  32498  unbdqndv2lem1  32500  unbdqndv2lem2  32501  knoppndvlem11  32513  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem21  32523  bj-lineq  33158  bj-bary1lem  33160  bj-bary1lem1  33161  bj-bary1  33162  ftc1cnnclem  33483  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  ftc2nc  33494  areacirclem1  33500  areacirclem4  33503  areacirc  33505  cntotbnd  33595  rencldnfilem  37384  pellexlem2  37394  pellexlem6  37398  pell1234qrne0  37417  pell1234qrmulcl  37419  rmyluc  37502  jm2.18  37555  jm2.19  37560  areaquad  37802  lhe4.4ex1a  38528  bcc0  38539  bccp1k  38540  bccm1k  38541  binomcxplemwb  38547  binomcxplemnn0  38548  binomcxplemrat  38549  binomcxplemfrat  38550  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  isosctrlem1ALT  39170  sineq0ALT  39173  oddfl  39489  dstregt0  39493  subadd4b  39494  sub31  39503  fzisoeu  39514  absnpncan2d  39516  absnpncan3d  39521  supxrgelem  39553  absimlere  39710  mullimc  39848  ellimcabssub0  39849  mullimcf  39855  limcrecl  39861  lptre2pt  39872  limcleqr  39876  neglimc  39879  addlimc  39880  0ellimcdiv  39881  limclner  39883  reclimc  39885  climleltrp  39908  climisp  39978  climxrrelem  39981  climxrre  39982  cnrefiisplem  40055  climxlim2lem  40071  fprodsubrecnncnvlem  40121  fperdvper  40133  dvdivbd  40138  dvbdfbdioolem2  40144  ioodvbdlimc1lem1  40146  volioc  40188  volico  40200  stoweidlem1  40218  stoweidlem11  40228  stoweidlem13  40230  stoweidlem26  40243  stoweid  40280  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  wallispi2  40290  stirlinglem1  40291  stirlinglem4  40294  stirlinglem5  40295  stirlinglem7  40297  stirlinglem11  40301  dirkertrigeqlem2  40316  fourierdlem4  40328  fourierdlem26  40350  fourierdlem30  40354  fourierdlem42  40366  fourierdlem63  40386  fourierdlem65  40388  fourierdlem72  40395  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem80  40403  fourierdlem81  40404  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem107  40430  fourierdlem109  40432  fouriersw  40448  etransclem1  40452  etransclem4  40455  etransclem8  40459  etransclem18  40469  etransclem20  40471  etransclem21  40472  etransclem23  40474  etransclem35  40486  etransclem46  40497  rrxtopnfi  40506  rrndistlt  40510  sge0gtfsumgt  40660  hoidmv1lelem2  40806  hoidmvlelem2  40810  smfmullem1  40998  sigarmf  41043  sigarms  41045  sigarexp  41048  sigardiv  41050  sigarcol  41053  sharhght  41054  sigaradd  41055  cevathlem2  41057  cevath  41058  pfxccatin12lem2  41424  fmtnorec2lem  41454  fmtnorec3  41460  fmtnorec4  41461  pwdif  41501  lighneallem3  41524  fldivmod  42313  dignn0flhalflem2  42410  sinhpcosh  42481  i2linesd  42525