Theorem: BrunTitchmarsh.pows_small_primes_le (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    ↑(Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1)).card
Tactic:
norm_cast
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1)).card

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ (Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card ≤
    (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1)).card
Tactic:
exact Finset.card_image_le
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1)).card ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Tactic:
simp only [Finset.card_product, Nat.card_Ico, Finset.card_range, Nat.cast_mul, Nat.cast_add,
  Nat.cast_one]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Tactic:
by_cases hN : N = 0
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : N = 0
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Tactic:
have : 1 ≤ Nat.ceil (Real.sqrt N) := by
  simp only [Nat.one_le_ceil_iff, Real.sqrt_pos, Nat.cast_pos]
  omega
State after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Tactic:
gcongr ?_ * ?_
State after:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(⌈√↑N⌉₊ - 1) ≤ ↑N ^ (1 / 2)

case neg.h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(Nat.log 2 N) + 1 ≤ 1 + (↑N).log / Real.log 2

State before:
case neg.h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(Nat.log 2 N) + 1 ≤ 1 + (↑N).log / Real.log 2
Tactic:
rw [Nat.log_eq_floor_logb _ _ (by norm_num), Real.log_div_log, Nat.cast_two]
State after:
case neg.h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑⌊Real.logb 2 ↑N⌋₊ + 1 ≤ 1 + Real.logb 2 ↑N

State before:
case neg.h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
hlogb_nonneg : 0 ≤ Real.logb 2 ↑N
⊢ ↑⌊Real.logb 2 ↑N⌋₊ + 1 ≤ 1 + Real.logb 2 ↑N
Tactic:
linarith [Nat.floor_le hlogb_nonneg]
State after:
no goals

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : N = 0
⊢ ↑(⌈√↑N⌉₊ - 1) * (↑(Nat.log 2 N) + 1) ≤ ↑N ^ (1 / 2) * (1 + (↑N).log / Real.log 2)
Tactic:
simp [hN]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 1 ≤ ⌈√↑N⌉₊
Tactic:
simp only [Nat.one_le_ceil_iff, Real.sqrt_pos, Nat.cast_pos]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 0 < N

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ 0 < N
Tactic:
omega
State after:
no goals

State before:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑(⌈√↑N⌉₊ - 1) ≤ ↑N ^ (1 / 2)
Tactic:
rw [← Real.sqrt_eq_rpow, Nat.cast_sub this, Nat.cast_one]
State after:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N

State before:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N
Tactic:
have := Nat.ceil_lt_add_one (show 0 ≤ Real.sqrt N by positivity)
State after:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this✝ : 1 ≤ ⌈√↑N⌉₊
this : ↑⌈√↑N⌉₊ < √↑N + 1
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N

State before:
case neg.h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this✝ : 1 ≤ ⌈√↑N⌉₊
this : ↑⌈√↑N⌉₊ < √↑N + 1
⊢ ↑⌈√↑N⌉₊ - 1 ≤ √↑N
Tactic:
linarith
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 0 ≤ √↑N
Tactic:
positivity
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 0 ≤ Real.logb 2 ↑N
Tactic:
apply Real.logb_nonneg
State after:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 < 2

case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 ≤ ↑N

State before:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 < 2
Tactic:
norm_cast
State after:
no goals

State before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 ≤ ↑N
Tactic:
norm_cast
State after:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 ≤ N

State before:
case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
this : 1 ≤ ⌈√↑N⌉₊
⊢ 1 ≤ N
Tactic:
omega
State after:
no goals