![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nnexpcl | Structured version Visualization version GIF version |
Description: Closure of exponentiation of nonnegative integers. (Contributed by NM, 16-Dec-2005.) |
Ref | Expression |
---|---|
nnexpcl | ⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnsscn 11440 | . 2 ⊢ ℕ ⊆ ℂ | |
2 | nnmulcl 11460 | . 2 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 · 𝑦) ∈ ℕ) | |
3 | 1nn 11448 | . 2 ⊢ 1 ∈ ℕ | |
4 | 1, 2, 3 | expcllem 13252 | 1 ⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℕ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2048 (class class class)co 6974 ℕcn 11435 ℕ0cn0 11704 ↑cexp 13241 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2747 ax-sep 5058 ax-nul 5065 ax-pow 5117 ax-pr 5184 ax-un 7277 ax-cnex 10387 ax-resscn 10388 ax-1cn 10389 ax-icn 10390 ax-addcl 10391 ax-addrcl 10392 ax-mulcl 10393 ax-mulrcl 10394 ax-mulcom 10395 ax-addass 10396 ax-mulass 10397 ax-distr 10398 ax-i2m1 10399 ax-1ne0 10400 ax-1rid 10401 ax-rnegex 10402 ax-rrecex 10403 ax-cnre 10404 ax-pre-lttri 10405 ax-pre-lttrn 10406 ax-pre-ltadd 10407 ax-pre-mulgt0 10408 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2756 df-cleq 2768 df-clel 2843 df-nfc 2915 df-ne 2965 df-nel 3071 df-ral 3090 df-rex 3091 df-reu 3092 df-rab 3094 df-v 3414 df-sbc 3681 df-csb 3786 df-dif 3831 df-un 3833 df-in 3835 df-ss 3842 df-pss 3844 df-nul 4178 df-if 4349 df-pw 4422 df-sn 4440 df-pr 4442 df-tp 4444 df-op 4446 df-uni 4711 df-iun 4792 df-br 4928 df-opab 4990 df-mpt 5007 df-tr 5029 df-id 5309 df-eprel 5314 df-po 5323 df-so 5324 df-fr 5363 df-we 5365 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-pred 5984 df-ord 6030 df-on 6031 df-lim 6032 df-suc 6033 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-om 7395 df-2nd 7499 df-wrecs 7747 df-recs 7809 df-rdg 7847 df-er 8085 df-en 8303 df-dom 8304 df-sdom 8305 df-pnf 10472 df-mnf 10473 df-xr 10474 df-ltxr 10475 df-le 10476 df-sub 10668 df-neg 10669 df-nn 11436 df-n0 11705 df-z 11791 df-uz 12056 df-seq 13182 df-exp 13242 |
This theorem is referenced by: digit1 13410 nnexpcld 13418 faclbnd4lem3 13467 faclbnd5 13470 climcndslem1 15058 climcndslem2 15059 climcnds 15060 harmonic 15068 geo2sum 15083 geo2lim 15085 ege2le3 15297 eftlub 15316 ef01bndlem 15391 phiprmpw 15963 pcdvdsb 16055 pcmptcl 16077 pcfac 16085 pockthi 16093 prmreclem3 16104 prmreclem5 16106 prmreclem6 16107 modxai 16254 1259lem5 16318 2503lem3 16322 4001lem4 16327 ovollb2lem 23786 ovoliunlem1 23800 ovoliunlem3 23802 dyadf 23889 dyadovol 23891 dyadss 23892 dyaddisjlem 23893 dyadmaxlem 23895 opnmbllem 23899 mbfi1fseqlem1 24013 mbfi1fseqlem3 24015 mbfi1fseqlem4 24016 mbfi1fseqlem5 24017 mbfi1fseqlem6 24018 aalioulem1 24618 aaliou2b 24627 aaliou3lem9 24636 log2cnv 25218 log2tlbnd 25219 log2ublem1 25220 log2ublem2 25221 log2ub 25223 zetacvg 25288 vmappw 25389 sgmnncl 25420 dvdsppwf1o 25459 0sgmppw 25470 1sgm2ppw 25472 vmasum 25488 mersenne 25499 perfect1 25500 perfectlem1 25501 perfectlem2 25502 perfect 25503 pcbcctr 25548 bclbnd 25552 bposlem2 25557 bposlem6 25561 bposlem8 25563 chebbnd1lem1 25741 rplogsumlem2 25757 ostth2lem3 25907 ostth3 25910 oddpwdc 31248 tgoldbachgt 31573 faclim2 32470 opnmbllem0 34347 heiborlem3 34511 heiborlem5 34513 heiborlem6 34514 heiborlem7 34515 heiborlem8 34516 heibor 34519 expgcd 38593 hoicvrrex 42248 ovnsubaddlem2 42263 ovolval5lem1 42344 fmtnoprmfac2lem1 43070 fmtno4prm 43079 perfectALTVlem1 43228 perfectALTVlem2 43229 perfectALTV 43230 bgoldbachlt 43320 tgblthelfgott 43322 tgoldbachlt 43323 blenpw2 43980 nnpw2pb 43989 nnolog2flm1 43992 |
Copyright terms: Public domain | W3C validator |