Theorem subcld 11592

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   − cmin 11464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-ltxr 11272  df-sub 11466

This theorem is referenced by:  pnpncand  11656  muleqadd  11879  lineq  12076  modmuladdnn0  13931  hashfz  14443  hashfzo  14445  hashf1lem2  14472  hashf1  14473  ccatswrd  14684  pfxccatin12lem2  14747  crre  15131  remim  15134  remullem  15145  abs3lem  15355  caubnd2  15374  bhmafibid1cn  15480  bhmafibid2cn  15481  bhmafibid2  15483  rlimuni  15564  climuni  15566  rlimcld2  15592  rlimrege0  15593  rlimrecl  15594  mulcn2  15610  reccn2  15611  cn1lem  15612  o1sub  15630  rlimo1  15631  o1dif  15644  rlimsqzlem  15663  caucvgrlem2  15689  iseralt  15699  fsumparts  15820  cvgcmpce  15832  incexclem  15850  arisum2  15875  geoserg  15880  pwdif  15882  geo2sum2  15888  fallfacfwd  16050  binomfallfaclem2  16054  bpolycl  16066  bpoly3  16072  bpoly4  16073  fsumcube  16074  sinf  16140  tanval2  16149  tanval3  16150  sinneg  16162  efival  16168  sinhval  16170  bitsinv1lem  16458  bitsres  16490  pythagtriplem1  16834  pythagtriplem14  16846  pythagtriplem17  16849  dvdsprmpweqle  16904  4sqlem5  16960  mul4sqlem  16971  4sqlem17  16979  vdwlem5  17003  vdwlem6  17004  vdwlem8  17006  blcvx  24735  recld2  24752  addcnlem  24802  cnllycmp  24904  cphipval2  25191  4cphipval2  25192  cphipval  25193  ipcnlem2  25194  rrxmval  25355  rrxmetlem  25357  pjthlem1  25387  ovollb2lem  25439  itgcnlem  25741  dvlem  25847  dvconst  25868  dvid  25869  dvcnp2  25871  dvcnp2OLD  25872  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvcobr  25899  dvcobrOLD  25900  dvcjbr  25903  dvrec  25909  dvmptim  25924  dvcnvlem  25930  dveflem  25933  dvsincos  25935  cmvth  25945  cmvthOLD  25946  dvlip  25948  dvlipcn  25949  c1liplem1  25951  dveq0  25955  dv11cn  25956  dvle  25962  lhop1lem  25968  dvfsumabs  25979  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumrlim  25988  dvfsumrlim2  25989  ftc1lem4  25996  ftc1lem5  25997  ftc2  26001  dgrcolem2  26230  plydiveu  26256  aaliou2b  26299  taylfvallem1  26314  taylply2  26325  taylply2OLD  26326  dvtaylp  26328  dvntaylp  26329  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmbdd  26357  ulmcn  26358  ulmdvlem1  26359  mtest  26363  iblulm  26366  itgulm  26367  abelthlem9  26400  ptolemy  26455  tangtx  26464  sineq0  26483  efeq1  26487  efif1olem4  26504  tanarg  26578  logcnlem3  26603  logcnlem4  26604  advlogexp  26614  efopn  26617  cxpcn3lem  26707  cxpeq  26717  ang180lem4  26772  ang180lem5  26773  ang180  26774  isosctrlem2  26779  isosctrlem3  26780  isosctr  26781  ssscongptld  26782  affineequiv  26783  affineequiv2  26784  affineequiv3  26785  affineequiv4  26786  affineequivne  26787  angpieqvdlem  26788  angpieqvdlem2  26789  angpined  26790  angpieqvd  26791  chordthmlem  26792  chordthmlem2  26793  chordthmlem3  26794  chordthmlem4  26795  chordthmlem5  26796  heron  26798  quad2  26799  quad  26800  dcubic1lem  26803  dcubic  26806  mcubic  26807  cubic2  26808  cubic  26809  dquartlem1  26811  dquartlem2  26812  dquart  26813  quart1cl  26814  quart1lem  26815  quart1  26816  quartlem2  26818  quartlem4  26820  quart  26821  atanf  26840  sinasin  26849  asinsin  26852  atanneg  26867  atancj  26870  efiatan  26872  atanlogsub  26876  efiatan2  26877  2efiatan  26878  atanbndlem  26885  dvatan  26895  atantayl  26897  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem5  26993  lgamgulmlem6  26994  lgamgulm2  26996  lgamucov  26998  lgamcvg2  27015  gamcvg  27016  gamcvg2lem  27019  ftalem2  27034  logfacrlim  27185  logexprlim  27186  lgsdirprm  27292  gausslemma2dlem1a  27326  gausslemma2dlem4  27330  2sqmod  27397  addsq2nreurex  27405  vmadivsum  27443  rpvmasumlem  27448  dchrisumlem2  27451  dchrisumlem3  27452  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  rpvmasum2  27473  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  rplogsum  27488  mudivsum  27491  mulogsumlem  27492  mulogsum  27493  mulog2sumlem1  27495  mulog2sumlem2  27496  mulog2sumlem3  27497  vmalogdivsum2  27499  vmalogdivsum  27500  2vmadivsumlem  27501  selberglem1  27506  selberglem2  27507  selberg2lem  27511  selberg2  27512  selberg3lem1  27518  selberg4lem1  27521  selberg4  27522  pntrsumo1  27526  selberg3r  27530  selberg34r  27532  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntibndlem2  27552  pntlemf  27566  pntlemo  27568  ttgcontlem1  28810  brbtwn2  28830  colinearalglem1  28831  colinearalglem2  28832  colinearalg  28835  axsegconlem1  28842  ax5seglem1  28853  ax5seglem2  28854  ax5seglem6  28859  ax5seglem9  28862  axlowdimlem17  28883  axcontlem7  28895  axcontlem8  28896  clwlkclwwlk  29929  clwwlknonex2lem1  30034  2clwwlk2clwwlk  30277  numclwwlk3lem1  30309  smcnlem  30624  ipval2  30634  4ipval2  30635  dipcj  30641  pjhthlem1  31318  submuladdd  32663  binom2subadd  32665  pythagreim  32669  quad3d  32673  lt2addrd  32674  bcm1n  32718  cycpmco2lem5  33087  cycpmco2lem6  33088  constrrtll  33711  constrrtlc1  33712  constrrtcclem  33714  constrrtcc  33715  constrsslem  33721  constrconj  33725  constrfin  33726  constrelextdg2  33727  constraddcl  33742  iconstr  33746  constrremulcl  33747  constrrecl  33749  constrmulcl  33751  constrreinvcl  33752  constrresqrtcl  33757  cos9thpiminplylem2  33763  cos9thpiminplylem3  33764  sqsscirc2  33886  signslema  34540  circlemeth  34618  logdivsqrle  34628  revpfxsfxrev  35084  revwlk  35093  subfaclim  35156  divcnvlin  35696  iprodgam  35705  dnicld1  36436  dnibndlem2  36443  dnibndlem3  36444  dnibndlem6  36447  dnibndlem9  36450  dnibndlem10  36451  dnibndlem11  36452  unblimceq0  36471  unbdqndv2lem1  36473  unbdqndv2lem2  36474  knoppndvlem11  36486  knoppndvlem15  36490  knoppndvlem17  36492  knoppndvlem21  36496  bj-bary1lem  37274  bj-bary1lem1  37275  bj-bary1  37276  ftc1cnnclem  37661  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  ftc2nc  37672  areacirclem1  37678  areacirclem4  37681  areacirc  37683  cntotbnd  37766  lcmineqlem8  41995  lcmineqlem10  41997  lcmineqlem11  41998  lcmineqlem12  41999  lcmineqlem23  42010  aks4d1p1  42035  aks6d1c5lem1  42095  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones22  42127  bcle2d  42138  metakunt15  42178  metakunt16  42179  metakunt29  42192  metakunt30  42193  mvrrsubd  42271  lsubrotld  42274  lsubswap23d  42276  nicomachus  42308  sumcubes  42309  ef11d  42335  tanhalfpim  42345  dffltz  42604  fltnltalem  42632  rencldnfilem  42790  pellexlem2  42800  pellexlem6  42804  pell1234qrne0  42823  pell1234qrmulcl  42825  rmyluc  42908  jm2.18  42959  jm2.19  42964  areaquad  43187  lhe4.4ex1a  44301  bcc0  44312  bccp1k  44313  bccm1k  44314  binomcxplemwb  44320  binomcxplemnn0  44321  binomcxplemrat  44322  binomcxplemfrat  44323  binomcxplemdvbinom  44325  binomcxplemnotnn0  44328  isosctrlem1ALT  44906  sineq0ALT  44909  oddfl  45254  dstregt0  45258  subadd4b  45259  sub31  45267  fzisoeu  45277  absnpncan2d  45279  absnpncan3d  45284  supxrgelem  45312  absimlere  45454  cvgcaule  45466  mullimc  45593  ellimcabssub0  45594  mullimcf  45600  limcrecl  45606  lptre2pt  45617  limcleqr  45621  neglimc  45624  addlimc  45625  0ellimcdiv  45626  limclner  45628  reclimc  45630  climleltrp  45653  climisp  45723  climxrrelem  45726  climxrre  45727  cnrefiisplem  45806  climxlim2lem  45822  fprodsubrecnncnvlem  45884  fperdvper  45896  dvdivbd  45900  dvbdfbdioolem2  45906  ioodvbdlimc1lem1  45908  volioc  45949  volico  45960  stoweidlem1  45978  stoweidlem11  45988  stoweidlem13  45990  stoweidlem26  46003  stoweid  46040  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem1  46051  stirlinglem4  46054  stirlinglem5  46055  stirlinglem7  46057  stirlinglem11  46061  dirkertrigeqlem2  46076  fourierdlem4  46088  fourierdlem26  46110  fourierdlem30  46114  fourierdlem42  46126  fourierdlem63  46146  fourierdlem65  46148  fourierdlem72  46155  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem80  46163  fourierdlem81  46164  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem107  46190  fourierdlem109  46192  fouriersw  46208  etransclem1  46212  etransclem4  46215  etransclem8  46219  etransclem18  46229  etransclem20  46231  etransclem21  46232  etransclem23  46234  etransclem35  46246  etransclem46  46257  rrxtopnfi  46264  rrndistlt  46267  sge0gtfsumgt  46420  hoidmv1lelem2  46569  hoidmvlelem2  46573  smfmullem1  46768  sigarmf  46831  sigarms  46833  sigarexp  46836  sigardiv  46838  sigarcol  46841  sharhght  46842  sigaradd  46843  cevathlem2  46845  cevath  46846  resubcnnred  47281  fldivmod  47315  ceildivmod  47316  fmtnorec2lem  47504  fmtnorec3  47510  fmtnorec4  47511  lighneallem3  47569  quad1  47582  requad01  47583  requad2  47585  fppr2odd  47693  dignn0flhalflem2  48544  affinecomb2  48631  1subrec1sub  48633  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  rrx2vlinest  48669  rrx2linest  48670  line2  48680  itsclc0yqsollem1  48690  itsclc0yqsol  48692  itscnhlc0xyqsol  48693  itschlc0xyqsol1  48694  itschlc0xyqsol  48695  itsclc0xyqsolr  48697  2itscplem1  48706  2itscplem2  48707  2itscplem3  48708  itscnhlinecirc02plem1  48710  inlinecirc02plem  48714  sinhpcosh  49552  i2linesd  49591