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

Theorem expcld 14057
Description: Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
Hypotheses
Ref Expression
expcld.1 (𝜑𝐴 ∈ ℂ)
expcld.2 (𝜑𝑁 ∈ ℕ0)
Assertion
Ref Expression
expcld (𝜑 → (𝐴𝑁) ∈ ℂ)

Proof of Theorem expcld
StepHypRef Expression
1 expcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 expcld.2 . 2 (𝜑𝑁 ∈ ℕ0)
3 expcl 13991 . 2 ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴𝑁) ∈ ℂ)
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴𝑁) ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  (class class class)co 7358  cc 11054  0cn0 12418  cexp 13973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-er 8651  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-nn 12159  df-n0 12419  df-z 12505  df-uz 12769  df-seq 13913  df-exp 13974
This theorem is referenced by:  absexpz  15196  binomlem  15719  incexclem  15726  incexc  15727  incexc2  15728  geoserg  15756  pwdif  15758  pwm1geoser  15759  geolim  15760  geolim2  15761  geo2sum2  15764  geomulcvg  15766  bpolycl  15940  bpolydiflem  15942  efaddlem  15980  oexpneg  16232  pwp1fsum  16278  oddpwp1fsum  16279  cphipval  24623  dvexp3  25358  itgpowd  25430  ply1termlem  25580  dgrcolem2  25651  dvply1  25660  aareccl  25702  aalioulem1  25708  taylfvallem1  25732  tayl0  25737  dvtaylp  25745  taylthlem2  25749  radcnvlem1  25788  pserulm  25797  logtayl  26031  cxpeq  26126  atantayl2  26304  atantayl3  26305  dfef2  26336  ftalem1  26438  ftalem2  26439  ftalem5  26442  basellem4  26449  logexprlim  26589  psgnfzto1st  32003  madjusmdetlem4  32468  oddpwdc  33011  eulerpartlemgs2  33037  signsplypnf  33219  signsply0  33220  breprexplemc  33302  breprexpnat  33304  bcprod  34367  knoppcnlem4  35005  knoppcnlem10  35011  knoppndvlem2  35022  knoppndvlem6  35026  knoppndvlem7  35027  knoppndvlem8  35028  knoppndvlem9  35029  knoppndvlem10  35030  knoppndvlem14  35034  knoppndvlem17  35037  lcmineqlem8  40539  lcmineqlem10  40541  lcmineqlem12  40543  dvrelogpow2b  40571  aks4d1p1p6  40576  aks4d1p1p7  40577  aks4d1p1  40579  2ap1caineq  40599  exp11d  40854  dffltz  41015  fltmul  41016  fltdiv  41017  fltaccoprm  41021  flt4lem6  41039  fltltc  41042  fltnltalem  41043  3cubeslem3l  41052  3cubeslem3r  41053  3cubeslem4  41055  jm2.18  41355  jm2.22  41362  jm2.23  41363  radcnvrat  42682  binomcxplemnn0  42717  binomcxplemnotnn0  42724  expcnfg  43918  fprodexp  43921  climexp  43932  dvsinexp  44238  dvxpaek  44267  dvnxpaek  44269  ibliccsinexp  44278  iblioosinexp  44280  itgsinexplem1  44281  itgsinexp  44282  iblsplit  44293  stoweidlem1  44328  stoweidlem7  44334  wallispi2lem2  44399  wallispi2  44400  stirlinglem3  44403  stirlinglem4  44404  stirlinglem5  44405  stirlinglem7  44407  stirlinglem8  44408  stirlinglem10  44410  stirlinglem11  44411  stirlinglem13  44413  stirlinglem14  44414  stirlinglem15  44415  elaa2lem  44560  etransclem1  44562  etransclem4  44565  etransclem8  44569  etransclem18  44579  etransclem20  44581  etransclem21  44582  etransclem23  44584  etransclem35  44596  etransclem41  44602  etransclem46  44607  etransclem48  44609  2pwp1prm  45867  lighneallem4  45888  oexpnegALTV  45955  fppr2odd  46009  altgsumbcALT  46515  dignn0flhalflem1  46787  nn0sumshdiglemA  46791  nn0sumshdiglemB  46792
  Copyright terms: Public domain W3C validator