Theorem subcld 10800

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

Syntax hints:   → wi 4   ∈ wcel 2050  (class class class)co 6978  ℂcc 10335   − cmin 10672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-po 5327  df-so 5328  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-riota 6939  df-ov 6981  df-oprab 6982  df-mpo 6983  df-er 8091  df-en 8309  df-dom 8310  df-sdom 8311  df-pnf 10478  df-mnf 10479  df-ltxr 10481  df-sub 10674

This theorem is referenced by:  pnpncand  10864  muleqadd  11087  lineq  11280  modmuladdnn0  13101  hashfz  13604  hashfzo  13606  hashf1lem2  13630  hashf1  13631  ccatswrd  13852  pfxccatin12lem2  13934  crre  14337  remim  14340  remullem  14351  abs3lem  14562  caubnd2  14581  bhmafibid1cn  14687  bhmafibid2cn  14688  bhmafibid2  14690  rlimuni  14771  climuni  14773  rlimcld2  14799  rlimrege0  14800  rlimrecl  14801  mulcn2  14816  reccn2  14817  cn1lem  14818  o1sub  14836  rlimo1  14837  o1dif  14850  rlimsqzlem  14869  caucvgrlem2  14895  iseralt  14905  fsumparts  15024  cvgcmpce  15036  incexclem  15054  arisum2  15079  geoserg  15084  pwdif  15086  geo2sum2  15093  fallfacfwd  15253  binomfallfaclem2  15257  bpolycl  15269  bpoly3  15275  bpoly4  15276  fsumcube  15277  sinf  15340  tanval2  15349  tanval3  15350  sinneg  15362  efival  15368  sinhval  15370  bitsinv1lem  15653  bitsres  15685  pythagtriplem1  16012  pythagtriplem14  16024  pythagtriplem17  16027  dvdsprmpweqle  16081  4sqlem5  16137  mul4sqlem  16148  4sqlem17  16156  vdwlem5  16180  vdwlem6  16181  vdwlem8  16183  blcvx  23112  recld2  23128  addcnlem  23178  cnllycmp  23266  cphipval2  23550  4cphipval2  23551  cphipval  23552  ipcnlem2  23553  rrxmval  23714  rrxmetlem  23716  pjthlem1  23746  ovollb2lem  23795  itgcnlem  24096  dvlem  24200  dvconst  24220  dvid  24221  dvcnp2  24223  dvaddbr  24241  dvmulbr  24242  dvcobr  24249  dvcjbr  24252  dvrec  24258  dvmptim  24273  dvcnvlem  24279  dveflem  24282  dvsincos  24284  cmvth  24294  dvlip  24296  dvlipcn  24297  c1liplem1  24299  dveq0  24303  dv11cn  24304  dvle  24310  lhop1lem  24316  dvfsumabs  24326  dvfsumlem1  24329  dvfsumlem2  24330  dvfsumrlim  24334  dvfsumrlim2  24335  ftc1lem4  24342  ftc1lem5  24343  ftc2  24347  dgrcolem2  24570  plydiveu  24593  aaliou2b  24636  taylfvallem1  24651  taylply2  24662  dvtaylp  24664  dvntaylp  24665  taylthlem1  24667  taylthlem2  24668  ulmbdd  24692  ulmcn  24693  ulmdvlem1  24694  mtest  24698  iblulm  24701  itgulm  24702  abelthlem9  24734  ptolemy  24788  tangtx  24797  sineq0  24815  efeq1  24817  efif1olem4  24833  tanarg  24906  logcnlem3  24931  logcnlem4  24932  advlogexp  24942  efopn  24945  cxpcn3lem  25032  cxpeq  25042  ang180lem4  25094  ang180lem5  25095  ang180  25096  isosctrlem2  25101  isosctrlem3  25102  isosctr  25103  ssscongptld  25104  affineequiv  25105  affineequiv2  25106  affineequiv3  25107  affineequiv4  25108  affineequivne  25109  angpieqvdlem  25110  angpieqvdlem2  25111  angpined  25112  angpieqvd  25113  chordthmlem  25114  chordthmlem2  25115  chordthmlem3  25116  chordthmlem4  25117  chordthmlem5  25118  heron  25120  quad2  25121  quad  25122  dcubic1lem  25125  dcubic  25128  mcubic  25129  cubic2  25130  cubic  25131  dquartlem1  25133  dquartlem2  25134  dquart  25135  quart1cl  25136  quart1lem  25137  quart1  25138  quartlem2  25140  quartlem4  25142  quart  25143  atanf  25162  sinasin  25171  asinsin  25174  atanneg  25189  atancj  25192  efiatan  25194  atanlogsub  25198  efiatan2  25199  2efiatan  25200  atanbndlem  25207  dvatan  25217  atantayl  25219  lgamgulmlem2  25312  lgamgulmlem3  25313  lgamgulmlem5  25315  lgamgulmlem6  25316  lgamgulm2  25318  lgamucov  25320  lgamcvg2  25337  gamcvg  25338  gamcvg2lem  25341  ftalem2  25356  logfacrlim  25505  logexprlim  25506  lgsdirprm  25612  gausslemma2dlem1a  25646  gausslemma2dlem4  25650  2sqmod  25717  addsq2nreurex  25725  vmadivsum  25763  rpvmasumlem  25768  dchrisumlem2  25771  dchrisumlem3  25772  dchrmusum2  25775  dchrvmasumlem2  25779  dchrvmasumlem3  25780  dchrvmasumiflem1  25782  rpvmasum2  25793  dchrisum0lem1b  25796  dchrisum0lem1  25797  dchrisum0lem2a  25798  rplogsum  25808  mudivsum  25811  mulogsumlem  25812  mulogsum  25813  mulog2sumlem1  25815  mulog2sumlem2  25816  mulog2sumlem3  25817  vmalogdivsum2  25819  vmalogdivsum  25820  2vmadivsumlem  25821  selberglem1  25826  selberglem2  25827  selberg2lem  25831  selberg2  25832  selberg3lem1  25838  selberg4lem1  25841  selberg4  25842  pntrsumo1  25846  selberg3r  25850  selberg34r  25852  pntrlog2bndlem1  25858  pntrlog2bndlem2  25859  pntrlog2bndlem3  25860  pntrlog2bndlem4  25861  pntrlog2bndlem5  25862  pntibndlem2  25872  pntlemf  25886  pntlemo  25888  ttgcontlem1  26377  brbtwn2  26397  colinearalglem1  26398  colinearalglem2  26399  colinearalg  26402  axsegconlem1  26409  ax5seglem1  26420  ax5seglem2  26421  ax5seglem6  26426  ax5seglem9  26429  axlowdimlem17  26450  axcontlem7  26462  axcontlem8  26463  clwlkclwwlk  27511  clwlkclwwlkOLD  27512  clwwlknonex2lem1  27638  2clwwlk2clwwlk  27890  2clwwlk2clwwlkOLD  27891  numclwwlk3lem1  27942  smcnlem  28254  ipval2  28264  4ipval2  28265  dipcj  28271  pjhthlem1  28952  lt2addrd  30230  bcm1n  30270  sqsscirc2  30796  signslema  31478  circlemeth  31559  logdivsqrle  31569  subfaclim  32020  divcnvlin  32484  iprodgam  32494  dnicld1  33331  dnibndlem2  33338  dnibndlem3  33339  dnibndlem6  33342  dnibndlem9  33345  dnibndlem10  33346  dnibndlem11  33347  unblimceq0  33366  unbdqndv2lem1  33368  unbdqndv2lem2  33369  knoppndvlem11  33381  knoppndvlem15  33385  knoppndvlem17  33387  knoppndvlem21  33391  bj-bary1lem  34039  bj-bary1lem1  34040  bj-bary1  34041  ftc1cnnclem  34406  ftc1anclem7  34414  ftc1anclem8  34415  ftc1anc  34416  ftc2nc  34417  areacirclem1  34423  areacirclem4  34426  areacirc  34428  cntotbnd  34516  dffltz  38678  fltnltalem  38681  rencldnfilem  38813  pellexlem2  38823  pellexlem6  38827  pell1234qrne0  38846  pell1234qrmulcl  38848  rmyluc  38930  jm2.18  38981  jm2.19  38986  areaquad  39219  lhe4.4ex1a  40077  bcc0  40088  bccp1k  40089  bccm1k  40090  binomcxplemwb  40096  binomcxplemnn0  40097  binomcxplemrat  40098  binomcxplemfrat  40099  binomcxplemdvbinom  40101  binomcxplemnotnn0  40104  isosctrlem1ALT  40687  sineq0ALT  40690  oddfl  40973  dstregt0  40977  subadd4b  40978  sub31  40987  fzisoeu  40997  absnpncan2d  40999  absnpncan3d  41004  supxrgelem  41035  absimlere  41188  mullimc  41329  ellimcabssub0  41330  mullimcf  41336  limcrecl  41342  lptre2pt  41353  limcleqr  41357  neglimc  41360  addlimc  41361  0ellimcdiv  41362  limclner  41364  reclimc  41366  climleltrp  41389  climisp  41459  climxrrelem  41462  climxrre  41463  cnrefiisplem  41542  climxlim2lem  41558  fprodsubrecnncnvlem  41622  fperdvper  41634  dvdivbd  41639  dvbdfbdioolem2  41645  ioodvbdlimc1lem1  41647  volioc  41688  volico  41700  stoweidlem1  41718  stoweidlem11  41728  stoweidlem13  41730  stoweidlem26  41743  stoweid  41780  wallispi  41787  wallispi2lem1  41788  wallispi2lem2  41789  wallispi2  41790  stirlinglem1  41791  stirlinglem4  41794  stirlinglem5  41795  stirlinglem7  41797  stirlinglem11  41801  dirkertrigeqlem2  41816  fourierdlem4  41828  fourierdlem26  41850  fourierdlem30  41854  fourierdlem42  41866  fourierdlem63  41886  fourierdlem65  41888  fourierdlem72  41895  fourierdlem74  41897  fourierdlem75  41898  fourierdlem76  41899  fourierdlem80  41903  fourierdlem81  41904  fourierdlem89  41912  fourierdlem90  41913  fourierdlem91  41914  fourierdlem107  41930  fourierdlem109  41932  fouriersw  41948  etransclem1  41952  etransclem4  41955  etransclem8  41959  etransclem18  41969  etransclem20  41971  etransclem21  41972  etransclem23  41974  etransclem35  41986  etransclem46  41997  rrxtopnfi  42004  rrndistlt  42007  sge0gtfsumgt  42157  hoidmv1lelem2  42306  hoidmvlelem2  42310  smfmullem1  42498  sigarmf  42543  sigarms  42545  sigarexp  42548  sigardiv  42550  sigarcol  42553  sharhght  42554  sigaradd  42555  cevathlem2  42557  cevath  42558  resubcnnred  42911  fmtnorec2lem  43073  fmtnorec3  43079  fmtnorec4  43080  lighneallem3  43141  quad1  43154  requad01  43155  requad2  43157  fppr2odd  43265  fldivmod  43947  dignn0flhalflem2  44045  affinecomb2  44059  1subrec1sub  44061  eenglngeehlnmlem1  44093  eenglngeehlnmlem2  44094  rrx2vlinest  44097  rrx2linest  44098  line2  44108  itsclc0yqsollem1  44118  itsclc0yqsol  44120  itscnhlc0xyqsol  44121  itschlc0xyqsol1  44122  itschlc0xyqsol  44123  itsclc0xyqsolr  44125  2itscplem1  44134  2itscplem2  44135  2itscplem3  44136  itscnhlinecirc02plem1  44138  inlinecirc02plem  44142  sinhpcosh  44207  i2linesd  44248