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

Theorem subcld 10430
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 10318 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) ∈ ℂ)
41, 2, 3syl2anc 694 1 (𝜑 → (𝐴𝐵) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  (class class class)co 6690  cc 9972  cmin 10304
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-ltxr 10117  df-sub 10306
This theorem is referenced by:  pnpncand  10490  subdir2d  10526  muleqadd  10709  modmuladdnn0  12754  hashfz  13252  hashfzo  13254  hashf1lem2  13278  hashf1  13279  ccatswrd  13502  crre  13898  remim  13901  remullem  13912  abs3lem  14122  caubnd2  14141  rlimuni  14325  climuni  14327  rlimcld2  14353  rlimrege0  14354  rlimrecl  14355  mulcn2  14370  reccn2  14371  cn1lem  14372  o1sub  14390  rlimo1  14391  o1dif  14404  rlimsqzlem  14423  caucvgrlem2  14449  iseralt  14459  fsumparts  14582  cvgcmpce  14594  incexclem  14612  arisum2  14637  geoserg  14642  geo2sum2  14649  fallfacfwd  14811  binomfallfaclem2  14815  bpolycl  14827  bpoly3  14833  bpoly4  14834  fsumcube  14835  sinf  14898  tanval2  14907  tanval3  14908  sinneg  14920  efival  14926  sinhval  14928  bitsinv1lem  15210  bitsres  15242  pythagtriplem1  15568  pythagtriplem14  15580  pythagtriplem17  15583  dvdsprmpweqle  15637  4sqlem5  15693  mul4sqlem  15704  4sqlem17  15712  vdwlem5  15736  vdwlem6  15737  vdwlem8  15739  blcvx  22648  recld2  22664  addcnlem  22714  cnllycmp  22802  cphipval2  23086  4cphipval2  23087  cphipval  23088  ipcnlem2  23089  rrxmval  23234  rrxmetlem  23236  pjthlem1  23254  ovollb2lem  23302  itgcnlem  23601  dvlem  23705  dvconst  23725  dvid  23726  dvcnp2  23728  dvaddbr  23746  dvmulbr  23747  dvcobr  23754  dvcjbr  23757  dvrec  23763  dvmptim  23778  dvcnvlem  23784  dveflem  23787  dvsincos  23789  cmvth  23799  dvlip  23801  dvlipcn  23802  c1liplem1  23804  dveq0  23808  dv11cn  23809  dvle  23815  lhop1lem  23821  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem2  23835  dvfsumrlim  23839  dvfsumrlim2  23840  ftc1lem4  23847  ftc1lem5  23848  ftc2  23852  dgrcolem2  24075  plydiveu  24098  aaliou2b  24141  taylfvallem1  24156  taylply2  24167  dvtaylp  24169  dvntaylp  24170  taylthlem1  24172  taylthlem2  24173  ulmbdd  24197  ulmcn  24198  ulmdvlem1  24199  mtest  24203  iblulm  24206  itgulm  24207  abelthlem9  24239  ptolemy  24293  tangtx  24302  sineq0  24318  efeq1  24320  efif1olem4  24336  tanarg  24410  logcnlem3  24435  logcnlem4  24436  advlogexp  24446  efopn  24449  cxpcn3lem  24533  cxpeq  24543  ang180lem4  24587  ang180lem5  24588  ang180  24589  isosctrlem2  24594  isosctrlem3  24595  isosctr  24596  ssscongptld  24597  affineequiv  24598  affineequiv2  24599  angpieqvdlem  24600  angpieqvdlem2  24601  angpined  24602  angpieqvd  24603  chordthmlem  24604  chordthmlem2  24605  chordthmlem3  24606  chordthmlem4  24607  chordthmlem5  24608  heron  24610  quad2  24611  quad  24612  dcubic1lem  24615  dcubic  24618  mcubic  24619  cubic2  24620  cubic  24621  dquartlem1  24623  dquartlem2  24624  dquart  24625  quart1cl  24626  quart1lem  24627  quart1  24628  quartlem2  24630  quartlem4  24632  quart  24633  atanf  24652  sinasin  24661  asinsin  24664  atanneg  24679  atancj  24682  efiatan  24684  atanlogsub  24688  efiatan2  24689  2efiatan  24690  atanbndlem  24697  dvatan  24707  atantayl  24709  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem5  24804  lgamgulmlem6  24805  lgamgulm2  24807  lgamucov  24809  lgamcvg2  24826  gamcvg  24827  gamcvg2lem  24830  ftalem2  24845  logfacrlim  24994  logexprlim  24995  lgsdirprm  25101  gausslemma2dlem1a  25135  gausslemma2dlem4  25139  vmadivsum  25216  rpvmasumlem  25221  dchrisumlem2  25224  dchrisumlem3  25225  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumlem3  25233  dchrvmasumiflem1  25235  rpvmasum2  25246  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  rplogsum  25261  mudivsum  25264  mulogsumlem  25265  mulogsum  25266  mulog2sumlem1  25268  mulog2sumlem2  25269  mulog2sumlem3  25270  vmalogdivsum2  25272  vmalogdivsum  25273  2vmadivsumlem  25274  selberglem1  25279  selberglem2  25280  selberg2lem  25284  selberg2  25285  selberg3lem1  25291  selberg4lem1  25294  selberg4  25295  pntrsumo1  25299  selberg3r  25303  selberg34r  25305  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntibndlem2  25325  pntlemf  25339  pntlemo  25341  ttgcontlem1  25810  brbtwn2  25830  colinearalglem1  25831  colinearalglem2  25832  colinearalg  25835  axsegconlem1  25842  ax5seglem2  25854  ax5seglem6  25859  ax5seglem9  25862  axlowdimlem17  25883  axcontlem7  25895  axcontlem8  25896  clwlkclwwlk  26968  clwwlknonex2lem1  27082  numclwlk3lem3  27322  2clwwlk2clwwlklem2lem2  27329  2clwwlk2clwwlk  27338  smcnlem  27680  ipval2  27690  4ipval2  27691  dipcj  27697  pjhthlem1  28378  lt2addrd  29644  bcm1n  29682  bhmafibid2  29773  2sqmod  29776  sqsscirc2  30083  signslema  30767  circlemeth  30846  logdivsqrle  30856  subfaclim  31296  divcnvlin  31744  iprodgam  31754  dnicld1  32587  dnibndlem2  32594  dnibndlem3  32595  dnibndlem6  32598  dnibndlem9  32601  dnibndlem10  32602  dnibndlem11  32603  unblimceq0  32623  unbdqndv2lem1  32625  unbdqndv2lem2  32626  knoppndvlem11  32638  knoppndvlem15  32642  knoppndvlem17  32644  knoppndvlem21  32648  bj-lineq  33288  bj-bary1lem  33290  bj-bary1lem1  33291  bj-bary1  33292  ftc1cnnclem  33613  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  ftc2nc  33624  areacirclem1  33630  areacirclem4  33633  areacirc  33635  cntotbnd  33725  rencldnfilem  37701  pellexlem2  37711  pellexlem6  37715  pell1234qrne0  37734  pell1234qrmulcl  37736  rmyluc  37819  jm2.18  37872  jm2.19  37877  areaquad  38119  lhe4.4ex1a  38845  bcc0  38856  bccp1k  38857  bccm1k  38858  binomcxplemwb  38864  binomcxplemnn0  38865  binomcxplemrat  38866  binomcxplemfrat  38867  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  isosctrlem1ALT  39484  sineq0ALT  39487  oddfl  39803  dstregt0  39807  subadd4b  39808  sub31  39817  fzisoeu  39828  absnpncan2d  39830  absnpncan3d  39835  supxrgelem  39866  absimlere  40023  mullimc  40166  ellimcabssub0  40167  mullimcf  40173  limcrecl  40179  lptre2pt  40190  limcleqr  40194  neglimc  40197  addlimc  40198  0ellimcdiv  40199  limclner  40201  reclimc  40203  climleltrp  40226  climisp  40296  climxrrelem  40299  climxrre  40300  cnrefiisplem  40373  climxlim2lem  40389  fprodsubrecnncnvlem  40439  fperdvper  40451  dvdivbd  40456  dvbdfbdioolem2  40462  ioodvbdlimc1lem1  40464  volioc  40506  volico  40518  stoweidlem1  40536  stoweidlem11  40546  stoweidlem13  40548  stoweidlem26  40561  stoweid  40598  wallispi  40605  wallispi2lem1  40606  wallispi2lem2  40607  wallispi2  40608  stirlinglem1  40609  stirlinglem4  40612  stirlinglem5  40613  stirlinglem7  40615  stirlinglem11  40619  dirkertrigeqlem2  40634  fourierdlem4  40646  fourierdlem26  40668  fourierdlem30  40672  fourierdlem42  40684  fourierdlem63  40704  fourierdlem65  40706  fourierdlem72  40713  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem80  40721  fourierdlem81  40722  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem107  40748  fourierdlem109  40750  fouriersw  40766  etransclem1  40770  etransclem4  40773  etransclem8  40777  etransclem18  40787  etransclem20  40789  etransclem21  40790  etransclem23  40792  etransclem35  40804  etransclem46  40815  rrxtopnfi  40824  rrndistlt  40828  sge0gtfsumgt  40978  hoidmv1lelem2  41127  hoidmvlelem2  41131  smfmullem1  41319  sigarmf  41364  sigarms  41366  sigarexp  41369  sigardiv  41371  sigarcol  41374  sharhght  41375  sigaradd  41376  cevathlem2  41378  cevath  41379  pfxccatin12lem2  41749  fmtnorec2lem  41779  fmtnorec3  41785  fmtnorec4  41786  pwdif  41826  lighneallem3  41849  fldivmod  42638  dignn0flhalflem2  42735  sinhpcosh  42809  i2linesd  42853
  Copyright terms: Public domain W3C validator