MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  expcl Structured version   Unicode version

Theorem expcl 12166
Description: Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.)
Assertion
Ref Expression
expcl  |-  ( ( A  e.  CC  /\  N  e.  NN0 )  -> 
( A ^ N
)  e.  CC )

Proof of Theorem expcl
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3508 . 2  |-  CC  C_  CC
2 mulcl 9579 . 2  |-  ( ( x  e.  CC  /\  y  e.  CC )  ->  ( x  x.  y
)  e.  CC )
3 ax-1cn 9553 . 2  |-  1  e.  CC
41, 2, 3expcllem 12159 1  |-  ( ( A  e.  CC  /\  N  e.  NN0 )  -> 
( A ^ N
)  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804  (class class class)co 6281   CCcc 9493   NN0cn0 10802   ^cexp 12148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-2nd 6786  df-recs 7044  df-rdg 7078  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10544  df-n0 10803  df-z 10872  df-uz 11093  df-seq 12090  df-exp 12149
This theorem is referenced by:  expeq0  12178  expnegz  12182  mulexp  12187  mulexpz  12188  expadd  12190  expaddzlem  12191  expaddz  12192  expmul  12193  expmulz  12194  expdiv  12198  binom3  12269  digit2  12281  digit1  12282  expcld  12292  faclbnd2  12351  faclbnd4lem4  12356  faclbnd6  12359  cjexp  12965  absexp  13119  ackbijnn  13622  binomlem  13623  binom1p  13625  binom1dif  13627  expcnv  13657  geolim  13661  geolim2  13662  geo2sum  13664  geomulcvg  13667  geoisum  13668  geoisumr  13669  geoisum1  13670  geoisum1c  13671  0.999...  13672  eftcl  13791  eftabs  13793  efcllem  13795  efcj  13809  efaddlem  13810  eflegeo  13838  efi4p  13854  prmreclem6  14421  decsplit  14551  karatsuba  14552  expmhm  18464  mbfi1fseqlem6  22105  itg0  22164  itgz  22165  itgcl  22168  itgcnlem  22174  itgsplit  22220  dvexp  22334  dvexp3  22357  plyf  22573  ply1termlem  22578  plypow  22580  plyeq0lem  22585  plypf1  22587  plyaddlem1  22588  plymullem1  22589  coeeulem  22599  coeidlem  22612  coeid3  22615  plyco  22616  dgrcolem2  22649  plycjlem  22651  plyrecj  22654  vieta1  22686  elqaalem3  22695  aareccl  22700  aalioulem1  22706  geolim3  22713  psergf  22785  dvradcnv  22794  psercn2  22796  pserdvlem2  22801  pserdv2  22803  abelthlem4  22807  abelthlem5  22808  abelthlem6  22809  abelthlem7  22811  abelthlem9  22813  advlogexp  23014  logtayllem  23018  logtayl  23019  logtaylsum  23020  logtayl2  23021  cxpeq  23109  dcubic1lem  23152  dcubic2  23153  dcubic1  23154  dcubic  23155  mcubic  23156  cubic2  23157  cubic  23158  binom4  23159  dquartlem2  23161  dquart  23162  quart1cl  23163  quart1lem  23164  quart1  23165  quartlem1  23166  quartlem2  23167  quart  23170  atantayl  23246  atantayl2  23247  atantayl3  23248  leibpi  23251  log2cnv  23253  log2tlbnd  23254  log2ublem3  23257  ftalem1  23324  ftalem4  23327  ftalem5  23328  basellem3  23334  musum  23445  1sgmprm  23452  perfect  23484  lgsquadlem1  23607  rplogsumlem2  23648  ostth2lem2  23797  numclwlk3lem3  25051  ipval2  25595  dipcl  25603  dipcn  25611  sspival  25629  subfacval2  28609  fallrisefac  29123  0risefac  29136  binomrisefac  29140  bpolysum  29791  bpolydiflem  29792  fsumkthpow  29794  bpoly3  29796  bpoly4  29797  fsumcube  29798  jm2.23  30914  lhe4.4ex1a  31210  altgsumbc  32809  altgsumbcALT  32810
  Copyright terms: Public domain W3C validator