MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subcld Structured version   Visualization version   GIF version

Theorem subcld 10244
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
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 pncand.2 . 2 (𝜑𝐵 ∈ ℂ)
3 subcl 10132 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) ∈ ℂ)
41, 2, 3syl2anc 690 1 (𝜑 → (𝐴𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6527  cc 9791  cmin 10118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-ltxr 9936  df-sub 10120
This theorem is referenced by:  pnpncand  10304  subdir2d  10340  muleqadd  10523  modmuladdnn0  12534  hashfz  13029  hashfzo  13031  hashf1lem2  13052  hashf1  13053  ccatswrd  13257  crre  13651  remim  13654  remullem  13665  abs3lem  13875  caubnd2  13894  rlimuni  14078  climuni  14080  rlimcld2  14106  rlimrege0  14107  rlimrecl  14108  mulcn2  14123  reccn2  14124  cn1lem  14125  o1sub  14143  rlimo1  14144  o1dif  14157  rlimsqzlem  14176  caucvgrlem2  14202  iseralt  14212  fsumparts  14328  cvgcmpce  14340  incexclem  14356  arisum2  14381  geoserg  14386  geo2sum2  14393  fallfacfwd  14555  binomfallfaclem2  14559  bpolycl  14571  bpoly3  14577  bpoly4  14578  fsumcube  14579  sinf  14642  tanval2  14651  tanval3  14652  sinneg  14664  efival  14670  sinhval  14672  bitsinv1lem  14950  bitsres  14982  pythagtriplem1  15308  pythagtriplem14  15320  pythagtriplem17  15323  dvdsprmpweqle  15377  4sqlem5  15433  mul4sqlem  15444  4sqlem17  15452  vdwlem5  15476  vdwlem6  15477  vdwlem8  15479  blcvx  22357  recld2  22373  addcnlem  22423  cnllycmp  22511  cphipval2  22793  4cphipval2  22794  cphipval  22795  ipcnlem2  22796  rrxmval  22941  rrxmetlem  22943  pjthlem1  22961  ovollb2lem  23008  itgcnlem  23307  dvlem  23411  dvconst  23431  dvid  23432  dvcnp2  23434  dvaddbr  23452  dvmulbr  23453  dvcobr  23460  dvcjbr  23463  dvrec  23469  dvmptim  23484  dvcnvlem  23488  dveflem  23491  dvsincos  23493  cmvth  23503  dvlip  23505  dvlipcn  23506  c1liplem1  23508  dveq0  23512  dv11cn  23513  dvle  23519  lhop1lem  23525  dvfsumabs  23535  dvfsumlem1  23538  dvfsumlem2  23539  dvfsumrlim  23543  dvfsumrlim2  23544  ftc1lem4  23551  ftc1lem5  23552  ftc2  23556  dgrcolem2  23779  plydiveu  23802  aaliou2b  23845  taylfvallem1  23860  taylply2  23871  dvtaylp  23873  dvntaylp  23874  taylthlem1  23876  taylthlem2  23877  ulmbdd  23901  ulmcn  23902  ulmdvlem1  23903  mtest  23907  iblulm  23910  itgulm  23911  abelthlem9  23943  ptolemy  23997  tangtx  24006  sineq0  24022  efeq1  24024  efif1olem4  24040  tanarg  24114  logcnlem3  24135  logcnlem4  24136  advlogexp  24146  efopn  24149  cxpcn3lem  24233  cxpeq  24243  ang180lem4  24287  ang180lem5  24288  ang180  24289  isosctrlem2  24294  isosctrlem3  24295  isosctr  24296  ssscongptld  24297  affineequiv  24298  affineequiv2  24299  angpieqvdlem  24300  angpieqvdlem2  24301  angpined  24302  angpieqvd  24303  chordthmlem  24304  chordthmlem2  24305  chordthmlem3  24306  chordthmlem4  24307  chordthmlem5  24308  heron  24310  quad2  24311  quad  24312  dcubic1lem  24315  dcubic  24318  mcubic  24319  cubic2  24320  cubic  24321  dquartlem1  24323  dquartlem2  24324  dquart  24325  quart1cl  24326  quart1lem  24327  quart1  24328  quartlem2  24330  quartlem4  24332  quart  24333  atanf  24352  sinasin  24361  asinsin  24364  atanneg  24379  atancj  24382  efiatan  24384  atanlogsub  24388  efiatan2  24389  2efiatan  24390  atanbndlem  24397  dvatan  24407  atantayl  24409  lgamgulmlem2  24501  lgamgulmlem3  24502  lgamgulmlem5  24504  lgamgulmlem6  24505  lgamgulm2  24507  lgamucov  24509  lgamcvg2  24526  gamcvg  24527  gamcvg2lem  24530  ftalem2  24545  logfacrlim  24694  logexprlim  24695  lgsdirprm  24801  gausslemma2dlem1a  24835  gausslemma2dlem4  24839  vmadivsum  24916  rpvmasumlem  24921  dchrisumlem2  24924  dchrisumlem3  24925  dchrmusum2  24928  dchrvmasumlem2  24932  dchrvmasumlem3  24933  dchrvmasumiflem1  24935  rpvmasum2  24946  dchrisum0lem1b  24949  dchrisum0lem1  24950  dchrisum0lem2a  24951  rplogsum  24961  mudivsum  24964  mulogsumlem  24965  mulogsum  24966  mulog2sumlem1  24968  mulog2sumlem2  24969  mulog2sumlem3  24970  vmalogdivsum2  24972  vmalogdivsum  24973  2vmadivsumlem  24974  selberglem1  24979  selberglem2  24980  selberg2lem  24984  selberg2  24985  selberg3lem1  24991  selberg4lem1  24994  selberg4  24995  pntrsumo1  24999  selberg3r  25003  selberg34r  25005  pntrlog2bndlem1  25011  pntrlog2bndlem2  25012  pntrlog2bndlem3  25013  pntrlog2bndlem4  25014  pntrlog2bndlem5  25015  pntibndlem2  25025  pntlemf  25039  pntlemo  25041  ttgcontlem1  25511  brbtwn2  25531  colinearalglem1  25532  colinearalglem2  25533  colinearalg  25536  axsegconlem1  25543  ax5seglem2  25555  ax5seglem6  25560  ax5seglem9  25563  axlowdimlem17  25584  axcontlem7  25596  axcontlem8  25597  cusgrasizeinds  25798  clwlkisclwwlk  26111  frghash2spot  26384  usgreghash2spotv  26387  frgregordn0  26391  numclwlk3lem3  26394  numclwlk1lem2fo  26416  smcnlem  26765  ipval2  26775  4ipval2  26776  4ipval3  26780  dipcj  26785  pjhthlem1  27468  lt2addrd  28737  bcm1n  28775  bhmafibid2  28810  2sqmod  28813  sqsscirc2  29117  signslema  29799  subfaclim  30258  divcnvlin  30705  iprodgam  30715  dnicld1  31466  dnibndlem2  31473  dnibndlem3  31474  dnibndlem6  31477  dnibndlem9  31480  dnibndlem10  31481  dnibndlem11  31482  unblimceq0  31502  unbdqndv2lem1  31504  unbdqndv2lem2  31505  knoppndvlem11  31517  knoppndvlem15  31521  knoppndvlem17  31523  knoppndvlem21  31527  bj-lineq  32159  bj-bary1lem  32161  bj-bary1lem1  32162  bj-bary1  32163  ftc1cnnclem  32477  ftc1anclem7  32485  ftc1anclem8  32486  ftc1anc  32487  ftc2nc  32488  areacirclem1  32494  areacirclem4  32497  areacirc  32499  cntotbnd  32589  rencldnfilem  36226  pellexlem2  36236  pellexlem6  36240  pell1234qrne0  36259  pell1234qrmulcl  36261  rmyluc  36344  jm2.18  36397  jm2.19  36402  areaquad  36645  lhe4.4ex1a  37374  bcc0  37385  bccp1k  37386  bccm1k  37387  binomcxplemwb  37393  binomcxplemnn0  37394  binomcxplemrat  37395  binomcxplemfrat  37396  binomcxplemdvbinom  37398  binomcxplemnotnn0  37401  isosctrlem1ALT  38016  sineq0ALT  38019  oddfl  38254  dstregt0  38258  subadd4b  38259  sub31  38268  fzisoeu  38279  absnpncan2d  38281  absnpncan3d  38286  supxrgelem  38318  mullimc  38507  ellimcabssub0  38508  mullimcf  38514  limcrecl  38520  lptre2pt  38531  limcleqr  38535  neglimc  38538  addlimc  38539  0ellimcdiv  38540  limclner  38542  reclimc  38544  climleltrp  38567  fprodsubrecnncnvlem  38618  fperdvper  38632  dvdivbd  38637  dvbdfbdioolem2  38643  ioodvbdlimc1lem1  38645  volioc  38688  volico  38700  stoweidlem1  38718  stoweidlem11  38728  stoweidlem13  38730  stoweidlem26  38743  stoweid  38780  wallispi  38787  wallispi2lem1  38788  wallispi2lem2  38789  wallispi2  38790  stirlinglem1  38791  stirlinglem4  38794  stirlinglem5  38795  stirlinglem7  38797  stirlinglem11  38801  dirkertrigeqlem2  38816  fourierdlem4  38828  fourierdlem26  38850  fourierdlem30  38854  fourierdlem42  38866  fourierdlem63  38886  fourierdlem65  38888  fourierdlem72  38895  fourierdlem74  38897  fourierdlem75  38898  fourierdlem76  38899  fourierdlem80  38903  fourierdlem81  38904  fourierdlem89  38912  fourierdlem90  38913  fourierdlem91  38914  fourierdlem107  38930  fourierdlem109  38932  fouriersw  38948  etransclem1  38952  etransclem4  38955  etransclem8  38959  etransclem18  38969  etransclem20  38971  etransclem21  38972  etransclem23  38974  etransclem35  38986  etransclem46  38997  rrxtopnfi  39006  rrndistlt  39010  sge0gtfsumgt  39160  hoidmv1lelem2  39306  hoidmvlelem2  39310  smfmullem1  39500  sigarmf  39516  sigarms  39518  sigarexp  39521  sigardiv  39523  sigarcol  39526  sharhght  39527  sigaradd  39528  cevathlem2  39530  cevath  39531  fmtnorec2lem  39817  fmtnorec3  39823  fmtnorec4  39824  pwdif  39864  lighneallem3  39887  pfxccatin12lem2  40112  clwlkclwwlk  41233  frgrhash2wsp  41519  fusgreghash2wspv  41521  frrusgrord0  41525  av-numclwlk3lem3  41528  av-numclwlk1lem2fo  41547  fldivmod  42129  dignn0flhalflem2  42230  sinhpcosh  42263  i2linesd  42317
  Copyright terms: Public domain W3C validator