Theorem subcld 11594

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7414  ℂcc 11123   − cmin 11466

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-er 8697  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11270  df-mnf 11271  df-ltxr 11273  df-sub 11468

This theorem is used by:  subsubadd23  11646  addsubsub23  11647  pnpncand  11660  muleqadd  11883  lineq  12077  modmuladdnn0  13980  hashfz  14493  hashfzo  14495  hashf1lem2  14522  hashf1  14523  ccatswrd  14739  pfxccatin12lem2  14801  revpfxsfxrev  14838  crre  15202  remim  15205  remullem  15216  abs3lem  15427  caubnd2  15446  bhmafibid1cn  15554  bhmafibid2cn  15555  bhmafibid2  15557  rlimuni  15638  climuni  15640  rlimcld2  15666  rlimrege0  15667  rlimrecl  15668  mulcn2  15684  reccn2  15685  cn1lem  15686  o1sub  15704  rlimo1  15705  o1dif  15718  rlimsqzlem  15737  caucvgrlem2  15763  iseralt  15773  fsumparts  15894  cvgcmpce  15906  incexclem  15926  arisum2  15951  geoserg  15956  pwdif  15958  geo2sum2  15964  fallfacfwd  16123  binomfallfaclem2  16127  bpolycl  16139  bpoly3  16145  bpoly4  16146  fsumcube  16147  sinf  16213  tanval2  16222  tanval3  16223  sinneg  16235  efival  16241  sinhval  16243  bitsinv1lem  16532  bitsres  16564  pythagtriplem1  16909  pythagtriplem14  16921  pythagtriplem17  16924  dvdsprmpweqle  16979  4sqlem5  17035  mul4sqlem  17046  4sqlem17  17054  vdwlem5  17078  vdwlem6  17079  vdwlem8  17081  blcvx  25025  recld2  25042  addcnlem  25092  cnllycmp  25185  cphipval2  25470  4cphipval2  25471  cphipval  25472  ipcnlem2  25473  rrxmval  25634  rrxmetlem  25636  pjthlem1  25666  ovollb2lem  25717  itgcnlem  26018  dvlem  26124  dvconst  26145  dvid  26146  dvcnp2  26148  dvaddbr  26166  dvmulbr  26167  dvcobr  26174  dvcjbr  26177  dvrec  26183  dvmptim  26198  dvcnvlem  26204  dveflem  26207  dvsincos  26209  cmvth  26219  dvlip  26221  dvlipcn  26222  c1liplem1  26224  dveq0  26228  dv11cn  26229  dvle  26235  lhop1lem  26241  dvfsumabs  26251  dvfsumlem1  26254  dvfsumlem2  26255  dvfsumrlim  26259  dvfsumrlim2  26260  ftc1lem4  26267  ftc1lem5  26268  ftc2  26272  dgrcolem2  26501  plydiveu  26529  aaliou2b  26578  taylfvallem1  26594  taylply2  26605  dvtaylp  26607  dvntaylp  26608  taylthlem1  26610  taylthlem2  26611  ulmbdd  26635  ulmcn  26636  ulmdvlem1  26637  mtest  26641  iblulm  26644  itgulm  26645  abelthlem9  26677  ptolemy  26735  tangtx  26744  sineq0  26762  efeq1  26766  efif1olem4  26783  tanarg  26857  logcnlem3  26882  logcnlem4  26883  advlogexp  26893  efopn  26896  cxpcn3lem  26985  cxpeq  26995  ang180lem4  27050  ang180lem5  27051  ang180  27052  isosctrlem2  27057  isosctrlem3  27058  isosctr  27059  ssscongptld  27060  affineequiv  27061  affineequiv2  27062  affineequiv3  27063  affineequiv4  27064  affineequivne  27065  angpieqvdlem  27066  angpieqvdlem2  27067  angpined  27068  angpieqvd  27069  chordthmlem  27070  chordthmlem2  27071  chordthmlem3  27072  chordthmlem4  27073  chordthmlem5  27074  heron  27076  quad2  27077  quad  27078  dcubic1lem  27081  dcubic  27084  mcubic  27085  cubic2  27086  cubic  27087  dquartlem1  27089  dquartlem2  27090  dquart  27091  quart1cl  27092  quart1lem  27093  quart1  27094  quartlem2  27096  quartlem4  27098  quart  27099  atanf  27118  sinasin  27127  asinsin  27130  atanneg  27145  atancj  27148  efiatan  27150  atanlogsub  27154  efiatan2  27155  2efiatan  27156  atanbndlem  27163  dvatan  27173  atantayl  27175  lgamgulmlem2  27267  lgamgulmlem3  27268  lgamgulmlem5  27270  lgamgulmlem6  27271  lgamgulm2  27273  lgamucov  27275  lgamcvg2  27292  gamcvg  27293  gamcvg2lem  27296  ftalem2  27311  logfacrlim  27461  logexprlim  27462  lgsdirprm  27568  gausslemma2dlem1a  27602  gausslemma2dlem4  27606  2sqmod  27673  addsq2nreurex  27681  vmadivsum  27719  rpvmasumlem  27724  dchrisumlem2  27727  dchrisumlem3  27728  dchrmusum2  27731  dchrvmasumlem2  27735  dchrvmasumlem3  27736  dchrvmasumiflem1  27738  rpvmasum2  27749  dchrisum0lem1b  27752  dchrisum0lem1  27753  dchrisum0lem2a  27754  rplogsum  27764  mudivsum  27767  mulogsumlem  27768  mulogsum  27769  mulog2sumlem1  27771  mulog2sumlem2  27772  mulog2sumlem3  27773  vmalogdivsum2  27775  vmalogdivsum  27776  2vmadivsumlem  27777  selberglem1  27782  selberglem2  27783  selberg2lem  27787  selberg2  27788  selberg3lem1  27794  selberg4lem1  27797  selberg4  27798  pntrsumo1  27802  selberg3r  27806  selberg34r  27808  pntrlog2bndlem1  27814  pntrlog2bndlem2  27815  pntrlog2bndlem3  27816  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  pntibndlem2  27828  pntlemf  27842  pntlemo  27844  ttgcontlem1  29342  brbtwn2  29363  colinearalglem1  29364  colinearalglem2  29365  colinearalg  29368  axsegconlem1  29375  ax5seglem1  29386  ax5seglem2  29387  ax5seglem6  29392  ax5seglem9  29395  axlowdimlem17  29416  axcontlem7  29428  axcontlem8  29429  revwlk  30147  clwlkclwwlk  30473  clwwlknonex2lem1  30578  2clwwlk2clwwlk  30831  numclwwlk3lem1  30863  smcnlem  31179  ipval2  31189  4ipval2  31190  dipcj  31196  pjhthlem1  31873  submuladdd  33212  binom2subadd  33213  pythagreim  33217  quad3d  33221  lt2addrd  33222  bcm1n  33267  cycpmco2lem5  33571  cycpmco2lem6  33572  vietalem  34090  constrrtll  34242  constrrtlc1  34243  constrrtcclem  34245  constrrtcc  34246  constrsslem  34252  constrconj  34256  constrfin  34257  constrelextdg2  34258  constraddcl  34273  iconstr  34277  constrremulcl  34278  constrrecl  34280  constrmulcl  34282  constrreinvcl  34283  constrresqrtcl  34288  cos9thpiminplylem2  34294  cos9thpiminplylem3  34295  sqsscirc2  34420  signslema  35071  circlemeth  35149  logdivsqrle  35159  subfaclim  35768  divcnvlin  36313  iprodgam  36322  dnicld1  37170  dnibndlem2  37177  dnibndlem3  37178  dnibndlem6  37181  dnibndlem9  37184  dnibndlem10  37185  dnibndlem11  37186  unblimceq0  37205  unbdqndv2lem1  37207  unbdqndv2lem2  37208  knoppndvlem11  37220  knoppndvlem15  37224  knoppndvlem17  37226  knoppndvlem21  37230  bj-bary1lem  38063  bj-bary1lem1  38064  bj-bary1  38065  qdiff  38080  ftc1cnnclem  38441  ftc1anclem7  38449  ftc1anclem8  38450  ftc1anc  38451  ftc2nc  38452  areacirclem1  38458  areacirclem4  38461  areacirc  38463  cntotbnd  38547  lcmineqlem8  42903  lcmineqlem10  42905  lcmineqlem11  42906  lcmineqlem12  42907  lcmineqlem23  42918  aks4d1p1  42943  aks6d1c5lem1  43003  sticksstones10  43022  sticksstones12a  43024  sticksstones12  43025  sticksstones22  43035  bcle2d  43046  quadfac  43072  mvrrsubd  43150  lsubrotld  43153  lsubswap23d  43155  nicomachus  43188  sumcubes  43189  ef11d  43215  tanhalfpim  43225  sinpim  43226  cospim  43227  dffltz  43481  fltnltalem  43509  rencldnfilem  43662  pellexlem2  43672  pellexlem6  43676  pell1234qrne0  43695  pell1234qrmulcl  43697  rmyluc  43779  jm2.18  43830  jm2.19  43835  areaquad  44058  lhe4.4ex1a  45154  bcc0  45165  bccp1k  45166  bccm1k  45167  binomcxplemwb  45173  binomcxplemnn0  45174  binomcxplemrat  45175  binomcxplemfrat  45176  binomcxplemdvbinom  45178  binomcxplemnotnn0  45181  isosctrlem1ALT  45757  sineq0ALT  45760  oddfl  46112  dstregt0  46116  subadd4b  46117  sub31  46124  fzisoeu  46134  absnpncan2d  46136  absnpncan3d  46141  supxrgelem  46168  absimlere  46308  cvgcaule  46320  mullimc  46447  ellimcabssub0  46448  mullimcf  46454  limcrecl  46460  lptre2pt  46469  limcleqr  46473  neglimc  46476  addlimc  46477  0ellimcdiv  46478  limclner  46480  reclimc  46482  climleltrp  46505  climisp  46575  climxrrelem  46578  climxrre  46579  cnrefiisplem  46658  climxlim2lem  46674  fprodsubrecnncnvlem  46736  fperdvper  46748  dvdivbd  46752  dvbdfbdioolem2  46758  ioodvbdlimc1lem1  46760  volioc  46801  volico  46812  stoweidlem1  46830  stoweidlem11  46840  stoweidlem13  46842  stoweidlem26  46855  stoweid  46892  wallispi  46899  wallispi2lem1  46900  wallispi2lem2  46901  wallispi2  46902  stirlinglem1  46903  stirlinglem4  46906  stirlinglem5  46907  stirlinglem7  46909  stirlinglem11  46913  dirkertrigeqlem2  46928  fourierdlem4  46940  fourierdlem26  46962  fourierdlem30  46966  fourierdlem42  46978  fourierdlem63  46998  fourierdlem65  47000  fourierdlem72  47007  fourierdlem74  47009  fourierdlem75  47010  fourierdlem76  47011  fourierdlem80  47015  fourierdlem81  47016  fourierdlem89  47024  fourierdlem90  47025  fourierdlem91  47026  fourierdlem107  47042  fourierdlem109  47044  fouriersw  47060  etransclem1  47064  etransclem4  47067  etransclem8  47071  etransclem18  47081  etransclem20  47083  etransclem21  47084  etransclem23  47086  etransclem35  47098  etransclem46  47109  rrxtopnfi  47116  rrndistlt  47119  sge0gtfsumgt  47272  hoidmv1lelem2  47421  hoidmvlelem2  47425  smfmullem1  47620  sigarmf  47683  sigarms  47685  sigarexp  47688  sigardiv  47690  sigarcol  47693  sharhght  47694  sigaradd  47695  cevathlem2  47697  cevath  47698  sin5tlem3  47740  sin5tlem4  47741  sin5tlem5  47742  cos5t  47744  resubcnnred  48193  fldivmod  48233  ceildivmod  48234  fmtnorec2lem  48446  fmtnorec3  48452  fmtnorec4  48453  lighneallem3  48511  quad1  48537  requad01  48538  requad2  48540  fppr2odd  48648  dignn0flhalflem2  49547  affinecomb2  49634  1subrec1sub  49636  eenglngeehlnmlem1  49668  eenglngeehlnmlem2  49669  rrx2vlinest  49672  rrx2linest  49673  line2  49683  itsclc0yqsollem1  49693  itsclc0yqsol  49695  itscnhlc0xyqsol  49696  itschlc0xyqsol1  49697  itschlc0xyqsol  49698  itsclc0xyqsolr  49700  2itscplem1  49709  2itscplem2  49710  2itscplem3  49711  itscnhlinecirc02plem1  49713  inlinecirc02plem  49717  sinhpcosh  50667  i2linesd  50709  crossp3d  50801