Step |
Hyp |
Ref |
Expression |
1 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 ∈ ℝ+ ) |
2 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ∈ ℝ ) |
3 |
2
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ∈ ℂ ) |
4 |
|
cxprec |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) = ( 1 / ( 𝐴 ↑𝑐 𝐵 ) ) ) |
5 |
1 3 4
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) = ( 1 / ( 𝐴 ↑𝑐 𝐵 ) ) ) |
6 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐶 ∈ ℝ ) |
7 |
6
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐶 ∈ ℂ ) |
8 |
|
cxprec |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℂ ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐶 ) = ( 1 / ( 𝐴 ↑𝑐 𝐶 ) ) ) |
9 |
1 7 8
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( 1 / 𝐴 ) ↑𝑐 𝐶 ) = ( 1 / ( 𝐴 ↑𝑐 𝐶 ) ) ) |
10 |
5 9
|
breq12d |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) < ( ( 1 / 𝐴 ) ↑𝑐 𝐶 ) ↔ ( 1 / ( 𝐴 ↑𝑐 𝐵 ) ) < ( 1 / ( 𝐴 ↑𝑐 𝐶 ) ) ) ) |
11 |
1
|
rprecred |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 1 / 𝐴 ) ∈ ℝ ) |
12 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 < 1 ) |
13 |
1
|
reclt1d |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 < 1 ↔ 1 < ( 1 / 𝐴 ) ) ) |
14 |
12 13
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 1 < ( 1 / 𝐴 ) ) |
15 |
|
cxplt |
⊢ ( ( ( ( 1 / 𝐴 ) ∈ ℝ ∧ 1 < ( 1 / 𝐴 ) ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 < 𝐶 ↔ ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) < ( ( 1 / 𝐴 ) ↑𝑐 𝐶 ) ) ) |
16 |
11 14 2 6 15
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 < 𝐶 ↔ ( ( 1 / 𝐴 ) ↑𝑐 𝐵 ) < ( ( 1 / 𝐴 ) ↑𝑐 𝐶 ) ) ) |
17 |
|
rpcxpcl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ ) |
18 |
17
|
ad2ant2rl |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ ) |
19 |
|
rpcxpcl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ ) |
20 |
19
|
ad2ant2r |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ ) |
21 |
18 20
|
ltrecd |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( 𝐴 ↑𝑐 𝐶 ) < ( 𝐴 ↑𝑐 𝐵 ) ↔ ( 1 / ( 𝐴 ↑𝑐 𝐵 ) ) < ( 1 / ( 𝐴 ↑𝑐 𝐶 ) ) ) ) |
22 |
10 16 21
|
3bitr4d |
⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 < 𝐶 ↔ ( 𝐴 ↑𝑐 𝐶 ) < ( 𝐴 ↑𝑐 𝐵 ) ) ) |