![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > recxpcld | Structured version Visualization version GIF version |
Description: Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.) |
Ref | Expression |
---|---|
recxpcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
recxpcld.2 | ⊢ (𝜑 → 0 ≤ 𝐴) |
recxpcld.3 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
Ref | Expression |
---|---|
recxpcld | ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recxpcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | recxpcld.2 | . 2 ⊢ (𝜑 → 0 ≤ 𝐴) | |
3 | recxpcld.3 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
4 | recxpcl 26705 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ) | |
5 | 1, 2, 3, 4 | syl3anc 1368 | 1 ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 class class class wbr 5155 (class class class)co 7426 ℝcr 11159 0cc0 11160 ≤ cle 11301 ↑𝑐ccxp 26585 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5292 ax-sep 5306 ax-nul 5313 ax-pow 5371 ax-pr 5435 ax-un 7748 ax-inf2 9686 ax-cnex 11216 ax-resscn 11217 ax-1cn 11218 ax-icn 11219 ax-addcl 11220 ax-addrcl 11221 ax-mulcl 11222 ax-mulrcl 11223 ax-mulcom 11224 ax-addass 11225 ax-mulass 11226 ax-distr 11227 ax-i2m1 11228 ax-1ne0 11229 ax-1rid 11230 ax-rnegex 11231 ax-rrecex 11232 ax-cnre 11233 ax-pre-lttri 11234 ax-pre-lttrn 11235 ax-pre-ltadd 11236 ax-pre-mulgt0 11237 ax-pre-sup 11238 ax-addf 11239 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-tp 4638 df-op 4640 df-uni 4916 df-int 4957 df-iun 5005 df-iin 5006 df-br 5156 df-opab 5218 df-mpt 5239 df-tr 5273 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5639 df-se 5640 df-we 5641 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6314 df-ord 6381 df-on 6382 df-lim 6383 df-suc 6384 df-iota 6508 df-fun 6558 df-fn 6559 df-f 6560 df-f1 6561 df-fo 6562 df-f1o 6563 df-fv 6564 df-isom 6565 df-riota 7382 df-ov 7429 df-oprab 7430 df-mpo 7431 df-of 7692 df-om 7879 df-1st 8005 df-2nd 8006 df-supp 8177 df-frecs 8298 df-wrecs 8329 df-recs 8403 df-rdg 8442 df-1o 8498 df-2o 8499 df-er 8736 df-map 8859 df-pm 8860 df-ixp 8929 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-fsupp 9408 df-fi 9456 df-sup 9487 df-inf 9488 df-oi 9555 df-card 9984 df-pnf 11302 df-mnf 11303 df-xr 11304 df-ltxr 11305 df-le 11306 df-sub 11498 df-neg 11499 df-div 11924 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12613 df-dec 12732 df-uz 12877 df-q 12987 df-rp 13031 df-xneg 13148 df-xadd 13149 df-xmul 13150 df-ioo 13384 df-ioc 13385 df-ico 13386 df-icc 13387 df-fz 13541 df-fzo 13684 df-fl 13814 df-mod 13892 df-seq 14024 df-exp 14084 df-fac 14293 df-bc 14322 df-hash 14350 df-shft 15074 df-cj 15106 df-re 15107 df-im 15108 df-sqrt 15242 df-abs 15243 df-limsup 15475 df-clim 15492 df-rlim 15493 df-sum 15693 df-ef 16071 df-sin 16073 df-cos 16074 df-pi 16076 df-struct 17151 df-sets 17168 df-slot 17186 df-ndx 17198 df-base 17216 df-ress 17245 df-plusg 17281 df-mulr 17282 df-starv 17283 df-sca 17284 df-vsca 17285 df-ip 17286 df-tset 17287 df-ple 17288 df-ds 17290 df-unif 17291 df-hom 17292 df-cco 17293 df-rest 17439 df-topn 17440 df-0g 17458 df-gsum 17459 df-topgen 17460 df-pt 17461 df-prds 17464 df-xrs 17519 df-qtop 17524 df-imas 17525 df-xps 17527 df-mre 17601 df-mrc 17602 df-acs 17604 df-mgm 18635 df-sgrp 18714 df-mnd 18730 df-submnd 18776 df-mulg 19064 df-cntz 19313 df-cmn 19782 df-psmet 21337 df-xmet 21338 df-met 21339 df-bl 21340 df-mopn 21341 df-fbas 21342 df-fg 21343 df-cnfld 21346 df-top 22890 df-topon 22907 df-topsp 22929 df-bases 22943 df-cld 23017 df-ntr 23018 df-cls 23019 df-nei 23096 df-lp 23134 df-perf 23135 df-cn 23225 df-cnp 23226 df-haus 23313 df-tx 23560 df-hmeo 23753 df-fil 23844 df-fm 23936 df-flim 23937 df-flf 23938 df-xms 24320 df-ms 24321 df-tms 24322 df-cncf 24892 df-limc 25889 df-dv 25890 df-log 26586 df-cxp 26587 |
This theorem is referenced by: recxpf1lem 26759 2irrexpq 26761 cxpaddlelem 26782 cxpaddle 26783 abscxpbnd 26784 rtprmirr 26791 cxplim 27003 o1cxp 27006 regamcl 27092 chpchtsum 27251 bposlem5 27320 abvcxp 27647 ostth2lem3 27667 nrt2irr 30409 logdivsqrle 34498 aks4d1p1p2 41771 aks4d1p1p4 41772 aks6d1c7lem1 41880 etransclem23 45896 etransclem46 45919 dignn0ldlem 48008 |
Copyright terms: Public domain | W3C validator |