Theorem subcld 11569

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

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098   − cmin 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-ltxr 11248  df-sub 11443

This theorem is referenced by:  subsubadd23  11621  addsubsub23  11622  pnpncand  11635  muleqadd  11858  lineq  12052  modmuladdnn0  13951  hashfz  14464  hashfzo  14466  hashf1lem2  14493  hashf1  14494  ccatswrd  14706  pfxccatin12lem2  14768  crre  15165  remim  15168  remullem  15179  abs3lem  15390  caubnd2  15409  bhmafibid1cn  15517  bhmafibid2cn  15518  bhmafibid2  15520  rlimuni  15601  climuni  15603  rlimcld2  15629  rlimrege0  15630  rlimrecl  15631  mulcn2  15647  reccn2  15648  cn1lem  15649  o1sub  15667  rlimo1  15668  o1dif  15681  rlimsqzlem  15700  caucvgrlem2  15726  iseralt  15736  fsumparts  15858  cvgcmpce  15870  incexclem  15890  arisum2  15915  geoserg  15920  pwdif  15922  geo2sum2  15928  fallfacfwd  16090  binomfallfaclem2  16094  bpolycl  16106  bpoly3  16112  bpoly4  16113  fsumcube  16114  sinf  16180  tanval2  16189  tanval3  16190  sinneg  16202  efival  16208  sinhval  16210  bitsinv1lem  16499  bitsres  16531  pythagtriplem1  16876  pythagtriplem14  16888  pythagtriplem17  16891  dvdsprmpweqle  16946  4sqlem5  17002  mul4sqlem  17013  4sqlem17  17021  vdwlem5  17045  vdwlem6  17046  vdwlem8  17048  blcvx  24924  recld2  24941  addcnlem  24991  cnllycmp  25084  cphipval2  25369  4cphipval2  25370  cphipval  25371  ipcnlem2  25372  rrxmval  25533  rrxmetlem  25535  pjthlem1  25565  ovollb2lem  25616  itgcnlem  25918  dvlem  26024  dvconst  26045  dvid  26046  dvcnp2  26048  dvaddbr  26066  dvmulbr  26067  dvcobr  26074  dvcjbr  26077  dvrec  26083  dvmptim  26098  dvcnvlem  26104  dveflem  26107  dvsincos  26109  cmvth  26119  dvlip  26121  dvlipcn  26122  c1liplem1  26124  dveq0  26128  dv11cn  26129  dvle  26135  lhop1lem  26141  dvfsumabs  26151  dvfsumlem1  26154  dvfsumlem2  26155  dvfsumrlim  26159  dvfsumrlim2  26160  ftc1lem4  26167  ftc1lem5  26168  ftc2  26172  dgrcolem2  26400  plydiveu  26428  aaliou2b  26471  taylfvallem1  26486  taylply2  26497  dvtaylp  26499  dvntaylp  26500  taylthlem1  26502  taylthlem2  26503  ulmbdd  26527  ulmcn  26528  ulmdvlem1  26529  mtest  26533  iblulm  26536  itgulm  26537  abelthlem9  26569  ptolemy  26627  tangtx  26636  sineq0  26655  efeq1  26659  efif1olem4  26676  tanarg  26750  logcnlem3  26775  logcnlem4  26776  advlogexp  26786  efopn  26789  cxpcn3lem  26878  cxpeq  26888  ang180lem4  26943  ang180lem5  26944  ang180  26945  isosctrlem2  26950  isosctrlem3  26951  isosctr  26952  ssscongptld  26953  affineequiv  26954  affineequiv2  26955  affineequiv3  26956  affineequiv4  26957  affineequivne  26958  angpieqvdlem  26959  angpieqvdlem2  26960  angpined  26961  angpieqvd  26962  chordthmlem  26963  chordthmlem2  26964  chordthmlem3  26965  chordthmlem4  26966  chordthmlem5  26967  heron  26969  quad2  26970  quad  26971  dcubic1lem  26974  dcubic  26977  mcubic  26978  cubic2  26979  cubic  26980  dquartlem1  26982  dquartlem2  26983  dquart  26984  quart1cl  26985  quart1lem  26986  quart1  26987  quartlem2  26989  quartlem4  26991  quart  26992  atanf  27011  sinasin  27020  asinsin  27023  atanneg  27038  atancj  27041  efiatan  27043  atanlogsub  27047  efiatan2  27048  2efiatan  27049  atanbndlem  27056  dvatan  27066  atantayl  27068  lgamgulmlem2  27160  lgamgulmlem3  27161  lgamgulmlem5  27163  lgamgulmlem6  27164  lgamgulm2  27166  lgamucov  27168  lgamcvg2  27185  gamcvg  27186  gamcvg2lem  27189  ftalem2  27204  logfacrlim  27354  logexprlim  27355  lgsdirprm  27461  gausslemma2dlem1a  27495  gausslemma2dlem4  27499  2sqmod  27566  addsq2nreurex  27574  vmadivsum  27612  rpvmasumlem  27617  dchrisumlem2  27620  dchrisumlem3  27621  dchrmusum2  27624  dchrvmasumlem2  27628  dchrvmasumlem3  27629  dchrvmasumiflem1  27631  rpvmasum2  27642  dchrisum0lem1b  27645  dchrisum0lem1  27646  dchrisum0lem2a  27647  rplogsum  27657  mudivsum  27660  mulogsumlem  27661  mulogsum  27662  mulog2sumlem1  27664  mulog2sumlem2  27665  mulog2sumlem3  27666  vmalogdivsum2  27668  vmalogdivsum  27669  2vmadivsumlem  27670  selberglem1  27675  selberglem2  27676  selberg2lem  27680  selberg2  27681  selberg3lem1  27687  selberg4lem1  27690  selberg4  27691  pntrsumo1  27695  selberg3r  27699  selberg34r  27701  pntrlog2bndlem1  27707  pntrlog2bndlem2  27708  pntrlog2bndlem3  27709  pntrlog2bndlem4  27710  pntrlog2bndlem5  27711  pntibndlem2  27721  pntlemf  27735  pntlemo  27737  ttgcontlem1  29175  brbtwn2  29196  colinearalglem1  29197  colinearalglem2  29198  colinearalg  29201  axsegconlem1  29208  ax5seglem1  29219  ax5seglem2  29220  ax5seglem6  29225  ax5seglem9  29228  axlowdimlem17  29249  axcontlem7  29261  axcontlem8  29262  clwlkclwwlk  30294  clwwlknonex2lem1  30399  2clwwlk2clwwlk  30642  numclwwlk3lem1  30674  smcnlem  30990  ipval2  31000  4ipval2  31001  dipcj  31007  pjhthlem1  31684  submuladdd  33026  binom2subadd  33027  pythagreim  33031  quad3d  33035  lt2addrd  33036  bcm1n  33081  cycpmco2lem5  33391  cycpmco2lem6  33392  vietalem  33914  constrrtll  34066  constrrtlc1  34067  constrrtcclem  34069  constrrtcc  34070  constrsslem  34076  constrconj  34080  constrfin  34081  constrelextdg2  34082  constraddcl  34097  iconstr  34101  constrremulcl  34102  constrrecl  34104  constrmulcl  34106  constrreinvcl  34107  constrresqrtcl  34112  cos9thpiminplylem2  34118  cos9thpiminplylem3  34119  sqsscirc2  34244  signslema  34894  circlemeth  34972  logdivsqrle  34982  revpfxsfxrev  35506  revwlk  35516  subfaclim  35579  divcnvlin  36124  iprodgam  36133  dnicld1  36950  dnibndlem2  36957  dnibndlem3  36958  dnibndlem6  36961  dnibndlem9  36964  dnibndlem10  36965  dnibndlem11  36966  unblimceq0  36985  unbdqndv2lem1  36987  unbdqndv2lem2  36988  knoppndvlem11  37000  knoppndvlem15  37004  knoppndvlem17  37006  knoppndvlem21  37010  bj-bary1lem  37842  bj-bary1lem1  37843  bj-bary1  37844  qdiff  37859  ftc1cnnclem  38230  ftc1anclem7  38238  ftc1anclem8  38239  ftc1anc  38240  ftc2nc  38241  areacirclem1  38247  areacirclem4  38250  areacirc  38252  cntotbnd  38335  lcmineqlem8  42693  lcmineqlem10  42695  lcmineqlem11  42696  lcmineqlem12  42697  lcmineqlem23  42708  aks4d1p1  42733  aks6d1c5lem1  42793  sticksstones10  42812  sticksstones12a  42814  sticksstones12  42815  sticksstones22  42825  bcle2d  42836  quadfac  42862  mvrrsubd  42925  lsubrotld  42928  lsubswap23d  42930  nicomachus  42963  sumcubes  42964  ef11d  42990  tanhalfpim  43000  sinpim  43001  cospim  43002  dffltz  43258  fltnltalem  43286  rencldnfilem  43439  pellexlem2  43449  pellexlem6  43453  pell1234qrne0  43472  pell1234qrmulcl  43474  rmyluc  43556  jm2.18  43607  jm2.19  43612  areaquad  43835  lhe4.4ex1a  44931  bcc0  44942  bccp1k  44943  bccm1k  44944  binomcxplemwb  44950  binomcxplemnn0  44951  binomcxplemrat  44952  binomcxplemfrat  44953  binomcxplemdvbinom  44955  binomcxplemnotnn0  44958  isosctrlem1ALT  45534  sineq0ALT  45537  oddfl  45889  dstregt0  45893  subadd4b  45894  sub31  45901  fzisoeu  45911  absnpncan2d  45913  absnpncan3d  45918  supxrgelem  45945  absimlere  46085  cvgcaule  46097  mullimc  46224  ellimcabssub0  46225  mullimcf  46231  limcrecl  46237  lptre2pt  46246  limcleqr  46250  neglimc  46253  addlimc  46254  0ellimcdiv  46255  limclner  46257  reclimc  46259  climleltrp  46282  climisp  46352  climxrrelem  46355  climxrre  46356  cnrefiisplem  46435  climxlim2lem  46451  fprodsubrecnncnvlem  46513  fperdvper  46525  dvdivbd  46529  dvbdfbdioolem2  46535  ioodvbdlimc1lem1  46537  volioc  46578  volico  46589  stoweidlem1  46607  stoweidlem11  46617  stoweidlem13  46619  stoweidlem26  46632  stoweid  46669  wallispi  46676  wallispi2lem1  46677  wallispi2lem2  46678  wallispi2  46679  stirlinglem1  46680  stirlinglem4  46683  stirlinglem5  46684  stirlinglem7  46686  stirlinglem11  46690  dirkertrigeqlem2  46705  fourierdlem4  46717  fourierdlem26  46739  fourierdlem30  46743  fourierdlem42  46755  fourierdlem63  46775  fourierdlem65  46777  fourierdlem72  46784  fourierdlem74  46786  fourierdlem75  46787  fourierdlem76  46788  fourierdlem80  46792  fourierdlem81  46793  fourierdlem89  46801  fourierdlem90  46802  fourierdlem91  46803  fourierdlem107  46819  fourierdlem109  46821  fouriersw  46837  etransclem1  46841  etransclem4  46844  etransclem8  46848  etransclem18  46858  etransclem20  46860  etransclem21  46861  etransclem23  46863  etransclem35  46875  etransclem46  46886  rrxtopnfi  46893  rrndistlt  46896  sge0gtfsumgt  47049  hoidmv1lelem2  47198  hoidmvlelem2  47202  smfmullem1  47397  sigarmf  47460  sigarms  47462  sigarexp  47465  sigardiv  47467  sigarcol  47470  sharhght  47471  sigaradd  47472  cevathlem2  47474  cevath  47475  sin5tlem3  47501  sin5tlem4  47502  sin5tlem5  47503  cos5t  47505  resubcnnred  47930  fldivmod  47970  ceildivmod  47971  fmtnorec2lem  48183  fmtnorec3  48189  fmtnorec4  48190  lighneallem3  48248  quad1  48274  requad01  48275  requad2  48277  fppr2odd  48385  dignn0flhalflem2  49281  affinecomb2  49368  1subrec1sub  49370  eenglngeehlnmlem1  49402  eenglngeehlnmlem2  49403  rrx2vlinest  49406  rrx2linest  49407  line2  49417  itsclc0yqsollem1  49427  itsclc0yqsol  49429  itscnhlc0xyqsol  49430  itschlc0xyqsol1  49431  itschlc0xyqsol  49432  itsclc0xyqsolr  49434  2itscplem1  49443  2itscplem2  49444  2itscplem3  49445  itscnhlinecirc02plem1  49447  inlinecirc02plem  49451  sinhpcosh  50403  i2linesd  50442