-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem dValue_pos (hN₃ : 8 ≤ N) : 0 < dValue N

Proof state:
case h
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ^ 2 ≤ log ↑N

Tactic:
rw [one_pow, le_log_iff_exp_le hN₀]

Result:
case h
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ rexp 1 ≤ ↑N

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 0 < 8

Tactic:
norm_num

Result:
no goals

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * ↑(nValue N) ≤ log ↑N

Tactic:
apply (mul_le_mul_of_nonneg_left this <| log_nonneg one_le_two).trans _

Result:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * (2 * √(log ↑N)) ≤ log ↑N

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ≤ √(log ↑N)

Tactic:
apply le_sqrt_of_sq_le

Result:
case h
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ^ 2 ≤ log ↑N

Proof state:
case h
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ rexp 1 ≤ ↑N

Tactic:
exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)

Result:
no goals

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ √(log ↑N) + 1 ≤ 2 * √(log ↑N)

Tactic:
rw [two_mul, add_le_add_iff_left]

Result:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ≤ √(log ↑N)

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * 2 ≤ √(log ↑N)

Tactic:
apply log_two_mul_two_le_sqrt_log_eight.trans

Result:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ √(log 8) ≤ √(log ↑N)

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑N ^ (↑(nValue N))⁻¹ ≠ 0

Tactic:
exact (rpow_pos_of_pos hN₀ _).ne'

Result:
no goals

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < dValue N

Tactic:
rw [dValue, floor_pos, ← log_le_log_iff zero_lt_one, log_one, log_div _ two_ne_zero, log_rpow hN₀,
  inv_mul_eq_div, sub_nonneg, le_div_iff₀]

Result:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ log 2 * ↑(nValue N) ≤ log ↑N

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑(nValue N)

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑N ^ (↑(nValue N))⁻¹ ≠ 0

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹ / 2

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 2 ≤ 8

Tactic:
norm_num

Result:
no goals

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ √(log 8) ≤ √(log ↑N)

Tactic:
apply Real.sqrt_le_sqrt

Result:
case h
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 8 ≤ log ↑N

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < 8

Tactic:
norm_num

Result:
no goals

Proof state:
N : ℕ
hN₃ : 8 ≤ N
⊢ 0 < dValue N

Tactic:
have hN₀ : 0 < (N : ℝ) := cast_pos.2 (succ_pos'.trans_le hN₃)

Result:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < dValue N

Proof state:
case h
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 8 ≤ log ↑N

Tactic:
exact log_le_log (by norm_num) (mod_cast hN₃)

Result:
no goals

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 2.7182818286 ≤ ↑8

Tactic:
norm_num

Result:
no goals

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * (2 * √(log ↑N)) ≤ log ↑N

Tactic:
rw [← mul_assoc, ← le_div_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 _), div_sqrt]

Result:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * 2 ≤ √(log ↑N)

N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < N

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ log 2 * ↑(nValue N) ≤ log ↑N

Tactic:
have : (nValue N : ℝ) ≤ 2 * √(log N) := by
  apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
  rw [two_mul, add_le_add_iff_left]
  apply le_sqrt_of_sq_le
  rw [one_pow, le_log_iff_exp_le hN₀]
  exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)

Result:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * ↑(nValue N) ≤ log ↑N

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹ / 2

Tactic:
exact div_pos (rpow_pos_of_pos hN₀ _) zero_lt_two

Result:
no goals

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ ↑(nValue N) ≤ 2 * √(log ↑N)

Tactic:
apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans

Result:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ √(log ↑N) + 1 ≤ 2 * √(log ↑N)

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 0 < ↑(nValue N)

Tactic:
exact cast_pos.2 (nValue_pos <| hN₃.trans' <| by norm_num)

Result:
no goals

Proof state:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ 1 < N

Tactic:
exact hN₃.trans_lt' (by norm_num)

Result:
no goals