![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > nnexpcld | Structured version Unicode version |
Description: Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
nnexpcld.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
nnexpcld.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nnexpcld |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnexpcld.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nnexpcld.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | nnexpcl 11994 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 661 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468 ax-pre-mulgt0 9469 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-reu 2805 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-uni 4199 df-iun 4280 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-om 6586 df-2nd 6687 df-recs 6941 df-rdg 6975 df-er 7210 df-en 7420 df-dom 7421 df-sdom 7422 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-sub 9707 df-neg 9708 df-nn 10433 df-n0 10690 df-z 10757 df-uz 10972 df-seq 11923 df-exp 11982 |
This theorem is referenced by: bitsp1 13744 bitsfzolem 13747 bitsfzo 13748 bitsmod 13749 bitsfi 13750 bitscmp 13751 bitsinv1lem 13754 bitsinv1 13755 2ebits 13760 bitsinvp1 13762 sadcaddlem 13770 sadadd3 13774 sadaddlem 13779 sadasslem 13783 bitsres 13786 bitsuz 13787 bitsshft 13788 smumullem 13805 smumul 13806 rplpwr 13857 rppwr 13858 pclem 14022 pcprendvds2 14025 pcpre1 14026 pcpremul 14027 pcdvdsb 14052 pcidlem 14055 pcid 14056 pcdvdstr 14059 pcgcd1 14060 pcprmpw2 14065 pcaddlem 14067 pcadd 14068 pcfaclem 14077 pcfac 14078 pcbc 14079 prmpwdvds 14082 pockthlem 14083 2expltfac 14236 pgpfi1 16214 sylow1lem1 16217 sylow1lem3 16219 sylow1lem4 16220 sylow1lem5 16221 pgpfi 16224 gexexlem 16454 ablfac1lem 16690 ablfac1b 16692 ablfac1eu 16695 aalioulem2 21931 aalioulem5 21934 aaliou3lem9 21948 isppw2 22585 sgmppw 22668 fsumvma2 22685 pclogsum 22686 chpchtsum 22690 logfacubnd 22692 bposlem1 22755 bposlem5 22759 lgseisen 22824 chebbnd1lem1 22850 rpvmasumlem 22868 dchrisum0flblem1 22889 dchrisum0flblem2 22890 ostth2lem2 23015 ostth2lem3 23016 oddpwdc 26880 eulerpartlemgh 26904 jm3.1lem3 29515 stoweidlem25 29967 stoweidlem45 29987 wallispi2lem1 30013 |
Copyright terms: Public domain | W3C validator |