Theorem: Usa1974P2.usa1974_p2_wlog (Compfiles/Usa1974P2.lean)

State before:
⊢ ∀ (a b c : ℝ), a > 0 → b > 0 → c > 0 → a ≥ b → b ≥ c → a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Tactic:
intros a b c ha hb hc hab hbc
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Tactic:
have habc : a * b * c > 0 := Real.mul_pos (Real.mul_pos ha hb) hc
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Tactic:
have h : (a ^ a * b ^ b * c ^ c) * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) =
          (a * b * c) ^ (a + b + c) := by
  simp (discharger := positivity) only [Real.rpow_add, Real.mul_rpow]
  ring
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c ≥ (a * b * c) ^ ((a + b + c) / 3)
Tactic:
apply le_of_pow_le_pow_left (by decide : 3 ≠ 0) (by positivity)
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ ((a * b * c) ^ ((a + b + c) / 3)) ^ 3 ≤ (a ^ a * b ^ b * c ^ c) ^ 3

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ ((a * b * c) ^ ((a + b + c) / 3)) ^ 3 ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
rw [←Real.rpow_natCast]
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ ((a * b * c) ^ ((a + b + c) / 3)) ^ ↑3 ≤ (a ^ a * b ^ b * c ^ c) ^ 3

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ ((a * b * c) ^ ((a + b + c) / 3)) ^ ↑3 ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
rw [←(Real.rpow_mul (le_of_lt habc))]
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ (a * b * c) ^ ((a + b + c) / 3 * ↑3) ≤ (a ^ a * b ^ b * c ^ c) ^ 3

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ (a * b * c) ^ ((a + b + c) / 3 * ↑3) ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
norm_num
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ (a * b * c) ^ (a + b + c) ≤ (a ^ a * b ^ b * c ^ c) ^ 3

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ (a * b * c) ^ (a + b + c) ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
rw [←h]
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤ (a ^ a * b ^ b * c ^ c) ^ 3

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤ (a ^ a * b ^ b * c ^ c) ^ 3
Tactic:
rw [pow_three']
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)
Tactic:
have hab' := Real.log_le_log hb hab
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)
Tactic:
have hbc' := Real.log_le_log hc hbc
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) ≤
    a ^ a * b ^ b * c ^ c * (a ^ a * b ^ b * c ^ c) * (a ^ a * b ^ b * c ^ c)
Tactic:
gcongr ?_ * ?_ * ?_
State after:
case h₁.h₁
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ a * b ^ b * c ^ c ≤ a ^ a * b ^ b * c ^ c

case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ b * b ^ c * c ^ a ≤ a ^ a * b ^ b * c ^ c

case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ c * b ^ a * c ^ b ≤ a ^ a * b ^ b * c ^ c

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
Tactic:
simp (discharger := positivity) only [Real.rpow_add, Real.mul_rpow]
State after:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) =
    a ^ a * b ^ a * c ^ a * (a ^ b * b ^ b * c ^ b) * (a ^ c * b ^ c * c ^ c)

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
⊢ a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) =
    a ^ a * b ^ a * c ^ a * (a ^ b * b ^ b * c ^ b) * (a ^ c * b ^ c * c ^ c)
Tactic:
ring
State after:
no goals

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ 3 ≠ 0
Tactic:
decide
State after:
no goals

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
⊢ 0 ≤ a ^ a * b ^ b * c ^ c
Tactic:
positivity
State after:
no goals

State before:
case h₁.h₁
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ a * b ^ b * c ^ c ≤ a ^ a * b ^ b * c ^ c
Tactic:
rfl
State after:
no goals

State before:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ b * b ^ c * c ^ a ≤ a ^ a * b ^ b * c ^ c
Tactic:
rw [←(Real.log_le_log_iff (by positivity) (by positivity))]
State after:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ (a ^ b * b ^ c * c ^ a).log ≤ (a ^ a * b ^ b * c ^ c).log

State before:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ (a ^ b * b ^ c * c ^ a).log ≤ (a ^ a * b ^ b * c ^ c).log
Tactic:
simp (discharger := positivity) only [Real.log_mul, Real.log_rpow]
State after:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ b * a.log + c * b.log + a * c.log ≤ a * a.log + b * b.log + c * c.log

State before:
case h₁.h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ b * a.log + c * b.log + a * c.log ≤ a * a.log + b * b.log + c * c.log
Tactic:
nlinarith only [hab', hbc', hab, hbc]
State after:
no goals

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ 0 < a ^ b * b ^ c * c ^ a
Tactic:
positivity
State after:
no goals

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ 0 < a ^ a * b ^ b * c ^ c
Tactic:
positivity
State after:
no goals

State before:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ a ^ c * b ^ a * c ^ b ≤ a ^ a * b ^ b * c ^ c
Tactic:
rw [←(Real.log_le_log_iff (by positivity) (by positivity))]
State after:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ (a ^ c * b ^ a * c ^ b).log ≤ (a ^ a * b ^ b * c ^ c).log

State before:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ (a ^ c * b ^ a * c ^ b).log ≤ (a ^ a * b ^ b * c ^ c).log
Tactic:
simp (discharger := positivity) only [Real.log_mul, Real.log_rpow]
State after:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ c * a.log + a * b.log + b * c.log ≤ a * a.log + b * b.log + c * c.log

State before:
case h₂
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ c * a.log + a * b.log + b * c.log ≤ a * a.log + b * b.log + c * c.log
Tactic:
nlinarith only [hab', hbc', hab, hbc]
State after:
no goals

State before:
a b c : ℝ
ha : a > 0
hb : b > 0
hc : c > 0
hab : a ≥ b
hbc : b ≥ c
habc : a * b * c > 0
h : a ^ a * b ^ b * c ^ c * (a ^ b * b ^ c * c ^ a) * (a ^ c * b ^ a * c ^ b) = (a * b * c) ^ (a + b + c)
hab' : b.log ≤ a.log
hbc' : c.log ≤ b.log
⊢ 0 < a ^ c * b ^ a * c ^ b
Tactic:
positivity
State after:
no goals