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

Metamath Proof Explorer

Theorem cxple2

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

Ref Expression
Assertion cxple2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simpl1l ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
2 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → 0 < 𝐴 )
3 1 2 elrpd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ+ )
4 3 adantr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) ∧ 0 < 𝐵 ) → 𝐴 ∈ ℝ+ )
5 simp2l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
6 5 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ )
7 simpr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) ∧ 0 < 𝐵 ) → 0 < 𝐵 )
8 6 7 elrpd ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ+ )
9 simp3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ+ )
10 9 ad2antrr ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) ∧ 0 < 𝐵 ) → 𝐶 ∈ ℝ+ )
11 simp3 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ+ )
12 11 rpred ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
13 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
14 13 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℝ )
15 12 14 remulcld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( log ‘ 𝐴 ) ) ∈ ℝ )
16 relogcl ⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
17 16 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ∈ ℝ )
18 12 17 remulcld ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐶 · ( log ‘ 𝐵 ) ) ∈ ℝ )
19 efle ⊢ ( ( ( 𝐶 · ( log ‘ 𝐴 ) ) ∈ ℝ ∧ ( 𝐶 · ( log ‘ 𝐵 ) ) ∈ ℝ ) → ( ( 𝐶 · ( log ‘ 𝐴 ) ) ≤ ( 𝐶 · ( log ‘ 𝐵 ) ) ↔ ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ≤ ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) )
20 15 18 19 syl2anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐶 · ( log ‘ 𝐴 ) ) ≤ ( 𝐶 · ( log ‘ 𝐵 ) ) ↔ ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ≤ ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) )
21 efle ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ ( log ‘ 𝐵 ) ∈ ℝ ) → ( ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ↔ ( exp ‘ ( log ‘ 𝐴 ) ) ≤ ( exp ‘ ( log ‘ 𝐵 ) ) ) )
22 14 17 21 syl2anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ↔ ( exp ‘ ( log ‘ 𝐴 ) ) ≤ ( exp ‘ ( log ‘ 𝐵 ) ) ) )
23 14 17 11 lemul2d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) ≤ ( log ‘ 𝐵 ) ↔ ( 𝐶 · ( log ‘ 𝐴 ) ) ≤ ( 𝐶 · ( log ‘ 𝐵 ) ) ) )
24 reeflog ⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
25 24 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
26 reeflog ⊢ ( 𝐵 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
27 26 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( exp ‘ ( log ‘ 𝐵 ) ) = 𝐵 )
28 25 27 breq12d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( ( exp ‘ ( log ‘ 𝐴 ) ) ≤ ( exp ‘ ( log ‘ 𝐵 ) ) ↔ 𝐴 ≤ 𝐵 ) )
29 22 23 28 3bitr3rd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐶 · ( log ‘ 𝐴 ) ) ≤ ( 𝐶 · ( log ‘ 𝐵 ) ) ) )
30 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
31 30 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
32 31 recnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
33 rpne0 ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
34 33 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ≠ 0 )
35 12 recnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
36 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
37 32 34 35 36 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) )
38 rpre ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
39 38 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
40 39 recnd ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
41 rpne0 ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
42 41 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ≠ 0 )
43 cxpef ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐶 ∈ ℂ ) → ( 𝐵 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) )
44 40 42 35 43 syl3anc ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 ↑𝑐 𝐶 ) = ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) )
45 37 44 breq12d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ↔ ( exp ‘ ( 𝐶 · ( log ‘ 𝐴 ) ) ) ≤ ( exp ‘ ( 𝐶 · ( log ‘ 𝐵 ) ) ) ) )
46 20 29 45 3bitr4d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )
47 4 8 10 46 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) ∧ 0 < 𝐵 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )
48 0re ⊢ 0 ∈ ℝ
49 simp1l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
50 ltnle ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 < 𝐴 ↔ ¬ 𝐴 ≤ 0 ) )
51 48 49 50 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 0 < 𝐴 ↔ ¬ 𝐴 ≤ 0 ) )
52 51 biimpa ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ¬ 𝐴 ≤ 0 )
53 9 rpred ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
54 53 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → 𝐶 ∈ ℝ )
55 rpcxpcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ )
56 3 54 55 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ )
57 rpgt0 ⊢ ( ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ → 0 < ( 𝐴 ↑𝑐 𝐶 ) )
58 rpre ⊢ ( ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ → ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ )
59 ltnle ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ ) → ( 0 < ( 𝐴 ↑𝑐 𝐶 ) ↔ ¬ ( 𝐴 ↑𝑐 𝐶 ) ≤ 0 ) )
60 48 58 59 sylancr ⊢ ( ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ → ( 0 < ( 𝐴 ↑𝑐 𝐶 ) ↔ ¬ ( 𝐴 ↑𝑐 𝐶 ) ≤ 0 ) )
61 57 60 mpbid ⊢ ( ( 𝐴 ↑𝑐 𝐶 ) ∈ ℝ+ → ¬ ( 𝐴 ↑𝑐 𝐶 ) ≤ 0 )
62 56 61 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ¬ ( 𝐴 ↑𝑐 𝐶 ) ≤ 0 )
63 53 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
64 9 rpne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ≠ 0 )
65 0cxp ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 0 ↑𝑐 𝐶 ) = 0 )
66 63 64 65 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 0 ↑𝑐 𝐶 ) = 0 )
67 66 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ( 0 ↑𝑐 𝐶 ) = 0 )
68 67 breq2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ( ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 0 ↑𝑐 𝐶 ) ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ 0 ) )
69 62 68 mtbird ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ¬ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 0 ↑𝑐 𝐶 ) )
70 52 69 2falsed ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ( 𝐴 ≤ 0 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 0 ↑𝑐 𝐶 ) ) )
71 breq2 ⊢ ( 0 = 𝐵 → ( 𝐴 ≤ 0 ↔ 𝐴 ≤ 𝐵 ) )
72 oveq1 ⊢ ( 0 = 𝐵 → ( 0 ↑𝑐 𝐶 ) = ( 𝐵 ↑𝑐 𝐶 ) )
73 72 breq2d ⊢ ( 0 = 𝐵 → ( ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 0 ↑𝑐 𝐶 ) ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )
74 71 73 bibi12d ⊢ ( 0 = 𝐵 → ( ( 𝐴 ≤ 0 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 0 ↑𝑐 𝐶 ) ) ↔ ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) ) )
75 70 74 syl5ibcom ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ( 0 = 𝐵 → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) ) )
76 75 imp ⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) ∧ 0 = 𝐵 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )
77 simp2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → 0 ≤ 𝐵 )
78 leloe ⊢ ( ( 0 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐵 ↔ ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) )
79 48 5 78 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 0 ≤ 𝐵 ↔ ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) )
80 77 79 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 0 < 𝐵 ∨ 0 = 𝐵 ) )
81 80 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ( 0 < 𝐵 ∨ 0 = 𝐵 ) )
82 47 76 81 mpjaodan ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 < 𝐴 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )
83 simpr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → 0 = 𝐴 )
84 simpl2r ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → 0 ≤ 𝐵 )
85 83 84 eqbrtrrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → 𝐴 ≤ 𝐵 )
86 66 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → ( 0 ↑𝑐 𝐶 ) = 0 )
87 83 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → ( 0 ↑𝑐 𝐶 ) = ( 𝐴 ↑𝑐 𝐶 ) )
88 86 87 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → 0 = ( 𝐴 ↑𝑐 𝐶 ) )
89 simpl2l ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → 𝐵 ∈ ℝ )
90 53 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → 𝐶 ∈ ℝ )
91 cxpge0 ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ∧ 𝐶 ∈ ℝ ) → 0 ≤ ( 𝐵 ↑𝑐 𝐶 ) )
92 89 84 90 91 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → 0 ≤ ( 𝐵 ↑𝑐 𝐶 ) )
93 88 92 eqbrtrrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) )
94 85 93 2thd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) ∧ 0 = 𝐴 ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )
95 simp1r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → 0 ≤ 𝐴 )
96 leloe ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
97 48 49 96 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
98 95 97 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 0 < 𝐴 ∨ 0 = 𝐴 ) )
99 82 94 98 mpjaodan ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) )