Theorem subcld 10271

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

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   − cmin 10145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-ltxr 9958  df-sub 10147

This theorem is referenced by:  pnpncand  10331  subdir2d  10367  muleqadd  10550  modmuladdnn0  12576  hashfz  13074  hashfzo  13076  hashf1lem2  13097  hashf1  13098  ccatswrd  13308  crre  13702  remim  13705  remullem  13716  abs3lem  13926  caubnd2  13945  rlimuni  14129  climuni  14131  rlimcld2  14157  rlimrege0  14158  rlimrecl  14159  mulcn2  14174  reccn2  14175  cn1lem  14176  o1sub  14194  rlimo1  14195  o1dif  14208  rlimsqzlem  14227  caucvgrlem2  14253  iseralt  14263  fsumparts  14379  cvgcmpce  14391  incexclem  14407  arisum2  14432  geoserg  14437  geo2sum2  14444  fallfacfwd  14606  binomfallfaclem2  14610  bpolycl  14622  bpoly3  14628  bpoly4  14629  fsumcube  14630  sinf  14693  tanval2  14702  tanval3  14703  sinneg  14715  efival  14721  sinhval  14723  bitsinv1lem  15001  bitsres  15033  pythagtriplem1  15359  pythagtriplem14  15371  pythagtriplem17  15374  dvdsprmpweqle  15428  4sqlem5  15484  mul4sqlem  15495  4sqlem17  15503  vdwlem5  15527  vdwlem6  15528  vdwlem8  15530  blcvx  22409  recld2  22425  addcnlem  22475  cnllycmp  22563  cphipval2  22848  4cphipval2  22849  cphipval  22850  ipcnlem2  22851  rrxmval  22996  rrxmetlem  22998  pjthlem1  23016  ovollb2lem  23063  itgcnlem  23362  dvlem  23466  dvconst  23486  dvid  23487  dvcnp2  23489  dvaddbr  23507  dvmulbr  23508  dvcobr  23515  dvcjbr  23518  dvrec  23524  dvmptim  23539  dvcnvlem  23543  dveflem  23546  dvsincos  23548  cmvth  23558  dvlip  23560  dvlipcn  23561  c1liplem1  23563  dveq0  23567  dv11cn  23568  dvle  23574  lhop1lem  23580  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem2  23594  dvfsumrlim  23598  dvfsumrlim2  23599  ftc1lem4  23606  ftc1lem5  23607  ftc2  23611  dgrcolem2  23834  plydiveu  23857  aaliou2b  23900  taylfvallem1  23915  taylply2  23926  dvtaylp  23928  dvntaylp  23929  taylthlem1  23931  taylthlem2  23932  ulmbdd  23956  ulmcn  23957  ulmdvlem1  23958  mtest  23962  iblulm  23965  itgulm  23966  abelthlem9  23998  ptolemy  24052  tangtx  24061  sineq0  24077  efeq1  24079  efif1olem4  24095  tanarg  24169  logcnlem3  24190  logcnlem4  24191  advlogexp  24201  efopn  24204  cxpcn3lem  24288  cxpeq  24298  ang180lem4  24342  ang180lem5  24343  ang180  24344  isosctrlem2  24349  isosctrlem3  24350  isosctr  24351  ssscongptld  24352  affineequiv  24353  affineequiv2  24354  angpieqvdlem  24355  angpieqvdlem2  24356  angpined  24357  angpieqvd  24358  chordthmlem  24359  chordthmlem2  24360  chordthmlem3  24361  chordthmlem4  24362  chordthmlem5  24363  heron  24365  quad2  24366  quad  24367  dcubic1lem  24370  dcubic  24373  mcubic  24374  cubic2  24375  cubic  24376  dquartlem1  24378  dquartlem2  24379  dquart  24380  quart1cl  24381  quart1lem  24382  quart1  24383  quartlem2  24385  quartlem4  24387  quart  24388  atanf  24407  sinasin  24416  asinsin  24419  atanneg  24434  atancj  24437  efiatan  24439  atanlogsub  24443  efiatan2  24444  2efiatan  24445  atanbndlem  24452  dvatan  24462  atantayl  24464  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgamucov  24564  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  ftalem2  24600  logfacrlim  24749  logexprlim  24750  lgsdirprm  24856  gausslemma2dlem1a  24890  gausslemma2dlem4  24894  vmadivsum  24971  rpvmasumlem  24976  dchrisumlem2  24979  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrvmasumiflem1  24990  rpvmasum2  25001  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0lem2a  25006  rplogsum  25016  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  mulog2sumlem1  25023  mulog2sumlem2  25024  mulog2sumlem3  25025  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  selberglem1  25034  selberglem2  25035  selberg2lem  25039  selberg2  25040  selberg3lem1  25046  selberg4lem1  25049  selberg4  25050  pntrsumo1  25054  selberg3r  25058  selberg34r  25060  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntibndlem2  25080  pntlemf  25094  pntlemo  25096  ttgcontlem1  25565  brbtwn2  25585  colinearalglem1  25586  colinearalglem2  25587  colinearalg  25590  axsegconlem1  25597  ax5seglem2  25609  ax5seglem6  25614  ax5seglem9  25617  axlowdimlem17  25638  axcontlem7  25650  axcontlem8  25651  cusgrasizeinds  26004  clwlkisclwwlk  26317  frghash2spot  26590  usgreghash2spotv  26593  frgregordn0  26597  numclwlk3lem3  26600  numclwlk1lem2fo  26622  smcnlem  26936  ipval2  26946  4ipval2  26947  dipcj  26953  pjhthlem1  27634  lt2addrd  28903  bcm1n  28941  bhmafibid2  28976  2sqmod  28979  sqsscirc2  29283  signslema  29965  subfaclim  30424  divcnvlin  30871  iprodgam  30881  dnicld1  31632  dnibndlem2  31639  dnibndlem3  31640  dnibndlem6  31643  dnibndlem9  31646  dnibndlem10  31647  dnibndlem11  31648  unblimceq0  31668  unbdqndv2lem1  31670  unbdqndv2lem2  31671  knoppndvlem11  31683  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem21  31693  bj-lineq  32335  bj-bary1lem  32337  bj-bary1lem1  32338  bj-bary1  32339  ftc1cnnclem  32653  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  ftc2nc  32664  areacirclem1  32670  areacirclem4  32673  areacirc  32675  cntotbnd  32765  rencldnfilem  36402  pellexlem2  36412  pellexlem6  36416  pell1234qrne0  36435  pell1234qrmulcl  36437  rmyluc  36520  jm2.18  36573  jm2.19  36578  areaquad  36821  lhe4.4ex1a  37550  bcc0  37561  bccp1k  37562  bccm1k  37563  binomcxplemwb  37569  binomcxplemnn0  37570  binomcxplemrat  37571  binomcxplemfrat  37572  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  isosctrlem1ALT  38192  sineq0ALT  38195  oddfl  38430  dstregt0  38434  subadd4b  38435  sub31  38444  fzisoeu  38455  absnpncan2d  38457  absnpncan3d  38462  supxrgelem  38494  mullimc  38683  ellimcabssub0  38684  mullimcf  38690  limcrecl  38696  lptre2pt  38707  limcleqr  38711  neglimc  38714  addlimc  38715  0ellimcdiv  38716  limclner  38718  reclimc  38720  climleltrp  38743  fprodsubrecnncnvlem  38794  fperdvper  38808  dvdivbd  38813  dvbdfbdioolem2  38819  ioodvbdlimc1lem1  38821  volioc  38864  volico  38876  stoweidlem1  38894  stoweidlem11  38904  stoweidlem13  38906  stoweidlem26  38919  stoweid  38956  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  wallispi2  38966  stirlinglem1  38967  stirlinglem4  38970  stirlinglem5  38971  stirlinglem7  38973  stirlinglem11  38977  dirkertrigeqlem2  38992  fourierdlem4  39004  fourierdlem26  39026  fourierdlem30  39030  fourierdlem42  39042  fourierdlem63  39062  fourierdlem65  39064  fourierdlem72  39071  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem80  39079  fourierdlem81  39080  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem107  39106  fourierdlem109  39108  fouriersw  39124  etransclem1  39128  etransclem4  39131  etransclem8  39135  etransclem18  39145  etransclem20  39147  etransclem21  39148  etransclem23  39150  etransclem35  39162  etransclem46  39173  rrxtopnfi  39182  rrndistlt  39186  sge0gtfsumgt  39336  hoidmv1lelem2  39482  hoidmvlelem2  39486  smfmullem1  39676  sigarmf  39692  sigarms  39694  sigarexp  39697  sigardiv  39699  sigarcol  39702  sharhght  39703  sigaradd  39704  cevathlem2  39706  cevath  39707  fmtnorec2lem  39992  fmtnorec3  39998  fmtnorec4  39999  pwdif  40039  lighneallem3  40062  pfxccatin12lem2  40287  clwlkclwwlk  41211  frgrhash2wsp  41497  fusgreghash2wspv  41499  frrusgrord0  41503  av-numclwlk3lem3  41506  av-numclwlk1lem2fo  41525  fldivmod  42107  dignn0flhalflem2  42208  sinhpcosh  42280  i2linesd  42334