Step |
Hyp |
Ref |
Expression |
1 |
|
rpcn |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ ) |
2 |
|
cxpcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ ) |
3 |
1 2
|
sylan |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℂ ) |
4 |
|
rpreccl |
⊢ ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) ∈ ℝ+ ) |
5 |
4
|
rpcnd |
⊢ ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) ∈ ℂ ) |
6 |
|
cxpcl |
⊢ ( ( ( 1 / 𝐴 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ∈ ℂ ) |
7 |
5 6
|
sylan |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ∈ ℂ ) |
8 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ ) |
9 |
|
rpne0 |
⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 ) |
10 |
9
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → 𝐴 ≠ 0 ) |
11 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ ) |
12 |
|
cxpne0 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ≠ 0 ) |
13 |
8 10 11 12
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) ≠ 0 ) |
14 |
8 10
|
recidd |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · ( 1 / 𝐴 ) ) = 1 ) |
15 |
14
|
oveq1d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ↑𝑐 𝐵 ) = ( 1 ↑𝑐 𝐵 ) ) |
16 |
|
rprege0 |
⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) |
17 |
16
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ) |
18 |
4
|
rprege0d |
⊢ ( 𝐴 ∈ ℝ+ → ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐴 ) ) ) |
19 |
18
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐴 ) ) ) |
20 |
|
mulcxp |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐴 ) ) ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ↑𝑐 𝐵 ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ) ) |
21 |
17 19 11 20
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · ( 1 / 𝐴 ) ) ↑𝑐 𝐵 ) = ( ( 𝐴 ↑𝑐 𝐵 ) · ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ) ) |
22 |
|
1cxp |
⊢ ( 𝐵 ∈ ℂ → ( 1 ↑𝑐 𝐵 ) = 1 ) |
23 |
11 22
|
syl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( 1 ↑𝑐 𝐵 ) = 1 ) |
24 |
15 21 23
|
3eqtr3d |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑𝑐 𝐵 ) · ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) ) = 1 ) |
25 |
3 7 13 24
|
mvllmuld |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) = ( 1 / ( 𝐴 ↑𝑐 𝐵 ) ) ) |