Metamath Proof Explorer

Theorem cxplt2

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

Ref Expression
Assertion cxplt2 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → A < B ↔ A C < B C

Proof

Step Hyp Ref Expression
1 cxple2 ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ A ∈ ℝ ∧ 0 ≤ A ∧ C ∈ ℝ + → B ≤ A ↔ B C ≤ A C
2 1 3com12 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → B ≤ A ↔ B C ≤ A C
3 2 notbid ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → ¬ B ≤ A ↔ ¬ B C ≤ A C
4 simp1l ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → A ∈ ℝ
5 simp2l ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → B ∈ ℝ
6 4 5 ltnled ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → A < B ↔ ¬ B ≤ A
7 simp1r ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → 0 ≤ A
8 rpre ⊢ C ∈ ℝ + → C ∈ ℝ
9 8 3ad2ant3 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → C ∈ ℝ
10 recxpcl ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ C ∈ ℝ → A C ∈ ℝ
11 4 7 9 10 syl3anc ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → A C ∈ ℝ
12 simp2r ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → 0 ≤ B
13 recxpcl ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ → B C ∈ ℝ
14 5 12 9 13 syl3anc ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → B C ∈ ℝ
15 11 14 ltnled ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → A C < B C ↔ ¬ B C ≤ A C
16 3 6 15 3bitr4d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B ∧ C ∈ ℝ + → A < B ↔ A C < B C