Theorem subcld 11492

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   − cmin 11364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171  df-sub 11366

This theorem is referenced by:  subsubadd23  11544  addsubsub23  11545  pnpncand  11558  muleqadd  11781  lineq  11978  modmuladdnn0  13838  hashfz  14350  hashfzo  14352  hashf1lem2  14379  hashf1  14380  ccatswrd  14592  pfxccatin12lem2  14654  crre  15037  remim  15040  remullem  15051  abs3lem  15262  caubnd2  15281  bhmafibid1cn  15389  bhmafibid2cn  15390  bhmafibid2  15392  rlimuni  15473  climuni  15475  rlimcld2  15501  rlimrege0  15502  rlimrecl  15503  mulcn2  15519  reccn2  15520  cn1lem  15521  o1sub  15539  rlimo1  15540  o1dif  15553  rlimsqzlem  15572  caucvgrlem2  15598  iseralt  15608  fsumparts  15729  cvgcmpce  15741  incexclem  15759  arisum2  15784  geoserg  15789  pwdif  15791  geo2sum2  15797  fallfacfwd  15959  binomfallfaclem2  15963  bpolycl  15975  bpoly3  15981  bpoly4  15982  fsumcube  15983  sinf  16049  tanval2  16058  tanval3  16059  sinneg  16071  efival  16077  sinhval  16079  bitsinv1lem  16368  bitsres  16400  pythagtriplem1  16744  pythagtriplem14  16756  pythagtriplem17  16759  dvdsprmpweqle  16814  4sqlem5  16870  mul4sqlem  16881  4sqlem17  16889  vdwlem5  16913  vdwlem6  16914  vdwlem8  16916  blcvx  24742  recld2  24759  addcnlem  24809  cnllycmp  24911  cphipval2  25197  4cphipval2  25198  cphipval  25199  ipcnlem2  25200  rrxmval  25361  rrxmetlem  25363  pjthlem1  25393  ovollb2lem  25445  itgcnlem  25747  dvlem  25853  dvconst  25874  dvid  25875  dvcnp2  25877  dvcnp2OLD  25878  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvcobr  25905  dvcobrOLD  25906  dvcjbr  25909  dvrec  25915  dvmptim  25930  dvcnvlem  25936  dveflem  25939  dvsincos  25941  cmvth  25951  cmvthOLD  25952  dvlip  25954  dvlipcn  25955  c1liplem1  25957  dveq0  25961  dv11cn  25962  dvle  25968  lhop1lem  25974  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumrlim  25994  dvfsumrlim2  25995  ftc1lem4  26002  ftc1lem5  26003  ftc2  26007  dgrcolem2  26236  plydiveu  26262  aaliou2b  26305  taylfvallem1  26320  taylply2  26331  taylply2OLD  26332  dvtaylp  26334  dvntaylp  26335  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmbdd  26363  ulmcn  26364  ulmdvlem1  26365  mtest  26369  iblulm  26372  itgulm  26373  abelthlem9  26406  ptolemy  26461  tangtx  26470  sineq0  26489  efeq1  26493  efif1olem4  26510  tanarg  26584  logcnlem3  26609  logcnlem4  26610  advlogexp  26620  efopn  26623  cxpcn3lem  26713  cxpeq  26723  ang180lem4  26778  ang180lem5  26779  ang180  26780  isosctrlem2  26785  isosctrlem3  26786  isosctr  26787  ssscongptld  26788  affineequiv  26789  affineequiv2  26790  affineequiv3  26791  affineequiv4  26792  affineequivne  26793  angpieqvdlem  26794  angpieqvdlem2  26795  angpined  26796  angpieqvd  26797  chordthmlem  26798  chordthmlem2  26799  chordthmlem3  26800  chordthmlem4  26801  chordthmlem5  26802  heron  26804  quad2  26805  quad  26806  dcubic1lem  26809  dcubic  26812  mcubic  26813  cubic2  26814  cubic  26815  dquartlem1  26817  dquartlem2  26818  dquart  26819  quart1cl  26820  quart1lem  26821  quart1  26822  quartlem2  26824  quartlem4  26826  quart  26827  atanf  26846  sinasin  26855  asinsin  26858  atanneg  26873  atancj  26876  efiatan  26878  atanlogsub  26882  efiatan2  26883  2efiatan  26884  atanbndlem  26891  dvatan  26901  atantayl  26903  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamgulm2  27002  lgamucov  27004  lgamcvg2  27021  gamcvg  27022  gamcvg2lem  27025  ftalem2  27040  logfacrlim  27191  logexprlim  27192  lgsdirprm  27298  gausslemma2dlem1a  27332  gausslemma2dlem4  27336  2sqmod  27403  addsq2nreurex  27411  vmadivsum  27449  rpvmasumlem  27454  dchrisumlem2  27457  dchrisumlem3  27458  dchrmusum2  27461  dchrvmasumlem2  27465  dchrvmasumlem3  27466  dchrvmasumiflem1  27468  rpvmasum2  27479  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  rplogsum  27494  mudivsum  27497  mulogsumlem  27498  mulogsum  27499  mulog2sumlem1  27501  mulog2sumlem2  27502  mulog2sumlem3  27503  vmalogdivsum2  27505  vmalogdivsum  27506  2vmadivsumlem  27507  selberglem1  27512  selberglem2  27513  selberg2lem  27517  selberg2  27518  selberg3lem1  27524  selberg4lem1  27527  selberg4  27528  pntrsumo1  27532  selberg3r  27536  selberg34r  27538  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntibndlem2  27558  pntlemf  27572  pntlemo  27574  ttgcontlem1  28957  brbtwn2  28978  colinearalglem1  28979  colinearalglem2  28980  colinearalg  28983  axsegconlem1  28990  ax5seglem1  29001  ax5seglem2  29002  ax5seglem6  29007  ax5seglem9  29010  axlowdimlem17  29031  axcontlem7  29043  axcontlem8  29044  clwlkclwwlk  30077  clwwlknonex2lem1  30182  2clwwlk2clwwlk  30425  numclwwlk3lem1  30457  smcnlem  30772  ipval2  30782  4ipval2  30783  dipcj  30789  pjhthlem1  31466  submuladdd  32819  binom2subadd  32821  pythagreim  32825  quad3d  32829  lt2addrd  32830  bcm1n  32875  cycpmco2lem5  33212  cycpmco2lem6  33213  vietalem  33735  constrrtll  33888  constrrtlc1  33889  constrrtcclem  33891  constrrtcc  33892  constrsslem  33898  constrconj  33902  constrfin  33903  constrelextdg2  33904  constraddcl  33919  iconstr  33923  constrremulcl  33924  constrrecl  33926  constrmulcl  33928  constrreinvcl  33929  constrresqrtcl  33934  cos9thpiminplylem2  33940  cos9thpiminplylem3  33941  sqsscirc2  34066  signslema  34719  circlemeth  34797  logdivsqrle  34807  revpfxsfxrev  35310  revwlk  35319  subfaclim  35382  divcnvlin  35927  iprodgam  35936  dnicld1  36672  dnibndlem2  36679  dnibndlem3  36680  dnibndlem6  36683  dnibndlem9  36686  dnibndlem10  36687  dnibndlem11  36688  unblimceq0  36707  unbdqndv2lem1  36709  unbdqndv2lem2  36710  knoppndvlem11  36722  knoppndvlem15  36726  knoppndvlem17  36728  knoppndvlem21  36732  bj-bary1lem  37515  bj-bary1lem1  37516  bj-bary1  37517  ftc1cnnclem  37892  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  ftc2nc  37903  areacirclem1  37909  areacirclem4  37912  areacirc  37914  cntotbnd  37997  lcmineqlem8  42300  lcmineqlem10  42302  lcmineqlem11  42303  lcmineqlem12  42304  lcmineqlem23  42315  aks4d1p1  42340  aks6d1c5lem1  42400  sticksstones10  42419  sticksstones12a  42421  sticksstones12  42422  sticksstones22  42432  bcle2d  42443  mvrrsubd  42539  lsubrotld  42542  lsubswap23d  42544  nicomachus  42577  sumcubes  42578  ef11d  42604  tanhalfpim  42614  sinpim  42615  cospim  42616  dffltz  42887  fltnltalem  42915  rencldnfilem  43072  pellexlem2  43082  pellexlem6  43086  pell1234qrne0  43105  pell1234qrmulcl  43107  rmyluc  43189  jm2.18  43240  jm2.19  43245  areaquad  43468  lhe4.4ex1a  44580  bcc0  44591  bccp1k  44592  bccm1k  44593  binomcxplemwb  44599  binomcxplemnn0  44600  binomcxplemrat  44601  binomcxplemfrat  44602  binomcxplemdvbinom  44604  binomcxplemnotnn0  44607  isosctrlem1ALT  45184  sineq0ALT  45187  oddfl  45536  dstregt0  45540  subadd4b  45541  sub31  45548  fzisoeu  45558  absnpncan2d  45560  absnpncan3d  45565  supxrgelem  45592  absimlere  45733  cvgcaule  45745  mullimc  45872  ellimcabssub0  45873  mullimcf  45879  limcrecl  45885  lptre2pt  45894  limcleqr  45898  neglimc  45901  addlimc  45902  0ellimcdiv  45903  limclner  45905  reclimc  45907  climleltrp  45930  climisp  46000  climxrrelem  46003  climxrre  46004  cnrefiisplem  46083  climxlim2lem  46099  fprodsubrecnncnvlem  46161  fperdvper  46173  dvdivbd  46177  dvbdfbdioolem2  46183  ioodvbdlimc1lem1  46185  volioc  46226  volico  46237  stoweidlem1  46255  stoweidlem11  46265  stoweidlem13  46267  stoweidlem26  46280  stoweid  46317  wallispi  46324  wallispi2lem1  46325  wallispi2lem2  46326  wallispi2  46327  stirlinglem1  46328  stirlinglem4  46331  stirlinglem5  46332  stirlinglem7  46334  stirlinglem11  46338  dirkertrigeqlem2  46353  fourierdlem4  46365  fourierdlem26  46387  fourierdlem30  46391  fourierdlem42  46403  fourierdlem63  46423  fourierdlem65  46425  fourierdlem72  46432  fourierdlem74  46434  fourierdlem75  46435  fourierdlem76  46436  fourierdlem80  46440  fourierdlem81  46441  fourierdlem89  46449  fourierdlem90  46450  fourierdlem91  46451  fourierdlem107  46467  fourierdlem109  46469  fouriersw  46485  etransclem1  46489  etransclem4  46492  etransclem8  46496  etransclem18  46506  etransclem20  46508  etransclem21  46509  etransclem23  46511  etransclem35  46523  etransclem46  46534  rrxtopnfi  46541  rrndistlt  46544  sge0gtfsumgt  46697  hoidmv1lelem2  46846  hoidmvlelem2  46850  smfmullem1  47045  sigarmf  47108  sigarms  47110  sigarexp  47113  sigardiv  47115  sigarcol  47118  sharhght  47119  sigaradd  47120  cevathlem2  47122  cevath  47123  resubcnnred  47560  fldivmod  47594  ceildivmod  47595  fmtnorec2lem  47798  fmtnorec3  47804  fmtnorec4  47805  lighneallem3  47863  quad1  47876  requad01  47877  requad2  47879  fppr2odd  47987  dignn0flhalflem2  48872  affinecomb2  48959  1subrec1sub  48961  eenglngeehlnmlem1  48993  eenglngeehlnmlem2  48994  rrx2vlinest  48997  rrx2linest  48998  line2  49008  itsclc0yqsollem1  49018  itsclc0yqsol  49020  itscnhlc0xyqsol  49021  itschlc0xyqsol1  49022  itschlc0xyqsol  49023  itsclc0xyqsolr  49025  2itscplem1  49034  2itscplem2  49035  2itscplem3  49036  itscnhlinecirc02plem1  49038  inlinecirc02plem  49042  sinhpcosh  49995  i2linesd  50034