| 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 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 ↑𝑐 𝐶 ) ≤ ( 𝐵 ↑𝑐 𝐶 ) ) ) |