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↔AB≤AC

Proof

Step Hyp Ref Expression
1 cxplt ⊢A∈ℝ∧1<A∧C∈ℝ∧B∈ℝ→C<B↔AC<AB
2 1 ancom2s ⊢A∈ℝ∧1<A∧B∈ℝ∧C∈ℝ→C<B↔AC<AB
3 2 notbid ⊢A∈ℝ∧1<A∧B∈ℝ∧C∈ℝ→¬C<B↔¬AC<AB
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∈ℝ→AB∈ℝ
16 6 13 14 15 syl3anc ⊢A∈ℝ∧1<A∧B∈ℝ∧C∈ℝ→AB∈ℝ
17 simprr ⊢A∈ℝ∧1<A∧B∈ℝ∧C∈ℝ→C∈ℝ
18 recxpcl ⊢A∈ℝ∧0≤A∧C∈ℝ→AC∈ℝ
19 6 13 17 18 syl3anc ⊢A∈ℝ∧1<A∧B∈ℝ∧C∈ℝ→AC∈ℝ
20 16 19 lenltd ⊢A∈ℝ∧1<A∧B∈ℝ∧C∈ℝ→AB≤AC↔¬AC<AB
21 3 5 20 3bitr4d ⊢A∈ℝ∧1<A∧B∈ℝ∧C∈ℝ→B≤C↔AB≤AC