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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ Finset.filter IsPrimePow (Finset.range N) ⊆
    Finset.filter Nat.Prime (Finset.range N) ∪
      Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))
Tactic:
intro n
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (Finset.range N) →
    n ∈
      Finset.filter Nat.Prime (Finset.range N) ∪
        Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter IsPrimePow (Finset.range N) →
    n ∈
      Finset.filter Nat.Prime (Finset.range N) ∪
        Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))
Tactic:
simp only [Finset.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_union, Finset.mem_image,
  Finset.mem_product, Prod.exists, and_imp]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → IsPrimePow n → n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n < N → IsPrimePow n → n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
intro hnN hnprime
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
rcases prime_or_pow N n hnN hnprime with hp | ⟨m, hm, k, hk, h⟩
State after:
case inl
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
hp : n.Prime
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n

case inr.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n

State before:
case inl
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
hp : n.Prime
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
left
State after:
case inl.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
hp : n.Prime
⊢ n < N ∧ n.Prime

State before:
case inl.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
hp : n.Prime
⊢ n < N ∧ n.Prime
Tactic:
exact ⟨hnN, hp⟩
State after:
no goals

State before:
case inr.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ n < N ∧ n.Prime ∨ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
right
State after:
case inr.intro.intro.intro.intro.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n

State before:
case inr.intro.intro.intro.intro.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ ∃ a b, ((1 ≤ a ∧ a < ⌈√↑N⌉₊) ∧ b < Nat.log 2 N + 1) ∧ a ^ b = n
Tactic:
refine ⟨m, k, ?_⟩
State after:
case inr.intro.intro.intro.intro.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n

State before:
case inr.intro.intro.intro.intro.h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n
Tactic:
by_cases hm : m = 0
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n
Tactic:
rw [Nat.lt_ceil, Nat.lt_succ_iff]
State after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ ((1 ≤ m ∧ ↑m < √↑N) ∧ k ≤ Nat.log 2 N) ∧ m ^ k = n

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ ((1 ≤ m ∧ ↑m < √↑N) ∧ k ≤ Nat.log 2 N) ∧ m ^ k = n
Tactic:
have : 1 ≤ m := by omega
State after:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
this : 1 ≤ m
⊢ ((1 ≤ m ∧ ↑m < √↑N) ∧ k ≤ Nat.log 2 N) ∧ m ^ k = n

State before:
case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
this : 1 ≤ m
⊢ ((1 ≤ m ∧ ↑m < √↑N) ∧ k ≤ Nat.log 2 N) ∧ m ^ k = n
Tactic:
aesop
State after:
no goals

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n
Tactic:
rw [hm, zero_pow] at h
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0
hm : m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n

case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0 ^ k
hm : m = 0
⊢ k ≠ 0

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0
hm : m = 0
⊢ ((1 ≤ m ∧ m < ⌈√↑N⌉₊) ∧ k < Nat.log 2 N + 1) ∧ m ^ k = n

case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0 ^ k
hm : m = 0
⊢ k ≠ 0
Tactic:
exact False.elim (hnprime.ne_zero h)
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0 ^ k
hm : m = 0
⊢ k ≠ 0

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = 0 ^ k
hm : m = 0
⊢ k ≠ 0
Tactic:
rintro rfl
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
hm : m = 0
hk : 0 ≤ Nat.log 2 N
h : n = 0 ^ 0
⊢ False

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
hm : m = 0
hk : 0 ≤ Nat.log 2 N
h : n = 0 ^ 0
⊢ False
Tactic:
simp only [pow_zero] at h
State after:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
hm : m = 0
hk : 0 ≤ Nat.log 2 N
h : n = 1
⊢ False

State before:
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
hm : m = 0
hk : 0 ≤ Nat.log 2 N
h : n = 1
⊢ False
Tactic:
exact False.elim (hnprime.ne_one h)
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
hnprime : IsPrimePow n
m : ℕ
hm✝ : ↑m < √↑N
k : ℕ
hk : k ≤ Nat.log 2 N
h : n = m ^ k
hm : ¬m = 0
⊢ 1 ≤ m
Tactic:
omega
State after:
no goals