Metamath Proof Explorer

Theorem cxplea

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

Ref Expression
Assertion cxplea ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → A B ≤ A C

Proof

Step Hyp Ref Expression
1 simpl3 ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C ∧ 1 < A → B ≤ C
2 simpl1l ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C ∧ 1 < A → A ∈ ℝ
3 simpr ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C ∧ 1 < A → 1 < A
4 simpl2 ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C ∧ 1 < A → B ∈ ℝ ∧ C ∈ ℝ
5 cxple ⊢ A ∈ ℝ ∧ 1 < A ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ A B ≤ A C
6 2 3 4 5 syl21anc ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C ∧ 1 < A → B ≤ C ↔ A B ≤ A C
7 1 6 mpbid ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C ∧ 1 < A → A B ≤ A C
8 1le1 ⊢ 1 ≤ 1
9 simp2l ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → B ∈ ℝ
10 9 recnd ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → B ∈ ℂ
11 1cxp ⊢ B ∈ ℂ → 1 B = 1
12 10 11 syl ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → 1 B = 1
13 simp2r ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → C ∈ ℝ
14 13 recnd ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → C ∈ ℂ
15 1cxp ⊢ C ∈ ℂ → 1 C = 1
16 14 15 syl ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → 1 C = 1
17 12 16 breq12d ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → 1 B ≤ 1 C ↔ 1 ≤ 1
18 8 17 mpbiri ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → 1 B ≤ 1 C
19 oveq1 ⊢ 1 = A → 1 B = A B
20 oveq1 ⊢ 1 = A → 1 C = A C
21 19 20 breq12d ⊢ 1 = A → 1 B ≤ 1 C ↔ A B ≤ A C
22 18 21 syl5ibcom ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → 1 = A → A B ≤ A C
23 22 imp ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C ∧ 1 = A → A B ≤ A C
24 1re ⊢ 1 ∈ ℝ
25 leloe ⊢ 1 ∈ ℝ ∧ A ∈ ℝ → 1 ≤ A ↔ 1 < A ∨ 1 = A
26 24 25 mpan ⊢ A ∈ ℝ → 1 ≤ A ↔ 1 < A ∨ 1 = A
27 26 biimpa ⊢ A ∈ ℝ ∧ 1 ≤ A → 1 < A ∨ 1 = A
28 27 3ad2ant1 ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → 1 < A ∨ 1 = A
29 7 23 28 mpjaodan ⊢ A ∈ ℝ ∧ 1 ≤ A ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ B ≤ C → A B ≤ A C