![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > efcl | GIF version |
Description: Closure law for the exponential function. (Contributed by NM, 8-Jan-2006.) (Revised by Mario Carneiro, 10-Nov-2013.) |
Ref | Expression |
---|---|
efcl | ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eff 11698 | . 2 ⊢ exp:ℂ⟶ℂ | |
2 | 1 | ffvelcdmi 5667 | 1 ⊢ (𝐴 ∈ ℂ → (exp‘𝐴) ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ‘cfv 5232 ℂcc 7834 expce 11677 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4189 ax-pr 4224 ax-un 4448 ax-setind 4551 ax-iinf 4602 ax-cnex 7927 ax-resscn 7928 ax-1cn 7929 ax-1re 7930 ax-icn 7931 ax-addcl 7932 ax-addrcl 7933 ax-mulcl 7934 ax-mulrcl 7935 ax-addcom 7936 ax-mulcom 7937 ax-addass 7938 ax-mulass 7939 ax-distr 7940 ax-i2m1 7941 ax-0lt1 7942 ax-1rid 7943 ax-0id 7944 ax-rnegex 7945 ax-precex 7946 ax-cnre 7947 ax-pre-ltirr 7948 ax-pre-ltwlin 7949 ax-pre-lttrn 7950 ax-pre-apti 7951 ax-pre-ltadd 7952 ax-pre-mulgt0 7953 ax-pre-mulext 7954 ax-arch 7955 ax-caucvg 7956 |
This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rmo 2476 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-if 3550 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-int 3860 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4308 df-po 4311 df-iso 4312 df-iord 4381 df-on 4383 df-ilim 4384 df-suc 4386 df-iom 4605 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-rn 4652 df-res 4653 df-ima 4654 df-iota 5193 df-fun 5234 df-fn 5235 df-f 5236 df-f1 5237 df-fo 5238 df-f1o 5239 df-fv 5240 df-isom 5241 df-riota 5848 df-ov 5895 df-oprab 5896 df-mpo 5897 df-1st 6160 df-2nd 6161 df-recs 6325 df-irdg 6390 df-frec 6411 df-1o 6436 df-oadd 6440 df-er 6554 df-en 6762 df-dom 6763 df-fin 6764 df-pnf 8019 df-mnf 8020 df-xr 8021 df-ltxr 8022 df-le 8023 df-sub 8155 df-neg 8156 df-reap 8557 df-ap 8564 df-div 8655 df-inn 8945 df-2 9003 df-3 9004 df-4 9005 df-n0 9202 df-z 9279 df-uz 9554 df-q 9645 df-rp 9679 df-ico 9919 df-fz 10034 df-fzo 10168 df-seqfrec 10472 df-exp 10546 df-fac 10733 df-ihash 10783 df-cj 10878 df-re 10879 df-im 10880 df-rsqrt 11034 df-abs 11035 df-clim 11314 df-sumdc 11389 df-ef 11683 |
This theorem is referenced by: efap0 11712 efne0 11713 efneg 11714 eff2 11715 efsub 11716 efexp 11717 ef4p 11729 sinval 11737 cosval 11738 sinf 11739 cosf 11740 tanval2ap 11748 tanval3ap 11749 resinval 11750 recosval 11751 resincl 11755 recoscl 11756 sinneg 11761 cosneg 11762 efival 11767 absef 11804 efieq1re 11806 dveflem 14624 dvef 14625 reeff1oleme 14630 efper 14665 rpcxpef 14752 rpcncxpcl 14760 |
Copyright terms: Public domain | W3C validator |