Theorem subcld 10687

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

Syntax hints:   → wi 4   ∈ wcel 2157  (class class class)co 6884  ℂcc 10229   − cmin 10561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-po 5245  df-so 5246  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-er 7989  df-en 8203  df-dom 8204  df-sdom 8205  df-pnf 10371  df-mnf 10372  df-ltxr 10374  df-sub 10563

This theorem is referenced by:  pnpncand  10747  subdir2d  10783  muleqadd  10966  modmuladdnn0  12958  hashfz  13451  hashfzo  13453  hashf1lem2  13477  hashf1  13478  ccatswrd  13700  crre  14097  remim  14100  remullem  14111  abs3lem  14321  caubnd2  14340  rlimuni  14524  climuni  14526  rlimcld2  14552  rlimrege0  14553  rlimrecl  14554  mulcn2  14569  reccn2  14570  cn1lem  14571  o1sub  14589  rlimo1  14590  o1dif  14603  rlimsqzlem  14622  caucvgrlem2  14648  iseralt  14658  fsumparts  14780  cvgcmpce  14792  incexclem  14810  arisum2  14835  geoserg  14840  geo2sum2  14847  fallfacfwd  15007  binomfallfaclem2  15011  bpolycl  15023  bpoly3  15029  bpoly4  15030  fsumcube  15031  sinf  15094  tanval2  15103  tanval3  15104  sinneg  15116  efival  15122  sinhval  15124  bitsinv1lem  15402  bitsres  15434  pythagtriplem1  15758  pythagtriplem14  15770  pythagtriplem17  15773  dvdsprmpweqle  15827  4sqlem5  15883  mul4sqlem  15894  4sqlem17  15902  vdwlem5  15926  vdwlem6  15927  vdwlem8  15929  blcvx  22835  recld2  22851  addcnlem  22901  cnllycmp  22989  cphipval2  23273  4cphipval2  23274  cphipval  23275  ipcnlem2  23276  rrxmval  23423  rrxmetlem  23425  pjthlem1  23443  ovollb2lem  23492  itgcnlem  23793  dvlem  23897  dvconst  23917  dvid  23918  dvcnp2  23920  dvaddbr  23938  dvmulbr  23939  dvcobr  23946  dvcjbr  23949  dvrec  23955  dvmptim  23970  dvcnvlem  23976  dveflem  23979  dvsincos  23981  cmvth  23991  dvlip  23993  dvlipcn  23994  c1liplem1  23996  dveq0  24000  dv11cn  24001  dvle  24007  lhop1lem  24013  dvfsumabs  24023  dvfsumlem1  24026  dvfsumlem2  24027  dvfsumrlim  24031  dvfsumrlim2  24032  ftc1lem4  24039  ftc1lem5  24040  ftc2  24044  dgrcolem2  24267  plydiveu  24290  aaliou2b  24333  taylfvallem1  24348  taylply2  24359  dvtaylp  24361  dvntaylp  24362  taylthlem1  24364  taylthlem2  24365  ulmbdd  24389  ulmcn  24390  ulmdvlem1  24391  mtest  24395  iblulm  24398  itgulm  24399  abelthlem9  24431  ptolemy  24486  tangtx  24495  sineq0  24511  efeq1  24513  efif1olem4  24529  tanarg  24602  logcnlem3  24627  logcnlem4  24628  advlogexp  24638  efopn  24641  cxpcn3lem  24725  cxpeq  24735  ang180lem4  24779  ang180lem5  24780  ang180  24781  isosctrlem2  24786  isosctrlem3  24787  isosctr  24788  ssscongptld  24789  affineequiv  24790  affineequiv2  24791  angpieqvdlem  24792  angpieqvdlem2  24793  angpined  24794  angpieqvd  24795  chordthmlem  24796  chordthmlem2  24797  chordthmlem3  24798  chordthmlem4  24799  chordthmlem5  24800  heron  24802  quad2  24803  quad  24804  dcubic1lem  24807  dcubic  24810  mcubic  24811  cubic2  24812  cubic  24813  dquartlem1  24815  dquartlem2  24816  dquart  24817  quart1cl  24818  quart1lem  24819  quart1  24820  quartlem2  24822  quartlem4  24824  quart  24825  atanf  24844  sinasin  24853  asinsin  24856  atanneg  24871  atancj  24874  efiatan  24876  atanlogsub  24880  efiatan2  24881  2efiatan  24882  atanbndlem  24889  dvatan  24899  atantayl  24901  lgamgulmlem2  24993  lgamgulmlem3  24994  lgamgulmlem5  24996  lgamgulmlem6  24997  lgamgulm2  24999  lgamucov  25001  lgamcvg2  25018  gamcvg  25019  gamcvg2lem  25022  ftalem2  25037  logfacrlim  25186  logexprlim  25187  lgsdirprm  25293  gausslemma2dlem1a  25327  gausslemma2dlem4  25331  vmadivsum  25408  rpvmasumlem  25413  dchrisumlem2  25416  dchrisumlem3  25417  dchrmusum2  25420  dchrvmasumlem2  25424  dchrvmasumlem3  25425  dchrvmasumiflem1  25427  rpvmasum2  25438  dchrisum0lem1b  25441  dchrisum0lem1  25442  dchrisum0lem2a  25443  rplogsum  25453  mudivsum  25456  mulogsumlem  25457  mulogsum  25458  mulog2sumlem1  25460  mulog2sumlem2  25461  mulog2sumlem3  25462  vmalogdivsum2  25464  vmalogdivsum  25465  2vmadivsumlem  25466  selberglem1  25471  selberglem2  25472  selberg2lem  25476  selberg2  25477  selberg3lem1  25483  selberg4lem1  25486  selberg4  25487  pntrsumo1  25491  selberg3r  25495  selberg34r  25497  pntrlog2bndlem1  25503  pntrlog2bndlem2  25504  pntrlog2bndlem3  25505  pntrlog2bndlem4  25506  pntrlog2bndlem5  25507  pntibndlem2  25517  pntlemf  25531  pntlemo  25533  ttgcontlem1  26002  brbtwn2  26022  colinearalglem1  26023  colinearalglem2  26024  colinearalg  26027  axsegconlem1  26034  ax5seglem2  26046  ax5seglem6  26051  ax5seglem9  26054  axlowdimlem17  26075  axcontlem7  26087  axcontlem8  26088  clwlkclwwlk  27168  clwwlknonex2lem1  27299  2clwwlk2clwwlk  27550  numclwwlk3lem1  27593  smcnlem  27903  ipval2  27913  4ipval2  27914  dipcj  27920  pjhthlem1  28601  lt2addrd  29866  bcm1n  29904  bhmafibid2  29993  2sqmod  29996  sqsscirc2  30303  signslema  30987  circlemeth  31066  logdivsqrle  31076  subfaclim  31515  divcnvlin  31962  iprodgam  31972  dnicld1  32801  dnibndlem2  32808  dnibndlem3  32809  dnibndlem6  32812  dnibndlem9  32815  dnibndlem10  32816  dnibndlem11  32817  unblimceq0  32837  unbdqndv2lem1  32839  unbdqndv2lem2  32840  knoppndvlem11  32852  knoppndvlem15  32856  knoppndvlem17  32858  knoppndvlem21  32862  bj-lineq  33494  bj-bary1lem  33496  bj-bary1lem1  33497  bj-bary1  33498  ftc1cnnclem  33814  ftc1anclem7  33822  ftc1anclem8  33823  ftc1anc  33824  ftc2nc  33825  areacirclem1  33831  areacirclem4  33834  areacirc  33836  cntotbnd  33925  rencldnfilem  37904  pellexlem2  37914  pellexlem6  37918  pell1234qrne0  37937  pell1234qrmulcl  37939  rmyluc  38021  jm2.18  38074  jm2.19  38079  areaquad  38320  lhe4.4ex1a  39046  bcc0  39057  bccp1k  39058  bccm1k  39059  binomcxplemwb  39065  binomcxplemnn0  39066  binomcxplemrat  39067  binomcxplemfrat  39068  binomcxplemdvbinom  39070  binomcxplemnotnn0  39073  isosctrlem1ALT  39682  sineq0ALT  39685  oddfl  39989  dstregt0  39993  subadd4b  39994  sub31  40003  fzisoeu  40013  absnpncan2d  40015  absnpncan3d  40020  supxrgelem  40051  absimlere  40207  mullimc  40346  ellimcabssub0  40347  mullimcf  40353  limcrecl  40359  lptre2pt  40370  limcleqr  40374  neglimc  40377  addlimc  40378  0ellimcdiv  40379  limclner  40381  reclimc  40383  climleltrp  40406  climisp  40476  climxrrelem  40479  climxrre  40480  cnrefiisplem  40553  climxlim2lem  40569  fprodsubrecnncnvlem  40619  fperdvper  40631  dvdivbd  40636  dvbdfbdioolem2  40642  ioodvbdlimc1lem1  40644  volioc  40685  volico  40697  stoweidlem1  40715  stoweidlem11  40725  stoweidlem13  40727  stoweidlem26  40740  stoweid  40777  wallispi  40784  wallispi2lem1  40785  wallispi2lem2  40786  wallispi2  40787  stirlinglem1  40788  stirlinglem4  40791  stirlinglem5  40792  stirlinglem7  40794  stirlinglem11  40798  dirkertrigeqlem2  40813  fourierdlem4  40825  fourierdlem26  40847  fourierdlem30  40851  fourierdlem42  40863  fourierdlem63  40883  fourierdlem65  40885  fourierdlem72  40892  fourierdlem74  40894  fourierdlem75  40895  fourierdlem76  40896  fourierdlem80  40900  fourierdlem81  40901  fourierdlem89  40909  fourierdlem90  40910  fourierdlem91  40911  fourierdlem107  40927  fourierdlem109  40929  fouriersw  40945  etransclem1  40949  etransclem4  40952  etransclem8  40956  etransclem18  40966  etransclem20  40968  etransclem21  40969  etransclem23  40971  etransclem35  40983  etransclem46  40994  rrxtopnfi  41003  rrndistlt  41007  sge0gtfsumgt  41157  hoidmv1lelem2  41306  hoidmvlelem2  41310  smfmullem1  41498  sigarmf  41543  sigarms  41545  sigarexp  41548  sigardiv  41550  sigarcol  41553  sharhght  41554  sigaradd  41555  cevathlem2  41557  cevath  41558  pfxccatin12lem2  42017  fmtnorec2lem  42047  fmtnorec3  42053  fmtnorec4  42054  pwdif  42094  lighneallem3  42117  fldivmod  42899  dignn0flhalflem2  42996  sinhpcosh  43070  i2linesd  43114