Theorem zexpcl 14030

Description: Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.)

Assertion

Ref	Expression
zexpcl	⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℤ)

Proof of Theorem zexpcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zsscn 12524	. 2 ⊢ ℤ ⊆ ℂ
2		zmulcl 12568	. 2 ⊢ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝑥 · 𝑦) ∈ ℤ)
3		1z 12549	. 2 ⊢ 1 ∈ ℤ
4	1, 2, 3	expcllem 14026	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℤ)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  (class class class)co 7357  ℕ₀cn0 12429  ℤcz 12516  ↑cexp 14015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pow 5295  ax-pr 5363  ax-un 7679  ax-cnex 11086  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-iun 4924  df-br 5074  df-opab 5136  df-mpt 5155  df-tr 5181  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7314  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7808  df-2nd 7933  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11173  df-mnf 11174  df-xr 11175  df-ltxr 11176  df-le 11177  df-sub 11371  df-neg 11372  df-nn 12167  df-n0 12430  df-z 12517  df-uz 12781  df-seq 13956  df-exp 14016

This theorem is referenced by:  zexpcld  14041  zsqcl  14083  modexp  14192  climcndslem1  15806  iddvdsexp  16240  dvdsexp2im  16288  dvdsexp  16289  3dvds  16292  dvdsexpim  16516  zexpgcd  16526  prmdvdsexp  16677  rpexp  16684  rpexp12i  16686  numdenexp  16722  phiprmpw  16738  eulerthlem2  16744  fermltl  16746  prmdiv  16747  prmdiveq  16748  odzcllem  16755  odzdvds  16758  odzphi  16759  vfermltlALT  16765  powm2modprm  16766  pcneg  16837  pcprmpw  16846  prmpwdvds  16867  pockthlem  16868  dyaddisjlem  25581  aalioulem1  26317  aaliou3lem6  26333  muf  27122  dvdsppwf1o  27168  mersenne  27209  lgslem1  27279  lgsval2lem  27289  lgsvalmod  27298  lgsmod  27305  lgsdirprm  27313  lgsne0  27317  lgsqrlem1  27328  gausslemma2dlem7  27355  gausslemma2d  27356  lgseisenlem2  27358  lgseisenlem4  27360  m1lgs  27370  2sqreultlem  27429  2sqreunnltlem  27432  znfermltl  33450  mdetlap  34025  oddpwdc  34547  nn0prpwlem  36559  nn0prpw  36560  knoppndvlem2  36828  aks4d1p3  42572  aks4d1p6  42575  aks6d1c2p2  42613  jm2.18  43442  jm2.22  43449  jm2.23  43450  jm2.20nn  43451  inductionexd  44608  etransclem3  46688  etransclem7  46692  etransclem10  46695  etransclem24  46709  etransclem27  46712  etransclem35  46720  2pwp1prm  48075  sfprmdvdsmersenne  48089  lighneallem4b  48095  lighneallem4  48096  proththd  48100  41prothprmlem2  48104  nnpw2evenALTV  48201  fpprmod  48226  fppr2odd  48230  dfwppr  48237  fpprwppr  48238  fpprwpprb  48239  pw2m1lepw2m1  49019  nnpw2blenfzo  49080  dignn0fr  49100  digexp  49106  dignn0flhalflem1  49114