abscxp - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > abscxp		GIF version

Theorem abscxp 15177

Description: Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014.)

**Assertion**
Ref	Expression
abscxp	⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑_𝑐𝐵)) = (𝐴↑_𝑐(ℜ‘𝐵)))

**Proof of Theorem abscxp**
Step	Hyp	Ref	Expression
1		simpr 110	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → 𝐵 ∈ ℂ)
2		relogcl 15124	. . . . . . 7 ⊢ (𝐴 ∈ ℝ⁺ → (log‘𝐴) ∈ ℝ)
3	2	recnd 8058	. . . . . 6 ⊢ (𝐴 ∈ ℝ⁺ → (log‘𝐴) ∈ ℂ)
4	3	adantr 276	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (log‘𝐴) ∈ ℂ)
5	1, 4	mulcld 8050	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (𝐵 · (log‘𝐴)) ∈ ℂ)
6		absef 11938	. . . 4 ⊢ ((𝐵 · (log‘𝐴)) ∈ ℂ → (abs‘(exp‘(𝐵 · (log‘𝐴)))) = (exp‘(ℜ‘(𝐵 · (log‘𝐴)))))
7	5, 6	syl 14	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (abs‘(exp‘(𝐵 · (log‘𝐴)))) = (exp‘(ℜ‘(𝐵 · (log‘𝐴)))))
8		remul2 11041	. . . . . 6 ⊢ (((log‘𝐴) ∈ ℝ ∧ 𝐵 ∈ ℂ) → (ℜ‘((log‘𝐴) · 𝐵)) = ((log‘𝐴) · (ℜ‘𝐵)))
9	2, 8	sylan 283	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (ℜ‘((log‘𝐴) · 𝐵)) = ((log‘𝐴) · (ℜ‘𝐵)))
10	1, 4	mulcomd 8051	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (𝐵 · (log‘𝐴)) = ((log‘𝐴) · 𝐵))
11	10	fveq2d 5563	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐵 · (log‘𝐴))) = (ℜ‘((log‘𝐴) · 𝐵)))
12		recl 11021	. . . . . . . 8 ⊢ (𝐵 ∈ ℂ → (ℜ‘𝐵) ∈ ℝ)
13	12	adantl 277	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (ℜ‘𝐵) ∈ ℝ)
14	13	recnd 8058	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (ℜ‘𝐵) ∈ ℂ)
15	14, 4	mulcomd 8051	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → ((ℜ‘𝐵) · (log‘𝐴)) = ((log‘𝐴) · (ℜ‘𝐵)))
16	9, 11, 15	3eqtr4d 2239	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (ℜ‘(𝐵 · (log‘𝐴))) = ((ℜ‘𝐵) · (log‘𝐴)))
17	16	fveq2d 5563	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (exp‘(ℜ‘(𝐵 · (log‘𝐴)))) = (exp‘((ℜ‘𝐵) · (log‘𝐴))))
18	7, 17	eqtrd 2229	. 2 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (abs‘(exp‘(𝐵 · (log‘𝐴)))) = (exp‘((ℜ‘𝐵) · (log‘𝐴))))
19		rpcxpef 15156	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (𝐴↑_𝑐𝐵) = (exp‘(𝐵 · (log‘𝐴))))
20	19	fveq2d 5563	. 2 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑_𝑐𝐵)) = (abs‘(exp‘(𝐵 · (log‘𝐴)))))
21		rpcxpef 15156	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (ℜ‘𝐵) ∈ ℂ) → (𝐴↑_𝑐(ℜ‘𝐵)) = (exp‘((ℜ‘𝐵) · (log‘𝐴))))
22	14, 21	syldan 282	. 2 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (𝐴↑_𝑐(ℜ‘𝐵)) = (exp‘((ℜ‘𝐵) · (log‘𝐴))))
23	18, 20, 22	3eqtr4d 2239	1 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑_𝑐𝐵)) = (𝐴↑_𝑐(ℜ‘𝐵)))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 = wceq 1364 ∈ wcel 2167 ‘cfv 5259 (class class class)co 5923 ℂcc 7880 ℝcr 7881 · cmul 7887 ℝ⁺crp 9731 ℜcre 11008 abscabs 11165 expce 11810 logclog 15118 ↑_𝑐ccxp 15119

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7973 ax-resscn 7974 ax-1cn 7975 ax-1re 7976 ax-icn 7977 ax-addcl 7978 ax-addrcl 7979 ax-mulcl 7980 ax-mulrcl 7981 ax-addcom 7982 ax-mulcom 7983 ax-addass 7984 ax-mulass 7985 ax-distr 7986 ax-i2m1 7987 ax-0lt1 7988 ax-1rid 7989 ax-0id 7990 ax-rnegex 7991 ax-precex 7992 ax-cnre 7993 ax-pre-ltirr 7994 ax-pre-ltwlin 7995 ax-pre-lttrn 7996 ax-pre-apti 7997 ax-pre-ltadd 7998 ax-pre-mulgt0 7999 ax-pre-mulext 8000 ax-arch 8001 ax-caucvg 8002 ax-pre-suploc 8003 ax-addf 8004 ax-mulf 8005

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-disj 4012 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5878 df-ov 5926 df-oprab 5927 df-mpo 5928 df-of 6137 df-1st 6200 df-2nd 6201 df-recs 6365 df-irdg 6430 df-frec 6451 df-1o 6476 df-oadd 6480 df-er 6594 df-map 6711 df-pm 6712 df-en 6802 df-dom 6803 df-fin 6804 df-sup 7052 df-inf 7053 df-pnf 8066 df-mnf 8067 df-xr 8068 df-ltxr 8069 df-le 8070 df-sub 8202 df-neg 8203 df-reap 8605 df-ap 8612 df-div 8703 df-inn 8994 df-2 9052 df-3 9053 df-4 9054 df-n0 9253 df-z 9330 df-uz 9605 df-q 9697 df-rp 9732 df-xneg 9850 df-xadd 9851 df-ioo 9970 df-ico 9972 df-icc 9973 df-fz 10087 df-fzo 10221 df-seqfrec 10543 df-exp 10634 df-fac 10821 df-bc 10843 df-ihash 10871 df-shft 10983 df-cj 11010 df-re 11011 df-im 11012 df-rsqrt 11166 df-abs 11167 df-clim 11447 df-sumdc 11522 df-ef 11816 df-e 11817 df-sin 11818 df-cos 11819 df-rest 12929 df-topgen 12948 df-psmet 14125 df-xmet 14126 df-met 14127 df-bl 14128 df-mopn 14129 df-top 14260 df-topon 14273 df-bases 14305 df-ntr 14358 df-cn 14450 df-cnp 14451 df-tx 14515 df-cncf 14833 df-limced 14918 df-dvap 14919 df-relog 15120 df-rpcxp 15121

This theorem is referenced by: (None)

W3C validator