Theorem subcld 11564

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

Hypotheses

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
pncand.2	⊢ (𝜑 → 𝐵 ∈ ℂ)

Assertion

Ref	Expression
subcld	⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)

Proof of Theorem subcld

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		pncand.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		subcl 11451	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093   − cmin 11436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-ltxr 11243  df-sub 11438

This theorem is referenced by:  subsubadd23  11616  addsubsub23  11617  pnpncand  11630  muleqadd  11853  lineq  12047  modmuladdnn0  13947  hashfz  14460  hashfzo  14462  hashf1lem2  14489  hashf1  14490  ccatswrd  14702  pfxccatin12lem2  14764  crre  15161  remim  15164  remullem  15175  abs3lem  15386  caubnd2  15405  bhmafibid1cn  15513  bhmafibid2cn  15514  bhmafibid2  15516  rlimuni  15597  climuni  15599  rlimcld2  15625  rlimrege0  15626  rlimrecl  15627  mulcn2  15643  reccn2  15644  cn1lem  15645  o1sub  15663  rlimo1  15664  o1dif  15677  rlimsqzlem  15696  caucvgrlem2  15722  iseralt  15732  fsumparts  15854  cvgcmpce  15866  incexclem  15886  arisum2  15911  geoserg  15916  pwdif  15918  geo2sum2  15924  fallfacfwd  16085  binomfallfaclem2  16089  bpolycl  16101  bpoly3  16107  bpoly4  16108  fsumcube  16109  sinf  16175  tanval2  16184  tanval3  16185  sinneg  16197  efival  16203  sinhval  16205  bitsinv1lem  16494  bitsres  16526  pythagtriplem1  16871  pythagtriplem14  16883  pythagtriplem17  16886  dvdsprmpweqle  16941  4sqlem5  16997  mul4sqlem  17008  4sqlem17  17016  vdwlem5  17040  vdwlem6  17041  vdwlem8  17043  blcvx  24955  recld2  24972  addcnlem  25022  cnllycmp  25115  cphipval2  25400  4cphipval2  25401  cphipval  25402  ipcnlem2  25403  rrxmval  25564  rrxmetlem  25566  pjthlem1  25596  ovollb2lem  25647  itgcnlem  25949  dvlem  26055  dvconst  26076  dvid  26077  dvcnp2  26079  dvaddbr  26097  dvmulbr  26098  dvcobr  26105  dvcjbr  26108  dvrec  26114  dvmptim  26129  dvcnvlem  26135  dveflem  26138  dvsincos  26140  cmvth  26150  dvlip  26152  dvlipcn  26153  c1liplem1  26155  dveq0  26159  dv11cn  26160  dvle  26166  lhop1lem  26172  dvfsumabs  26182  dvfsumlem1  26185  dvfsumlem2  26186  dvfsumrlim  26190  dvfsumrlim2  26191  ftc1lem4  26198  ftc1lem5  26199  ftc2  26203  dgrcolem2  26431  plydiveu  26459  aaliou2b  26504  taylfvallem1  26520  taylply2  26531  dvtaylp  26533  dvntaylp  26534  taylthlem1  26536  taylthlem2  26537  ulmbdd  26561  ulmcn  26562  ulmdvlem1  26563  mtest  26567  iblulm  26570  itgulm  26571  abelthlem9  26603  ptolemy  26661  tangtx  26670  sineq0  26689  efeq1  26693  efif1olem4  26710  tanarg  26784  logcnlem3  26809  logcnlem4  26810  advlogexp  26820  efopn  26823  cxpcn3lem  26912  cxpeq  26922  ang180lem4  26977  ang180lem5  26978  ang180  26979  isosctrlem2  26984  isosctrlem3  26985  isosctr  26986  ssscongptld  26987  affineequiv  26988  affineequiv2  26989  affineequiv3  26990  affineequiv4  26991  affineequivne  26992  angpieqvdlem  26993  angpieqvdlem2  26994  angpined  26995  angpieqvd  26996  chordthmlem  26997  chordthmlem2  26998  chordthmlem3  26999  chordthmlem4  27000  chordthmlem5  27001  heron  27003  quad2  27004  quad  27005  dcubic1lem  27008  dcubic  27011  mcubic  27012  cubic2  27013  cubic  27014  dquartlem1  27016  dquartlem2  27017  dquart  27018  quart1cl  27019  quart1lem  27020  quart1  27021  quartlem2  27023  quartlem4  27025  quart  27026  atanf  27045  sinasin  27054  asinsin  27057  atanneg  27072  atancj  27075  efiatan  27077  atanlogsub  27081  efiatan2  27082  2efiatan  27083  atanbndlem  27090  dvatan  27100  atantayl  27102  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem5  27197  lgamgulmlem6  27198  lgamgulm2  27200  lgamucov  27202  lgamcvg2  27219  gamcvg  27220  gamcvg2lem  27223  ftalem2  27238  logfacrlim  27388  logexprlim  27389  lgsdirprm  27495  gausslemma2dlem1a  27529  gausslemma2dlem4  27533  2sqmod  27600  addsq2nreurex  27608  vmadivsum  27646  rpvmasumlem  27651  dchrisumlem2  27654  dchrisumlem3  27655  dchrmusum2  27658  dchrvmasumlem2  27662  dchrvmasumlem3  27663  dchrvmasumiflem1  27665  rpvmasum2  27676  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  rplogsum  27691  mudivsum  27694  mulogsumlem  27695  mulogsum  27696  mulog2sumlem1  27698  mulog2sumlem2  27699  mulog2sumlem3  27700  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  selberglem1  27709  selberglem2  27710  selberg2lem  27714  selberg2  27715  selberg3lem1  27721  selberg4lem1  27724  selberg4  27725  pntrsumo1  27729  selberg3r  27733  selberg34r  27735  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntibndlem2  27755  pntlemf  27769  pntlemo  27771  ttgcontlem1  29234  brbtwn2  29255  colinearalglem1  29256  colinearalglem2  29257  colinearalg  29260  axsegconlem1  29267  ax5seglem1  29278  ax5seglem2  29279  ax5seglem6  29284  ax5seglem9  29287  axlowdimlem17  29308  axcontlem7  29320  axcontlem8  29321  clwlkclwwlk  30353  clwwlknonex2lem1  30458  2clwwlk2clwwlk  30701  numclwwlk3lem1  30733  smcnlem  31049  ipval2  31059  4ipval2  31060  dipcj  31066  pjhthlem1  31743  submuladdd  33085  binom2subadd  33086  pythagreim  33090  quad3d  33094  lt2addrd  33095  bcm1n  33140  cycpmco2lem5  33450  cycpmco2lem6  33451  vietalem  33969  constrrtll  34121  constrrtlc1  34122  constrrtcclem  34124  constrrtcc  34125  constrsslem  34131  constrconj  34135  constrfin  34136  constrelextdg2  34137  constraddcl  34152  iconstr  34156  constrremulcl  34157  constrrecl  34159  constrmulcl  34161  constrreinvcl  34162  constrresqrtcl  34167  cos9thpiminplylem2  34173  cos9thpiminplylem3  34174  sqsscirc2  34299  signslema  34949  circlemeth  35027  logdivsqrle  35037  revpfxsfxrev  35607  revwlk  35617  subfaclim  35680  divcnvlin  36225  iprodgam  36234  dnicld1  37081  dnibndlem2  37088  dnibndlem3  37089  dnibndlem6  37092  dnibndlem9  37095  dnibndlem10  37096  dnibndlem11  37097  unblimceq0  37116  unbdqndv2lem1  37118  unbdqndv2lem2  37119  knoppndvlem11  37131  knoppndvlem15  37135  knoppndvlem17  37137  knoppndvlem21  37141  bj-bary1lem  37974  bj-bary1lem1  37975  bj-bary1  37976  qdiff  37991  ftc1cnnclem  38362  ftc1anclem7  38370  ftc1anclem8  38371  ftc1anc  38372  ftc2nc  38373  areacirclem1  38379  areacirclem4  38382  areacirc  38384  cntotbnd  38467  lcmineqlem8  42823  lcmineqlem10  42825  lcmineqlem11  42826  lcmineqlem12  42827  lcmineqlem23  42838  aks4d1p1  42863  aks6d1c5lem1  42923  sticksstones10  42942  sticksstones12a  42944  sticksstones12  42945  sticksstones22  42955  bcle2d  42966  quadfac  42992  mvrrsubd  43055  lsubrotld  43058  lsubswap23d  43060  nicomachus  43093  sumcubes  43094  ef11d  43120  tanhalfpim  43130  sinpim  43131  cospim  43132  dffltz  43386  fltnltalem  43414  rencldnfilem  43567  pellexlem2  43577  pellexlem6  43581  pell1234qrne0  43600  pell1234qrmulcl  43602  rmyluc  43684  jm2.18  43735  jm2.19  43740  areaquad  43963  lhe4.4ex1a  45059  bcc0  45070  bccp1k  45071  bccm1k  45072  binomcxplemwb  45078  binomcxplemnn0  45079  binomcxplemrat  45080  binomcxplemfrat  45081  binomcxplemdvbinom  45083  binomcxplemnotnn0  45086  isosctrlem1ALT  45662  sineq0ALT  45665  oddfl  46017  dstregt0  46021  subadd4b  46022  sub31  46029  fzisoeu  46039  absnpncan2d  46041  absnpncan3d  46046  supxrgelem  46073  absimlere  46213  cvgcaule  46225  mullimc  46352  ellimcabssub0  46353  mullimcf  46359  limcrecl  46365  lptre2pt  46374  limcleqr  46378  neglimc  46381  addlimc  46382  0ellimcdiv  46383  limclner  46385  reclimc  46387  climleltrp  46410  climisp  46480  climxrrelem  46483  climxrre  46484  cnrefiisplem  46563  climxlim2lem  46579  fprodsubrecnncnvlem  46641  fperdvper  46653  dvdivbd  46657  dvbdfbdioolem2  46663  ioodvbdlimc1lem1  46665  volioc  46706  volico  46717  stoweidlem1  46735  stoweidlem11  46745  stoweidlem13  46747  stoweidlem26  46760  stoweid  46797  wallispi  46804  wallispi2lem1  46805  wallispi2lem2  46806  wallispi2  46807  stirlinglem1  46808  stirlinglem4  46811  stirlinglem5  46812  stirlinglem7  46814  stirlinglem11  46818  dirkertrigeqlem2  46833  fourierdlem4  46845  fourierdlem26  46867  fourierdlem30  46871  fourierdlem42  46883  fourierdlem63  46903  fourierdlem65  46905  fourierdlem72  46912  fourierdlem74  46914  fourierdlem75  46915  fourierdlem76  46916  fourierdlem80  46920  fourierdlem81  46921  fourierdlem89  46929  fourierdlem90  46930  fourierdlem91  46931  fourierdlem107  46947  fourierdlem109  46949  fouriersw  46965  etransclem1  46969  etransclem4  46972  etransclem8  46976  etransclem18  46986  etransclem20  46988  etransclem21  46989  etransclem23  46991  etransclem35  47003  etransclem46  47014  rrxtopnfi  47021  rrndistlt  47024  sge0gtfsumgt  47177  hoidmv1lelem2  47326  hoidmvlelem2  47330  smfmullem1  47525  sigarmf  47588  sigarms  47590  sigarexp  47593  sigardiv  47595  sigarcol  47598  sharhght  47599  sigaradd  47600  cevathlem2  47602  cevath  47603  sin5tlem3  47632  sin5tlem4  47633  sin5tlem5  47634  cos5t  47636  resubcnnred  48061  fldivmod  48101  ceildivmod  48102  fmtnorec2lem  48314  fmtnorec3  48320  fmtnorec4  48321  lighneallem3  48379  quad1  48405  requad01  48406  requad2  48408  fppr2odd  48516  dignn0flhalflem2  49416  affinecomb2  49503  1subrec1sub  49505  eenglngeehlnmlem1  49537  eenglngeehlnmlem2  49538  rrx2vlinest  49541  rrx2linest  49542  line2  49552  itsclc0yqsollem1  49562  itsclc0yqsol  49564  itscnhlc0xyqsol  49565  itschlc0xyqsol1  49566  itschlc0xyqsol  49567  itsclc0xyqsolr  49569  2itscplem1  49578  2itscplem2  49579  2itscplem3  49580  itscnhlinecirc02plem1  49582  inlinecirc02plem  49586  sinhpcosh  50538  i2linesd  50577