Metamath Proof Explorer

Theorem cxplt

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

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

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
2 rplogcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
3 2 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
4 3 rpred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
5 1 4 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ )
6 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
7 6 4 remulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐶 · ( log ‘ 𝐴 ) ) ∈ ℝ )
8 eflt ⊢ ( ( ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐶 · ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( ( 𝐵 · ( log ‘ 𝐴 ) ) < ( 𝐶 · ( log ‘ 𝐴 ) ) ↔ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) < ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) )
9 5 7 8 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( 𝐵 · ( log ‘ 𝐴 ) ) < ( 𝐶 · ( log ‘ 𝐴 ) ) ↔ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) < ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) )
10 1 6 3 ltmul1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 < 𝐶 ↔ ( 𝐵 · ( log ‘ 𝐴 ) ) < ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
11 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
12 11 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 ∈ ℂ )
13 0red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 ∈ ℝ )
14 1red ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 1 ∈ ℝ )
15 0lt1 ⊢ 0 < 1
16 15 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 < 1 )
17 simplr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 1 < 𝐴 )
18 13 14 11 16 17 lttrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 0 < 𝐴 )
19 18 gt0ne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐴 ≠ 0 )
20 1 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
21 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
22 12 19 20 21 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
23 6 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
24 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
25 12 19 23 24 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐴 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
26 22 25 breq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( ( 𝐴 ↑𝑐 𝐵 ) < ( 𝐴 ↑𝑐 𝐶 ) ↔ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) < ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ) )
27 9 10 26 3bitr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) → ( 𝐵 < 𝐶 ↔ ( 𝐴 ↑𝑐 𝐵 ) < ( 𝐴 ↑𝑐 𝐶 ) ) )