![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > zexpcl | Structured version Visualization version Unicode version |
Description: Closure of exponentiation of integers. (Contributed by NM, 16-Dec-2005.) |
Ref | Expression |
---|---|
zexpcl |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zsscn 10974 |
. 2
![]() ![]() ![]() ![]() | |
2 | zmulcl 11014 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1z 10996 |
. 2
![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | expcllem 12315 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-cnex 9621 ax-resscn 9622 ax-1cn 9623 ax-icn 9624 ax-addcl 9625 ax-addrcl 9626 ax-mulcl 9627 ax-mulrcl 9628 ax-mulcom 9629 ax-addass 9630 ax-mulass 9631 ax-distr 9632 ax-i2m1 9633 ax-1ne0 9634 ax-1rid 9635 ax-rnegex 9636 ax-rrecex 9637 ax-cnre 9638 ax-pre-lttri 9639 ax-pre-lttrn 9640 ax-pre-ltadd 9641 ax-pre-mulgt0 9642 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-iun 4294 df-br 4417 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6277 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-om 6720 df-2nd 6821 df-wrecs 7054 df-recs 7116 df-rdg 7154 df-er 7389 df-en 7596 df-dom 7597 df-sdom 7598 df-pnf 9703 df-mnf 9704 df-xr 9705 df-ltxr 9706 df-le 9707 df-sub 9888 df-neg 9889 df-nn 10638 df-n0 10899 df-z 10967 df-uz 11189 df-seq 12246 df-exp 12305 |
This theorem is referenced by: zsqcl 12377 modexp 12439 climcndslem1 13956 iddvdsexp 14375 dvdsexp 14410 3dvds 14418 prmdvdsexp 14716 rpexp 14721 rpexp12i 14723 phiprmpw 14773 eulerthlem2 14779 fermltl 14781 prmdiv 14782 prmdiveq 14783 odzcllem 14786 odzdvds 14789 odzphi 14790 odzcllemOLD 14792 odzdvdsOLD 14795 odzphiOLD 14796 vfermltlALT 14802 powm2modprm 14803 pcneg 14872 pcprmpw 14881 prmpwdvds 14897 pockthlem 14898 dyaddisjlem 22602 aalioulem1 23337 aaliou3lem6 23353 muf 24116 dvdsppwf1o 24164 mersenne 24204 lgslem1 24273 lgslem4 24276 lgsval2lem 24283 lgsvalmod 24292 lgsmod 24298 lgsdirprm 24306 lgsne0 24310 lgsqrlem1 24318 lgseisenlem2 24327 lgseisenlem4 24329 m1lgs 24339 mdetlap 28707 oddpwdc 29236 dvdspw 30435 nn0prpwlem 31027 nn0prpw 31028 jm2.18 35888 jm2.22 35895 jm2.23 35896 jm2.20nn 35897 inductionexd 36638 etransclem3 38140 etransclem7 38144 etransclem10 38147 etransclem24 38161 etransclem27 38164 etransclem35 38172 nnpw2evenALTV 38867 proththd 38952 41prothprmlem2 38956 pw2m1lepw2m1 40591 nnpw2blenfzo 40665 dignn0fr 40685 digexp 40691 dignn0flhalflem1 40699 |
Copyright terms: Public domain | W3C validator |