1. FormalConjectures
  2. ErdosProblems
  3. «17»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 17

Reference: erdosproblems.com/17

open Filter Asymptotics Realnamespace Erdos17

A prime $p$ is a cluster prime if every even natural number $n \le p - 3$ can be written as a difference of two primes $q_1 - q_2$ with $q_1, q_2 \le p$.

def IsClusterPrime (p : ℕ) : Prop := p.Prime ∧ ∀ {n : ℕ}, Even n → n ≤ (p - 3 : ℤ) → ∃ q₁ q₂ : ℕ, q₁.Prime ∧ q₂.Prime ∧ q₁ ≤ p ∧ q₂ ≤ p ∧ n = (q₁ - q₂ : ℤ)

Erdős Problem 17. Are there infinitely many cluster primes?

@[category research open, AMS 11] theorem erdos_17 : answer(sorry) ↔ {p : ℕ | IsClusterPrime p}.Infinite := ⊢ True ↔ {p | IsClusterPrime p}.Infinite All goals completed! 🐙

The counting function of cluster primes $\le n$.

noncomputable def clusterPrimeCount (n : ℕ) : ℕ := Nat.card {p : ℕ | p ≤ n ∧ IsClusterPrime p}

In 1999 Blecksmith, Erdős, and Selfridge [BES99] proved the upper bound $$\pi^{\mathcal{C}}(x) \ll_A x(\log x)^{-A}$$ for every real $A > 0$.

[BES99] Blecksmith, Richard and Erd\H os, Paul and Selfridge, J. L., Cluster primes. Amer. Math. Monthly (1999), 43--48.

@[category research solved, AMS 11] theorem erdos_17.variants.upper_BES {A : ℝ} (hA : 0 < A) : (fun x ↦ (clusterPrimeCount x : ℝ)) =O[atTop] fun x ↦ x / (log x) ^ A := A:ℝhA:0 < A⊢ (fun x ↦ ↑(clusterPrimeCount x)) =O[atTop] fun x ↦ ↑x / log ↑x ^ A All goals completed! 🐙

In 2003, Elsholtz [El03] refined the upper bound to $$\pi^{\mathcal{C}}(x) \ll x,\exp!\bigl(-c(\log\log x)^2\bigr)$$ for every real $0 < c < 1/8$.

[El03] Elsholtz, Christian, On cluster primes. Acta Arith. (2003), 281--284.

@[category research solved, AMS 11] theorem erdos_17.variants.upper_Elsholtz : ∃ C : ℝ, 0 < C ∧ ∀ c ∈ Set.Ioo 0 (1 / 8), IsBigOWith C atTop (fun x ↦ (clusterPrimeCount x : ℝ)) (fun x ↦ x * exp (-c * (log (log x)) ^ 2)) := ⊢ ∃ C, 0 < C ∧ ∀ c ∈ Set.Ioo 0 (1 / 8), IsBigOWith C atTop (fun x ↦ ↑(clusterPrimeCount x)) fun x ↦ ↑x * rexp (-c * log (log ↑x) ^ 2) All goals completed! 🐙

$97$ is the smallest prime that is not a cluster prime.

cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:x < 98hx:Nat.Prime xxl:Nat.Prime (x + 88)⊢ 9 < x cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:x < 98hx:Nat.Prime xxl:x ≤ 9⊢ ¬Nat.Prime (x + 88) cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:0 < 98hx:Nat.Prime 0xl:0 ≤ 9⊢ ¬Nat.Prime (0 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:1 < 98hx:Nat.Prime 1xl:1 ≤ 9⊢ ¬Nat.Prime (1 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:2 < 98hx:Nat.Prime 2xl:2 ≤ 9⊢ ¬Nat.Prime (2 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:3 < 98hx:Nat.Prime 3xl:3 ≤ 9⊢ ¬Nat.Prime (3 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:4 < 98hx:Nat.Prime 4xl:4 ≤ 9⊢ ¬Nat.Prime (4 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:5 < 98hx:Nat.Prime 5xl:5 ≤ 9⊢ ¬Nat.Prime (5 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:6 < 98hx:Nat.Prime 6xl:6 ≤ 9⊢ ¬Nat.Prime (6 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:7 < 98hx:Nat.Prime 7xl:7 ≤ 9⊢ ¬Nat.Prime (7 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:8 < 98hx:Nat.Prime 8xl:8 ≤ 9⊢ ¬Nat.Prime (8 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:9 < 98hx:Nat.Prime 9xl:9 ≤ 9⊢ ¬Nat.Prime (9 + 88) cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:0 < 98hx:Nat.Prime 0xl:0 ≤ 9⊢ ¬Nat.Prime (0 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:1 < 98hx:Nat.Prime 1xl:1 ≤ 9⊢ ¬Nat.Prime (1 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:2 < 98hx:Nat.Prime 2xl:2 ≤ 9⊢ ¬Nat.Prime (2 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:3 < 98hx:Nat.Prime 3xl:3 ≤ 9⊢ ¬Nat.Prime (3 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:4 < 98hx:Nat.Prime 4xl:4 ≤ 9⊢ ¬Nat.Prime (4 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:5 < 98hx:Nat.Prime 5xl:5 ≤ 9⊢ ¬Nat.Prime (5 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:6 < 98hx:Nat.Prime 6xl:6 ≤ 9⊢ ¬Nat.Prime (6 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:7 < 98hx:Nat.Prime 7xl:7 ≤ 9⊢ ¬Nat.Prime (7 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:8 < 98hx:Nat.Prime 8xl:8 ≤ 9⊢ ¬Nat.Prime (8 + 88)cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:9 < 98hx:Nat.Prime 9xl:9 ≤ 9⊢ ¬Nat.Prime (9 + 88) cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:9 < 98hx:Nat.Prime 9xl:9 ≤ 9⊢ False cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:1 < 98hx:Nat.Prime 1xl:1 ≤ 9⊢ False cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:1 < 98xl:1 ≤ 9hx:¬False⊢ ¬Nat.Prime 1 All goals completed! 🐙 cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:9 < 98hx:Nat.Prime 9xl:9 ≤ 9⊢ False cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)x:ℕxl✝:9 < 98xl:9 ≤ 9hx:¬False⊢ ¬Nat.Prime 9 All goals completed! 🐙 cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)⊢ 97 ∈ lowerBounds {p | Nat.Prime p ∧ ¬IsClusterPrime p} -- `97` is a lower bound: every prime `< 97` is a cluster prime, so cannot lie -- in the set of non-cluster primes. cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime bhbnc:¬IsClusterPrime b⊢ 97 ≤ b cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime bhbnc:¬IsClusterPrime bhlt:b < 97⊢ False cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 0hbnc:¬IsClusterPrime 0hlt:0 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 1hbnc:¬IsClusterPrime 1hlt:1 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 2hbnc:¬IsClusterPrime 2hlt:2 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 3hbnc:¬IsClusterPrime 3hlt:3 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 4hbnc:¬IsClusterPrime 4hlt:4 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 5hbnc:¬IsClusterPrime 5hlt:5 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 6hbnc:¬IsClusterPrime 6hlt:6 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 7hbnc:¬IsClusterPrime 7hlt:7 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 8hbnc:¬IsClusterPrime 8hlt:8 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 9hbnc:¬IsClusterPrime 9hlt:9 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 10hbnc:¬IsClusterPrime 10hlt:10 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 11hbnc:¬IsClusterPrime 11hlt:11 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 12hbnc:¬IsClusterPrime 12hlt:12 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 13hbnc:¬IsClusterPrime 13hlt:13 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 14hbnc:¬IsClusterPrime 14hlt:14 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 15hbnc:¬IsClusterPrime 15hlt:15 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 16hbnc:¬IsClusterPrime 16hlt:16 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 17hbnc:¬IsClusterPrime 17hlt:17 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 18hbnc:¬IsClusterPrime 18hlt:18 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 19hbnc:¬IsClusterPrime 19hlt:19 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 20hbnc:¬IsClusterPrime 20hlt:20 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 21hbnc:¬IsClusterPrime 21hlt:21 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 22hbnc:¬IsClusterPrime 22hlt:22 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 23hbnc:¬IsClusterPrime 23hlt:23 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 24hbnc:¬IsClusterPrime 24hlt:24 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 25hbnc:¬IsClusterPrime 25hlt:25 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 26hbnc:¬IsClusterPrime 26hlt:26 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 27hbnc:¬IsClusterPrime 27hlt:27 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 28hbnc:¬IsClusterPrime 28hlt:28 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 29hbnc:¬IsClusterPrime 29hlt:29 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 30hbnc:¬IsClusterPrime 30hlt:30 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 31hbnc:¬IsClusterPrime 31hlt:31 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 32hbnc:¬IsClusterPrime 32hlt:32 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 33hbnc:¬IsClusterPrime 33hlt:33 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 34hbnc:¬IsClusterPrime 34hlt:34 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 35hbnc:¬IsClusterPrime 35hlt:35 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 36hbnc:¬IsClusterPrime 36hlt:36 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 37hbnc:¬IsClusterPrime 37hlt:37 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 38hbnc:¬IsClusterPrime 38hlt:38 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 39hbnc:¬IsClusterPrime 39hlt:39 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 40hbnc:¬IsClusterPrime 40hlt:40 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 41hbnc:¬IsClusterPrime 41hlt:41 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 42hbnc:¬IsClusterPrime 42hlt:42 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 43hbnc:¬IsClusterPrime 43hlt:43 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 44hbnc:¬IsClusterPrime 44hlt:44 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 45hbnc:¬IsClusterPrime 45hlt:45 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 46hbnc:¬IsClusterPrime 46hlt:46 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 47hbnc:¬IsClusterPrime 47hlt:47 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 48hbnc:¬IsClusterPrime 48hlt:48 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 49hbnc:¬IsClusterPrime 49hlt:49 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 50hbnc:¬IsClusterPrime 50hlt:50 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 51hbnc:¬IsClusterPrime 51hlt:51 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 52hbnc:¬IsClusterPrime 52hlt:52 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 53hbnc:¬IsClusterPrime 53hlt:53 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 54hbnc:¬IsClusterPrime 54hlt:54 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 55hbnc:¬IsClusterPrime 55hlt:55 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 56hbnc:¬IsClusterPrime 56hlt:56 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 57hbnc:¬IsClusterPrime 57hlt:57 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 58hbnc:¬IsClusterPrime 58hlt:58 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 59hbnc:¬IsClusterPrime 59hlt:59 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 60hbnc:¬IsClusterPrime 60hlt:60 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 61hbnc:¬IsClusterPrime 61hlt:61 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 62hbnc:¬IsClusterPrime 62hlt:62 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 63hbnc:¬IsClusterPrime 63hlt:63 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 64hbnc:¬IsClusterPrime 64hlt:64 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 65hbnc:¬IsClusterPrime 65hlt:65 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 66hbnc:¬IsClusterPrime 66hlt:66 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 67hbnc:¬IsClusterPrime 67hlt:67 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 68hbnc:¬IsClusterPrime 68hlt:68 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 69hbnc:¬IsClusterPrime 69hlt:69 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 70hbnc:¬IsClusterPrime 70hlt:70 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 71hbnc:¬IsClusterPrime 71hlt:71 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 72hbnc:¬IsClusterPrime 72hlt:72 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 73hbnc:¬IsClusterPrime 73hlt:73 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 74hbnc:¬IsClusterPrime 74hlt:74 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 75hbnc:¬IsClusterPrime 75hlt:75 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 76hbnc:¬IsClusterPrime 76hlt:76 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 77hbnc:¬IsClusterPrime 77hlt:77 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 78hbnc:¬IsClusterPrime 78hlt:78 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 79hbnc:¬IsClusterPrime 79hlt:79 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 80hbnc:¬IsClusterPrime 80hlt:80 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 81hbnc:¬IsClusterPrime 81hlt:81 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 82hbnc:¬IsClusterPrime 82hlt:82 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 83hbnc:¬IsClusterPrime 83hlt:83 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 84hbnc:¬IsClusterPrime 84hlt:84 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 85hbnc:¬IsClusterPrime 85hlt:85 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 86hbnc:¬IsClusterPrime 86hlt:86 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 87hbnc:¬IsClusterPrime 87hlt:87 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 88hbnc:¬IsClusterPrime 88hlt:88 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 89hbnc:¬IsClusterPrime 89hlt:89 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 90hbnc:¬IsClusterPrime 90hlt:90 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 91hbnc:¬IsClusterPrime 91hlt:91 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 92hbnc:¬IsClusterPrime 92hlt:92 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 93hbnc:¬IsClusterPrime 93hlt:93 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 94hbnc:¬IsClusterPrime 94hlt:94 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 95hbnc:¬IsClusterPrime 95hlt:95 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 96hbnc:¬IsClusterPrime 96hlt:96 < 97⊢ False cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 0hbnc:¬IsClusterPrime 0hlt:0 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 1hbnc:¬IsClusterPrime 1hlt:1 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 2hbnc:¬IsClusterPrime 2hlt:2 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 3hbnc:¬IsClusterPrime 3hlt:3 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 4hbnc:¬IsClusterPrime 4hlt:4 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 5hbnc:¬IsClusterPrime 5hlt:5 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 6hbnc:¬IsClusterPrime 6hlt:6 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 7hbnc:¬IsClusterPrime 7hlt:7 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 8hbnc:¬IsClusterPrime 8hlt:8 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 9hbnc:¬IsClusterPrime 9hlt:9 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 10hbnc:¬IsClusterPrime 10hlt:10 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 11hbnc:¬IsClusterPrime 11hlt:11 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 12hbnc:¬IsClusterPrime 12hlt:12 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 13hbnc:¬IsClusterPrime 13hlt:13 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 14hbnc:¬IsClusterPrime 14hlt:14 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 15hbnc:¬IsClusterPrime 15hlt:15 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 16hbnc:¬IsClusterPrime 16hlt:16 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 17hbnc:¬IsClusterPrime 17hlt:17 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 18hbnc:¬IsClusterPrime 18hlt:18 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 19hbnc:¬IsClusterPrime 19hlt:19 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 20hbnc:¬IsClusterPrime 20hlt:20 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 21hbnc:¬IsClusterPrime 21hlt:21 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 22hbnc:¬IsClusterPrime 22hlt:22 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 23hbnc:¬IsClusterPrime 23hlt:23 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 24hbnc:¬IsClusterPrime 24hlt:24 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 25hbnc:¬IsClusterPrime 25hlt:25 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 26hbnc:¬IsClusterPrime 26hlt:26 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 27hbnc:¬IsClusterPrime 27hlt:27 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 28hbnc:¬IsClusterPrime 28hlt:28 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 29hbnc:¬IsClusterPrime 29hlt:29 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 30hbnc:¬IsClusterPrime 30hlt:30 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 31hbnc:¬IsClusterPrime 31hlt:31 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 32hbnc:¬IsClusterPrime 32hlt:32 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 33hbnc:¬IsClusterPrime 33hlt:33 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 34hbnc:¬IsClusterPrime 34hlt:34 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 35hbnc:¬IsClusterPrime 35hlt:35 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 36hbnc:¬IsClusterPrime 36hlt:36 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 37hbnc:¬IsClusterPrime 37hlt:37 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 38hbnc:¬IsClusterPrime 38hlt:38 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 39hbnc:¬IsClusterPrime 39hlt:39 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 40hbnc:¬IsClusterPrime 40hlt:40 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 41hbnc:¬IsClusterPrime 41hlt:41 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 42hbnc:¬IsClusterPrime 42hlt:42 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 43hbnc:¬IsClusterPrime 43hlt:43 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 44hbnc:¬IsClusterPrime 44hlt:44 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 45hbnc:¬IsClusterPrime 45hlt:45 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 46hbnc:¬IsClusterPrime 46hlt:46 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 47hbnc:¬IsClusterPrime 47hlt:47 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 48hbnc:¬IsClusterPrime 48hlt:48 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 49hbnc:¬IsClusterPrime 49hlt:49 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 50hbnc:¬IsClusterPrime 50hlt:50 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 51hbnc:¬IsClusterPrime 51hlt:51 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 52hbnc:¬IsClusterPrime 52hlt:52 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 53hbnc:¬IsClusterPrime 53hlt:53 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 54hbnc:¬IsClusterPrime 54hlt:54 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 55hbnc:¬IsClusterPrime 55hlt:55 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 56hbnc:¬IsClusterPrime 56hlt:56 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 57hbnc:¬IsClusterPrime 57hlt:57 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 58hbnc:¬IsClusterPrime 58hlt:58 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 59hbnc:¬IsClusterPrime 59hlt:59 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 60hbnc:¬IsClusterPrime 60hlt:60 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 61hbnc:¬IsClusterPrime 61hlt:61 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 62hbnc:¬IsClusterPrime 62hlt:62 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 63hbnc:¬IsClusterPrime 63hlt:63 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 64hbnc:¬IsClusterPrime 64hlt:64 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 65hbnc:¬IsClusterPrime 65hlt:65 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 66hbnc:¬IsClusterPrime 66hlt:66 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 67hbnc:¬IsClusterPrime 67hlt:67 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 68hbnc:¬IsClusterPrime 68hlt:68 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 69hbnc:¬IsClusterPrime 69hlt:69 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 70hbnc:¬IsClusterPrime 70hlt:70 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 71hbnc:¬IsClusterPrime 71hlt:71 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 72hbnc:¬IsClusterPrime 72hlt:72 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 73hbnc:¬IsClusterPrime 73hlt:73 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 74hbnc:¬IsClusterPrime 74hlt:74 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 75hbnc:¬IsClusterPrime 75hlt:75 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 76hbnc:¬IsClusterPrime 76hlt:76 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 77hbnc:¬IsClusterPrime 77hlt:77 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 78hbnc:¬IsClusterPrime 78hlt:78 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 79hbnc:¬IsClusterPrime 79hlt:79 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 80hbnc:¬IsClusterPrime 80hlt:80 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 81hbnc:¬IsClusterPrime 81hlt:81 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 82hbnc:¬IsClusterPrime 82hlt:82 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 83hbnc:¬IsClusterPrime 83hlt:83 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 84hbnc:¬IsClusterPrime 84hlt:84 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 85hbnc:¬IsClusterPrime 85hlt:85 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 86hbnc:¬IsClusterPrime 86hlt:86 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 87hbnc:¬IsClusterPrime 87hlt:87 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 88hbnc:¬IsClusterPrime 88hlt:88 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 89hbnc:¬IsClusterPrime 89hlt:89 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 90hbnc:¬IsClusterPrime 90hlt:90 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 91hbnc:¬IsClusterPrime 91hlt:91 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 92hbnc:¬IsClusterPrime 92hlt:92 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 93hbnc:¬IsClusterPrime 93hlt:93 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 94hbnc:¬IsClusterPrime 94hlt:94 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 95hbnc:¬IsClusterPrime 95hlt:95 < 97⊢ Falsecluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 96hbnc:¬IsClusterPrime 96hlt:96 < 97⊢ False first | exact absurd hbp (cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 96hbnc:¬IsClusterPrime 96hlt:96 < 97⊢ ¬Nat.Prime 96 All goals completed! 🐙) | exact hbnc ((cluster_iff _ (cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 89hbnc:¬IsClusterPrime 89hlt:89 < 97⊢ Nat.Prime 89 All goals completed! 🐙)).mpr (cluster_iff:∀ (p : ℕ), Nat.Prime p → (IsClusterPrime p ↔ ∀ n ∈ Finset.range (p - 2), Even n → ∃ q₂ ∈ Finset.range (p + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ p)b:ℕhbp:Nat.Prime 89hbnc:¬IsClusterPrime 89hlt:89 < 97⊢ ∀ n ∈ Finset.range (89 - 2), Even n → ∃ q₂ ∈ Finset.range (89 + 1), Nat.Prime q₂ ∧ Nat.Prime (q₂ + n) ∧ q₂ + n ≤ 89 set_option maxRecDepth 8000 in All goals completed! 🐙))end Erdos17