Metamath Proof Explorer


Theorem cxplt3

Description: Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Assertion cxplt3 ( ( ( 𝐴 ∈ ℝ+𝐴 < 1 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 < 𝐶 ↔ ( 𝐴𝑐 𝐶 ) < ( 𝐴𝑐 𝐵 ) ) )

Proof

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 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 < 𝐶 ↔ ( 𝐴𝑐 𝐶 ) < ( 𝐴𝑐 𝐵 ) ) )