Theorem subcld 11504

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 11391	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 − 𝐵) ∈ ℂ)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   − cmin 11376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-sub 11378

This theorem is referenced by:  subsubadd23  11556  addsubsub23  11557  pnpncand  11570  muleqadd  11793  lineq  11990  modmuladdnn0  13850  hashfz  14362  hashfzo  14364  hashf1lem2  14391  hashf1  14392  ccatswrd  14604  pfxccatin12lem2  14666  crre  15049  remim  15052  remullem  15063  abs3lem  15274  caubnd2  15293  bhmafibid1cn  15401  bhmafibid2cn  15402  bhmafibid2  15404  rlimuni  15485  climuni  15487  rlimcld2  15513  rlimrege0  15514  rlimrecl  15515  mulcn2  15531  reccn2  15532  cn1lem  15533  o1sub  15551  rlimo1  15552  o1dif  15565  rlimsqzlem  15584  caucvgrlem2  15610  iseralt  15620  fsumparts  15741  cvgcmpce  15753  incexclem  15771  arisum2  15796  geoserg  15801  pwdif  15803  geo2sum2  15809  fallfacfwd  15971  binomfallfaclem2  15975  bpolycl  15987  bpoly3  15993  bpoly4  15994  fsumcube  15995  sinf  16061  tanval2  16070  tanval3  16071  sinneg  16083  efival  16089  sinhval  16091  bitsinv1lem  16380  bitsres  16412  pythagtriplem1  16756  pythagtriplem14  16768  pythagtriplem17  16771  dvdsprmpweqle  16826  4sqlem5  16882  mul4sqlem  16893  4sqlem17  16901  vdwlem5  16925  vdwlem6  16926  vdwlem8  16928  blcvx  24754  recld2  24771  addcnlem  24821  cnllycmp  24923  cphipval2  25209  4cphipval2  25210  cphipval  25211  ipcnlem2  25212  rrxmval  25373  rrxmetlem  25375  pjthlem1  25405  ovollb2lem  25457  itgcnlem  25759  dvlem  25865  dvconst  25886  dvid  25887  dvcnp2  25889  dvcnp2OLD  25890  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcobr  25917  dvcobrOLD  25918  dvcjbr  25921  dvrec  25927  dvmptim  25942  dvcnvlem  25948  dveflem  25951  dvsincos  25953  cmvth  25963  cmvthOLD  25964  dvlip  25966  dvlipcn  25967  c1liplem1  25969  dveq0  25973  dv11cn  25974  dvle  25980  lhop1lem  25986  dvfsumabs  25997  dvfsumlem1  26000  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumrlim  26006  dvfsumrlim2  26007  ftc1lem4  26014  ftc1lem5  26015  ftc2  26019  dgrcolem2  26248  plydiveu  26274  aaliou2b  26317  taylfvallem1  26332  taylply2  26343  taylply2OLD  26344  dvtaylp  26346  dvntaylp  26347  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmbdd  26375  ulmcn  26376  ulmdvlem1  26377  mtest  26381  iblulm  26384  itgulm  26385  abelthlem9  26418  ptolemy  26473  tangtx  26482  sineq0  26501  efeq1  26505  efif1olem4  26522  tanarg  26596  logcnlem3  26621  logcnlem4  26622  advlogexp  26632  efopn  26635  cxpcn3lem  26725  cxpeq  26735  ang180lem4  26790  ang180lem5  26791  ang180  26792  isosctrlem2  26797  isosctrlem3  26798  isosctr  26799  ssscongptld  26800  affineequiv  26801  affineequiv2  26802  affineequiv3  26803  affineequiv4  26804  affineequivne  26805  angpieqvdlem  26806  angpieqvdlem2  26807  angpined  26808  angpieqvd  26809  chordthmlem  26810  chordthmlem2  26811  chordthmlem3  26812  chordthmlem4  26813  chordthmlem5  26814  heron  26816  quad2  26817  quad  26818  dcubic1lem  26821  dcubic  26824  mcubic  26825  cubic2  26826  cubic  26827  dquartlem1  26829  dquartlem2  26830  dquart  26831  quart1cl  26832  quart1lem  26833  quart1  26834  quartlem2  26836  quartlem4  26838  quart  26839  atanf  26858  sinasin  26867  asinsin  26870  atanneg  26885  atancj  26888  efiatan  26890  atanlogsub  26894  efiatan2  26895  2efiatan  26896  atanbndlem  26903  dvatan  26913  atantayl  26915  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamgulm2  27014  lgamucov  27016  lgamcvg2  27033  gamcvg  27034  gamcvg2lem  27037  ftalem2  27052  logfacrlim  27203  logexprlim  27204  lgsdirprm  27310  gausslemma2dlem1a  27344  gausslemma2dlem4  27348  2sqmod  27415  addsq2nreurex  27423  vmadivsum  27461  rpvmasumlem  27466  dchrisumlem2  27469  dchrisumlem3  27470  dchrmusum2  27473  dchrvmasumlem2  27477  dchrvmasumlem3  27478  dchrvmasumiflem1  27480  rpvmasum2  27491  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  rplogsum  27506  mudivsum  27509  mulogsumlem  27510  mulogsum  27511  mulog2sumlem1  27513  mulog2sumlem2  27514  mulog2sumlem3  27515  vmalogdivsum2  27517  vmalogdivsum  27518  2vmadivsumlem  27519  selberglem1  27524  selberglem2  27525  selberg2lem  27529  selberg2  27530  selberg3lem1  27536  selberg4lem1  27539  selberg4  27540  pntrsumo1  27544  selberg3r  27548  selberg34r  27550  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntibndlem2  27570  pntlemf  27584  pntlemo  27586  ttgcontlem1  28969  brbtwn2  28990  colinearalglem1  28991  colinearalglem2  28992  colinearalg  28995  axsegconlem1  29002  ax5seglem1  29013  ax5seglem2  29014  ax5seglem6  29019  ax5seglem9  29022  axlowdimlem17  29043  axcontlem7  29055  axcontlem8  29056  clwlkclwwlk  30089  clwwlknonex2lem1  30194  2clwwlk2clwwlk  30437  numclwwlk3lem1  30469  smcnlem  30785  ipval2  30795  4ipval2  30796  dipcj  30802  pjhthlem1  31479  submuladdd  32830  binom2subadd  32832  pythagreim  32836  quad3d  32840  lt2addrd  32841  bcm1n  32886  cycpmco2lem5  33224  cycpmco2lem6  33225  vietalem  33756  constrrtll  33909  constrrtlc1  33910  constrrtcclem  33912  constrrtcc  33913  constrsslem  33919  constrconj  33923  constrfin  33924  constrelextdg2  33925  constraddcl  33940  iconstr  33944  constrremulcl  33945  constrrecl  33947  constrmulcl  33949  constrreinvcl  33950  constrresqrtcl  33955  cos9thpiminplylem2  33961  cos9thpiminplylem3  33962  sqsscirc2  34087  signslema  34740  circlemeth  34818  logdivsqrle  34828  revpfxsfxrev  35332  revwlk  35341  subfaclim  35404  divcnvlin  35949  iprodgam  35958  dnicld1  36694  dnibndlem2  36701  dnibndlem3  36702  dnibndlem6  36705  dnibndlem9  36708  dnibndlem10  36709  dnibndlem11  36710  unblimceq0  36729  unbdqndv2lem1  36731  unbdqndv2lem2  36732  knoppndvlem11  36744  knoppndvlem15  36748  knoppndvlem17  36750  knoppndvlem21  36754  bj-bary1lem  37565  bj-bary1lem1  37566  bj-bary1  37567  ftc1cnnclem  37942  ftc1anclem7  37950  ftc1anclem8  37951  ftc1anc  37952  ftc2nc  37953  areacirclem1  37959  areacirclem4  37962  areacirc  37964  cntotbnd  38047  lcmineqlem8  42406  lcmineqlem10  42408  lcmineqlem11  42409  lcmineqlem12  42410  lcmineqlem23  42421  aks4d1p1  42446  aks6d1c5lem1  42506  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  sticksstones22  42538  bcle2d  42549  mvrrsubd  42644  lsubrotld  42647  lsubswap23d  42649  nicomachus  42682  sumcubes  42683  ef11d  42709  tanhalfpim  42719  sinpim  42720  cospim  42721  dffltz  42992  fltnltalem  43020  rencldnfilem  43177  pellexlem2  43187  pellexlem6  43191  pell1234qrne0  43210  pell1234qrmulcl  43212  rmyluc  43294  jm2.18  43345  jm2.19  43350  areaquad  43573  lhe4.4ex1a  44685  bcc0  44696  bccp1k  44697  bccm1k  44698  binomcxplemwb  44704  binomcxplemnn0  44705  binomcxplemrat  44706  binomcxplemfrat  44707  binomcxplemdvbinom  44709  binomcxplemnotnn0  44712  isosctrlem1ALT  45289  sineq0ALT  45292  oddfl  45640  dstregt0  45644  subadd4b  45645  sub31  45652  fzisoeu  45662  absnpncan2d  45664  absnpncan3d  45669  supxrgelem  45696  absimlere  45837  cvgcaule  45849  mullimc  45976  ellimcabssub0  45977  mullimcf  45983  limcrecl  45989  lptre2pt  45998  limcleqr  46002  neglimc  46005  addlimc  46006  0ellimcdiv  46007  limclner  46009  reclimc  46011  climleltrp  46034  climisp  46104  climxrrelem  46107  climxrre  46108  cnrefiisplem  46187  climxlim2lem  46203  fprodsubrecnncnvlem  46265  fperdvper  46277  dvdivbd  46281  dvbdfbdioolem2  46287  ioodvbdlimc1lem1  46289  volioc  46330  volico  46341  stoweidlem1  46359  stoweidlem11  46369  stoweidlem13  46371  stoweidlem26  46384  stoweid  46421  wallispi  46428  wallispi2lem1  46429  wallispi2lem2  46430  wallispi2  46431  stirlinglem1  46432  stirlinglem4  46435  stirlinglem5  46436  stirlinglem7  46438  stirlinglem11  46442  dirkertrigeqlem2  46457  fourierdlem4  46469  fourierdlem26  46491  fourierdlem30  46495  fourierdlem42  46507  fourierdlem63  46527  fourierdlem65  46529  fourierdlem72  46536  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem80  46544  fourierdlem81  46545  fourierdlem89  46553  fourierdlem90  46554  fourierdlem91  46555  fourierdlem107  46571  fourierdlem109  46573  fouriersw  46589  etransclem1  46593  etransclem4  46596  etransclem8  46600  etransclem18  46610  etransclem20  46612  etransclem21  46613  etransclem23  46615  etransclem35  46627  etransclem46  46638  rrxtopnfi  46645  rrndistlt  46648  sge0gtfsumgt  46801  hoidmv1lelem2  46950  hoidmvlelem2  46954  smfmullem1  47149  sigarmf  47212  sigarms  47214  sigarexp  47217  sigardiv  47219  sigarcol  47222  sharhght  47223  sigaradd  47224  cevathlem2  47226  cevath  47227  resubcnnred  47664  fldivmod  47698  ceildivmod  47699  fmtnorec2lem  47902  fmtnorec3  47908  fmtnorec4  47909  lighneallem3  47967  quad1  47980  requad01  47981  requad2  47983  fppr2odd  48091  dignn0flhalflem2  48976  affinecomb2  49063  1subrec1sub  49065  eenglngeehlnmlem1  49097  eenglngeehlnmlem2  49098  rrx2vlinest  49101  rrx2linest  49102  line2  49112  itsclc0yqsollem1  49122  itsclc0yqsol  49124  itscnhlc0xyqsol  49125  itschlc0xyqsol1  49126  itschlc0xyqsol  49127  itsclc0xyqsolr  49129  2itscplem1  49138  2itscplem2  49139  2itscplem3  49140  itscnhlinecirc02plem1  49142  inlinecirc02plem  49146  sinhpcosh  50099  i2linesd  50138