Theorem subcld 11586

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115   − cmin 11458

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-ltxr 11265  df-sub 11460

This theorem is used by:  subsubadd23  11638  addsubsub23  11639  pnpncand  11652  muleqadd  11875  lineq  12069  modmuladdnn0  13971  hashfz  14484  hashfzo  14486  hashf1lem2  14513  hashf1  14514  ccatswrd  14730  pfxccatin12lem2  14792  revpfxsfxrev  14829  crre  15191  remim  15194  remullem  15205  abs3lem  15416  caubnd2  15435  bhmafibid1cn  15543  bhmafibid2cn  15544  bhmafibid2  15546  rlimuni  15627  climuni  15629  rlimcld2  15655  rlimrege0  15656  rlimrecl  15657  mulcn2  15673  reccn2  15674  cn1lem  15675  o1sub  15693  rlimo1  15694  o1dif  15707  rlimsqzlem  15726  caucvgrlem2  15752  iseralt  15762  fsumparts  15883  cvgcmpce  15895  incexclem  15915  arisum2  15940  geoserg  15945  pwdif  15947  geo2sum2  15953  fallfacfwd  16114  binomfallfaclem2  16118  bpolycl  16130  bpoly3  16136  bpoly4  16137  fsumcube  16138  sinf  16204  tanval2  16213  tanval3  16214  sinneg  16226  efival  16232  sinhval  16234  bitsinv1lem  16523  bitsres  16555  pythagtriplem1  16900  pythagtriplem14  16912  pythagtriplem17  16915  dvdsprmpweqle  16970  4sqlem5  17026  mul4sqlem  17037  4sqlem17  17045  vdwlem5  17069  vdwlem6  17070  vdwlem8  17072  blcvx  25008  recld2  25025  addcnlem  25075  cnllycmp  25168  cphipval2  25453  4cphipval2  25454  cphipval  25455  ipcnlem2  25456  rrxmval  25617  rrxmetlem  25619  pjthlem1  25649  ovollb2lem  25700  itgcnlem  26002  dvlem  26108  dvconst  26129  dvid  26130  dvcnp2  26132  dvaddbr  26150  dvmulbr  26151  dvcobr  26158  dvcjbr  26161  dvrec  26167  dvmptim  26182  dvcnvlem  26188  dveflem  26191  dvsincos  26193  cmvth  26203  dvlip  26205  dvlipcn  26206  c1liplem1  26208  dveq0  26212  dv11cn  26213  dvle  26219  lhop1lem  26225  dvfsumabs  26235  dvfsumlem1  26238  dvfsumlem2  26239  dvfsumrlim  26243  dvfsumrlim2  26244  ftc1lem4  26251  ftc1lem5  26252  ftc2  26256  dgrcolem2  26484  plydiveu  26512  aaliou2b  26557  taylfvallem1  26573  taylply2  26584  dvtaylp  26586  dvntaylp  26587  taylthlem1  26589  taylthlem2  26590  ulmbdd  26614  ulmcn  26615  ulmdvlem1  26616  mtest  26620  iblulm  26623  itgulm  26624  abelthlem9  26656  ptolemy  26714  tangtx  26723  sineq0  26742  efeq1  26746  efif1olem4  26763  tanarg  26837  logcnlem3  26862  logcnlem4  26863  advlogexp  26873  efopn  26876  cxpcn3lem  26965  cxpeq  26975  ang180lem4  27030  ang180lem5  27031  ang180  27032  isosctrlem2  27037  isosctrlem3  27038  isosctr  27039  ssscongptld  27040  affineequiv  27041  affineequiv2  27042  affineequiv3  27043  affineequiv4  27044  affineequivne  27045  angpieqvdlem  27046  angpieqvdlem2  27047  angpined  27048  angpieqvd  27049  chordthmlem  27050  chordthmlem2  27051  chordthmlem3  27052  chordthmlem4  27053  chordthmlem5  27054  heron  27056  quad2  27057  quad  27058  dcubic1lem  27061  dcubic  27064  mcubic  27065  cubic2  27066  cubic  27067  dquartlem1  27069  dquartlem2  27070  dquart  27071  quart1cl  27072  quart1lem  27073  quart1  27074  quartlem2  27076  quartlem4  27078  quart  27079  atanf  27098  sinasin  27107  asinsin  27110  atanneg  27125  atancj  27128  efiatan  27130  atanlogsub  27134  efiatan2  27135  2efiatan  27136  atanbndlem  27143  dvatan  27153  atantayl  27155  lgamgulmlem2  27247  lgamgulmlem3  27248  lgamgulmlem5  27250  lgamgulmlem6  27251  lgamgulm2  27253  lgamucov  27255  lgamcvg2  27272  gamcvg  27273  gamcvg2lem  27276  ftalem2  27291  logfacrlim  27441  logexprlim  27442  lgsdirprm  27548  gausslemma2dlem1a  27582  gausslemma2dlem4  27586  2sqmod  27653  addsq2nreurex  27661  vmadivsum  27699  rpvmasumlem  27704  dchrisumlem2  27707  dchrisumlem3  27708  dchrmusum2  27711  dchrvmasumlem2  27715  dchrvmasumlem3  27716  dchrvmasumiflem1  27718  rpvmasum2  27729  dchrisum0lem1b  27732  dchrisum0lem1  27733  dchrisum0lem2a  27734  rplogsum  27744  mudivsum  27747  mulogsumlem  27748  mulogsum  27749  mulog2sumlem1  27751  mulog2sumlem2  27752  mulog2sumlem3  27753  vmalogdivsum2  27755  vmalogdivsum  27756  2vmadivsumlem  27757  selberglem1  27762  selberglem2  27763  selberg2lem  27767  selberg2  27768  selberg3lem1  27774  selberg4lem1  27777  selberg4  27778  pntrsumo1  27782  selberg3r  27786  selberg34r  27788  pntrlog2bndlem1  27794  pntrlog2bndlem2  27795  pntrlog2bndlem3  27796  pntrlog2bndlem4  27797  pntrlog2bndlem5  27798  pntibndlem2  27808  pntlemf  27822  pntlemo  27824  ttgcontlem1  29291  brbtwn2  29312  colinearalglem1  29313  colinearalglem2  29314  colinearalg  29317  axsegconlem1  29324  ax5seglem1  29335  ax5seglem2  29336  ax5seglem6  29341  ax5seglem9  29344  axlowdimlem17  29365  axcontlem7  29377  axcontlem8  29378  revwlk  30096  clwlkclwwlk  30422  clwwlknonex2lem1  30527  2clwwlk2clwwlk  30774  numclwwlk3lem1  30806  smcnlem  31122  ipval2  31132  4ipval2  31133  dipcj  31139  pjhthlem1  31816  submuladdd  33157  binom2subadd  33158  pythagreim  33162  quad3d  33166  lt2addrd  33167  bcm1n  33212  cycpmco2lem5  33516  cycpmco2lem6  33517  vietalem  34035  constrrtll  34187  constrrtlc1  34188  constrrtcclem  34190  constrrtcc  34191  constrsslem  34197  constrconj  34201  constrfin  34202  constrelextdg2  34203  constraddcl  34218  iconstr  34222  constrremulcl  34223  constrrecl  34225  constrmulcl  34227  constrreinvcl  34228  constrresqrtcl  34233  cos9thpiminplylem2  34239  cos9thpiminplylem3  34240  sqsscirc2  34365  signslema  35016  circlemeth  35094  logdivsqrle  35104  subfaclim  35719  divcnvlin  36264  iprodgam  36273  dnicld1  37120  dnibndlem2  37127  dnibndlem3  37128  dnibndlem6  37131  dnibndlem9  37134  dnibndlem10  37135  dnibndlem11  37136  unblimceq0  37155  unbdqndv2lem1  37157  unbdqndv2lem2  37158  knoppndvlem11  37170  knoppndvlem15  37174  knoppndvlem17  37176  knoppndvlem21  37180  bj-bary1lem  38013  bj-bary1lem1  38014  bj-bary1  38015  qdiff  38030  ftc1cnnclem  38401  ftc1anclem7  38409  ftc1anclem8  38410  ftc1anc  38411  ftc2nc  38412  areacirclem1  38418  areacirclem4  38421  areacirc  38423  cntotbnd  38507  lcmineqlem8  42863  lcmineqlem10  42865  lcmineqlem11  42866  lcmineqlem12  42867  lcmineqlem23  42878  aks4d1p1  42903  aks6d1c5lem1  42963  sticksstones10  42982  sticksstones12a  42984  sticksstones12  42985  sticksstones22  42995  bcle2d  43006  quadfac  43032  mvrrsubd  43095  lsubrotld  43098  lsubswap23d  43100  nicomachus  43133  sumcubes  43134  ef11d  43160  tanhalfpim  43170  sinpim  43171  cospim  43172  dffltz  43426  fltnltalem  43454  rencldnfilem  43607  pellexlem2  43617  pellexlem6  43621  pell1234qrne0  43640  pell1234qrmulcl  43642  rmyluc  43724  jm2.18  43775  jm2.19  43780  areaquad  44003  lhe4.4ex1a  45099  bcc0  45110  bccp1k  45111  bccm1k  45112  binomcxplemwb  45118  binomcxplemnn0  45119  binomcxplemrat  45120  binomcxplemfrat  45121  binomcxplemdvbinom  45123  binomcxplemnotnn0  45126  isosctrlem1ALT  45702  sineq0ALT  45705  oddfl  46057  dstregt0  46061  subadd4b  46062  sub31  46069  fzisoeu  46079  absnpncan2d  46081  absnpncan3d  46086  supxrgelem  46113  absimlere  46253  cvgcaule  46265  mullimc  46392  ellimcabssub0  46393  mullimcf  46399  limcrecl  46405  lptre2pt  46414  limcleqr  46418  neglimc  46421  addlimc  46422  0ellimcdiv  46423  limclner  46425  reclimc  46427  climleltrp  46450  climisp  46520  climxrrelem  46523  climxrre  46524  cnrefiisplem  46603  climxlim2lem  46619  fprodsubrecnncnvlem  46681  fperdvper  46693  dvdivbd  46697  dvbdfbdioolem2  46703  ioodvbdlimc1lem1  46705  volioc  46746  volico  46757  stoweidlem1  46775  stoweidlem11  46785  stoweidlem13  46787  stoweidlem26  46800  stoweid  46837  wallispi  46844  wallispi2lem1  46845  wallispi2lem2  46846  wallispi2  46847  stirlinglem1  46848  stirlinglem4  46851  stirlinglem5  46852  stirlinglem7  46854  stirlinglem11  46858  dirkertrigeqlem2  46873  fourierdlem4  46885  fourierdlem26  46907  fourierdlem30  46911  fourierdlem42  46923  fourierdlem63  46943  fourierdlem65  46945  fourierdlem72  46952  fourierdlem74  46954  fourierdlem75  46955  fourierdlem76  46956  fourierdlem80  46960  fourierdlem81  46961  fourierdlem89  46969  fourierdlem90  46970  fourierdlem91  46971  fourierdlem107  46987  fourierdlem109  46989  fouriersw  47005  etransclem1  47009  etransclem4  47012  etransclem8  47016  etransclem18  47026  etransclem20  47028  etransclem21  47029  etransclem23  47031  etransclem35  47043  etransclem46  47054  rrxtopnfi  47061  rrndistlt  47064  sge0gtfsumgt  47217  hoidmv1lelem2  47366  hoidmvlelem2  47370  smfmullem1  47565  sigarmf  47628  sigarms  47630  sigarexp  47633  sigardiv  47635  sigarcol  47638  sharhght  47639  sigaradd  47640  cevathlem2  47642  cevath  47643  sin5tlem3  47672  sin5tlem4  47673  sin5tlem5  47674  cos5t  47676  resubcnnred  48101  fldivmod  48141  ceildivmod  48142  fmtnorec2lem  48354  fmtnorec3  48360  fmtnorec4  48361  lighneallem3  48419  quad1  48445  requad01  48446  requad2  48448  fppr2odd  48556  dignn0flhalflem2  49455  affinecomb2  49542  1subrec1sub  49544  eenglngeehlnmlem1  49576  eenglngeehlnmlem2  49577  rrx2vlinest  49580  rrx2linest  49581  line2  49591  itsclc0yqsollem1  49601  itsclc0yqsol  49603  itscnhlc0xyqsol  49604  itschlc0xyqsol1  49605  itschlc0xyqsol  49606  itsclc0xyqsolr  49608  2itscplem1  49617  2itscplem2  49618  2itscplem3  49619  itscnhlinecirc02plem1  49621  inlinecirc02plem  49625  sinhpcosh  50577  i2linesd  50616  crossp3d  50708