Theorem: Nat.self_div_floor_bound (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
t : ℝ
t_ge : 1 ≤ |t|
⊢ let N := ⌊|t|⌋₊;
  |t| / ↑N ∈ Icc 1 2
Tactic:
intro N
State after:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
⊢ |t| / ↑N ∈ Icc 1 2

State before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
⊢ |t| / ↑N ∈ Icc 1 2
Tactic:
have Npos : 0 < N := Nat.floor_pos.mpr (by linarith)
State after:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
⊢ |t| / ↑N ∈ Icc 1 2

State before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
⊢ |t| / ↑N ∈ Icc 1 2
Tactic:
have N_le_t : N ≤ |t| := Nat.floor_le <| abs_nonneg _
State after:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| / ↑N ∈ Icc 1 2

State before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| / ↑N ∈ Icc 1 2
Tactic:
constructor
State after:
case left
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 1 ≤ |t| / ↑N

case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| / ↑N ≤ 2

State before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
⊢ 1 ≤ |t|
Tactic:
linarith
State after:
no goals

State before:
case left
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 1 ≤ |t| / ↑N
Tactic:
apply le_div_iff (by simp [Npos]) |>.mpr
State after:
case left
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 1 * ↑N ≤ |t|

State before:
case left
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 1 * ↑N ≤ |t|
Tactic:
simp [N_le_t]
State after:
no goals

State before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 0 < ↑N
Tactic:
simp [Npos]
State after:
no goals

State before:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| / ↑N ≤ 2
Tactic:
apply div_le_iff (by positivity) |>.mpr
State after:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| ≤ 2 * ↑N

State before:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| ≤ 2 * ↑N
Tactic:
suffices |t| < N + 1 by linarith [(by exact_mod_cast (by omega) : 1 ≤ (N : ℝ))]
State after:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| < ↑N + 1

State before:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| < ↑N + 1
Tactic:
apply Nat.lt_floor_add_one
State after:
no goals

State before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 0 < ↑N
Tactic:
positivity
State after:
no goals

State before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
this : |t| < ↑N + 1
⊢ |t| ≤ 2 * ↑N
Tactic:
linarith [(by exact_mod_cast (by omega) : 1 ≤ (N : ℝ))]
State after:
no goals

State before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
this : |t| < ↑N + 1
⊢ 1 ≤ ↑N
Tactic:
exact_mod_cast (by omega)
State after:
no goals

State before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
this : |t| < ↑N + 1
⊢ 1 ≤ N
Tactic:
omega
State after:
no goals