Theorem subcld 11617

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

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   − cmin 11489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-ltxr 11297  df-sub 11491

This theorem is referenced by:  pnpncand  11681  muleqadd  11904  lineq  12101  modmuladdnn0  13952  hashfz  14462  hashfzo  14464  hashf1lem2  14491  hashf1  14492  ccatswrd  14702  pfxccatin12lem2  14765  crre  15149  remim  15152  remullem  15163  abs3lem  15373  caubnd2  15392  bhmafibid1cn  15498  bhmafibid2cn  15499  bhmafibid2  15501  rlimuni  15582  climuni  15584  rlimcld2  15610  rlimrege0  15611  rlimrecl  15612  mulcn2  15628  reccn2  15629  cn1lem  15630  o1sub  15648  rlimo1  15649  o1dif  15662  rlimsqzlem  15681  caucvgrlem2  15707  iseralt  15717  fsumparts  15838  cvgcmpce  15850  incexclem  15868  arisum2  15893  geoserg  15898  pwdif  15900  geo2sum2  15906  fallfacfwd  16068  binomfallfaclem2  16072  bpolycl  16084  bpoly3  16090  bpoly4  16091  fsumcube  16092  sinf  16156  tanval2  16165  tanval3  16166  sinneg  16178  efival  16184  sinhval  16186  bitsinv1lem  16474  bitsres  16506  pythagtriplem1  16849  pythagtriplem14  16861  pythagtriplem17  16864  dvdsprmpweqle  16919  4sqlem5  16975  mul4sqlem  16986  4sqlem17  16994  vdwlem5  17018  vdwlem6  17019  vdwlem8  17021  blcvx  24833  recld2  24849  addcnlem  24899  cnllycmp  25001  cphipval2  25288  4cphipval2  25289  cphipval  25290  ipcnlem2  25291  rrxmval  25452  rrxmetlem  25454  pjthlem1  25484  ovollb2lem  25536  itgcnlem  25839  dvlem  25945  dvconst  25966  dvid  25967  dvcnp2  25969  dvcnp2OLD  25970  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  dvcjbr  26001  dvrec  26007  dvmptim  26022  dvcnvlem  26028  dveflem  26031  dvsincos  26033  cmvth  26043  cmvthOLD  26044  dvlip  26046  dvlipcn  26047  c1liplem1  26049  dveq0  26053  dv11cn  26054  dvle  26060  lhop1lem  26066  dvfsumabs  26077  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumrlim  26086  dvfsumrlim2  26087  ftc1lem4  26094  ftc1lem5  26095  ftc2  26099  dgrcolem2  26328  plydiveu  26354  aaliou2b  26397  taylfvallem1  26412  taylply2  26423  taylply2OLD  26424  dvtaylp  26426  dvntaylp  26427  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmbdd  26455  ulmcn  26456  ulmdvlem1  26457  mtest  26461  iblulm  26464  itgulm  26465  abelthlem9  26498  ptolemy  26552  tangtx  26561  sineq0  26580  efeq1  26584  efif1olem4  26601  tanarg  26675  logcnlem3  26700  logcnlem4  26701  advlogexp  26711  efopn  26714  cxpcn3lem  26804  cxpeq  26814  ang180lem4  26869  ang180lem5  26870  ang180  26871  isosctrlem2  26876  isosctrlem3  26877  isosctr  26878  ssscongptld  26879  affineequiv  26880  affineequiv2  26881  affineequiv3  26882  affineequiv4  26883  affineequivne  26884  angpieqvdlem  26885  angpieqvdlem2  26886  angpined  26887  angpieqvd  26888  chordthmlem  26889  chordthmlem2  26890  chordthmlem3  26891  chordthmlem4  26892  chordthmlem5  26893  heron  26895  quad2  26896  quad  26897  dcubic1lem  26900  dcubic  26903  mcubic  26904  cubic2  26905  cubic  26906  dquartlem1  26908  dquartlem2  26909  dquart  26910  quart1cl  26911  quart1lem  26912  quart1  26913  quartlem2  26915  quartlem4  26917  quart  26918  atanf  26937  sinasin  26946  asinsin  26949  atanneg  26964  atancj  26967  efiatan  26969  atanlogsub  26973  efiatan2  26974  2efiatan  26975  atanbndlem  26982  dvatan  26992  atantayl  26994  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamgulm2  27093  lgamucov  27095  lgamcvg2  27112  gamcvg  27113  gamcvg2lem  27116  ftalem2  27131  logfacrlim  27282  logexprlim  27283  lgsdirprm  27389  gausslemma2dlem1a  27423  gausslemma2dlem4  27427  2sqmod  27494  addsq2nreurex  27502  vmadivsum  27540  rpvmasumlem  27545  dchrisumlem2  27548  dchrisumlem3  27549  dchrmusum2  27552  dchrvmasumlem2  27556  dchrvmasumlem3  27557  dchrvmasumiflem1  27559  rpvmasum2  27570  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  rplogsum  27585  mudivsum  27588  mulogsumlem  27589  mulogsum  27590  mulog2sumlem1  27592  mulog2sumlem2  27593  mulog2sumlem3  27594  vmalogdivsum2  27596  vmalogdivsum  27597  2vmadivsumlem  27598  selberglem1  27603  selberglem2  27604  selberg2lem  27608  selberg2  27609  selberg3lem1  27615  selberg4lem1  27618  selberg4  27619  pntrsumo1  27623  selberg3r  27627  selberg34r  27629  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntibndlem2  27649  pntlemf  27663  pntlemo  27665  ttgcontlem1  28913  brbtwn2  28934  colinearalglem1  28935  colinearalglem2  28936  colinearalg  28939  axsegconlem1  28946  ax5seglem1  28957  ax5seglem2  28958  ax5seglem6  28963  ax5seglem9  28966  axlowdimlem17  28987  axcontlem7  28999  axcontlem8  29000  clwlkclwwlk  30030  clwwlknonex2lem1  30135  2clwwlk2clwwlk  30378  numclwwlk3lem1  30410  smcnlem  30725  ipval2  30735  4ipval2  30736  dipcj  30742  pjhthlem1  31419  submuladdd  32756  quad3d  32760  lt2addrd  32761  bcm1n  32802  cycpmco2lem5  33132  cycpmco2lem6  33133  constrrtll  33736  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  constrsslem  33745  constrconj  33749  constrfin  33750  constrelextdg2  33751  sqsscirc2  33869  signslema  34555  circlemeth  34633  logdivsqrle  34643  revpfxsfxrev  35099  revwlk  35108  subfaclim  35172  divcnvlin  35712  iprodgam  35721  dnicld1  36454  dnibndlem2  36461  dnibndlem3  36462  dnibndlem6  36465  dnibndlem9  36468  dnibndlem10  36469  dnibndlem11  36470  unblimceq0  36489  unbdqndv2lem1  36491  unbdqndv2lem2  36492  knoppndvlem11  36504  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem21  36514  bj-bary1lem  37292  bj-bary1lem1  37293  bj-bary1  37294  ftc1cnnclem  37677  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  ftc2nc  37688  areacirclem1  37694  areacirclem4  37697  areacirc  37699  cntotbnd  37782  lcmineqlem8  42017  lcmineqlem10  42019  lcmineqlem11  42020  lcmineqlem12  42021  lcmineqlem23  42032  aks4d1p1  42057  aks6d1c5lem1  42117  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  bcle2d  42160  metakunt15  42200  metakunt16  42201  metakunt29  42214  metakunt30  42215  mvrrsubd  42287  lsubrotld  42290  lsubswap23d  42292  nicomachus  42324  sumcubes  42325  ef11d  42353  tanhalfpim  42363  dffltz  42620  fltnltalem  42648  rencldnfilem  42807  pellexlem2  42817  pellexlem6  42821  pell1234qrne0  42840  pell1234qrmulcl  42842  rmyluc  42925  jm2.18  42976  jm2.19  42981  areaquad  43204  lhe4.4ex1a  44324  bcc0  44335  bccp1k  44336  bccm1k  44337  binomcxplemwb  44343  binomcxplemnn0  44344  binomcxplemrat  44345  binomcxplemfrat  44346  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  isosctrlem1ALT  44931  sineq0ALT  44934  oddfl  45227  dstregt0  45231  subadd4b  45232  sub31  45240  fzisoeu  45250  absnpncan2d  45252  absnpncan3d  45257  supxrgelem  45286  absimlere  45429  cvgcaule  45441  mullimc  45571  ellimcabssub0  45572  mullimcf  45578  limcrecl  45584  lptre2pt  45595  limcleqr  45599  neglimc  45602  addlimc  45603  0ellimcdiv  45604  limclner  45606  reclimc  45608  climleltrp  45631  climisp  45701  climxrrelem  45704  climxrre  45705  cnrefiisplem  45784  climxlim2lem  45800  fprodsubrecnncnvlem  45862  fperdvper  45874  dvdivbd  45878  dvbdfbdioolem2  45884  ioodvbdlimc1lem1  45886  volioc  45927  volico  45938  stoweidlem1  45956  stoweidlem11  45966  stoweidlem13  45968  stoweidlem26  45981  stoweid  46018  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem4  46032  stirlinglem5  46033  stirlinglem7  46035  stirlinglem11  46039  dirkertrigeqlem2  46054  fourierdlem4  46066  fourierdlem26  46088  fourierdlem30  46092  fourierdlem42  46104  fourierdlem63  46124  fourierdlem65  46126  fourierdlem72  46133  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem80  46141  fourierdlem81  46142  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem107  46168  fourierdlem109  46170  fouriersw  46186  etransclem1  46190  etransclem4  46193  etransclem8  46197  etransclem18  46207  etransclem20  46209  etransclem21  46210  etransclem23  46212  etransclem35  46224  etransclem46  46235  rrxtopnfi  46242  rrndistlt  46245  sge0gtfsumgt  46398  hoidmv1lelem2  46547  hoidmvlelem2  46551  smfmullem1  46746  sigarmf  46809  sigarms  46811  sigarexp  46814  sigardiv  46816  sigarcol  46819  sharhght  46820  sigaradd  46821  cevathlem2  46823  cevath  46824  resubcnnred  47253  fldivmod  47277  ceildivmod  47278  fmtnorec2lem  47466  fmtnorec3  47472  fmtnorec4  47473  lighneallem3  47531  quad1  47544  requad01  47545  requad2  47547  fppr2odd  47655  dignn0flhalflem2  48465  affinecomb2  48552  1subrec1sub  48554  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  rrx2vlinest  48590  rrx2linest  48591  line2  48601  itsclc0yqsollem1  48611  itsclc0yqsol  48613  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615  itschlc0xyqsol  48616  itsclc0xyqsolr  48618  2itscplem1  48627  2itscplem2  48628  2itscplem3  48629  itscnhlinecirc02plem1  48631  inlinecirc02plem  48635  sinhpcosh  48970  i2linesd  49009