Theorem: ZetaInvBnd_aux2 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Tactic:
simp only [inv_pos, sub_pos]
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * A < C₁ * A ^ (3 / 4)

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * A < C₁ * A ^ (3 / 4)
Tactic:
apply div_lt_iff (by positivity) |>.mp
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * A / A ^ (3 / 4) < C₁

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * A / A ^ (3 / 4) < C₁
Tactic:
rw [div_eq_mul_inv, ← Real.rpow_neg (by positivity), mul_assoc]
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * (A * A ^ (-(3 / 4))) < C₁

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * (A * A ^ (-(3 / 4))) < C₁
Tactic:
apply lt_div_iff' (by positivity) |>.mp
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A * A ^ (-(3 / 4)) < C₁ / (C₂ * 2)

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A * A ^ (-(3 / 4)) < C₁ / (C₂ * 2)
Tactic:
nth_rewrite 1 [← Real.rpow_one A]
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ 1 * A ^ (-(3 / 4)) < C₁ / (C₂ * 2)

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ 1 * A ^ (-(3 / 4)) < C₁ / (C₂ * 2)
Tactic:
rw [← Real.rpow_add (by positivity)]
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 + -(3 / 4)) < C₁ / (C₂ * 2)

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 + -(3 / 4)) < C₁ / (C₂ * 2)
Tactic:
norm_num
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 / 4) < C₁ / (C₂ * 2)

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 / 4) < C₁ / (C₂ * 2)
Tactic:
apply Real.rpow_lt_rpow_iff (z := 4) (by positivity) (by positivity) (by positivity) |>.mp
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ (A ^ (1 / 4)) ^ 4 < (C₁ / (C₂ * 2)) ^ 4

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ (A ^ (1 / 4)) ^ 4 < (C₁ / (C₂ * 2)) ^ 4
Tactic:
rw [← Real.rpow_mul (by positivity)]
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 / 4 * 4) < (C₁ / (C₂ * 2)) ^ 4

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 / 4 * 4) < (C₁ / (C₂ * 2)) ^ 4
Tactic:
norm_num
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A < (C₁ / (C₂ * 2)) ^ 4

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A < (C₁ / (C₂ * 2)) ^ 4
Tactic:
apply lt_of_le_of_lt hA
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4 < (C₁ / (C₂ * 2)) ^ 4

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4 < (C₁ / (C₂ * 2)) ^ 4
Tactic:
rw [div_mul_comm, mul_one]
State after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ (C₁ / (C₂ * 2)) ^ 4 / 2 < (C₁ / (C₂ * 2)) ^ 4

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ (C₁ / (C₂ * 2)) ^ 4 / 2 < (C₁ / (C₂ * 2)) ^ 4
Tactic:
apply half_lt_self
State after:
case a
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < (C₁ / (C₂ * 2)) ^ 4

State before:
case a
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < (C₁ / (C₂ * 2)) ^ 4
Tactic:
positivity
State after:
no goals

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < A ^ (3 / 4)
Tactic:
positivity
State after:
no goals

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 ≤ A
Tactic:
positivity
State after:
no goals

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < C₂ * 2
Tactic:
positivity
State after:
no goals

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < A
Tactic:
positivity
State after:
no goals

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 ≤ A ^ (1 / 4)
Tactic:
positivity
State after:
no goals

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 ≤ C₁ / (C₂ * 2)
Tactic:
positivity
State after:
no goals

State before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < 4
Tactic:
positivity
State after:
no goals