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

Metamath Proof Explorer

Theorem cxple3

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

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

Proof

Step Hyp Ref Expression
1 cxplt3 ⊢ A ∈ ℝ + ∧ A < 1 ∧ C ∈ ℝ ∧ B ∈ ℝ → C < B ↔ A B < A C
2 1 ancom2s ⊢ A ∈ ℝ + ∧ A < 1 ∧ B ∈ ℝ ∧ C ∈ ℝ → C < B ↔ A B < A C
3 2 notbid ⊢ A ∈ ℝ + ∧ A < 1 ∧ B ∈ ℝ ∧ C ∈ ℝ → ¬ C < B ↔ ¬ A B < A C
4 lenlt ⊢ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ ¬ C < B
5 4 adantl ⊢ A ∈ ℝ + ∧ A < 1 ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ ¬ C < B
6 rpcxpcl ⊢ A ∈ ℝ + ∧ C ∈ ℝ → A C ∈ ℝ +
7 6 ad2ant2rl ⊢ A ∈ ℝ + ∧ A < 1 ∧ B ∈ ℝ ∧ C ∈ ℝ → A C ∈ ℝ +
8 rpcxpcl ⊢ A ∈ ℝ + ∧ B ∈ ℝ → A B ∈ ℝ +
9 8 ad2ant2r ⊢ A ∈ ℝ + ∧ A < 1 ∧ B ∈ ℝ ∧ C ∈ ℝ → A B ∈ ℝ +
10 rpre ⊢ A C ∈ ℝ + → A C ∈ ℝ
11 rpre ⊢ A B ∈ ℝ + → A B ∈ ℝ
12 lenlt ⊢ A C ∈ ℝ ∧ A B ∈ ℝ → A C ≤ A B ↔ ¬ A B < A C
13 10 11 12 syl2an ⊢ A C ∈ ℝ + ∧ A B ∈ ℝ + → A C ≤ A B ↔ ¬ A B < A C
14 7 9 13 syl2anc ⊢ A ∈ ℝ + ∧ A < 1 ∧ B ∈ ℝ ∧ C ∈ ℝ → A C ≤ A B ↔ ¬ A B < A C
15 3 5 14 3bitr4d ⊢ A ∈ ℝ + ∧ A < 1 ∧ B ∈ ℝ ∧ C ∈ ℝ → B ≤ C ↔ A C ≤ A B