Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > expcl | Structured version Visualization version GIF version |
Description: Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005.) |
Ref | Expression |
---|---|
expcl | ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3986 | . 2 ⊢ ℂ ⊆ ℂ | |
2 | mulcl 10609 | . 2 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) | |
3 | ax-1cn 10583 | . 2 ⊢ 1 ∈ ℂ | |
4 | 1, 2, 3 | expcllem 13428 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝐴↑𝑁) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 ℕ0cn0 11885 ↑cexp 13417 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 ax-cnex 10581 ax-resscn 10582 ax-1cn 10583 ax-icn 10584 ax-addcl 10585 ax-addrcl 10586 ax-mulcl 10587 ax-mulrcl 10588 ax-mulcom 10589 ax-addass 10590 ax-mulass 10591 ax-distr 10592 ax-i2m1 10593 ax-1ne0 10594 ax-1rid 10595 ax-rnegex 10596 ax-rrecex 10597 ax-cnre 10598 ax-pre-lttri 10599 ax-pre-lttrn 10600 ax-pre-ltadd 10601 ax-pre-mulgt0 10602 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-nel 3121 df-ral 3140 df-rex 3141 df-reu 3142 df-rab 3144 df-v 3494 df-sbc 3770 df-csb 3881 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-pss 3951 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4831 df-iun 4912 df-br 5058 df-opab 5120 df-mpt 5138 df-tr 5164 df-id 5453 df-eprel 5458 df-po 5467 df-so 5468 df-fr 5507 df-we 5509 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6141 df-ord 6187 df-on 6188 df-lim 6189 df-suc 6190 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-riota 7103 df-ov 7148 df-oprab 7149 df-mpo 7150 df-om 7570 df-2nd 7679 df-wrecs 7936 df-recs 7997 df-rdg 8035 df-er 8278 df-en 8498 df-dom 8499 df-sdom 8500 df-pnf 10665 df-mnf 10666 df-xr 10667 df-ltxr 10668 df-le 10669 df-sub 10860 df-neg 10861 df-nn 11627 df-n0 11886 df-z 11970 df-uz 12232 df-seq 13358 df-exp 13418 |
This theorem is referenced by: expeq0 13447 expnegz 13451 mulexp 13456 mulexpz 13457 expadd 13459 expaddzlem 13460 expaddz 13461 expmul 13462 expmulz 13463 expdiv 13468 expcld 13498 binom3 13573 digit2 13585 digit1 13586 faclbnd2 13639 faclbnd4lem4 13644 faclbnd6 13647 cjexp 14497 absexp 14652 ackbijnn 15171 binomlem 15172 binom1p 15174 binom1dif 15176 expcnv 15207 geolim 15214 geolim2 15215 geo2sum 15217 geomulcvg 15220 geoisum 15221 geoisumr 15222 geoisum1 15223 geoisum1c 15224 0.999... 15225 fallrisefac 15367 0risefac 15380 binomrisefac 15384 bpolysum 15395 bpolydiflem 15396 fsumkthpow 15398 bpoly3 15400 bpoly4 15401 fsumcube 15402 eftcl 15415 eftabs 15417 efcllem 15419 efcj 15433 efaddlem 15434 eflegeo 15462 efi4p 15478 prmreclem6 16245 karatsuba 16408 expmhm 20542 mbfi1fseqlem6 24248 itg0 24307 itgz 24308 itgcl 24311 itgcnlem 24317 itgsplit 24363 dvexp 24477 dvexp3 24502 plyf 24715 ply1termlem 24720 plypow 24722 plyeq0lem 24727 plypf1 24729 plyaddlem1 24730 plymullem1 24731 coeeulem 24741 coeidlem 24754 coeid3 24757 plyco 24758 dgrcolem2 24791 plycjlem 24793 plyrecj 24796 vieta1 24828 elqaalem3 24837 aareccl 24842 aalioulem1 24848 geolim3 24855 psergf 24927 dvradcnv 24936 psercn2 24938 pserdvlem2 24943 pserdv2 24945 abelthlem4 24949 abelthlem5 24950 abelthlem6 24951 abelthlem7 24953 abelthlem9 24955 advlogexp 25165 logtayllem 25169 logtayl 25170 logtaylsum 25171 logtayl2 25172 cxpeq 25265 dcubic1lem 25348 dcubic2 25349 dcubic1 25350 dcubic 25351 mcubic 25352 cubic2 25353 cubic 25354 binom4 25355 dquartlem2 25357 dquart 25358 quart1cl 25359 quart1lem 25360 quart1 25361 quartlem1 25362 quartlem2 25363 quart 25366 atantayl 25442 atantayl2 25443 atantayl3 25444 leibpi 25447 log2cnv 25449 log2tlbnd 25450 log2ublem3 25453 ftalem1 25577 ftalem4 25580 ftalem5 25581 basellem3 25587 musum 25695 1sgmprm 25702 perfect 25734 lgsquadlem1 25883 rplogsumlem2 25988 ostth2lem2 26137 numclwwlk3lem1 28088 ipval2 28411 dipcl 28416 dipcn 28424 subfacval2 32331 jm2.23 39471 lhe4.4ex1a 40538 perfectALTV 43765 altgsumbc 44328 altgsumbcALT 44329 nn0digval 44588 |
Copyright terms: Public domain | W3C validator |