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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
rw [isPrimePow_nat_iff_bounded n] at hnprime
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : ∃ p ≤ n, ∃ k ≤ n, p.Prime ∧ 0 < k ∧ p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : ∃ p ≤ n, ∃ k ≤ n, p.Prime ∧ 0 < k ∧ p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
obtain ⟨p, -, k, -, hp, hk_pos, hpkn⟩ := hnprime
State after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k

State before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
by_cases hk : k = 1
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
right
State after:
case neg.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k

State before:
case neg.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
refine ⟨p, ?_, k, ?_, ?_⟩
State after:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ↑p < √↑N

case neg.h.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ k ≤ Nat.log 2 N

case neg.h.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ n = p ^ k

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ n.Prime ∨ ∃ m, ↑m < √↑N ∧ ∃ k ≤ Nat.log 2 N, n = m ^ k
Tactic:
left
State after:
case pos.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ n.Prime

State before:
case pos.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ n.Prime
Tactic:
rw [← hpkn, hk, pow_one]
State after:
case pos.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ p.Prime

State before:
case pos.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : k = 1
⊢ p.Prime
Tactic:
exact hp
State after:
no goals

State before:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ↑p < √↑N
Tactic:
rw [Real.lt_sqrt]
State after:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ↑p ^ 2 < ↑N

case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 0 ≤ ↑p

State before:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ ↑p ^ 2 < ↑N

case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 0 ≤ ↑p
Tactic:
norm_cast
State after:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ p ^ 2 < N

case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 0 ≤ ↑p

State before:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ p ^ 2 < N
Tactic:
calc
  p^2 ≤ p^k := by
    gcongr; exact hp.one_le;omega
_ = n := hpkn
_ < N := hnN
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ p ^ 2 ≤ p ^ k
Tactic:
gcongr
State after:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 1 ≤ p

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 2 ≤ k

State before:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 1 ≤ p

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 2 ≤ k
Tactic:
exact hp.one_le
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 2 ≤ k

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 2 ≤ k
Tactic:
omega
State after:
no goals

State before:
case neg.h.refine_1
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 0 ≤ ↑p
Tactic:
positivity
State after:
no goals

State before:
case neg.h.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ k ≤ Nat.log 2 N
Tactic:
calc
  _ ≤ Nat.log p n := by
    apply Nat.le_log_of_pow_le hp.one_lt hpkn.le
  _ ≤ Nat.log 2 n := by
    apply Nat.log_anti_left (by norm_num) hp.two_le
  _ ≤ Nat.log 2 N := by
    apply Nat.log_mono_right hnN.le
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ k ≤ p.log n
Tactic:
apply Nat.le_log_of_pow_le hp.one_lt hpkn.le
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ p.log n ≤ Nat.log 2 n
Tactic:
apply Nat.log_anti_left (by norm_num) hp.two_le
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ Nat.log 2 n ≤ Nat.log 2 N
Tactic:
apply Nat.log_mono_right hnN.le
State after:
no goals

State before:
case neg.h.refine_3
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ n = p ^ k
Tactic:
exact hpkn.symm
State after:
no goals