Theorem subcld 11154

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

Syntax hints:   → wi 4   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692   − cmin 11027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-po 5453  df-so 5454  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-ltxr 10837  df-sub 11029

This theorem is referenced by:  pnpncand  11218  muleqadd  11441  lineq  11634  modmuladdnn0  13453  hashfz  13959  hashfzo  13961  hashf1lem2  13987  hashf1  13988  ccatswrd  14198  pfxccatin12lem2  14261  crre  14642  remim  14645  remullem  14656  abs3lem  14867  caubnd2  14886  bhmafibid1cn  14992  bhmafibid2cn  14993  bhmafibid2  14995  rlimuni  15076  climuni  15078  rlimcld2  15104  rlimrege0  15105  rlimrecl  15106  mulcn2  15122  reccn2  15123  cn1lem  15124  o1sub  15142  rlimo1  15143  o1dif  15156  rlimsqzlem  15177  caucvgrlem2  15203  iseralt  15213  fsumparts  15333  cvgcmpce  15345  incexclem  15363  arisum2  15388  geoserg  15393  pwdif  15395  geo2sum2  15401  fallfacfwd  15561  binomfallfaclem2  15565  bpolycl  15577  bpoly3  15583  bpoly4  15584  fsumcube  15585  sinf  15648  tanval2  15657  tanval3  15658  sinneg  15670  efival  15676  sinhval  15678  bitsinv1lem  15963  bitsres  15995  pythagtriplem1  16332  pythagtriplem14  16344  pythagtriplem17  16347  dvdsprmpweqle  16402  4sqlem5  16458  mul4sqlem  16469  4sqlem17  16477  vdwlem5  16501  vdwlem6  16502  vdwlem8  16504  blcvx  23649  recld2  23665  addcnlem  23715  cnllycmp  23807  cphipval2  24092  4cphipval2  24093  cphipval  24094  ipcnlem2  24095  rrxmval  24256  rrxmetlem  24258  pjthlem1  24288  ovollb2lem  24339  itgcnlem  24641  dvlem  24747  dvconst  24768  dvid  24769  dvcnp2  24771  dvaddbr  24789  dvmulbr  24790  dvcobr  24797  dvcjbr  24800  dvrec  24806  dvmptim  24821  dvcnvlem  24827  dveflem  24830  dvsincos  24832  cmvth  24842  dvlip  24844  dvlipcn  24845  c1liplem1  24847  dveq0  24851  dv11cn  24852  dvle  24858  lhop1lem  24864  dvfsumabs  24874  dvfsumlem1  24877  dvfsumlem2  24878  dvfsumrlim  24882  dvfsumrlim2  24883  ftc1lem4  24890  ftc1lem5  24891  ftc2  24895  dgrcolem2  25122  plydiveu  25145  aaliou2b  25188  taylfvallem1  25203  taylply2  25214  dvtaylp  25216  dvntaylp  25217  taylthlem1  25219  taylthlem2  25220  ulmbdd  25244  ulmcn  25245  ulmdvlem1  25246  mtest  25250  iblulm  25253  itgulm  25254  abelthlem9  25286  ptolemy  25340  tangtx  25349  sineq0  25367  efeq1  25371  efif1olem4  25388  tanarg  25461  logcnlem3  25486  logcnlem4  25487  advlogexp  25497  efopn  25500  cxpcn3lem  25587  cxpeq  25597  ang180lem4  25649  ang180lem5  25650  ang180  25651  isosctrlem2  25656  isosctrlem3  25657  isosctr  25658  ssscongptld  25659  affineequiv  25660  affineequiv2  25661  affineequiv3  25662  affineequiv4  25663  affineequivne  25664  angpieqvdlem  25665  angpieqvdlem2  25666  angpined  25667  angpieqvd  25668  chordthmlem  25669  chordthmlem2  25670  chordthmlem3  25671  chordthmlem4  25672  chordthmlem5  25673  heron  25675  quad2  25676  quad  25677  dcubic1lem  25680  dcubic  25683  mcubic  25684  cubic2  25685  cubic  25686  dquartlem1  25688  dquartlem2  25689  dquart  25690  quart1cl  25691  quart1lem  25692  quart1  25693  quartlem2  25695  quartlem4  25697  quart  25698  atanf  25717  sinasin  25726  asinsin  25729  atanneg  25744  atancj  25747  efiatan  25749  atanlogsub  25753  efiatan2  25754  2efiatan  25755  atanbndlem  25762  dvatan  25772  atantayl  25774  lgamgulmlem2  25866  lgamgulmlem3  25867  lgamgulmlem5  25869  lgamgulmlem6  25870  lgamgulm2  25872  lgamucov  25874  lgamcvg2  25891  gamcvg  25892  gamcvg2lem  25895  ftalem2  25910  logfacrlim  26059  logexprlim  26060  lgsdirprm  26166  gausslemma2dlem1a  26200  gausslemma2dlem4  26204  2sqmod  26271  addsq2nreurex  26279  vmadivsum  26317  rpvmasumlem  26322  dchrisumlem2  26325  dchrisumlem3  26326  dchrmusum2  26329  dchrvmasumlem2  26333  dchrvmasumlem3  26334  dchrvmasumiflem1  26336  rpvmasum2  26347  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2a  26352  rplogsum  26362  mudivsum  26365  mulogsumlem  26366  mulogsum  26367  mulog2sumlem1  26369  mulog2sumlem2  26370  mulog2sumlem3  26371  vmalogdivsum2  26373  vmalogdivsum  26374  2vmadivsumlem  26375  selberglem1  26380  selberglem2  26381  selberg2lem  26385  selberg2  26386  selberg3lem1  26392  selberg4lem1  26395  selberg4  26396  pntrsumo1  26400  selberg3r  26404  selberg34r  26406  pntrlog2bndlem1  26412  pntrlog2bndlem2  26413  pntrlog2bndlem3  26414  pntrlog2bndlem4  26415  pntrlog2bndlem5  26416  pntibndlem2  26426  pntlemf  26440  pntlemo  26442  ttgcontlem1  26930  brbtwn2  26950  colinearalglem1  26951  colinearalglem2  26952  colinearalg  26955  axsegconlem1  26962  ax5seglem1  26973  ax5seglem2  26974  ax5seglem6  26979  ax5seglem9  26982  axlowdimlem17  27003  axcontlem7  27015  axcontlem8  27016  clwlkclwwlk  28039  clwwlknonex2lem1  28144  2clwwlk2clwwlk  28387  numclwwlk3lem1  28419  smcnlem  28732  ipval2  28742  4ipval2  28743  dipcj  28749  pjhthlem1  29426  lt2addrd  30748  bcm1n  30790  cycpmco2lem5  31070  cycpmco2lem6  31071  sqsscirc2  31527  signslema  32207  circlemeth  32286  logdivsqrle  32296  revpfxsfxrev  32744  revwlk  32753  subfaclim  32817  divcnvlin  33367  iprodgam  33377  dnicld1  34338  dnibndlem2  34345  dnibndlem3  34346  dnibndlem6  34349  dnibndlem9  34352  dnibndlem10  34353  dnibndlem11  34354  unblimceq0  34373  unbdqndv2lem1  34375  unbdqndv2lem2  34376  knoppndvlem11  34388  knoppndvlem15  34392  knoppndvlem17  34394  knoppndvlem21  34398  bj-bary1lem  35164  bj-bary1lem1  35165  bj-bary1  35166  ftc1cnnclem  35534  ftc1anclem7  35542  ftc1anclem8  35543  ftc1anc  35544  ftc2nc  35545  areacirclem1  35551  areacirclem4  35554  areacirc  35556  cntotbnd  35640  lcmineqlem8  39727  lcmineqlem10  39729  lcmineqlem11  39730  lcmineqlem12  39731  lcmineqlem23  39742  aks4d1p1  39766  sticksstones10  39780  sticksstones12a  39782  sticksstones12  39783  metakunt15  39802  metakunt16  39803  metakunt29  39816  metakunt30  39817  mvrrsubd  39951  lsubrotld  39954  lsubcom23d  39955  dffltz  40115  fltnltalem  40143  rencldnfilem  40286  pellexlem2  40296  pellexlem6  40300  pell1234qrne0  40319  pell1234qrmulcl  40321  rmyluc  40403  jm2.18  40454  jm2.19  40459  areaquad  40691  lhe4.4ex1a  41561  bcc0  41572  bccp1k  41573  bccm1k  41574  binomcxplemwb  41580  binomcxplemnn0  41581  binomcxplemrat  41582  binomcxplemfrat  41583  binomcxplemdvbinom  41585  binomcxplemnotnn0  41588  isosctrlem1ALT  42168  sineq0ALT  42171  oddfl  42429  dstregt0  42433  subadd4b  42434  sub31  42443  fzisoeu  42453  absnpncan2d  42455  absnpncan3d  42460  supxrgelem  42490  absimlere  42636  mullimc  42775  ellimcabssub0  42776  mullimcf  42782  limcrecl  42788  lptre2pt  42799  limcleqr  42803  neglimc  42806  addlimc  42807  0ellimcdiv  42808  limclner  42810  reclimc  42812  climleltrp  42835  climisp  42905  climxrrelem  42908  climxrre  42909  cnrefiisplem  42988  climxlim2lem  43004  fprodsubrecnncnvlem  43066  fperdvper  43078  dvdivbd  43082  dvbdfbdioolem2  43088  ioodvbdlimc1lem1  43090  volioc  43131  volico  43142  stoweidlem1  43160  stoweidlem11  43170  stoweidlem13  43172  stoweidlem26  43185  stoweid  43222  wallispi  43229  wallispi2lem1  43230  wallispi2lem2  43231  wallispi2  43232  stirlinglem1  43233  stirlinglem4  43236  stirlinglem5  43237  stirlinglem7  43239  stirlinglem11  43243  dirkertrigeqlem2  43258  fourierdlem4  43270  fourierdlem26  43292  fourierdlem30  43296  fourierdlem42  43308  fourierdlem63  43328  fourierdlem65  43330  fourierdlem72  43337  fourierdlem74  43339  fourierdlem75  43340  fourierdlem76  43341  fourierdlem80  43345  fourierdlem81  43346  fourierdlem89  43354  fourierdlem90  43355  fourierdlem91  43356  fourierdlem107  43372  fourierdlem109  43374  fouriersw  43390  etransclem1  43394  etransclem4  43397  etransclem8  43401  etransclem18  43411  etransclem20  43413  etransclem21  43414  etransclem23  43416  etransclem35  43428  etransclem46  43439  rrxtopnfi  43446  rrndistlt  43449  sge0gtfsumgt  43599  hoidmv1lelem2  43748  hoidmvlelem2  43752  smfmullem1  43940  sigarmf  43985  sigarms  43987  sigarexp  43990  sigardiv  43992  sigarcol  43995  sharhght  43996  sigaradd  43997  cevathlem2  43999  cevath  44000  resubcnnred  44412  fmtnorec2lem  44610  fmtnorec3  44616  fmtnorec4  44617  lighneallem3  44675  quad1  44688  requad01  44689  requad2  44691  fppr2odd  44799  fldivmod  45480  dignn0flhalflem2  45578  affinecomb2  45665  1subrec1sub  45667  eenglngeehlnmlem1  45699  eenglngeehlnmlem2  45700  rrx2vlinest  45703  rrx2linest  45704  line2  45714  itsclc0yqsollem1  45724  itsclc0yqsol  45726  itscnhlc0xyqsol  45727  itschlc0xyqsol1  45728  itschlc0xyqsol  45729  itsclc0xyqsolr  45731  2itscplem1  45740  2itscplem2  45741  2itscplem3  45742  itscnhlinecirc02plem1  45744  inlinecirc02plem  45748  sinhpcosh  46056  i2linesd  46097