Theorem subcld 11682

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7430  ℂcc 11211   − cmin 11554

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-addrcl 11274  ax-mulcl 11275  ax-mulrcl 11276  ax-mulcom 11277  ax-addass 11278  ax-mulass 11279  ax-distr 11280  ax-i2m1 11281  ax-1ne0 11282  ax-1rid 11283  ax-rnegex 11284  ax-rrecex 11285  ax-cnre 11286  ax-pre-lttri 11287  ax-pre-lttrn 11288  ax-pre-ltadd 11289

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  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 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8731  df-en 8988  df-dom 8989  df-sdom 8990  df-pnf 11358  df-mnf 11359  df-ltxr 11361  df-sub 11556

This theorem is used by:  subsubadd23  11734  addsubsub23  11735  mvrrsubd  11742  pnpncand  11750  muleqadd  11973  lineq  12167  modmuladdnn0  14071  hashfz  14585  hashfzo  14587  hashf1lem2  14614  hashf1  14615  ccatswrd  14832  pfxccatin12lem2  14894  revpfxsfxrev  14931  crre  15296  remim  15299  remullem  15310  abs3lem  15521  caubnd2  15540  bhmafibid1cn  15648  bhmafibid2cn  15649  bhmafibid2  15651  rlimuni  15732  climuni  15734  rlimcld2  15760  rlimrege0  15761  rlimrecl  15762  mulcn2  15778  reccn2  15779  cn1lem  15780  o1sub  15798  rlimo1  15799  o1dif  15812  rlimsqzlem  15831  caucvgrlem2  15857  iseralt  15867  fsumparts  15988  cvgcmpce  16000  incexclem  16020  arisum2  16045  geoserg  16050  pwdif  16052  geo2sum2  16058  fallfacfwd  16217  binomfallfaclem2  16221  bpolycl  16233  bpoly3  16239  bpoly4  16240  fsumcube  16241  sinf  16307  tanval2  16316  tanval3  16317  sinneg  16329  efival  16335  sinhval  16337  bitsinv1lem  16626  bitsres  16658  pythagtriplem1  17009  pythagtriplem14  17021  pythagtriplem17  17024  dvdsprmpweqle  17079  4sqlem5  17135  mul4sqlem  17146  4sqlem17  17154  vdwlem5  17178  vdwlem6  17179  vdwlem8  17181  blcvx  25132  recld2  25149  addcnlem  25199  cnllycmp  25292  cphipval2  25577  4cphipval2  25578  cphipval  25579  ipcnlem2  25580  rrxmval  25741  rrxmetlem  25743  pjthlem1  25773  ovollb2lem  25824  itgcnlem  26125  dvlem  26231  dvconst  26252  dvid  26253  dvcnp2  26255  dvaddbr  26273  dvmulbr  26274  dvcobr  26281  dvcjbr  26284  dvrec  26290  dvmptim  26305  dvcnvlem  26311  dveflem  26314  dvsincos  26316  cmvth  26326  dvlip  26328  dvlipcn  26329  c1liplem1  26331  dveq0  26335  dv11cn  26336  dvle  26342  lhop1lem  26348  dvfsumabs  26358  dvfsumlem1  26361  dvfsumlem2  26362  dvfsumrlim  26366  dvfsumrlim2  26367  ftc1lem4  26374  ftc1lem5  26375  ftc2  26379  dgrcolem2  26608  plydiveu  26634  aaliou2b  26683  taylfvallem1  26699  taylply2  26710  dvtaylp  26712  dvntaylp  26713  taylthlem1  26715  taylthlem2  26716  ulmbdd  26740  ulmcn  26741  ulmdvlem1  26742  mtest  26746  iblulm  26749  itgulm  26750  abelthlem9  26782  ptolemy  26840  tangtx  26849  sineq0  26867  efeq1  26871  efif1olem4  26888  tanarg  26962  logcnlem3  26987  logcnlem4  26988  advlogexp  26998  efopn  27001  cxpcn3lem  27090  cxpeq  27100  ang180lem4  27155  ang180lem5  27156  ang180  27157  isosctrlem2  27162  isosctrlem3  27163  isosctr  27164  ssscongptld  27165  affineequiv  27166  affineequiv2  27167  affineequiv3  27168  affineequiv4  27169  affineequivne  27170  angpieqvdlem  27171  angpieqvdlem2  27172  angpined  27173  angpieqvd  27174  chordthmlem  27175  chordthmlem2  27176  chordthmlem3  27177  chordthmlem4  27178  chordthmlem5  27179  heron  27181  quad2  27182  quad  27183  dcubic1lem  27186  dcubic  27189  mcubic  27190  cubic2  27191  cubic  27192  dquartlem1  27194  dquartlem2  27195  dquart  27196  quart1cl  27197  quart1lem  27198  quart1  27199  quartlem2  27201  quartlem4  27203  quart  27204  atanf  27223  sinasin  27232  asinsin  27235  atanneg  27250  atancj  27253  efiatan  27255  atanlogsub  27259  efiatan2  27260  2efiatan  27261  atanbndlem  27268  dvatan  27278  atantayl  27280  lgamgulmlem2  27372  lgamgulmlem3  27373  lgamgulmlem5  27375  lgamgulmlem6  27376  lgamgulm2  27378  lgamucov  27380  lgamcvg2  27397  gamcvg  27398  gamcvg2lem  27401  ftalem2  27416  logfacrlim  27566  logexprlim  27567  lgsdirprm  27673  gausslemma2dlem1a  27707  gausslemma2dlem4  27711  2sqmod  27778  addsq2nreurex  27786  vmadivsum  27824  rpvmasumlem  27829  dchrisumlem2  27832  dchrisumlem3  27833  dchrmusum2  27836  dchrvmasumlem2  27840  dchrvmasumlem3  27841  dchrvmasumiflem1  27843  rpvmasum2  27854  dchrisum0lem1b  27857  dchrisum0lem1  27858  dchrisum0lem2a  27859  rplogsum  27869  mudivsum  27872  mulogsumlem  27873  mulogsum  27874  mulog2sumlem1  27876  mulog2sumlem2  27877  mulog2sumlem3  27878  vmalogdivsum2  27880  vmalogdivsum  27881  2vmadivsumlem  27882  selberglem1  27887  selberglem2  27888  selberg2lem  27892  selberg2  27893  selberg3lem1  27899  selberg4lem1  27902  selberg4  27903  pntrsumo1  27907  selberg3r  27911  selberg34r  27913  pntrlog2bndlem1  27919  pntrlog2bndlem2  27920  pntrlog2bndlem3  27921  pntrlog2bndlem4  27922  pntrlog2bndlem5  27923  pntibndlem2  27933  pntlemf  27947  pntlemo  27949  ttgcontlem1  29477  brbtwn2  29498  colinearalglem1  29499  colinearalglem2  29500  colinearalg  29503  axsegconlem1  29510  ax5seglem1  29521  ax5seglem2  29522  ax5seglem6  29527  ax5seglem9  29530  axlowdimlem17  29551  axcontlem7  29563  axcontlem8  29564  revwlk  30282  clwlkclwwlk  30608  clwwlknonex2lem1  30713  2clwwlk2clwwlk  30966  numclwwlk3lem1  30998  smcnlem  31314  ipval2  31324  4ipval2  31325  dipcj  31331  pjhthlem1  32008  submuladdd  33388  binom2subadd  33389  pythagreim  33393  quad3d  33397  lt2addrd  33398  bcm1n  33443  cycpmco2lem5  33747  cycpmco2lem6  33748  vietalem  34267  constrrtll  34419  constrrtlc1  34420  constrrtcclem  34422  constrrtcc  34423  constrsslem  34429  constrconj  34433  constrfin  34434  constrelextdg2  34435  constraddcl  34450  iconstr  34454  constrremulcl  34455  constrrecl  34457  constrmulcl  34459  constrreinvcl  34460  constrresqrtcl  34465  cos9thpiminplylem2  34471  cos9thpiminplylem3  34472  sqsscirc2  34597  signslema  35247  circlemeth  35325  logdivsqrle  35335  subfaclim  36077  divcnvlin  36628  iprodgam  36637  dnicld1  37468  dnibndlem2  37475  dnibndlem3  37476  dnibndlem6  37479  dnibndlem9  37482  dnibndlem10  37483  dnibndlem11  37484  unblimceq0  37503  unbdqndv2lem1  37505  unbdqndv2lem2  37506  knoppndvlem11  37518  knoppndvlem15  37522  knoppndvlem17  37524  knoppndvlem21  37528  bj-bary1lem  38374  bj-bary1lem1  38375  bj-bary1  38376  qdiff  38391  ftc1cnnclem  38752  ftc1anclem7  38760  ftc1anclem8  38761  ftc1anc  38762  ftc2nc  38763  areacirclem1  38769  areacirclem4  38772  areacirc  38774  cntotbnd  38873  lcmineqlem8  43229  lcmineqlem10  43231  lcmineqlem11  43232  lcmineqlem12  43233  lcmineqlem23  43244  aks4d1p1  43269  aks6d1c5lem1  43329  sticksstones10  43348  sticksstones12a  43350  sticksstones12  43351  sticksstones22  43361  bcle2d  43372  quadfac  43398  lsubrotld  43477  lsubswap23d  43479  nicomachus  43512  sumcubes  43513  ef11d  43533  tanhalfpim  43543  sinpim  43544  cospim  43545  dffltz  43813  fltnltalem  43816  rencldnfilem  43970  pellexlem2  43980  pellexlem6  43984  pell1234qrne0  44003  pell1234qrmulcl  44005  rmyluc  44087  jm2.18  44138  jm2.19  44143  areaquad  44361  lhe4.4ex1a  45456  bcc0  45467  bccp1k  45468  bccm1k  45469  binomcxplemwb  45475  binomcxplemnn0  45476  binomcxplemrat  45477  binomcxplemfrat  45478  binomcxplemdvbinom  45480  binomcxplemnotnn0  45483  isosctrlem1ALT  46058  sineq0ALT  46061  oddfl  46436  dstregt0  46440  subadd4b  46441  sub31  46448  fzisoeu  46458  absnpncan2d  46460  absnpncan3d  46465  supxrgelem  46491  absimlere  46631  cvgcaule  46643  mullimc  46770  ellimcabssub0  46771  mullimcf  46777  limcrecl  46783  lptre2pt  46792  limcleqr  46796  neglimc  46799  addlimc  46800  0ellimcdiv  46801  limclner  46803  reclimc  46805  climleltrp  46828  climisp  46898  climxrrelem  46901  climxrre  46902  cnrefiisplem  46981  climxlim2lem  46997  fprodsubrecnncnvlem  47059  fperdvper  47071  dvdivbd  47075  dvbdfbdioolem2  47081  ioodvbdlimc1lem1  47083  volioc  47124  volico  47135  stoweidlem1  47153  stoweidlem11  47163  stoweidlem13  47165  stoweidlem26  47178  stoweid  47215  wallispi  47222  wallispi2lem1  47223  wallispi2lem2  47224  wallispi2  47225  stirlinglem1  47226  stirlinglem4  47229  stirlinglem5  47230  stirlinglem7  47232  stirlinglem11  47236  dirkertrigeqlem2  47251  fourierdlem4  47263  fourierdlem26  47285  fourierdlem30  47289  fourierdlem42  47301  fourierdlem63  47321  fourierdlem65  47323  fourierdlem72  47330  fourierdlem74  47332  fourierdlem75  47333  fourierdlem76  47334  fourierdlem80  47338  fourierdlem81  47339  fourierdlem89  47347  fourierdlem90  47348  fourierdlem91  47349  fourierdlem107  47365  fourierdlem109  47367  fouriersw  47383  etransclem1  47387  etransclem4  47390  etransclem8  47394  etransclem18  47404  etransclem20  47406  etransclem21  47407  etransclem23  47409  etransclem35  47421  etransclem46  47432  rrxtopnfi  47439  rrndistlt  47442  sge0gtfsumgt  47595  hoidmv1lelem2  47744  hoidmvlelem2  47748  smfmullem1  47943  sigarmf  48006  sigarms  48008  sigarexp  48011  sigardiv  48013  sigarcol  48016  sharhght  48017  sigaradd  48018  cevathlem2  48020  cevath  48021  sin5tlem3  48063  sin5tlem4  48064  sin5tlem5  48065  cos5t  48067  resubcnnred  48516  fldivmod  48556  ceildivmod  48557  fmtnorec2lem  48769  fmtnorec3  48775  fmtnorec4  48776  lighneallem3  48834  quad1  48860  requad01  48861  requad2  48863  fppr2odd  48971  dignn0flhalflem2  49870  affinecomb2  49957  1subrec1sub  49959  eenglngeehlnmlem1  49992  eenglngeehlnmlem2  49993  rrx2vlinest  49995  rrx2linest  49996  line2  50006  itsclc0yqsollem1  50016  itsclc0yqsol  50018  itscnhlc0xyqsol  50019  itschlc0xyqsol1  50020  itschlc0xyqsol  50021  itsclc0xyqsolr  50023  2itscplem1  50032  2itscplem2  50033  2itscplem3  50034  itscnhlinecirc02plem1  50036  inlinecirc02plem  50040  sinhpcosh  51050  i2linesd  51092  crossp3d  51184