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

Theorem zexpcl 12299
Description: Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.)
Assertion
Ref Expression
zexpcl  |-  ( ( A  e.  ZZ  /\  N  e.  NN0 )  -> 
( A ^ N
)  e.  ZZ )

Proof of Theorem zexpcl
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 zsscn 10958 . 2  |-  ZZ  C_  CC
2 zmulcl 10998 . 2  |-  ( ( x  e.  ZZ  /\  y  e.  ZZ )  ->  ( x  x.  y
)  e.  ZZ )
3 1z 10980 . 2  |-  1  e.  ZZ
41, 2, 3expcllem 12295 1  |-  ( ( A  e.  ZZ  /\  N  e.  NN0 )  -> 
( A ^ N
)  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1873  (class class class)co 6311   NN0cn0 10882   ZZcz 10950   ^cexp 12284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-8 1875  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-sep 4552  ax-nul 4561  ax-pow 4608  ax-pr 4666  ax-un 6603  ax-cnex 9608  ax-resscn 9609  ax-1cn 9610  ax-icn 9611  ax-addcl 9612  ax-addrcl 9613  ax-mulcl 9614  ax-mulrcl 9615  ax-mulcom 9616  ax-addass 9617  ax-mulass 9618  ax-distr 9619  ax-i2m1 9620  ax-1ne0 9621  ax-1rid 9622  ax-rnegex 9623  ax-rrecex 9624  ax-cnre 9625  ax-pre-lttri 9626  ax-pre-lttrn 9627  ax-pre-ltadd 9628  ax-pre-mulgt0 9629
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3087  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3918  df-pw 3989  df-sn 4005  df-pr 4007  df-tp 4009  df-op 4011  df-uni 4226  df-iun 4307  df-br 4430  df-opab 4489  df-mpt 4490  df-tr 4525  df-eprel 4770  df-id 4774  df-po 4780  df-so 4781  df-fr 4818  df-we 4820  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-pred 5405  df-ord 5451  df-on 5452  df-lim 5453  df-suc 5454  df-iota 5571  df-fun 5609  df-fn 5610  df-f 5611  df-f1 5612  df-fo 5613  df-f1o 5614  df-fv 5615  df-riota 6273  df-ov 6314  df-oprab 6315  df-mpt2 6316  df-om 6713  df-2nd 6814  df-wrecs 7045  df-recs 7107  df-rdg 7145  df-er 7380  df-en 7587  df-dom 7588  df-sdom 7589  df-pnf 9690  df-mnf 9691  df-xr 9692  df-ltxr 9693  df-le 9694  df-sub 9875  df-neg 9876  df-nn 10623  df-n0 10883  df-z 10951  df-uz 11173  df-seq 12226  df-exp 12285
This theorem is referenced by:  zsqcl  12357  modexp  12419  climcndslem1  13912  iddvdsexp  14331  dvdsexp  14366  3dvds  14374  prmdvdsexp  14672  rpexp  14677  rpexp12i  14679  phiprmpw  14729  eulerthlem2  14735  fermltl  14737  prmdiv  14738  prmdiveq  14739  odzcllem  14742  odzdvds  14745  odzphi  14746  odzcllemOLD  14748  odzdvdsOLD  14751  odzphiOLD  14752  vfermltlALT  14758  powm2modprm  14759  pcneg  14828  pcprmpw  14837  prmpwdvds  14853  pockthlem  14854  dyaddisjlem  22557  aalioulem1  23292  aaliou3lem6  23308  muf  24071  dvdsppwf1o  24119  mersenne  24159  lgslem1  24228  lgslem4  24231  lgsval2lem  24238  lgsvalmod  24247  lgsmod  24253  lgsdirprm  24261  lgsne0  24265  lgsqrlem1  24273  lgseisenlem2  24282  lgseisenlem4  24284  m1lgs  24294  mdetlap  28672  oddpwdc  29201  dvdspw  30399  nn0prpwlem  30989  nn0prpw  30990  jm2.18  35819  jm2.22  35826  jm2.23  35827  jm2.20nn  35828  inductionexd  36569  etransclem3  38048  etransclem7  38052  etransclem10  38055  etransclem24  38069  etransclem27  38072  etransclem35  38080  nnpw2evenALTV  38705  proththd  38790  41prothprmlem2  38794  pw2m1lepw2m1  39937  nnpw2blenfzo  40011  dignn0fr  40031  digexp  40037  dignn0flhalflem1  40045
  Copyright terms: Public domain W3C validator