Theorem subcld 11475

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  ℂcc 11007   − cmin 11347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-sub 11349

This theorem is referenced by:  subsubadd23  11527  addsubsub23  11528  pnpncand  11541  muleqadd  11764  lineq  11961  modmuladdnn0  13822  hashfz  14334  hashfzo  14336  hashf1lem2  14363  hashf1  14364  ccatswrd  14575  pfxccatin12lem2  14637  crre  15021  remim  15024  remullem  15035  abs3lem  15246  caubnd2  15265  bhmafibid1cn  15373  bhmafibid2cn  15374  bhmafibid2  15376  rlimuni  15457  climuni  15459  rlimcld2  15485  rlimrege0  15486  rlimrecl  15487  mulcn2  15503  reccn2  15504  cn1lem  15505  o1sub  15523  rlimo1  15524  o1dif  15537  rlimsqzlem  15556  caucvgrlem2  15582  iseralt  15592  fsumparts  15713  cvgcmpce  15725  incexclem  15743  arisum2  15768  geoserg  15773  pwdif  15775  geo2sum2  15781  fallfacfwd  15943  binomfallfaclem2  15947  bpolycl  15959  bpoly3  15965  bpoly4  15966  fsumcube  15967  sinf  16033  tanval2  16042  tanval3  16043  sinneg  16055  efival  16061  sinhval  16063  bitsinv1lem  16352  bitsres  16384  pythagtriplem1  16728  pythagtriplem14  16740  pythagtriplem17  16743  dvdsprmpweqle  16798  4sqlem5  16854  mul4sqlem  16865  4sqlem17  16873  vdwlem5  16897  vdwlem6  16898  vdwlem8  16900  blcvx  24684  recld2  24701  addcnlem  24751  cnllycmp  24853  cphipval2  25139  4cphipval2  25140  cphipval  25141  ipcnlem2  25142  rrxmval  25303  rrxmetlem  25305  pjthlem1  25335  ovollb2lem  25387  itgcnlem  25689  dvlem  25795  dvconst  25816  dvid  25817  dvcnp2  25819  dvcnp2OLD  25820  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvcobr  25847  dvcobrOLD  25848  dvcjbr  25851  dvrec  25857  dvmptim  25872  dvcnvlem  25878  dveflem  25881  dvsincos  25883  cmvth  25893  cmvthOLD  25894  dvlip  25896  dvlipcn  25897  c1liplem1  25899  dveq0  25903  dv11cn  25904  dvle  25910  lhop1lem  25916  dvfsumabs  25927  dvfsumlem1  25930  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumrlim  25936  dvfsumrlim2  25937  ftc1lem4  25944  ftc1lem5  25945  ftc2  25949  dgrcolem2  26178  plydiveu  26204  aaliou2b  26247  taylfvallem1  26262  taylply2  26273  taylply2OLD  26274  dvtaylp  26276  dvntaylp  26277  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmbdd  26305  ulmcn  26306  ulmdvlem1  26307  mtest  26311  iblulm  26314  itgulm  26315  abelthlem9  26348  ptolemy  26403  tangtx  26412  sineq0  26431  efeq1  26435  efif1olem4  26452  tanarg  26526  logcnlem3  26551  logcnlem4  26552  advlogexp  26562  efopn  26565  cxpcn3lem  26655  cxpeq  26665  ang180lem4  26720  ang180lem5  26721  ang180  26722  isosctrlem2  26727  isosctrlem3  26728  isosctr  26729  ssscongptld  26730  affineequiv  26731  affineequiv2  26732  affineequiv3  26733  affineequiv4  26734  affineequivne  26735  angpieqvdlem  26736  angpieqvdlem2  26737  angpined  26738  angpieqvd  26739  chordthmlem  26740  chordthmlem2  26741  chordthmlem3  26742  chordthmlem4  26743  chordthmlem5  26744  heron  26746  quad2  26747  quad  26748  dcubic1lem  26751  dcubic  26754  mcubic  26755  cubic2  26756  cubic  26757  dquartlem1  26759  dquartlem2  26760  dquart  26761  quart1cl  26762  quart1lem  26763  quart1  26764  quartlem2  26766  quartlem4  26768  quart  26769  atanf  26788  sinasin  26797  asinsin  26800  atanneg  26815  atancj  26818  efiatan  26820  atanlogsub  26824  efiatan2  26825  2efiatan  26826  atanbndlem  26833  dvatan  26843  atantayl  26845  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem5  26941  lgamgulmlem6  26942  lgamgulm2  26944  lgamucov  26946  lgamcvg2  26963  gamcvg  26964  gamcvg2lem  26967  ftalem2  26982  logfacrlim  27133  logexprlim  27134  lgsdirprm  27240  gausslemma2dlem1a  27274  gausslemma2dlem4  27278  2sqmod  27345  addsq2nreurex  27353  vmadivsum  27391  rpvmasumlem  27396  dchrisumlem2  27399  dchrisumlem3  27400  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumlem3  27408  dchrvmasumiflem1  27410  rpvmasum2  27421  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  rplogsum  27436  mudivsum  27439  mulogsumlem  27440  mulogsum  27441  mulog2sumlem1  27443  mulog2sumlem2  27444  mulog2sumlem3  27445  vmalogdivsum2  27447  vmalogdivsum  27448  2vmadivsumlem  27449  selberglem1  27454  selberglem2  27455  selberg2lem  27459  selberg2  27460  selberg3lem1  27466  selberg4lem1  27469  selberg4  27470  pntrsumo1  27474  selberg3r  27478  selberg34r  27480  pntrlog2bndlem1  27486  pntrlog2bndlem2  27487  pntrlog2bndlem3  27488  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntibndlem2  27500  pntlemf  27514  pntlemo  27516  ttgcontlem1  28830  brbtwn2  28850  colinearalglem1  28851  colinearalglem2  28852  colinearalg  28855  axsegconlem1  28862  ax5seglem1  28873  ax5seglem2  28874  ax5seglem6  28879  ax5seglem9  28882  axlowdimlem17  28903  axcontlem7  28915  axcontlem8  28916  clwlkclwwlk  29946  clwwlknonex2lem1  30051  2clwwlk2clwwlk  30294  numclwwlk3lem1  30326  smcnlem  30641  ipval2  30651  4ipval2  30652  dipcj  30658  pjhthlem1  31335  submuladdd  32683  binom2subadd  32685  pythagreim  32689  quad3d  32693  lt2addrd  32694  bcm1n  32738  cycpmco2lem5  33072  cycpmco2lem6  33073  constrrtll  33698  constrrtlc1  33699  constrrtcclem  33701  constrrtcc  33702  constrsslem  33708  constrconj  33712  constrfin  33713  constrelextdg2  33714  constraddcl  33729  iconstr  33733  constrremulcl  33734  constrrecl  33736  constrmulcl  33738  constrreinvcl  33739  constrresqrtcl  33744  cos9thpiminplylem2  33750  cos9thpiminplylem3  33751  sqsscirc2  33876  signslema  34530  circlemeth  34608  logdivsqrle  34618  revpfxsfxrev  35093  revwlk  35102  subfaclim  35165  divcnvlin  35710  iprodgam  35719  dnicld1  36450  dnibndlem2  36457  dnibndlem3  36458  dnibndlem6  36461  dnibndlem9  36464  dnibndlem10  36465  dnibndlem11  36466  unblimceq0  36485  unbdqndv2lem1  36487  unbdqndv2lem2  36488  knoppndvlem11  36500  knoppndvlem15  36504  knoppndvlem17  36506  knoppndvlem21  36510  bj-bary1lem  37288  bj-bary1lem1  37289  bj-bary1  37290  ftc1cnnclem  37675  ftc1anclem7  37683  ftc1anclem8  37684  ftc1anc  37685  ftc2nc  37686  areacirclem1  37692  areacirclem4  37695  areacirc  37697  cntotbnd  37780  lcmineqlem8  42013  lcmineqlem10  42015  lcmineqlem11  42016  lcmineqlem12  42017  lcmineqlem23  42028  aks4d1p1  42053  aks6d1c5lem1  42113  sticksstones10  42132  sticksstones12a  42134  sticksstones12  42135  sticksstones22  42145  bcle2d  42156  mvrrsubd  42251  lsubrotld  42254  lsubswap23d  42256  nicomachus  42289  sumcubes  42290  ef11d  42316  tanhalfpim  42326  sinpim  42327  cospim  42328  dffltz  42611  fltnltalem  42639  rencldnfilem  42797  pellexlem2  42807  pellexlem6  42811  pell1234qrne0  42830  pell1234qrmulcl  42832  rmyluc  42914  jm2.18  42965  jm2.19  42970  areaquad  43193  lhe4.4ex1a  44306  bcc0  44317  bccp1k  44318  bccm1k  44319  binomcxplemwb  44325  binomcxplemnn0  44326  binomcxplemrat  44327  binomcxplemfrat  44328  binomcxplemdvbinom  44330  binomcxplemnotnn0  44333  isosctrlem1ALT  44911  sineq0ALT  44914  oddfl  45264  dstregt0  45268  subadd4b  45269  sub31  45276  fzisoeu  45286  absnpncan2d  45288  absnpncan3d  45293  supxrgelem  45321  absimlere  45462  cvgcaule  45474  mullimc  45601  ellimcabssub0  45602  mullimcf  45608  limcrecl  45614  lptre2pt  45625  limcleqr  45629  neglimc  45632  addlimc  45633  0ellimcdiv  45634  limclner  45636  reclimc  45638  climleltrp  45661  climisp  45731  climxrrelem  45734  climxrre  45735  cnrefiisplem  45814  climxlim2lem  45830  fprodsubrecnncnvlem  45892  fperdvper  45904  dvdivbd  45908  dvbdfbdioolem2  45914  ioodvbdlimc1lem1  45916  volioc  45957  volico  45968  stoweidlem1  45986  stoweidlem11  45996  stoweidlem13  45998  stoweidlem26  46011  stoweid  46048  wallispi  46055  wallispi2lem1  46056  wallispi2lem2  46057  wallispi2  46058  stirlinglem1  46059  stirlinglem4  46062  stirlinglem5  46063  stirlinglem7  46065  stirlinglem11  46069  dirkertrigeqlem2  46084  fourierdlem4  46096  fourierdlem26  46118  fourierdlem30  46122  fourierdlem42  46134  fourierdlem63  46154  fourierdlem65  46156  fourierdlem72  46163  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem80  46171  fourierdlem81  46172  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem107  46198  fourierdlem109  46200  fouriersw  46216  etransclem1  46220  etransclem4  46223  etransclem8  46227  etransclem18  46237  etransclem20  46239  etransclem21  46240  etransclem23  46242  etransclem35  46254  etransclem46  46265  rrxtopnfi  46272  rrndistlt  46275  sge0gtfsumgt  46428  hoidmv1lelem2  46577  hoidmvlelem2  46581  smfmullem1  46776  sigarmf  46839  sigarms  46841  sigarexp  46844  sigardiv  46846  sigarcol  46849  sharhght  46850  sigaradd  46851  cevathlem2  46853  cevath  46854  resubcnnred  47292  fldivmod  47326  ceildivmod  47327  fmtnorec2lem  47530  fmtnorec3  47536  fmtnorec4  47537  lighneallem3  47595  quad1  47608  requad01  47609  requad2  47611  fppr2odd  47719  dignn0flhalflem2  48605  affinecomb2  48692  1subrec1sub  48694  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2vlinest  48730  rrx2linest  48731  line2  48741  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itschlc0xyqsol  48756  itsclc0xyqsolr  48758  2itscplem1  48767  2itscplem2  48768  2itscplem3  48769  itscnhlinecirc02plem1  48771  inlinecirc02plem  48775  sinhpcosh  49729  i2linesd  49768