Theorem: UpperBnd_aux (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ let N := ⌊|t|⌋₊;
  0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
intro N
State after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
have Npos : 0 < N := Nat.floor_pos.mpr (by linarith)
State after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
have N_le_t : N ≤ |t| := Nat.floor_le <| abs_nonneg _
State after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
have logt_gt := logt_gt_one t_gt
State after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
have σ_gt : 1 - A < σ := by
  apply lt_of_lt_of_le ((sub_lt_sub_iff_left (a := 1)).mpr ?_) σ_ge
  exact (div_lt_iff (by linarith)).mpr <| lt_mul_right hA.1 logt_gt
State after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
refine ⟨Npos, N_le_t, logt_gt, σ_gt, by linarith [hA.2], ?_⟩
State after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ ↑σ + ↑t * I ≠ 1

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ ↑σ + ↑t * I ≠ 1
Tactic:
contrapose! t_gt
State after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : ↑σ + ↑t * I = 1
⊢ |t| ≤ 3

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : ↑σ + ↑t * I = 1
⊢ |t| ≤ 3
Tactic:
simp only [Complex.ext_iff, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one,
  sub_self, add_zero, one_re, add_im, mul_im, zero_add, one_im] at t_gt
State after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : σ = 1 ∧ t = 0
⊢ |t| ≤ 3

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : σ = 1 ∧ t = 0
⊢ |t| ≤ 3
Tactic:
norm_num [t_gt.2]
State after:
no goals

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
⊢ 1 ≤ |t|
Tactic:
linarith
State after:
no goals

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ 1 - A < σ
Tactic:
apply lt_of_lt_of_le ((sub_lt_sub_iff_left (a := 1)).mpr ?_) σ_ge
State after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ A / |t|.log < A

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ A / |t|.log < A
Tactic:
exact (div_lt_iff (by linarith)).mpr <| lt_mul_right hA.1 logt_gt
State after:
no goals

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ 0 < |t|.log
Tactic:
linarith
State after:
no goals

State before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ 0 < σ
Tactic:
linarith [hA.2]
State after:
no goals