Theorem subcld 11402

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

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7313  ℂcc 10939   − cmin 11275

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626  ax-resscn 10998  ax-1cn 10999  ax-icn 11000  ax-addcl 11001  ax-addrcl 11002  ax-mulcl 11003  ax-mulrcl 11004  ax-mulcom 11005  ax-addass 11006  ax-mulass 11007  ax-distr 11008  ax-i2m1 11009  ax-1ne0 11010  ax-1rid 11011  ax-rnegex 11012  ax-rrecex 11013  ax-cnre 11014  ax-pre-lttri 11015  ax-pre-lttrn 11016  ax-pre-ltadd 11017

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-opab 5148  df-mpt 5169  df-id 5505  df-po 5519  df-so 5520  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-res 5617  df-ima 5618  df-iota 6415  df-fun 6465  df-fn 6466  df-f 6467  df-f1 6468  df-fo 6469  df-f1o 6470  df-fv 6471  df-riota 7270  df-ov 7316  df-oprab 7317  df-mpo 7318  df-er 8544  df-en 8780  df-dom 8781  df-sdom 8782  df-pnf 11081  df-mnf 11082  df-ltxr 11084  df-sub 11277

This theorem is referenced by:  pnpncand  11466  muleqadd  11689  lineq  11882  modmuladdnn0  13705  hashfz  14211  hashfzo  14213  hashf1lem2  14239  hashf1  14240  ccatswrd  14450  pfxccatin12lem2  14513  crre  14894  remim  14897  remullem  14908  abs3lem  15119  caubnd2  15138  bhmafibid1cn  15244  bhmafibid2cn  15245  bhmafibid2  15247  rlimuni  15328  climuni  15330  rlimcld2  15356  rlimrege0  15357  rlimrecl  15358  mulcn2  15374  reccn2  15375  cn1lem  15376  o1sub  15394  rlimo1  15395  o1dif  15408  rlimsqzlem  15429  caucvgrlem2  15455  iseralt  15465  fsumparts  15587  cvgcmpce  15599  incexclem  15617  arisum2  15642  geoserg  15647  pwdif  15649  geo2sum2  15655  fallfacfwd  15815  binomfallfaclem2  15819  bpolycl  15831  bpoly3  15837  bpoly4  15838  fsumcube  15839  sinf  15902  tanval2  15911  tanval3  15912  sinneg  15924  efival  15930  sinhval  15932  bitsinv1lem  16217  bitsres  16249  pythagtriplem1  16584  pythagtriplem14  16596  pythagtriplem17  16599  dvdsprmpweqle  16654  4sqlem5  16710  mul4sqlem  16721  4sqlem17  16729  vdwlem5  16753  vdwlem6  16754  vdwlem8  16756  blcvx  24032  recld2  24048  addcnlem  24098  cnllycmp  24190  cphipval2  24476  4cphipval2  24477  cphipval  24478  ipcnlem2  24479  rrxmval  24640  rrxmetlem  24642  pjthlem1  24672  ovollb2lem  24723  itgcnlem  25025  dvlem  25131  dvconst  25152  dvid  25153  dvcnp2  25155  dvaddbr  25173  dvmulbr  25174  dvcobr  25181  dvcjbr  25184  dvrec  25190  dvmptim  25205  dvcnvlem  25211  dveflem  25214  dvsincos  25216  cmvth  25226  dvlip  25228  dvlipcn  25229  c1liplem1  25231  dveq0  25235  dv11cn  25236  dvle  25242  lhop1lem  25248  dvfsumabs  25258  dvfsumlem1  25261  dvfsumlem2  25262  dvfsumrlim  25266  dvfsumrlim2  25267  ftc1lem4  25274  ftc1lem5  25275  ftc2  25279  dgrcolem2  25506  plydiveu  25529  aaliou2b  25572  taylfvallem1  25587  taylply2  25598  dvtaylp  25600  dvntaylp  25601  taylthlem1  25603  taylthlem2  25604  ulmbdd  25628  ulmcn  25629  ulmdvlem1  25630  mtest  25634  iblulm  25637  itgulm  25638  abelthlem9  25670  ptolemy  25724  tangtx  25733  sineq0  25751  efeq1  25755  efif1olem4  25772  tanarg  25845  logcnlem3  25870  logcnlem4  25871  advlogexp  25881  efopn  25884  cxpcn3lem  25971  cxpeq  25981  ang180lem4  26033  ang180lem5  26034  ang180  26035  isosctrlem2  26040  isosctrlem3  26041  isosctr  26042  ssscongptld  26043  affineequiv  26044  affineequiv2  26045  affineequiv3  26046  affineequiv4  26047  affineequivne  26048  angpieqvdlem  26049  angpieqvdlem2  26050  angpined  26051  angpieqvd  26052  chordthmlem  26053  chordthmlem2  26054  chordthmlem3  26055  chordthmlem4  26056  chordthmlem5  26057  heron  26059  quad2  26060  quad  26061  dcubic1lem  26064  dcubic  26067  mcubic  26068  cubic2  26069  cubic  26070  dquartlem1  26072  dquartlem2  26073  dquart  26074  quart1cl  26075  quart1lem  26076  quart1  26077  quartlem2  26079  quartlem4  26081  quart  26082  atanf  26101  sinasin  26110  asinsin  26113  atanneg  26128  atancj  26131  efiatan  26133  atanlogsub  26137  efiatan2  26138  2efiatan  26139  atanbndlem  26146  dvatan  26156  atantayl  26158  lgamgulmlem2  26250  lgamgulmlem3  26251  lgamgulmlem5  26253  lgamgulmlem6  26254  lgamgulm2  26256  lgamucov  26258  lgamcvg2  26275  gamcvg  26276  gamcvg2lem  26279  ftalem2  26294  logfacrlim  26443  logexprlim  26444  lgsdirprm  26550  gausslemma2dlem1a  26584  gausslemma2dlem4  26588  2sqmod  26655  addsq2nreurex  26663  vmadivsum  26701  rpvmasumlem  26706  dchrisumlem2  26709  dchrisumlem3  26710  dchrmusum2  26713  dchrvmasumlem2  26717  dchrvmasumlem3  26718  dchrvmasumiflem1  26720  rpvmasum2  26731  dchrisum0lem1b  26734  dchrisum0lem1  26735  dchrisum0lem2a  26736  rplogsum  26746  mudivsum  26749  mulogsumlem  26750  mulogsum  26751  mulog2sumlem1  26753  mulog2sumlem2  26754  mulog2sumlem3  26755  vmalogdivsum2  26757  vmalogdivsum  26758  2vmadivsumlem  26759  selberglem1  26764  selberglem2  26765  selberg2lem  26769  selberg2  26770  selberg3lem1  26776  selberg4lem1  26779  selberg4  26780  pntrsumo1  26784  selberg3r  26788  selberg34r  26790  pntrlog2bndlem1  26796  pntrlog2bndlem2  26797  pntrlog2bndlem3  26798  pntrlog2bndlem4  26799  pntrlog2bndlem5  26800  pntibndlem2  26810  pntlemf  26824  pntlemo  26826  ttgcontlem1  27360  brbtwn2  27381  colinearalglem1  27382  colinearalglem2  27383  colinearalg  27386  axsegconlem1  27393  ax5seglem1  27404  ax5seglem2  27405  ax5seglem6  27410  ax5seglem9  27413  axlowdimlem17  27434  axcontlem7  27446  axcontlem8  27447  clwlkclwwlk  28474  clwwlknonex2lem1  28579  2clwwlk2clwwlk  28822  numclwwlk3lem1  28854  smcnlem  29167  ipval2  29177  4ipval2  29178  dipcj  29184  pjhthlem1  29861  lt2addrd  31182  bcm1n  31224  cycpmco2lem5  31505  cycpmco2lem6  31506  sqsscirc2  31965  signslema  32647  circlemeth  32726  logdivsqrle  32736  revpfxsfxrev  33183  revwlk  33192  subfaclim  33256  divcnvlin  33802  iprodgam  33812  dnicld1  34713  dnibndlem2  34720  dnibndlem3  34721  dnibndlem6  34724  dnibndlem9  34727  dnibndlem10  34728  dnibndlem11  34729  unblimceq0  34748  unbdqndv2lem1  34750  unbdqndv2lem2  34751  knoppndvlem11  34763  knoppndvlem15  34767  knoppndvlem17  34769  knoppndvlem21  34773  bj-bary1lem  35541  bj-bary1lem1  35542  bj-bary1  35543  ftc1cnnclem  35908  ftc1anclem7  35916  ftc1anclem8  35917  ftc1anc  35918  ftc2nc  35919  areacirclem1  35925  areacirclem4  35928  areacirc  35930  cntotbnd  36014  lcmineqlem8  40256  lcmineqlem10  40258  lcmineqlem11  40259  lcmineqlem12  40260  lcmineqlem23  40271  aks4d1p1  40296  sticksstones10  40326  sticksstones12a  40328  sticksstones12  40329  sticksstones22  40339  metakunt15  40354  metakunt16  40355  metakunt29  40368  metakunt30  40369  mvrrsubd  40513  lsubrotld  40516  lsubcom23d  40517  dffltz  40681  fltnltalem  40709  rencldnfilem  40852  pellexlem2  40862  pellexlem6  40866  pell1234qrne0  40885  pell1234qrmulcl  40887  rmyluc  40970  jm2.18  41021  jm2.19  41026  areaquad  41258  lhe4.4ex1a  42175  bcc0  42186  bccp1k  42187  bccm1k  42188  binomcxplemwb  42194  binomcxplemnn0  42195  binomcxplemrat  42196  binomcxplemfrat  42197  binomcxplemdvbinom  42199  binomcxplemnotnn0  42202  isosctrlem1ALT  42782  sineq0ALT  42785  oddfl  43059  dstregt0  43063  subadd4b  43064  sub31  43072  fzisoeu  43082  absnpncan2d  43084  absnpncan3d  43089  supxrgelem  43119  absimlere  43263  mullimc  43401  ellimcabssub0  43402  mullimcf  43408  limcrecl  43414  lptre2pt  43425  limcleqr  43429  neglimc  43432  addlimc  43433  0ellimcdiv  43434  limclner  43436  reclimc  43438  climleltrp  43461  climisp  43531  climxrrelem  43534  climxrre  43535  cnrefiisplem  43614  climxlim2lem  43630  fprodsubrecnncnvlem  43692  fperdvper  43704  dvdivbd  43708  dvbdfbdioolem2  43714  ioodvbdlimc1lem1  43716  volioc  43757  volico  43768  stoweidlem1  43786  stoweidlem11  43796  stoweidlem13  43798  stoweidlem26  43811  stoweid  43848  wallispi  43855  wallispi2lem1  43856  wallispi2lem2  43857  wallispi2  43858  stirlinglem1  43859  stirlinglem4  43862  stirlinglem5  43863  stirlinglem7  43865  stirlinglem11  43869  dirkertrigeqlem2  43884  fourierdlem4  43896  fourierdlem26  43918  fourierdlem30  43922  fourierdlem42  43934  fourierdlem63  43954  fourierdlem65  43956  fourierdlem72  43963  fourierdlem74  43965  fourierdlem75  43966  fourierdlem76  43967  fourierdlem80  43971  fourierdlem81  43972  fourierdlem89  43980  fourierdlem90  43981  fourierdlem91  43982  fourierdlem107  43998  fourierdlem109  44000  fouriersw  44016  etransclem1  44020  etransclem4  44023  etransclem8  44027  etransclem18  44037  etransclem20  44039  etransclem21  44040  etransclem23  44042  etransclem35  44054  etransclem46  44065  rrxtopnfi  44072  rrndistlt  44075  sge0gtfsumgt  44226  hoidmv1lelem2  44375  hoidmvlelem2  44379  smfmullem1  44574  sigarmf  44629  sigarms  44631  sigarexp  44634  sigardiv  44636  sigarcol  44639  sharhght  44640  sigaradd  44641  cevathlem2  44643  cevath  44644  resubcnnred  45055  fmtnorec2lem  45253  fmtnorec3  45259  fmtnorec4  45260  lighneallem3  45318  quad1  45331  requad01  45332  requad2  45334  fppr2odd  45442  fldivmod  46123  dignn0flhalflem2  46221  affinecomb2  46308  1subrec1sub  46310  eenglngeehlnmlem1  46342  eenglngeehlnmlem2  46343  rrx2vlinest  46346  rrx2linest  46347  line2  46357  itsclc0yqsollem1  46367  itsclc0yqsol  46369  itscnhlc0xyqsol  46370  itschlc0xyqsol1  46371  itschlc0xyqsol  46372  itsclc0xyqsolr  46374  2itscplem1  46383  2itscplem2  46384  2itscplem3  46385  itscnhlinecirc02plem1  46387  inlinecirc02plem  46391  sinhpcosh  46701  i2linesd  46742