Metamath Proof Explorer

Theorem cxple

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

Ref Expression
Assertion cxple ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ A B ≤ A C

Proof

Step Hyp Ref Expression
1 cxplt ⊢ A ∈ ℝ ∧ 1 < A ∧ C ∈ ℝ ∧ B ∈ ℝ → C < B ↔ A C < A B
2 1 ancom2s ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → C < B ↔ A C < A B
3 2 notbid ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → ¬ C < B ↔ ¬ A C < A B
4 lenlt ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ ¬ C < B
5 4 adantl ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ ¬ C < B
6 simpll ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
7 0red ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → 0 ∈ ℝ
8 1red ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → 1 ∈ ℝ
9 0lt1 ⊢ 0 < 1
10 9 a1i ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → 0 < 1
11 simplr ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → 1 < A
12 7 8 6 10 11 lttrd ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → 0 < A
13 7 6 12 ltled ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → 0 ≤ A
14 simprl ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
15 recxpcl ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ → A B ∈ ℝ
16 6 13 14 15 syl3anc ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → A B ∈ ℝ
17 simprr ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
18 recxpcl ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ C ∈ ℝ → A C ∈ ℝ
19 6 13 17 18 syl3anc ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → A C ∈ ℝ
20 16 19 lenltd ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → A B ≤ A C ↔ ¬ A C < A B
21 3 5 20 3bitr4d ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ A B ≤ A C