Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exp1d | Structured version Visualization version GIF version |
Description: Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.) |
Ref | Expression |
---|---|
expcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
exp1d | ⊢ (𝜑 → (𝐴↑1) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | exp1 13673 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑1) = 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐴↑1) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2112 (class class class)co 7235 ℂcc 10757 1c1 10760 ↑cexp 13667 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-sep 5209 ax-nul 5216 ax-pow 5275 ax-pr 5339 ax-un 7545 ax-cnex 10815 ax-resscn 10816 ax-1cn 10817 ax-icn 10818 ax-addcl 10819 ax-addrcl 10820 ax-mulcl 10821 ax-mulrcl 10822 ax-mulcom 10823 ax-addass 10824 ax-mulass 10825 ax-distr 10826 ax-i2m1 10827 ax-1ne0 10828 ax-1rid 10829 ax-rnegex 10830 ax-rrecex 10831 ax-cnre 10832 ax-pre-lttri 10833 ax-pre-lttrn 10834 ax-pre-ltadd 10835 ax-pre-mulgt0 10836 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5179 df-id 5472 df-eprel 5478 df-po 5486 df-so 5487 df-fr 5527 df-we 5529 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-rn 5580 df-res 5581 df-ima 5582 df-pred 6179 df-ord 6237 df-on 6238 df-lim 6239 df-suc 6240 df-iota 6359 df-fun 6403 df-fn 6404 df-f 6405 df-f1 6406 df-fo 6407 df-f1o 6408 df-fv 6409 df-riota 7192 df-ov 7238 df-oprab 7239 df-mpo 7240 df-om 7667 df-2nd 7784 df-wrecs 8071 df-recs 8132 df-rdg 8170 df-er 8415 df-en 8651 df-dom 8652 df-sdom 8653 df-pnf 10899 df-mnf 10900 df-xr 10901 df-ltxr 10902 df-le 10903 df-sub 11094 df-neg 11095 df-nn 11861 df-n0 12121 df-z 12207 df-uz 12469 df-seq 13607 df-exp 13668 |
This theorem is referenced by: faclbnd4lem1 13892 fsumcube 15655 sin01gt0 15784 rplpwr 16152 prmdvdsexp 16305 phiprm 16363 eulerthlem2 16368 pcelnn 16456 expnprm 16488 prmpwdvds 16490 pockthg 16492 odcau 19026 plyco 25167 dgrcolem1 25199 vieta1 25237 taylthlem1 25297 ftalem2 25988 vmaprm 26031 vma1 26080 1sgmprm 26112 chtublem 26124 fsumvma2 26127 chpchtsum 26132 logfacrlim2 26139 bposlem2 26198 bposlem6 26202 lgsval2lem 26220 2sqblem 26344 chebbnd1lem1 26382 rplogsumlem2 26398 rpvmasumlem 26400 ostth3 26551 nn0prpwlem 34282 nn0prpw 34283 bfplem1 35754 dvrelogpow2b 39846 aks4d1p1p4 39849 aks4d1p1p7 39852 aks4d1p1p5 39853 aks4d1p1 39854 aks4d1p3 39856 2ap1caineq 39865 fltnltalem 40250 fltnlta 40251 3cubeslem3r 40260 rmxy1 40495 jm2.18 40561 jm2.23 40569 jm3.1lem2 40591 areaquad 40798 radcnvrat 41653 stoweidlem3 43265 wallispilem2 43328 stirlinglem1 43336 stirlinglem7 43342 stirlinglem10 43345 lighneal 44782 blenpw2m1 45644 |
Copyright terms: Public domain | W3C validator |