This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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