Problems / erdos-402 / erdos-402--h3-v2--h1
Remaining sizes, |B| neither prime nor prime plus one
erdos-402--h3-v2--h1
open
Hole hcomp of erdos-402--h3-v2 (split by 20260929T200020Z-t0929-6-partial.lean).
$\displaystyle \begin{aligned}&0 \notin B,\ B \ne \emptyset,\ \gcd(B) = 1,\ |B|\ \text{not prime},\ |B| \ne q + 1\ \text{for every prime } q,\\&\forall a, b \in B:\ a \le |B| \cdot \gcd(a,b),\qquad \forall a \in B,\ \forall p\ \text{prime},\ \forall k \in \mathbb{N}:\ p^k \mid a \Rightarrow p^k < |B|\\&\Longrightarrow\ \exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\end{aligned}$
For every finite set B of positive integers (0 ∉ B, B nonempty) whose elements have greatest common divisor 1, whose size |B| is neither a prime nor one more than a prime, in which a ≤ |B|·gcd(a, b) for all a, b ∈ B, and in which every prime power dividing an element is below |B|, there are a, b ∈ B (possibly equal) with gcd(a, b) ≤ a/|B|. gcd(B) is the greatest common divisor of all elements of B; the final division is in ℚ, the rest is over ℕ.
Lean
theorem erdos_402__h3_v2__h1 : ∀ (B : Finset ℕ),
(0 : ℕ) ∉ B →
B.Nonempty →
B.gcd id = (1 : ℕ) →
¬Nat.Prime B.card →
(∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
(∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
(∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ) := by
sorryWhy does it end in sorry?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
How it is being proved
Open. A direct proof, or proofs of its holes, close it.
Proved from this hole by 20261001T115500Z-t1001-402a-partial.lean (merged in 86f4ca221398, attestation 000331).
hsmooth→ erdos-402--h3-v2--h1--h1 (open)$\displaystyle \begin{aligned}&0 \notin B,\ B \ne \emptyset,\ \gcd(B) = 1,\ |B|\ \text{not prime},\ |B| \ne q + 1\ \text{for every prime } q,\\&\forall a, b \in B:\ a \le |B| \cdot \gcd(a,b),\qquad \forall a \in B,\ \forall p\ \text{prime},\ \forall k \in \mathbb{N}:\ p^k \mid a \Rightarrow p^k < |B|\\&\Longrightarrow\ \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \bigl(\exists\, p\ \text{prime}:\ |B| \le 2p,\ \exists\, a \in B,\ p \mid a\bigr)\end{aligned}$
Read the partial proof (Lean)
theorem erdos_402__h3_v2__h1 : ∀ (B : Finset ℕ),
(0 : ℕ) ∉ B →
B.Nonempty →
B.gcd id = (1 : ℕ) →
¬Nat.Prime B.card →
(∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
(∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
(∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ) := by
-- Informal argument: annex 6a64518f9cd863c9abea3114b518f3172f4c73c6a187eb928b43db35f77c0002 on this node (graph PR #325, in the merge queue when this was prechecked).
-- Hole `hsmooth`: B has a pair with gcd(a, b) ≤ a / n, or an element with a prime factor p ≥ n / 2.
-- The assembly proves that the second alternative contradicts the strict inequalities.
have hsmooth : ∀ B : Finset ℕ, 0 ∉ B → B.Nonempty → B.gcd id = 1 → ¬ B.card.Prime →
(∀ q : ℕ, q.Prime → B.card ≠ q + 1) →
(∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
(∀ a ∈ B, ∀ p k : ℕ, p.Prime → p ^ k ∣ a → p ^ k < B.card) →
(∃ a ∈ B, ∃ b ∈ B, (a.gcd b : ℚ) ≤ (a : ℚ) / (B.card : ℚ)) ∨
∃ p : ℕ, p.Prime ∧ B.card ≤ 2 * p ∧ ∃ a ∈ B, p ∣ a := sorry
have big : ∀ S : Finset ℕ, (∀ x ∈ S, 0 < x) → S.Nonempty → ∃ x ∈ S, S.card ≤ x := by
intro S hpos hS
by_contra h
push Not at h
have hsub : S ⊆ Finset.Ioo 0 S.card := by
intro x hx
exact Finset.mem_Ioo.mpr ⟨hpos x hx, h x hx⟩
have h1 := Finset.card_le_card hsub
rw [Nat.card_Ioo] at h1
have h2 := hS.card_pos
omega
have key : ∀ (n p : ℕ) (X T : Finset ℕ), 0 < p → p < n →
(∀ x ∈ X, ∀ t ∈ T, 0 < x * t ∧ x * t < n ∧ ¬ p ∣ x * t) →
X.Nonempty → T.Nonempty → n ≤ X.card + T.card → False := by
intro n p X T hp hpn hxt hX hT hcard
have hXpos : ∀ x ∈ X, 0 < x := by
intro x hx
obtain ⟨t, ht⟩ := hT
have h := (hxt x hx t ht).1
exact Nat.pos_of_ne_zero (by rintro rfl; simp at h)
have hTpos : ∀ t ∈ T, 0 < t := by
intro t ht
obtain ⟨x, hx⟩ := hX
have h := (hxt x hx t ht).1
exact Nat.pos_of_ne_zero (by rintro rfl; simp at h)
obtain ⟨x0, hx0, hx0c⟩ := big X hXpos hX
obtain ⟨t0, ht0, ht0c⟩ := big T hTpos hT
have h1 := (hxt x0 hx0 t0 ht0).2.1
have h2 : X.card * T.card ≤ x0 * t0 := Nat.mul_le_mul hx0c ht0c
have hu := hX.card_pos
have hv := hT.card_pos
have hc2 : ((Finset.Ioo 0 n).erase p).card = n - 2 := by
rw [Finset.card_erase_of_mem (Finset.mem_Ioo.mpr ⟨hp, hpn⟩), Nat.card_Ioo]
omega
have h3 : X.card = 1 ∨ T.card = 1 := by
by_contra h
push Not at h
have h4 : 2 ≤ X.card := by omega
have h5 : 2 ≤ T.card := by omega
nlinarith
rcases h3 with hu1 | hv1
· have hsub : T.image (fun t => x0 * t) ⊆ (Finset.Ioo 0 n).erase p := by
intro y hy
obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hy
have h := hxt x0 hx0 t ht
rw [Finset.mem_erase, Finset.mem_Ioo]
exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩
have hc1 : (T.image (fun t => x0 * t)).card = T.card :=
Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_left (hXpos x0 hx0) h)
have h6 := Finset.card_le_card hsub
omega
· have hsub : X.image (fun x => x * t0) ⊆ (Finset.Ioo 0 n).erase p := by
intro y hy
obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hy
have h := hxt x hx t0 ht0
rw [Finset.mem_erase, Finset.mem_Ioo]
exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩
have hc1 : (X.image (fun x => x * t0)).card = X.card :=
Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_right (hTpos t0 ht0) h)
have h6 := Finset.card_le_card hsub
omega
have hlarge : ∀ B : Finset ℕ, 0 ∉ B →
(∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b) →
∀ p : ℕ, p.Prime → p < B.card →
(∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a = p * a.gcd b) →
(∃ a ∈ B, p ∣ a) → (∃ b ∈ B, ¬ p ∣ b) → False := by
intro B h0 hlt p hp hpn hA hexa hexb
obtain ⟨a0, ha0, hpa0⟩ := hexa
obtain ⟨b0, hb0, hpb0⟩ := hexb
have hG0 : (B.filter (fun b => ¬ p ∣ b)).gcd id ≠ 0 := by
intro h
have h1 : (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ id b0 :=
Finset.gcd_dvd (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)
rw [h] at h1
exact hpb0 (by rw [show b0 = 0 from Nat.eq_zero_of_zero_dvd h1]; exact dvd_zero p)
have hGb : ∀ b ∈ B, ¬ p ∣ b → (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ b := by
intro b hb hpb
exact Finset.gcd_dvd (f := id) (Finset.mem_filter.mpr ⟨hb, hpb⟩)
have hdG : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b →
a.gcd b ∣ (B.filter (fun b => ¬ p ∣ b)).gcd id := by
intro a ha hpa b hb hpb
apply Finset.dvd_gcd
intro b' hb'
obtain ⟨hb'B, hpb'⟩ := Finset.mem_filter.mp hb'
have e1 := hA a ha hpa b hb hpb
have e2 := hA a ha hpa b' hb'B hpb'
have e3 : a.gcd b = a.gcd b' := Nat.eq_of_mul_eq_mul_left hp.pos (e1.symm.trans e2)
rw [e3]
exact Nat.gcd_dvd_right a b'
have hprod : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b →
0 < ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧
((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) < B.card ∧
¬ p ∣ ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧
a * ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) = (B.filter (fun b => ¬ p ∣ b)).gcd id * p := by
intro a ha hpa b hb hpb
generalize hG : (B.filter (fun b => ¬ p ∣ b)).gcd id = G at *
obtain ⟨e, he⟩ := hdG a ha hpa b hb hpb
obtain ⟨s, hs⟩ := hGb b hb hpb
have ea := hA a ha hpa b hb hpb
have ha0' : 0 < a := Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha))
have hb0' : b ≠ 0 := fun h => h0 (h ▸ hb)
have hGp : G * p = e * a :=
calc G * p = a.gcd b * e * p := by rw [he]
_ = e * (p * a.gcd b) := by ring
_ = e * a := by rw [← ea]
have hx : G * p / a = e := Nat.div_eq_of_eq_mul_left ha0' hGp
have ht : b / G = s := by
rw [hs]
exact Nat.mul_div_cancel_left s (Nat.pos_of_ne_zero hG0)
rw [hx, ht]
have hb2 : b = a.gcd b * (e * s) :=
calc b = G * s := hs
_ = a.gcd b * e * s := by rw [he]
_ = a.gcd b * (e * s) := by ring
have hes : e * s ≠ 0 := by
intro h
rw [h, Nat.mul_zero] at hb2
exact hb0' hb2
refine ⟨Nat.pos_of_ne_zero hes, ?_, ?_, ?_⟩
· have h1 := hlt b hb a ha
rw [Nat.gcd_comm b a] at h1
have h2 : a.gcd b * (e * s) < a.gcd b * B.card := by
rw [← hb2, Nat.mul_comm]; exact h1
exact Nat.lt_of_mul_lt_mul_left h2
· intro h
exact hpb (hb2 ▸ Dvd.dvd.mul_left h _)
· rw [hGp]; ring
have hcardsum : (B.filter (fun a => p ∣ a)).card + (B.filter (fun b => ¬ p ∣ b)).card = B.card := by
rw [← Finset.card_union_of_disjoint (Finset.disjoint_filter_filter_not B B (fun a => p ∣ a)),
Finset.filter_union_filter_not_eq]
have hinjX : Set.InjOn (fun a => (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a)
(B.filter (fun a => p ∣ a) : Finset ℕ) := by
intro a ha a' ha' h
obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
obtain ⟨haB', hpa'⟩ := Finset.mem_filter.mp ha'
have h1 := (hprod a haB hpa b0 hb0 hpb0)
have h2 := (hprod a' haB' hpa' b0 hb0 hpb0).2.2.2
simp only at h
rw [← h] at h2
have hq : 0 < (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a :=
Nat.pos_of_ne_zero (by
intro hz
have := h1.1
rw [hz, Nat.zero_mul] at this
exact lt_irrefl 0 this)
exact Nat.eq_of_mul_eq_mul_right hq (h1.2.2.2.trans h2.symm)
have hinjT : Set.InjOn (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id)
(B.filter (fun b => ¬ p ∣ b) : Finset ℕ) := by
intro b hb b' hb' h
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
obtain ⟨hbB', hpb'⟩ := Finset.mem_filter.mp hb'
simp only at h
rw [← Nat.div_mul_cancel (hGb b hbB hpb), ← Nat.div_mul_cancel (hGb b' hbB' hpb'), h]
refine key B.card p
((B.filter (fun a => p ∣ a)).image (fun a => (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a))
((B.filter (fun b => ¬ p ∣ b)).image (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id))
hp.pos hpn ?_ ?_ ?_ ?_
· intro x hx t ht
obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp ht
obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
have h := hprod a haB hpa b hbB hpb
exact ⟨h.1, h.2.1, h.2.2.1⟩
· exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨ha0, hpa0⟩)⟩
· exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)⟩
· rw [Finset.card_image_of_injOn hinjX, Finset.card_image_of_injOn hinjT, hcardsum]
intro B h0 hne hgcd hnp hnp1 hle hpp
by_contra hcon
have hn : 0 < B.card := hne.card_pos
have hnq : (0 : ℚ) < B.card := by exact_mod_cast hn
have hlt : ∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b := by
intro a ha b hb
rcases (hle a ha b hb).lt_or_eq with h | h
· exact h
· exfalso
apply hcon
refine ⟨a, ha, b, hb, ?_⟩
rw [le_div_iff₀ hnq]
have h2 : a.gcd b * B.card ≤ a := by rw [Nat.mul_comm]; exact h.ge
exact_mod_cast h2
have hA : ∀ p : ℕ, p.Prime → B.card ≤ 2 * p →
∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a = p * a.gcd b := by
intro p hp hnp2 a ha hpa b hb hpb
have ha0 : a ≠ 0 := fun h => h0 (h ▸ ha)
have hg0 : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero ha0)
obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b
have hpg : ¬ p ∣ a.gcd b := fun h => hpb (h.trans (Nat.gcd_dvd_right a b))
have hpx : p ∣ x := by
have h1 : p ∣ a.gcd b * x := hx ▸ hpa
exact (hp.dvd_mul.mp h1).resolve_left hpg
obtain ⟨t, ht⟩ := hpx
have hlt' := hlt a ha b hb
have hxn : x < B.card := by
have h3 : a.gcd b * x < a.gcd b * B.card := by
rw [← hx, Nat.mul_comm]; exact hlt'
exact Nat.lt_of_mul_lt_mul_left h3
have ht1 : t = 1 := by
have hx0 : x ≠ 0 := by
rintro rfl
rw [Nat.mul_zero] at hx
exact ha0 hx
have ht0 : t ≠ 0 := by
rintro rfl
rw [Nat.mul_zero] at ht
exact hx0 ht
by_contra hne1
have ht2 : 2 ≤ t := by omega
have h4 : p * 2 ≤ p * t := Nat.mul_le_mul_left p ht2
omega
calc a = a.gcd b * x := hx
_ = p * a.gcd b := by rw [ht, ht1]; ring
rcases hsmooth B h0 hne hgcd hnp hnp1 hle hpp with h | ⟨p, hp, hnp2, a, ha, hpa⟩
· exact hcon h
· have hpn : p < B.card := by
have h1 := hpp a ha p 1 hp (by rwa [pow_one])
rwa [pow_one] at h1
have hexb : ∃ b ∈ B, ¬ p ∣ b := by
by_contra h
push Not at h
have h1 : p ∣ B.gcd id := Finset.dvd_gcd (fun b hb => h b hb)
rw [hgcd] at h1
exact hp.one_lt.ne' (Nat.dvd_one.mp h1)
exact hlarge B h0 hlt p hp hpn (hA p hp hnp2) ⟨a, ha, hpa⟩ hexbThe gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-402/nodes/erdos-402--h3-v2--h1/attempts/20261001T115500Z-t1001-402a-partial.lean
Closing it through its holes
Closable through its holes: once they are proved, a proof of this statement may name their theorems, which its Context already carries. A direct proof is accepted at any time.
What is known
Notes
- Erdős 402, hole erdos-402--h3-v2--h1: the general "few or almost all" lemma for every prime, and the duality reduction to the "few" side. full text →
- Large primes cannot divide an element of a strict counterexample (erdos-402--h3-v2--h1). full text →
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (1 version)
Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.
import Mathlib
import Nodes.«erdos-402--h3-v2--h1».Context
open Filter
/-! Hole `hcomp` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/
theorem erdos_402__h3_v2__h1 : ∀ (B : Finset ℕ),
(0 : ℕ) ∉ B →
B.Nonempty →
B.gcd id = (1 : ℕ) →
¬Nat.Prime B.card →
(∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
(∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
(∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ) := by
sorryA statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \begin{aligned}&0 \notin B,\ B \ne \emptyset,\ \gcd(B) = 1,\ |B|\ \text{not prime},\ |B| \ne q + 1\ \text{for every prime } q,\\&\forall a, b \in B:\ a \le |B| \cdot \gcd(a,b),\qquad \forall a \in B,\ \forall p\ \text{prime},\ \forall k \in \mathbb{N}:\ p^k \mid a \Rightarrow p^k < |B|\\&\Longrightarrow\ \exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\end{aligned}$
For every finite set B of positive integers (0 ∉ B, B nonempty) whose elements have greatest common divisor 1, whose size |B| is neither a prime nor one more than a prime, in which a ≤ |B|·gcd(a, b) for all a, b ∈ B, and in which every prime power dividing an element is below |B|, there are a, b ∈ B (possibly equal) with gcd(a, b) ≤ a/|B|. gcd(B) is the greatest common divisor of all elements of B; the final division is in ℚ, the rest is over ℕ.
Rendered from gloss/37bdbeefb3ca….md · Improve these words →
Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1/Statement.lean. Origin: compiler-derived.
Depends on (1), each in words
Depends on, each in words where someone has written them:
- erdos-402--h3-v2--h1--h1: $\begin{aligned}&0 \notin B,\ B \ne \emptyset,\ \gcd(B) = 1,\ |B|\ \text{not prime},\ |B| \ne q + 1\ \text{for every prime } q,\\&\forall a, b \in B:\ a \le |B| \cdot \gcd(a,b),\qquad \forall a \in B,\ \forall p\ \text{prime},\ \forall k \in \mathbb{N}:\ p^k \mid a \Rightarrow p^k < |B|\\&\Longrightarrow\ \bigl(\exists\, a, b \in B:\ \gcd(a,b) \le \frac{a}{|B|}\bigr) \vee \bigl(\exists\, p\ \text{prime}:\ |B| \le 2p,\ \exists\, a \in B,\ p \mid a\bigr)\end{aligned}$
Attestation: none of a proof
No proof of this statement has been merged. A partial assembly merged under attestations/000331.json: it records an attempt, not a proof (see Attempts below).
Witness
Not checked — no run on this page records step 7 passing for it.
2dd353ac6f80.import Mathlib
import Nodes.«erdos-402--h3-v2--h1».Context
open Filter
theorem witness : ∃ B : Finset ℕ, 0 ∉ B ∧ B.Nonempty ∧ B.gcd id = 1 ∧ ¬ B.card.Prime ∧
(∀ q : ℕ, q.Prime → B.card ≠ q + 1) ∧
(∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) ∧
(∀ a ∈ B, ∀ p k : ℕ, p.Prime → p ^ k ∣ a → p ^ k < B.card) := by
have hc : ({1, 2, 3, 4, 5, 6, 7, 8, 9, 10} : Finset ℕ).card = 10 := by decide
refine ⟨{1, 2, 3, 4, 5, 6, 7, 8, 9, 10}, by decide, ⟨1, by decide⟩, by decide, ?_, ?_, ?_, ?_⟩
· rw [hc]
norm_num
· intro q hq h
rw [hc] at h
have hq9 : q = 9 := by omega
rw [hq9] at hq
norm_num at hq
· intro a ha b hb
rw [hc]
simp only [Finset.mem_insert, Finset.mem_singleton] at ha
have ha10 : a ≤ 10 := by omega
have hg : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (by omega)
calc a ≤ 10 := ha10
_ ≤ 10 * a.gcd b := Nat.le_mul_of_pos_right 10 hg
· intro a ha p k hp hdvd
rw [hc]
simp only [Finset.mem_insert, Finset.mem_singleton] at ha
have ha0 : 0 < a := by omega
have hle : p ^ k ≤ a := Nat.le_of_dvd ha0 hdvd
have hne : p ^ k ≠ 10 := by
intro h10
have hk : k ≠ 0 := by
rintro rfl
simp at h10
have hp10 : p ∣ 10 := by
rw [← h10]
exact dvd_pow_self p hk
have hp10' : p ≤ 10 := Nat.le_of_dvd (by norm_num) hp10
have hk4 : k < 4 := by
have h2 : 2 ^ k ≤ p ^ k := Nat.pow_le_pow_left hp.two_le k
by_contra hk4
push Not at hk4
have h16 : 2 ^ 4 ≤ 2 ^ k := Nat.pow_le_pow_right (by norm_num) hk4
omega
have hp2 := hp.two_le
interval_cases p <;> interval_cases k <;> simp_all (config := { decide := true })
omegaNo gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →
Attempts (1)
1 recorded. Routes refuted: none. Failure classes: none.
Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.
Untrusted: partial assembly (D-12 #5), by t1001-402a; merged in 86f4ca221398 under attestations/000331.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1/attempts/20261001T115500Z-t1001-402a-partial.lean.
Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.
Outline of 20261001T115500Z-t1001-402a-partial.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.
hsmoothhole∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card ≤ (2 : ℕ) * p ∧ ∃ a ∈ B, p ∣ aholeLeaves
∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → ∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ), withhsmooth : ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → (∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ)) ∨ ∃ (p : ℕ), Nat.Prime p ∧ B.card ≤ (2 : ℕ) * p ∧ ∃ a ∈ B, p ∣ a.Uses library
FinsetFinset αis the type of finite sets of elements ofα. ,idThe identity function. .Left open as a hole; its statement is erdos-402--h3-v2--h1--h1 (open).
Lean, lines 21–26
have hsmooth : ∀ B : Finset ℕ, 0 ∉ B → B.Nonempty → B.gcd id = 1 → ¬ B.card.Prime → (∀ q : ℕ, q.Prime → B.card ≠ q + 1) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ p k : ℕ, p.Prime → p ^ k ∣ a → p ^ k < B.card) → (∃ a ∈ B, ∃ b ∈ B, (a.gcd b : ℚ) ≤ (a : ℚ) / (B.card : ℚ)) ∨ ∃ p : ℕ, p.Prime ∧ B.card ≤ 2 * p ∧ ∃ a ∈ B, p ∣ a := sorrybighave∀ (S : Finset ℕ), (∀ x ∈ S, (0 : ℕ) < x) → S.Nonempty → ∃ x ∈ S, S.card ≤ xLeaves
∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → ∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ), withbig : ∀ (S : Finset ℕ), (∀ x ∈ S, (0 : ℕ) < x) → S.Nonempty → ∃ x ∈ S, S.card ≤ x.Uses library
FinsetFinset αis the type of finite sets of elements ofα. ,NotNot p, or¬p, is the negation ofp. ,Nat.card_Ioo.Lean, lines 27–37
have big : ∀ S : Finset ℕ, (∀ x ∈ S, 0 < x) → S.Nonempty → ∃ x ∈ S, S.card ≤ x := by intro S hpos hS by_contra h push Not at h have hsub : S ⊆ Finset.Ioo 0 S.card := by intro x hx exact Finset.mem_Ioo.mpr ⟨hpos x hx, h x hx⟩ have h1 := Finset.card_le_card hsub rw [Nat.card_Ioo] at h1 have h2 := hS.card_pos omegabig.hsubhaveS ⊆ Finset.Ioo (0 : ℕ) S.cardLeaves
False, withhsub : S ⊆ Finset.Ioo (0 : ℕ) S.card.Uses library
Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Finset.mem_Ioo,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. .Lean, lines 31–33
have hsub : S ⊆ Finset.Ioo 0 S.card := by intro x hx exact Finset.mem_Ioo.mpr ⟨hpos x hx, h x hx⟩big.h1haveS.card ≤ (Finset.Ioo (0 : ℕ) S.card).cardLeaves
False, withh1 : S.card ≤ (Finset.Ioo (0 : ℕ) S.card).card.Uses library
Finset.card_le_card.Lean, line 34
have h1 := Finset.card_le_card hsub
big.h2have(0 : ℕ) < S.cardLeaves
False, withh2 : (0 : ℕ) < S.card.Lean, line 36
have h2 := hS.card_pos
keyhave∀ (n p : ℕ) (X T : Finset ℕ), (0 : ℕ) < p → p < n → (∀ x ∈ X, ∀ t ∈ T, (0 : ℕ) < x * t ∧ x * t < n ∧ ¬p ∣ x * t) → X.Nonempty → T.Nonempty → n ≤ X.card + T.card → FalseLeaves
∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → ∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ), withkey : ∀ (n p : ℕ) (X T : Finset ℕ), (0 : ℕ) < p → p < n → (∀ x ∈ X, ∀ t ∈ T, (0 : ℕ) < x * t ∧ x * t < n ∧ ¬p ∣ x * t) → X.Nonempty → T.Nonempty → n ≤ X.card + T.card → False.Uses library
FinsetFinset αis the type of finite sets of elements ofα. ,FalseFalseis the empty proposition. .Lean, lines 38–87
have key : ∀ (n p : ℕ) (X T : Finset ℕ), 0 < p → p < n → (∀ x ∈ X, ∀ t ∈ T, 0 < x * t ∧ x * t < n ∧ ¬ p ∣ x * t) → X.Nonempty → T.Nonempty → n ≤ X.card + T.card → False := by intro n p X T hp hpn hxt hX hT hcard have hXpos : ∀ x ∈ X, 0 < x := by intro x hx obtain ⟨t, ht⟩ := hT have h := (hxt x hx t ht).1 exact Nat.pos_of_ne_zero (by rintro rfl; simp at h) have hTpos : ∀ t ∈ T, 0 < t := by intro t ht obtain ⟨x, hx⟩ := hX have h := (hxt x hx t ht).1 exact Nat.pos_of_ne_zero (by rintro rfl; simp at h) obtain ⟨x0, hx0, hx0c⟩ := big X hXpos hX obtain ⟨t0, ht0, ht0c⟩ := big T hTpos hT have h1 := (hxt x0 hx0 t0 ht0).2.1 have h2 : X.card * T.card ≤ x0 * t0 := Nat.mul_le_mul hx0c ht0c have hu := hX.card_pos have hv := hT.card_pos have hc2 : ((Finset.Ioo 0 n).erase p).card = n - 2 := by rw [Finset.card_erase_of_mem (Finset.mem_Ioo.mpr ⟨hp, hpn⟩), Nat.card_Ioo] omega have h3 : X.card = 1 ∨ T.card = 1 := by by_contra h push Not at h have h4 : 2 ≤ X.card := by omega have h5 : 2 ≤ T.card := by omega nlinarith rcases h3 with hu1 | hv1 · have hsub : T.image (fun t => x0 * t) ⊆ (Finset.Ioo 0 n).erase p := by intro y hy obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hy have h := hxt x0 hx0 t ht rw [Finset.mem_erase, Finset.mem_Ioo] exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩ have hc1 : (T.image (fun t => x0 * t)).card = T.card := Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_left (hXpos x0 hx0) h) have h6 := Finset.card_le_card hsub omega · have hsub : X.image (fun x => x * t0) ⊆ (Finset.Ioo 0 n).erase p := by intro y hy obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hy have h := hxt x hx t0 ht0 rw [Finset.mem_erase, Finset.mem_Ioo] exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩ have hc1 : (X.image (fun x => x * t0)).card = X.card := Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_right (hTpos t0 ht0) h) have h6 := Finset.card_le_card hsub omegakey.hXposhave∀ x ∈ X, (0 : ℕ) < xLeaves
False, withhXpos : ∀ x ∈ X, (0 : ℕ) < x.Uses library
Nat.pos_of_ne_zero.Lean, lines 42–46
have hXpos : ∀ x ∈ X, 0 < x := by intro x hx obtain ⟨t, ht⟩ := hT have h := (hxt x hx t ht).1 exact Nat.pos_of_ne_zero (by rintro rfl; simp at h)key.hXpos.s1obtainT.NonemptyLeaves
(0 : ℕ) < x, witht : ℕ,ht : t ∈ T.Lean, line 44
obtain ⟨t, ht⟩ := hT
key.hXpos.hhave(0 : ℕ) < x * tLeaves
(0 : ℕ) < x, withh : (0 : ℕ) < x * t.Lean, line 45
have h := (hxt x hx t ht).1
key.hTposhave∀ t ∈ T, (0 : ℕ) < tLeaves
False, withhTpos : ∀ t ∈ T, (0 : ℕ) < t.Uses library
Nat.pos_of_ne_zero.Lean, lines 47–51
have hTpos : ∀ t ∈ T, 0 < t := by intro t ht obtain ⟨x, hx⟩ := hX have h := (hxt x hx t ht).1 exact Nat.pos_of_ne_zero (by rintro rfl; simp at h)key.hTpos.s1obtainX.NonemptyLeaves
(0 : ℕ) < t, withx : ℕ,hx : x ∈ X.Lean, line 49
obtain ⟨x, hx⟩ := hX
key.hTpos.hhave(0 : ℕ) < x * tLeaves
(0 : ℕ) < t, withh : (0 : ℕ) < x * t.Lean, line 50
have h := (hxt x hx t ht).1
key.s3obtain∃ x ∈ X, X.card ≤ xLeaves
False, withx0 : ℕ,hx0 : x0 ∈ X,hx0c : X.card ≤ x0.Lean, line 52
obtain ⟨x0, hx0, hx0c⟩ := big X hXpos hX
key.s4obtain∃ x ∈ T, T.card ≤ xLeaves
False, witht0 : ℕ,ht0 : t0 ∈ T,ht0c : T.card ≤ t0.Lean, line 53
obtain ⟨t0, ht0, ht0c⟩ := big T hTpos hT
key.h1havex0 * t0 < nLeaves
False, withh1 : x0 * t0 < n.Lean, line 54
have h1 := (hxt x0 hx0 t0 ht0).2.1
key.h2haveX.card * T.card ≤ x0 * t0Leaves
False, withh2 : X.card * T.card ≤ x0 * t0.Uses library
Nat.mul_le_mul.Lean, line 55
have h2 : X.card * T.card ≤ x0 * t0 := Nat.mul_le_mul hx0c ht0c
key.huhave(0 : ℕ) < X.cardLeaves
False, withhu : (0 : ℕ) < X.card.Lean, line 56
have hu := hX.card_pos
key.hvhave(0 : ℕ) < T.cardLeaves
False, withhv : (0 : ℕ) < T.card.Lean, line 57
have hv := hT.card_pos
key.hc2have((Finset.Ioo (0 : ℕ) n).erase p).card = n - (2 : ℕ)Leaves
False, withhc2 : ((Finset.Ioo (0 : ℕ) n).erase p).card = n - (2 : ℕ).Uses library
Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Finset.card_erase_of_mem$\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. ,Finset.mem_Ioo,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. ,Nat.card_Ioo.Lean, lines 58–60
have hc2 : ((Finset.Ioo 0 n).erase p).card = n - 2 := by rw [Finset.card_erase_of_mem (Finset.mem_Ioo.mpr ⟨hp, hpn⟩), Nat.card_Ioo] omegakey.h3haveX.card = (1 : ℕ) ∨ T.card = (1 : ℕ)Leaves
False, withh3 : X.card = (1 : ℕ) ∨ T.card = (1 : ℕ).Uses library
NotNot p, or¬p, is the negation ofp. .Lean, lines 61–66
have h3 : X.card = 1 ∨ T.card = 1 := by by_contra h push Not at h have h4 : 2 ≤ X.card := by omega have h5 : 2 ≤ T.card := by omega nlinarithkey.h3.h4have(2 : ℕ) ≤ X.cardroutine: omegaLeaves
False, withh4 : (2 : ℕ) ≤ X.card.Lean, line 64
have h4 : 2 ≤ X.card := by omega
key.h3.h5have(2 : ℕ) ≤ T.cardroutine: omegaLeaves
False, withh5 : (2 : ℕ) ≤ T.card.Lean, line 65
have h5 : 2 ≤ T.card := by omega
key.s11caseLeaves
False.Lean, lines 68–77
· have hsub : T.image (fun t => x0 * t) ⊆ (Finset.Ioo 0 n).erase p := by intro y hy obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hy have h := hxt x0 hx0 t ht rw [Finset.mem_erase, Finset.mem_Ioo] exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩ have hc1 : (T.image (fun t => x0 * t)).card = T.card := Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_left (hXpos x0 hx0) h) have h6 := Finset.card_le_card hsub omegakey.s11.hsubhaveFinset.image (fun (t : ℕ) => x0 * t) T ⊆ (Finset.Ioo (0 : ℕ) n).erase pLeaves
False, withhsub : Finset.image (fun (t : ℕ) => x0 * t) T ⊆ (Finset.Ioo (0 : ℕ) n).erase p.Uses library
Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Finset.mem_erase,Finset.mem_Ioo,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. ,dvd_of_eq.Lean, lines 68–73
· have hsub : T.image (fun t => x0 * t) ⊆ (Finset.Ioo 0 n).erase p := by intro y hy obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hy have h := hxt x0 hx0 t ht rw [Finset.mem_erase, Finset.mem_Ioo] exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩key.s11.hsub.s1obtain∃ a ∈ T, x0 * a = yLeaves
x0 * t ∈ (Finset.Ioo (0 : ℕ) n).erase p, witht : ℕ,ht : t ∈ T,hy : x0 * t ∈ Finset.image (fun (t : ℕ) => x0 * t) T.Uses library
Finset.mem_image.Lean, line 70
obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hy
key.s11.hsub.hhave(0 : ℕ) < x0 * t ∧ x0 * t < n ∧ ¬p ∣ x0 * tLeaves
x0 * t ∈ (Finset.Ioo (0 : ℕ) n).erase p, withh : (0 : ℕ) < x0 * t ∧ x0 * t < n ∧ ¬p ∣ x0 * t.Lean, line 71
have h := hxt x0 hx0 t ht
key.s11.hc1have(Finset.image (fun (t : ℕ) => x0 * t) T).card = T.cardLeaves
False, withhc1 : (Finset.image (fun (t : ℕ) => x0 * t) T).card = T.card.Uses library
Finset.card_image_of_injective,Nat.eq_of_mul_eq_mul_left.Lean, lines 74–75
have hc1 : (T.image (fun t => x0 * t)).card = T.card := Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_left (hXpos x0 hx0) h)key.s11.h6have(Finset.image (fun (t : ℕ) => x0 * t) T).card ≤ ((Finset.Ioo (0 : ℕ) n).erase p).cardLeaves
False, withh6 : (Finset.image (fun (t : ℕ) => x0 * t) T).card ≤ ((Finset.Ioo (0 : ℕ) n).erase p).card.Uses library
Finset.card_le_card.Lean, line 76
have h6 := Finset.card_le_card hsub
key.s12caseLeaves
False.Lean, lines 78–87
· have hsub : X.image (fun x => x * t0) ⊆ (Finset.Ioo 0 n).erase p := by intro y hy obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hy have h := hxt x hx t0 ht0 rw [Finset.mem_erase, Finset.mem_Ioo] exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩ have hc1 : (X.image (fun x => x * t0)).card = X.card := Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_right (hTpos t0 ht0) h) have h6 := Finset.card_le_card hsub omegakey.s12.hsubhaveFinset.image (fun (x : ℕ) => x * t0) X ⊆ (Finset.Ioo (0 : ℕ) n).erase pLeaves
False, withhsub : Finset.image (fun (x : ℕ) => x * t0) X ⊆ (Finset.Ioo (0 : ℕ) n).erase p.Uses library
Finset.IooThe finset $(a, b)$ of elementsxsuch thata < xandx < b. ,Finset.mem_erase,Finset.mem_Ioo,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. ,dvd_of_eq.Lean, lines 78–83
· have hsub : X.image (fun x => x * t0) ⊆ (Finset.Ioo 0 n).erase p := by intro y hy obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hy have h := hxt x hx t0 ht0 rw [Finset.mem_erase, Finset.mem_Ioo] exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩key.s12.hsub.s1obtain∃ a ∈ X, a * t0 = yLeaves
x * t0 ∈ (Finset.Ioo (0 : ℕ) n).erase p, withx : ℕ,hx : x ∈ X,hy : x * t0 ∈ Finset.image (fun (x : ℕ) => x * t0) X.Uses library
Finset.mem_image.Lean, line 80
obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hy
key.s12.hsub.hhave(0 : ℕ) < x * t0 ∧ x * t0 < n ∧ ¬p ∣ x * t0Leaves
x * t0 ∈ (Finset.Ioo (0 : ℕ) n).erase p, withh : (0 : ℕ) < x * t0 ∧ x * t0 < n ∧ ¬p ∣ x * t0.Lean, line 81
have h := hxt x hx t0 ht0
key.s12.hc1have(Finset.image (fun (x : ℕ) => x * t0) X).card = X.cardLeaves
False, withhc1 : (Finset.image (fun (x : ℕ) => x * t0) X).card = X.card.Uses library
Finset.card_image_of_injective,Nat.eq_of_mul_eq_mul_right.Lean, lines 84–85
have hc1 : (X.image (fun x => x * t0)).card = X.card := Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_right (hTpos t0 ht0) h)key.s12.h6have(Finset.image (fun (x : ℕ) => x * t0) X).card ≤ ((Finset.Ioo (0 : ℕ) n).erase p).cardLeaves
False, withh6 : (Finset.image (fun (x : ℕ) => x * t0) X).card ≤ ((Finset.Ioo (0 : ℕ) n).erase p).card.Uses library
Finset.card_le_card.Lean, line 86
have h6 := Finset.card_le_card hsub
hlargehave∀ (B : Finset ℕ), (0 : ℕ) ∉ B → (∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b) → ∀ (p : ℕ), Nat.Prime p → p < B.card → (∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬p ∣ b → a = p * a.gcd b) → (∃ a ∈ B, p ∣ a) → (∃ b ∈ B, ¬p ∣ b) → FalseLeaves
∀ (B : Finset ℕ), (0 : ℕ) ∉ B → B.Nonempty → B.gcd id = (1 : ℕ) → ¬Nat.Prime B.card → (∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) → (∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) → (∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) → ∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ), withhlarge : ∀ (B : Finset ℕ), (0 : ℕ) ∉ B → (∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b) → ∀ (p : ℕ), Nat.Prime p → p < B.card → (∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬p ∣ b → a = p * a.gcd b) → (∃ a ∈ B, p ∣ a) → (∃ b ∈ B, ¬p ∣ b) → False.Uses library
FinsetFinset αis the type of finite sets of elements ofα. ,FalseFalseis the empty proposition. ,idThe identity function. .Lean, lines 88–193
have hlarge : ∀ B : Finset ℕ, 0 ∉ B → (∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b) → ∀ p : ℕ, p.Prime → p < B.card → (∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a = p * a.gcd b) → (∃ a ∈ B, p ∣ a) → (∃ b ∈ B, ¬ p ∣ b) → False := by intro B h0 hlt p hp hpn hA hexa hexb obtain ⟨a0, ha0, hpa0⟩ := hexa obtain ⟨b0, hb0, hpb0⟩ := hexb have hG0 : (B.filter (fun b => ¬ p ∣ b)).gcd id ≠ 0 := by intro h have h1 : (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ id b0 := Finset.gcd_dvd (Finset.mem_filter.mpr ⟨hb0, hpb0⟩) rw [h] at h1 exact hpb0 (by rw [show b0 = 0 from Nat.eq_zero_of_zero_dvd h1]; exact dvd_zero p) have hGb : ∀ b ∈ B, ¬ p ∣ b → (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ b := by intro b hb hpb exact Finset.gcd_dvd (f := id) (Finset.mem_filter.mpr ⟨hb, hpb⟩) have hdG : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a.gcd b ∣ (B.filter (fun b => ¬ p ∣ b)).gcd id := by intro a ha hpa b hb hpb apply Finset.dvd_gcd intro b' hb' obtain ⟨hb'B, hpb'⟩ := Finset.mem_filter.mp hb' have e1 := hA a ha hpa b hb hpb have e2 := hA a ha hpa b' hb'B hpb' have e3 : a.gcd b = a.gcd b' := Nat.eq_of_mul_eq_mul_left hp.pos (e1.symm.trans e2) rw [e3] exact Nat.gcd_dvd_right a b' have hprod : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → 0 < ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧ ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) < B.card ∧ ¬ p ∣ ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧ a * ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) = (B.filter (fun b => ¬ p ∣ b)).gcd id * p := by intro a ha hpa b hb hpb generalize hG : (B.filter (fun b => ¬ p ∣ b)).gcd id = G at * obtain ⟨e, he⟩ := hdG a ha hpa b hb hpb obtain ⟨s, hs⟩ := hGb b hb hpb have ea := hA a ha hpa b hb hpb have ha0' : 0 < a := Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha)) have hb0' : b ≠ 0 := fun h => h0 (h ▸ hb) have hGp : G * p = e * a := calc G * p = a.gcd b * e * p := by rw [he] _ = e * (p * a.gcd b) := by ring _ = e * a := by rw [← ea] have hx : G * p / a = e := Nat.div_eq_of_eq_mul_left ha0' hGp have ht : b / G = s := by rw [hs] exact Nat.mul_div_cancel_left s (Nat.pos_of_ne_zero hG0) rw [hx, ht] have hb2 : b = a.gcd b * (e * s) := calc b = G * s := hs _ = a.gcd b * e * s := by rw [he] _ = a.gcd b * (e * s) := by ring have hes : e * s ≠ 0 := by intro h rw [h, Nat.mul_zero] at hb2 exact hb0' hb2 refine ⟨Nat.pos_of_ne_zero hes, ?_, ?_, ?_⟩ · have h1 := hlt b hb a ha rw [Nat.gcd_comm b a] at h1 have h2 : a.gcd b * (e * s) < a.gcd b * B.card := by rw [← hb2, Nat.mul_comm]; exact h1 exact Nat.lt_of_mul_lt_mul_left h2 · intro h exact hpb (hb2 ▸ Dvd.dvd.mul_left h _) · rw [hGp]; ring have hcardsum : (B.filter (fun a => p ∣ a)).card + (B.filter (fun b => ¬ p ∣ b)).card = B.card := by rw [← Finset.card_union_of_disjoint (Finset.disjoint_filter_filter_not B B (fun a => p ∣ a)), Finset.filter_union_filter_not_eq] have hinjX : Set.InjOn (fun a => (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) (B.filter (fun a => p ∣ a) : Finset ℕ) := by intro a ha a' ha' h obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha obtain ⟨haB', hpa'⟩ := Finset.mem_filter.mp ha' have h1 := (hprod a haB hpa b0 hb0 hpb0) have h2 := (hprod a' haB' hpa' b0 hb0 hpb0).2.2.2 simp only at h rw [← h] at h2 have hq : 0 < (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a := Nat.pos_of_ne_zero (by intro hz have := h1.1 rw [hz, Nat.zero_mul] at this exact lt_irrefl 0 this) exact Nat.eq_of_mul_eq_mul_right hq (h1.2.2.2.trans h2.symm) have hinjT : Set.InjOn (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id) (B.filter (fun b => ¬ p ∣ b) : Finset ℕ) := by intro b hb b' hb' h obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb obtain ⟨hbB', hpb'⟩ := Finset.mem_filter.mp hb' simp only at h rw [← Nat.div_mul_cancel (hGb b hbB hpb), ← Nat.div_mul_cancel (hGb b' hbB' hpb'), h] refine key B.card p ((B.filter (fun a => p ∣ a)).image (fun a => (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a)) ((B.filter (fun b => ¬ p ∣ b)).image (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id)) hp.pos hpn ?_ ?_ ?_ ?_ · intro x hx t ht obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp ht obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb have h := hprod a haB hpa b hbB hpb exact ⟨h.1, h.2.1, h.2.2.1⟩ · exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨ha0, hpa0⟩)⟩ · exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)⟩ · rw [Finset.card_image_of_injOn hinjX, Finset.card_image_of_injOn hinjT, hcardsum]hlarge.s1obtain∃ a ∈ B, p ∣ aLeaves
False, witha0 : ℕ,ha0 : a0 ∈ B,hpa0 : p ∣ a0.Lean, line 94
obtain ⟨a0, ha0, hpa0⟩ := hexa
hlarge.s2obtain∃ b ∈ B, ¬p ∣ bLeaves
False, withb0 : ℕ,hb0 : b0 ∈ B,hpb0 : ¬p ∣ b0.Lean, line 95
obtain ⟨b0, hb0, hpb0⟩ := hexb
hlarge.hG0have{b ∈ B | ¬p ∣ b}.gcd id ≠ (0 : ℕ)Leaves
False, withhG0 : {b ∈ B | ¬p ∣ b}.gcd id ≠ (0 : ℕ).Uses library
idThe identity function. ,Nat.eq_zero_of_zero_dvd,dvd_zero.Lean, lines 96–101
have hG0 : (B.filter (fun b => ¬ p ∣ b)).gcd id ≠ 0 := by intro h have h1 : (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ id b0 := Finset.gcd_dvd (Finset.mem_filter.mpr ⟨hb0, hpb0⟩) rw [h] at h1 exact hpb0 (by rw [show b0 = 0 from Nat.eq_zero_of_zero_dvd h1]; exact dvd_zero p)hlarge.hG0.h1have{b ∈ B | ¬p ∣ b}.gcd id ∣ id b0Leaves
False, withh1 : {b ∈ B | ¬p ∣ b}.gcd id ∣ id b0.Uses library
idThe identity function. ,Finset.gcd_dvd,Finset.mem_filter,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. .Lean, lines 98–99
have h1 : (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ id b0 := Finset.gcd_dvd (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)
hlarge.hGbhave∀ b ∈ B, ¬p ∣ b → {b ∈ B | ¬p ∣ b}.gcd id ∣ bLeaves
False, withhGb : ∀ b ∈ B, ¬p ∣ b → {b ∈ B | ¬p ∣ b}.gcd id ∣ b.Uses library
idThe identity function. ,Finset.gcd_dvd,Finset.mem_filter,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. .Lean, lines 102–104
have hGb : ∀ b ∈ B, ¬ p ∣ b → (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ b := by intro b hb hpb exact Finset.gcd_dvd (f := id) (Finset.mem_filter.mpr ⟨hb, hpb⟩)hlarge.hdGhave∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬p ∣ b → a.gcd b ∣ {b ∈ B | ¬p ∣ b}.gcd idLeaves
False, withhdG : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬p ∣ b → a.gcd b ∣ {b ∈ B | ¬p ∣ b}.gcd id.Uses library
idThe identity function. ,Finset.dvd_gcd,Nat.gcd_dvd_right.Lean, lines 105–115
have hdG : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a.gcd b ∣ (B.filter (fun b => ¬ p ∣ b)).gcd id := by intro a ha hpa b hb hpb apply Finset.dvd_gcd intro b' hb' obtain ⟨hb'B, hpb'⟩ := Finset.mem_filter.mp hb' have e1 := hA a ha hpa b hb hpb have e2 := hA a ha hpa b' hb'B hpb' have e3 : a.gcd b = a.gcd b' := Nat.eq_of_mul_eq_mul_left hp.pos (e1.symm.trans e2) rw [e3] exact Nat.gcd_dvd_right a b'hlarge.hdG.s1obtainb' ∈ B ∧ ¬p ∣ b'Leaves
a.gcd b ∣ id b', withhb'B : b' ∈ B,hpb' : ¬p ∣ b'.Uses library
Finset.mem_filter.Lean, line 110
obtain ⟨hb'B, hpb'⟩ := Finset.mem_filter.mp hb'
hlarge.hdG.e1havea = p * a.gcd bLeaves
a.gcd b ∣ id b', withe1 : a = p * a.gcd b.Lean, line 111
have e1 := hA a ha hpa b hb hpb
hlarge.hdG.e2havea = p * a.gcd b'Leaves
a.gcd b ∣ id b', withe2 : a = p * a.gcd b'.Lean, line 112
have e2 := hA a ha hpa b' hb'B hpb'
hlarge.hdG.e3havea.gcd b = a.gcd b'Leaves
a.gcd b ∣ id b', withe3 : a.gcd b = a.gcd b'.Uses library
Nat.eq_of_mul_eq_mul_left.Lean, line 113
have e3 : a.gcd b = a.gcd b' := Nat.eq_of_mul_eq_mul_left hp.pos (e1.symm.trans e2)
hlarge.hprodhave∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬p ∣ b → (0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ a * ({b ∈ B | ¬p ∣ b}.gcd id * p / a) = {b ∈ B | ¬p ∣ b}.gcd id * pLeaves
False, withhprod : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬p ∣ b → (0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ a * ({b ∈ B | ¬p ∣ b}.gcd id * p / a) = {b ∈ B | ¬p ∣ b}.gcd id * p.Uses library
idThe identity function. ,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. ,Nat.pos_of_ne_zero.Lean, lines 116–153
have hprod : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → 0 < ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧ ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) < B.card ∧ ¬ p ∣ ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧ a * ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) = (B.filter (fun b => ¬ p ∣ b)).gcd id * p := by intro a ha hpa b hb hpb generalize hG : (B.filter (fun b => ¬ p ∣ b)).gcd id = G at * obtain ⟨e, he⟩ := hdG a ha hpa b hb hpb obtain ⟨s, hs⟩ := hGb b hb hpb have ea := hA a ha hpa b hb hpb have ha0' : 0 < a := Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha)) have hb0' : b ≠ 0 := fun h => h0 (h ▸ hb) have hGp : G * p = e * a := calc G * p = a.gcd b * e * p := by rw [he] _ = e * (p * a.gcd b) := by ring _ = e * a := by rw [← ea] have hx : G * p / a = e := Nat.div_eq_of_eq_mul_left ha0' hGp have ht : b / G = s := by rw [hs] exact Nat.mul_div_cancel_left s (Nat.pos_of_ne_zero hG0) rw [hx, ht] have hb2 : b = a.gcd b * (e * s) := calc b = G * s := hs _ = a.gcd b * e * s := by rw [he] _ = a.gcd b * (e * s) := by ring have hes : e * s ≠ 0 := by intro h rw [h, Nat.mul_zero] at hb2 exact hb0' hb2 refine ⟨Nat.pos_of_ne_zero hes, ?_, ?_, ?_⟩ · have h1 := hlt b hb a ha rw [Nat.gcd_comm b a] at h1 have h2 : a.gcd b * (e * s) < a.gcd b * B.card := by rw [← hb2, Nat.mul_comm]; exact h1 exact Nat.lt_of_mul_lt_mul_left h2 · intro h exact hpb (hb2 ▸ Dvd.dvd.mul_left h _) · rw [hGp]; ringhlarge.hprod.s1obtaina.gcd b ∣ GLeaves
(0 : ℕ) < G * p / a * (b / G) ∧ G * p / a * (b / G) < B.card ∧ ¬p ∣ G * p / a * (b / G) ∧ a * (G * p / a) = G * p, withe : ℕ,he : G = a.gcd b * e.Lean, line 123
obtain ⟨e, he⟩ := hdG a ha hpa b hb hpb
hlarge.hprod.s2obtainG ∣ bLeaves
(0 : ℕ) < G * p / a * (b / G) ∧ G * p / a * (b / G) < B.card ∧ ¬p ∣ G * p / a * (b / G) ∧ a * (G * p / a) = G * p, withs : ℕ,hs : b = G * s.Lean, line 124
obtain ⟨s, hs⟩ := hGb b hb hpb
hlarge.hprod.eahavea = p * a.gcd bLeaves
(0 : ℕ) < G * p / a * (b / G) ∧ G * p / a * (b / G) < B.card ∧ ¬p ∣ G * p / a * (b / G) ∧ a * (G * p / a) = G * p, withea : a = p * a.gcd b.Lean, line 125
have ea := hA a ha hpa b hb hpb
hlarge.hprod.ha0'have(0 : ℕ) < aLeaves
(0 : ℕ) < G * p / a * (b / G) ∧ G * p / a * (b / G) < B.card ∧ ¬p ∣ G * p / a * (b / G) ∧ a * (G * p / a) = G * p, withha0' : (0 : ℕ) < a.Uses library
Nat.pos_of_ne_zero.Lean, line 126
have ha0' : 0 < a := Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha))
hlarge.hprod.hb0'haveb ≠ (0 : ℕ)Leaves
(0 : ℕ) < G * p / a * (b / G) ∧ G * p / a * (b / G) < B.card ∧ ¬p ∣ G * p / a * (b / G) ∧ a * (G * p / a) = G * p, withhb0' : b ≠ (0 : ℕ).Lean, line 127
have hb0' : b ≠ 0 := fun h => h0 (h ▸ hb)
hlarge.hprod.hGphaveG * p = e * aLeaves
(0 : ℕ) < G * p / a * (b / G) ∧ G * p / a * (b / G) < B.card ∧ ¬p ∣ G * p / a * (b / G) ∧ a * (G * p / a) = G * p, withhGp : G * p = e * a.Lean, lines 128–131
have hGp : G * p = e * a := calc G * p = a.gcd b * e * p := by rw [he] _ = e * (p * a.gcd b) := by ring _ = e * a := by rw [← ea]hlarge.hprod.hGp.s1calcG * p = a.gcd b * e * pCloses the goal.
Lean, line 129
calc G * p = a.gcd b * e * p := by rw [he]
hlarge.hprod.hGp.s2calc routine: ringCloses the goal.
Lean, line 130
_ = e * (p * a.gcd b) := by ring
hlarge.hprod.hGp.s3calcCloses the goal.
Lean, line 131
_ = e * a := by rw [← ea]
hlarge.hprod.hxhaveG * p / a = eLeaves
(0 : ℕ) < G * p / a * (b / G) ∧ G * p / a * (b / G) < B.card ∧ ¬p ∣ G * p / a * (b / G) ∧ a * (G * p / a) = G * p, withhx : G * p / a = e.Uses library
Nat.div_eq_of_eq_mul_left.Lean, line 132
have hx : G * p / a = e := Nat.div_eq_of_eq_mul_left ha0' hGp
hlarge.hprod.hthaveb / G = sLeaves
(0 : ℕ) < G * p / a * (b / G) ∧ G * p / a * (b / G) < B.card ∧ ¬p ∣ G * p / a * (b / G) ∧ a * (G * p / a) = G * p, withht : b / G = s.Uses library
Nat.mul_div_cancel_left,Nat.pos_of_ne_zero.Lean, lines 133–135
have ht : b / G = s := by rw [hs] exact Nat.mul_div_cancel_left s (Nat.pos_of_ne_zero hG0)hlarge.hprod.hb2haveb = a.gcd b * (e * s)Leaves
(0 : ℕ) < e * s ∧ e * s < B.card ∧ ¬p ∣ e * s ∧ a * e = G * p, withhb2 : b = a.gcd b * (e * s).Lean, lines 137–140
have hb2 : b = a.gcd b * (e * s) := calc b = G * s := hs _ = a.gcd b * e * s := by rw [he] _ = a.gcd b * (e * s) := by ringhlarge.hprod.hb2.s1calcb = G * sCloses the goal.
Lean, line 138
calc b = G * s := hs
hlarge.hprod.hb2.s2calcCloses the goal.
Lean, line 139
_ = a.gcd b * e * s := by rw [he]
hlarge.hprod.hb2.s3calc routine: ringCloses the goal.
Lean, line 140
_ = a.gcd b * (e * s) := by ring
hlarge.hprod.heshavee * s ≠ (0 : ℕ)Leaves
(0 : ℕ) < e * s ∧ e * s < B.card ∧ ¬p ∣ e * s ∧ a * e = G * p, withhes : e * s ≠ (0 : ℕ).Uses library
Nat.mul_zero.Lean, lines 141–144
have hes : e * s ≠ 0 := by intro h rw [h, Nat.mul_zero] at hb2 exact hb0' hb2hlarge.hprod.s11caseLeaves
e * s < B.card.Uses library
Nat.gcd_comm,Nat.lt_of_mul_lt_mul_left.Lean, lines 146–150
· have h1 := hlt b hb a ha rw [Nat.gcd_comm b a] at h1 have h2 : a.gcd b * (e * s) < a.gcd b * B.card := by rw [← hb2, Nat.mul_comm]; exact h1 exact Nat.lt_of_mul_lt_mul_left h2hlarge.hprod.s11.h1haveb < B.card * b.gcd aLeaves
e * s < B.card, withh1 : b < B.card * b.gcd a.Lean, line 146
· have h1 := hlt b hb a ha
hlarge.hprod.s11.h2havea.gcd b * (e * s) < a.gcd b * B.cardLeaves
e * s < B.card, withh2 : a.gcd b * (e * s) < a.gcd b * B.card.Uses library
Nat.mul_comm.Lean, lines 148–149
have h2 : a.gcd b * (e * s) < a.gcd b * B.card := by rw [← hb2, Nat.mul_comm]; exact h1
hlarge.hprod.s12caseLeaves
¬p ∣ e * s.Uses library
Dvd.dvd.mul_leftAlias ofdvd_mul_of_dvd_right. .Lean, lines 151–152
· intro h exact hpb (hb2 ▸ Dvd.dvd.mul_left h _)hlarge.hprod.s13caseLeaves
a * e = G * p.Lean, line 153
· rw [hGp]; ring
hlarge.hcardsumhave{a ∈ B | p ∣ a}.card + {b ∈ B | ¬p ∣ b}.card = B.cardLeaves
False, withhcardsum : {a ∈ B | p ∣ a}.card + {b ∈ B | ¬p ∣ b}.card = B.card.Uses library
Finset.card_union_of_disjointAlias of the reverse direction ofFinset.card_union_eq_card_add_card. ,Finset.disjoint_filter_filter_not,Finset.filter_union_filter_not_eq.Lean, lines 154–156
have hcardsum : (B.filter (fun a => p ∣ a)).card + (B.filter (fun b => ¬ p ∣ b)).card = B.card := by rw [← Finset.card_union_of_disjoint (Finset.disjoint_filter_filter_not B B (fun a => p ∣ a)), Finset.filter_union_filter_not_eq]hlarge.hinjXhaveSet.InjOn (fun (a : ℕ) => {b ∈ B | ¬p ∣ b}.gcd id * p / a) (↑({a ∈ B | p ∣ a}) : Set ℕ)Leaves
False, withhinjX : Set.InjOn (fun (a : ℕ) => {b ∈ B | ¬p ∣ b}.gcd id * p / a) (↑({a ∈ B | p ∣ a}) : Set ℕ).Uses library
Set.InjOnfis injective onsif the restriction offtosis injective. ,idThe identity function. ,FinsetFinset αis the type of finite sets of elements ofα. ,Nat.eq_of_mul_eq_mul_right.Lean, lines 157–172
have hinjX : Set.InjOn (fun a => (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) (B.filter (fun a => p ∣ a) : Finset ℕ) := by intro a ha a' ha' h obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha obtain ⟨haB', hpa'⟩ := Finset.mem_filter.mp ha' have h1 := (hprod a haB hpa b0 hb0 hpb0) have h2 := (hprod a' haB' hpa' b0 hb0 hpb0).2.2.2 simp only at h rw [← h] at h2 have hq : 0 < (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a := Nat.pos_of_ne_zero (by intro hz have := h1.1 rw [hz, Nat.zero_mul] at this exact lt_irrefl 0 this) exact Nat.eq_of_mul_eq_mul_right hq (h1.2.2.2.trans h2.symm)hlarge.hinjX.s1obtaina ∈ B ∧ p ∣ aLeaves
a = a', withhaB : a ∈ B,hpa : p ∣ a.Uses library
Finset.mem_filter.Lean, line 160
obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
hlarge.hinjX.s2obtaina' ∈ B ∧ p ∣ a'Leaves
a = a', withhaB' : a' ∈ B,hpa' : p ∣ a'.Uses library
Finset.mem_filter.Lean, line 161
obtain ⟨haB', hpa'⟩ := Finset.mem_filter.mp ha'
hlarge.hinjX.h1have(0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b0 / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b0 / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b0 / {b ∈ B | ¬p ∣ b}.gcd id) ∧ a * ({b ∈ B | ¬p ∣ b}.gcd id * p / a) = {b ∈ B | ¬p ∣ b}.gcd id * pLeaves
a = a', withh1 : (0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b0 / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b0 / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b0 / {b ∈ B | ¬p ∣ b}.gcd id) ∧ a * ({b ∈ B | ¬p ∣ b}.gcd id * p / a) = {b ∈ B | ¬p ∣ b}.gcd id * p.Lean, line 162
have h1 := (hprod a haB hpa b0 hb0 hpb0)
hlarge.hinjX.h2havea' * ({b ∈ B | ¬p ∣ b}.gcd id * p / a') = {b ∈ B | ¬p ∣ b}.gcd id * pLeaves
a = a', withh2 : a' * ({b ∈ B | ¬p ∣ b}.gcd id * p / a') = {b ∈ B | ¬p ∣ b}.gcd id * p.Lean, line 163
have h2 := (hprod a' haB' hpa' b0 hb0 hpb0).2.2.2
hlarge.hinjX.hqhave(0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / aLeaves
a = a', withhq : (0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a.Uses library
idThe identity function. ,Nat.pos_of_ne_zero,Nat.zero_mul,lt_irrefl.Lean, lines 166–171
have hq : 0 < (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a := Nat.pos_of_ne_zero (by intro hz have := h1.1 rw [hz, Nat.zero_mul] at this exact lt_irrefl 0 this)hlarge.hinjX.hq.thishave(0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b0 / {b ∈ B | ¬p ∣ b}.gcd id)Leaves
False, withthis : (0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b0 / {b ∈ B | ¬p ∣ b}.gcd id).
hlarge.hinjThaveSet.InjOn (fun (b : ℕ) => b / {b ∈ B | ¬p ∣ b}.gcd id) (↑({b ∈ B | ¬p ∣ b}) : Set ℕ)Leaves
False, withhinjT : Set.InjOn (fun (b : ℕ) => b / {b ∈ B | ¬p ∣ b}.gcd id) (↑({b ∈ B | ¬p ∣ b}) : Set ℕ).Uses library
Set.InjOnfis injective onsif the restriction offtosis injective. ,idThe identity function. ,FinsetFinset αis the type of finite sets of elements ofα. ,Nat.div_mul_cancel.Lean, lines 173–179
have hinjT : Set.InjOn (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id) (B.filter (fun b => ¬ p ∣ b) : Finset ℕ) := by intro b hb b' hb' h obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb obtain ⟨hbB', hpb'⟩ := Finset.mem_filter.mp hb' simp only at h rw [← Nat.div_mul_cancel (hGb b hbB hpb), ← Nat.div_mul_cancel (hGb b' hbB' hpb'), h]hlarge.hinjT.s1obtainb ∈ B ∧ ¬p ∣ bLeaves
b = b', withhbB : b ∈ B,hpb : ¬p ∣ b.Uses library
Finset.mem_filter.Lean, line 176
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
hlarge.hinjT.s2obtainb' ∈ B ∧ ¬p ∣ b'Leaves
b = b', withhbB' : b' ∈ B,hpb' : ¬p ∣ b'.Uses library
Finset.mem_filter.Lean, line 177
obtain ⟨hbB', hpb'⟩ := Finset.mem_filter.mp hb'
hlarge.s10caseLeaves
∀ x ∈ Finset.image (fun (a : ℕ) => {b ∈ B | ¬p ∣ b}.gcd id * p / a) ({a ∈ B | p ∣ a}), ∀ t ∈ Finset.image (fun (b : ℕ) => b / {b ∈ B | ¬p ∣ b}.gcd id) ({b ∈ B | ¬p ∣ b}), (0 : ℕ) < x * t ∧ x * t < B.card ∧ ¬p ∣ x * t.Uses library
And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. .Lean, lines 184–190
· intro x hx t ht obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp ht obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb have h := hprod a haB hpa b hbB hpb exact ⟨h.1, h.2.1, h.2.2.1⟩hlarge.s10.s1obtain∃ a ∈ {a ∈ B | p ∣ a}, {b ∈ B | ¬p ∣ b}.gcd id * p / a = xLeaves
(0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * t ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * t < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * t, witha : ℕ,ha : a ∈ {a ∈ B | p ∣ a},hx : {b ∈ B | ¬p ∣ b}.gcd id * p / a ∈ Finset.image (fun (a : ℕ) => {b ∈ B | ¬p ∣ b}.gcd id * p / a) ({a ∈ B | p ∣ a}).Uses library
Finset.mem_image.Lean, line 185
obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
hlarge.s10.s2obtain∃ a ∈ {b ∈ B | ¬p ∣ b}, a / {b ∈ B | ¬p ∣ b}.gcd id = tLeaves
(0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id), withb : ℕ,hb : b ∈ {b ∈ B | ¬p ∣ b},ht : b / {b ∈ B | ¬p ∣ b}.gcd id ∈ Finset.image (fun (b : ℕ) => b / {b ∈ B | ¬p ∣ b}.gcd id) ({b ∈ B | ¬p ∣ b}).Uses library
Finset.mem_image.Lean, line 186
obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp ht
hlarge.s10.s3obtaina ∈ B ∧ p ∣ aLeaves
(0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id), withhaB : a ∈ B,hpa : p ∣ a.Uses library
Finset.mem_filter.Lean, line 187
obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
hlarge.s10.s4obtainb ∈ B ∧ ¬p ∣ bLeaves
(0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id), withhbB : b ∈ B,hpb : ¬p ∣ b.Uses library
Finset.mem_filter.Lean, line 188
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
hlarge.s10.hhave(0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ a * ({b ∈ B | ¬p ∣ b}.gcd id * p / a) = {b ∈ B | ¬p ∣ b}.gcd id * pLeaves
(0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id), withh : (0 : ℕ) < {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) < B.card ∧ ¬p ∣ {b ∈ B | ¬p ∣ b}.gcd id * p / a * (b / {b ∈ B | ¬p ∣ b}.gcd id) ∧ a * ({b ∈ B | ¬p ∣ b}.gcd id * p / a) = {b ∈ B | ¬p ∣ b}.gcd id * p.Lean, line 189
have h := hprod a haB hpa b hbB hpb
hlarge.s11caseLeaves
(Finset.image (fun (a : ℕ) => {b ∈ B | ¬p ∣ b}.gcd id * p / a) ({a ∈ B | p ∣ a})).Nonempty.Uses library
Exists.introExistential introduction. ,Finset.mem_image_of_mem,Finset.mem_filter,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. .Lean, line 191
· exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨ha0, hpa0⟩)⟩
hlarge.s12caseLeaves
(Finset.image (fun (b : ℕ) => b / {b ∈ B | ¬p ∣ b}.gcd id) ({b ∈ B | ¬p ∣ b})).Nonempty.Uses library
Exists.introExistential introduction. ,Finset.mem_image_of_mem,Finset.mem_filter,And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. .Lean, line 192
· exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)⟩
hlarge.s13caseLeaves
B.card ≤ (Finset.image (fun (a : ℕ) => {b ∈ B | ¬p ∣ b}.gcd id * p / a) ({a ∈ B | p ∣ a})).card + (Finset.image (fun (b : ℕ) => b / {b ∈ B | ¬p ∣ b}.gcd id) ({b ∈ B | ¬p ∣ b})).card.Uses library
Finset.card_image_of_injOn.Lean, line 193
· rw [Finset.card_image_of_injOn hinjX, Finset.card_image_of_injOn hinjT, hcardsum]
hnhave(0 : ℕ) < B.cardLeaves
False, withhn : (0 : ℕ) < B.card.Lean, line 196
have hn : 0 < B.card := hne.card_pos
hnqhave(0 : ℚ) < (↑B.card : ℚ)Leaves
False, withhnq : (0 : ℚ) < (↑B.card : ℚ).Lean, line 197
have hnq : (0 : ℚ) < B.card := by exact_mod_cast hn
hlthave∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd bLeaves
False, withhlt : ∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b.Lean, lines 198–207
have hlt : ∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b := by intro a ha b hb rcases (hle a ha b hb).lt_or_eq with h | h · exact h · exfalso apply hcon refine ⟨a, ha, b, hb, ?_⟩ rw [le_div_iff₀ hnq] have h2 : a.gcd b * B.card ≤ a := by rw [Nat.mul_comm]; exact h.ge exact_mod_cast h2hlt.s1caseLeaves
a < B.card * a.gcd b.hlt.s2caseLeaves
a < B.card * a.gcd b.Uses library
Exists.introExistential introduction. ,le_div_iff₀Seele_div_iff₀'for a version with multiplication on the other side. .Lean, lines 202–207
· exfalso apply hcon refine ⟨a, ha, b, hb, ?_⟩ rw [le_div_iff₀ hnq] have h2 : a.gcd b * B.card ≤ a := by rw [Nat.mul_comm]; exact h.ge exact_mod_cast h2hlt.s2.h2havea.gcd b * B.card ≤ aLeaves
(↑(a.gcd b) : ℚ) * (↑B.card : ℚ) ≤ (↑a : ℚ), withh2 : a.gcd b * B.card ≤ a.Uses library
Nat.mul_comm.Lean, line 206
have h2 : a.gcd b * B.card ≤ a := by rw [Nat.mul_comm]; exact h.ge
hAhave∀ (p : ℕ), Nat.Prime p → B.card ≤ (2 : ℕ) * p → ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬p ∣ b → a = p * a.gcd bLeaves
False, withhA : ∀ (p : ℕ), Nat.Prime p → B.card ≤ (2 : ℕ) * p → ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬p ∣ b → a = p * a.gcd b.Lean, lines 208–238
have hA : ∀ p : ℕ, p.Prime → B.card ≤ 2 * p → ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a = p * a.gcd b := by intro p hp hnp2 a ha hpa b hb hpb have ha0 : a ≠ 0 := fun h => h0 (h ▸ ha) have hg0 : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero ha0) obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b have hpg : ¬ p ∣ a.gcd b := fun h => hpb (h.trans (Nat.gcd_dvd_right a b)) have hpx : p ∣ x := by have h1 : p ∣ a.gcd b * x := hx ▸ hpa exact (hp.dvd_mul.mp h1).resolve_left hpg obtain ⟨t, ht⟩ := hpx have hlt' := hlt a ha b hb have hxn : x < B.card := by have h3 : a.gcd b * x < a.gcd b * B.card := by rw [← hx, Nat.mul_comm]; exact hlt' exact Nat.lt_of_mul_lt_mul_left h3 have ht1 : t = 1 := by have hx0 : x ≠ 0 := by rintro rfl rw [Nat.mul_zero] at hx exact ha0 hx have ht0 : t ≠ 0 := by rintro rfl rw [Nat.mul_zero] at ht exact hx0 ht by_contra hne1 have ht2 : 2 ≤ t := by omega have h4 : p * 2 ≤ p * t := Nat.mul_le_mul_left p ht2 omega calc a = a.gcd b * x := hx _ = p * a.gcd b := by rw [ht, ht1]; ringhA.ha0havea ≠ (0 : ℕ)Leaves
a = p * a.gcd b, withha0 : a ≠ (0 : ℕ).Lean, line 211
have ha0 : a ≠ 0 := fun h => h0 (h ▸ ha)
hA.hg0have(0 : ℕ) < a.gcd bLeaves
a = p * a.gcd b, withhg0 : (0 : ℕ) < a.gcd b.Uses library
Nat.gcd_pos_of_pos_left,Nat.pos_of_ne_zero.Lean, line 212
have hg0 : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero ha0)
hA.s3obtaina.gcd b ∣ aLeaves
a = p * a.gcd b, withx : ℕ,hx : a = a.gcd b * x.Uses library
Nat.gcd_dvd_left.Lean, line 213
obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b
hA.hpghave¬p ∣ a.gcd bLeaves
a = p * a.gcd b, withhpg : ¬p ∣ a.gcd b.Uses library
Nat.gcd_dvd_right.Lean, line 214
have hpg : ¬ p ∣ a.gcd b := fun h => hpb (h.trans (Nat.gcd_dvd_right a b))
hA.hpxhavep ∣ xLeaves
a = p * a.gcd b, withhpx : p ∣ x.Lean, lines 215–217
have hpx : p ∣ x := by have h1 : p ∣ a.gcd b * x := hx ▸ hpa exact (hp.dvd_mul.mp h1).resolve_left hpghA.hpx.h1havep ∣ a.gcd b * xLeaves
p ∣ x, withh1 : p ∣ a.gcd b * x.Lean, line 216
have h1 : p ∣ a.gcd b * x := hx ▸ hpa
hA.s6obtainp ∣ xLeaves
a = p * a.gcd b, witht : ℕ,ht : x = p * t.Lean, line 218
obtain ⟨t, ht⟩ := hpx
hA.hlt'havea < B.card * a.gcd bLeaves
a = p * a.gcd b, withhlt' : a < B.card * a.gcd b.Lean, line 219
have hlt' := hlt a ha b hb
hA.hxnhavex < B.cardLeaves
a = p * a.gcd b, withhxn : x < B.card.Uses library
Nat.lt_of_mul_lt_mul_left.Lean, lines 220–223
have hxn : x < B.card := by have h3 : a.gcd b * x < a.gcd b * B.card := by rw [← hx, Nat.mul_comm]; exact hlt' exact Nat.lt_of_mul_lt_mul_left h3hA.hxn.h3havea.gcd b * x < a.gcd b * B.cardLeaves
x < B.card, withh3 : a.gcd b * x < a.gcd b * B.card.Uses library
Nat.mul_comm.Lean, lines 221–222
have h3 : a.gcd b * x < a.gcd b * B.card := by rw [← hx, Nat.mul_comm]; exact hlt'
hA.ht1havet = (1 : ℕ)Leaves
a = p * a.gcd b, withht1 : t = (1 : ℕ).Lean, lines 224–236
have ht1 : t = 1 := by have hx0 : x ≠ 0 := by rintro rfl rw [Nat.mul_zero] at hx exact ha0 hx have ht0 : t ≠ 0 := by rintro rfl rw [Nat.mul_zero] at ht exact hx0 ht by_contra hne1 have ht2 : 2 ≤ t := by omega have h4 : p * 2 ≤ p * t := Nat.mul_le_mul_left p ht2 omegahA.ht1.hx0havex ≠ (0 : ℕ)Leaves
t = (1 : ℕ), withhx0 : x ≠ (0 : ℕ).Uses library
Nat.mul_zero.Lean, lines 225–228
have hx0 : x ≠ 0 := by rintro rfl rw [Nat.mul_zero] at hx exact ha0 hxhA.ht1.ht0havet ≠ (0 : ℕ)Leaves
t = (1 : ℕ), withht0 : t ≠ (0 : ℕ).Uses library
Nat.mul_zero.Lean, lines 229–232
have ht0 : t ≠ 0 := by rintro rfl rw [Nat.mul_zero] at ht exact hx0 hthA.ht1.ht2have(2 : ℕ) ≤ troutine: omegaLeaves
False, withht2 : (2 : ℕ) ≤ t.Lean, line 234
have ht2 : 2 ≤ t := by omega
hA.ht1.h4havep * (2 : ℕ) ≤ p * tLeaves
False, withh4 : p * (2 : ℕ) ≤ p * t.Uses library
Nat.mul_le_mul_left.Lean, line 235
have h4 : p * 2 ≤ p * t := Nat.mul_le_mul_left p ht2
hA.s10calca = a.gcd b * xCloses the goal.
Lean, line 237
calc a = a.gcd b * x := hx
hA.s11calcCloses the goal.
Lean, line 238
_ = p * a.gcd b := by rw [ht, ht1]; ring
s9caseLeaves
False.s10caseLeaves
False.Uses library
Exists.introExistential introduction. .Lean, lines 241–250
· have hpn : p < B.card := by have h1 := hpp a ha p 1 hp (by rwa [pow_one]) rwa [pow_one] at h1 have hexb : ∃ b ∈ B, ¬ p ∣ b := by by_contra h push Not at h have h1 : p ∣ B.gcd id := Finset.dvd_gcd (fun b hb => h b hb) rw [hgcd] at h1 exact hp.one_lt.ne' (Nat.dvd_one.mp h1) exact hlarge B h0 hlt p hp hpn (hA p hp hnp2) ⟨a, ha, hpa⟩ hexbs10.hpnhavep < B.cardLeaves
False, withhpn : p < B.card.Uses library
pow_one.Lean, lines 241–243
· have hpn : p < B.card := by have h1 := hpp a ha p 1 hp (by rwa [pow_one]) rwa [pow_one] at h1s10.hpn.h1havep ^ (1 : ℕ) < B.cardLeaves
p < B.card, withh1 : p ^ (1 : ℕ) < B.card.Uses library
pow_one.Lean, line 242
have h1 := hpp a ha p 1 hp (by rwa [pow_one])
s10.hexbhave∃ b ∈ B, ¬p ∣ bLeaves
False, withhexb : ∃ b ∈ B, ¬p ∣ b.Uses library
NotNot p, or¬p, is the negation ofp. ,Nat.dvd_one.Lean, lines 244–249
have hexb : ∃ b ∈ B, ¬ p ∣ b := by by_contra h push Not at h have h1 : p ∣ B.gcd id := Finset.dvd_gcd (fun b hb => h b hb) rw [hgcd] at h1 exact hp.one_lt.ne' (Nat.dvd_one.mp h1)s10.hexb.h1havep ∣ B.gcd idLeaves
False, withh1 : p ∣ B.gcd id.Uses library
idThe identity function. ,Finset.dvd_gcd.Lean, line 247
have h1 : p ∣ B.gcd id := Finset.dvd_gcd (fun b hb => h b hb)
import Mathlib
import Nodes.«erdos-402--h3-v2--h1».Context
open Filter
/-! Hole `hcomp` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/
theorem erdos_402__h3_v2__h1 : ∀ (B : Finset ℕ),
(0 : ℕ) ∉ B →
B.Nonempty →
B.gcd id = (1 : ℕ) →
¬Nat.Prime B.card →
(∀ (q : ℕ), Nat.Prime q → B.card ≠ q + (1 : ℕ)) →
(∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
(∀ a ∈ B, ∀ (p k : ℕ), Nat.Prime p → p ^ k ∣ a → p ^ k < B.card) →
∃ a ∈ B, ∃ b ∈ B, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑B.card : ℚ) := by
-- Informal argument: annex 6a64518f9cd863c9abea3114b518f3172f4c73c6a187eb928b43db35f77c0002 on this node (graph PR #325, in the merge queue when this was prechecked).
-- Hole `hsmooth`: B has a pair with gcd(a, b) ≤ a / n, or an element with a prime factor p ≥ n / 2.
-- The assembly proves that the second alternative contradicts the strict inequalities.
have hsmooth : ∀ B : Finset ℕ, 0 ∉ B → B.Nonempty → B.gcd id = 1 → ¬ B.card.Prime →
(∀ q : ℕ, q.Prime → B.card ≠ q + 1) →
(∀ a ∈ B, ∀ b ∈ B, a ≤ B.card * a.gcd b) →
(∀ a ∈ B, ∀ p k : ℕ, p.Prime → p ^ k ∣ a → p ^ k < B.card) →
(∃ a ∈ B, ∃ b ∈ B, (a.gcd b : ℚ) ≤ (a : ℚ) / (B.card : ℚ)) ∨
∃ p : ℕ, p.Prime ∧ B.card ≤ 2 * p ∧ ∃ a ∈ B, p ∣ a := sorry
have big : ∀ S : Finset ℕ, (∀ x ∈ S, 0 < x) → S.Nonempty → ∃ x ∈ S, S.card ≤ x := by
intro S hpos hS
by_contra h
push Not at h
have hsub : S ⊆ Finset.Ioo 0 S.card := by
intro x hx
exact Finset.mem_Ioo.mpr ⟨hpos x hx, h x hx⟩
have h1 := Finset.card_le_card hsub
rw [Nat.card_Ioo] at h1
have h2 := hS.card_pos
omega
have key : ∀ (n p : ℕ) (X T : Finset ℕ), 0 < p → p < n →
(∀ x ∈ X, ∀ t ∈ T, 0 < x * t ∧ x * t < n ∧ ¬ p ∣ x * t) →
X.Nonempty → T.Nonempty → n ≤ X.card + T.card → False := by
intro n p X T hp hpn hxt hX hT hcard
have hXpos : ∀ x ∈ X, 0 < x := by
intro x hx
obtain ⟨t, ht⟩ := hT
have h := (hxt x hx t ht).1
exact Nat.pos_of_ne_zero (by rintro rfl; simp at h)
have hTpos : ∀ t ∈ T, 0 < t := by
intro t ht
obtain ⟨x, hx⟩ := hX
have h := (hxt x hx t ht).1
exact Nat.pos_of_ne_zero (by rintro rfl; simp at h)
obtain ⟨x0, hx0, hx0c⟩ := big X hXpos hX
obtain ⟨t0, ht0, ht0c⟩ := big T hTpos hT
have h1 := (hxt x0 hx0 t0 ht0).2.1
have h2 : X.card * T.card ≤ x0 * t0 := Nat.mul_le_mul hx0c ht0c
have hu := hX.card_pos
have hv := hT.card_pos
have hc2 : ((Finset.Ioo 0 n).erase p).card = n - 2 := by
rw [Finset.card_erase_of_mem (Finset.mem_Ioo.mpr ⟨hp, hpn⟩), Nat.card_Ioo]
omega
have h3 : X.card = 1 ∨ T.card = 1 := by
by_contra h
push Not at h
have h4 : 2 ≤ X.card := by omega
have h5 : 2 ≤ T.card := by omega
nlinarith
rcases h3 with hu1 | hv1
· have hsub : T.image (fun t => x0 * t) ⊆ (Finset.Ioo 0 n).erase p := by
intro y hy
obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hy
have h := hxt x0 hx0 t ht
rw [Finset.mem_erase, Finset.mem_Ioo]
exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩
have hc1 : (T.image (fun t => x0 * t)).card = T.card :=
Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_left (hXpos x0 hx0) h)
have h6 := Finset.card_le_card hsub
omega
· have hsub : X.image (fun x => x * t0) ⊆ (Finset.Ioo 0 n).erase p := by
intro y hy
obtain ⟨x, hx, rfl⟩ := Finset.mem_image.mp hy
have h := hxt x hx t0 ht0
rw [Finset.mem_erase, Finset.mem_Ioo]
exact ⟨fun e => h.2.2 (dvd_of_eq e.symm), h.1, h.2.1⟩
have hc1 : (X.image (fun x => x * t0)).card = X.card :=
Finset.card_image_of_injective _ (fun a b h => Nat.eq_of_mul_eq_mul_right (hTpos t0 ht0) h)
have h6 := Finset.card_le_card hsub
omega
have hlarge : ∀ B : Finset ℕ, 0 ∉ B →
(∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b) →
∀ p : ℕ, p.Prime → p < B.card →
(∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a = p * a.gcd b) →
(∃ a ∈ B, p ∣ a) → (∃ b ∈ B, ¬ p ∣ b) → False := by
intro B h0 hlt p hp hpn hA hexa hexb
obtain ⟨a0, ha0, hpa0⟩ := hexa
obtain ⟨b0, hb0, hpb0⟩ := hexb
have hG0 : (B.filter (fun b => ¬ p ∣ b)).gcd id ≠ 0 := by
intro h
have h1 : (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ id b0 :=
Finset.gcd_dvd (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)
rw [h] at h1
exact hpb0 (by rw [show b0 = 0 from Nat.eq_zero_of_zero_dvd h1]; exact dvd_zero p)
have hGb : ∀ b ∈ B, ¬ p ∣ b → (B.filter (fun b => ¬ p ∣ b)).gcd id ∣ b := by
intro b hb hpb
exact Finset.gcd_dvd (f := id) (Finset.mem_filter.mpr ⟨hb, hpb⟩)
have hdG : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b →
a.gcd b ∣ (B.filter (fun b => ¬ p ∣ b)).gcd id := by
intro a ha hpa b hb hpb
apply Finset.dvd_gcd
intro b' hb'
obtain ⟨hb'B, hpb'⟩ := Finset.mem_filter.mp hb'
have e1 := hA a ha hpa b hb hpb
have e2 := hA a ha hpa b' hb'B hpb'
have e3 : a.gcd b = a.gcd b' := Nat.eq_of_mul_eq_mul_left hp.pos (e1.symm.trans e2)
rw [e3]
exact Nat.gcd_dvd_right a b'
have hprod : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b →
0 < ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧
((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) < B.card ∧
¬ p ∣ ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) * (b / (B.filter (fun b => ¬ p ∣ b)).gcd id) ∧
a * ((B.filter (fun b => ¬ p ∣ b)).gcd id * p / a) = (B.filter (fun b => ¬ p ∣ b)).gcd id * p := by
intro a ha hpa b hb hpb
generalize hG : (B.filter (fun b => ¬ p ∣ b)).gcd id = G at *
obtain ⟨e, he⟩ := hdG a ha hpa b hb hpb
obtain ⟨s, hs⟩ := hGb b hb hpb
have ea := hA a ha hpa b hb hpb
have ha0' : 0 < a := Nat.pos_of_ne_zero (fun h => h0 (h ▸ ha))
have hb0' : b ≠ 0 := fun h => h0 (h ▸ hb)
have hGp : G * p = e * a :=
calc G * p = a.gcd b * e * p := by rw [he]
_ = e * (p * a.gcd b) := by ring
_ = e * a := by rw [← ea]
have hx : G * p / a = e := Nat.div_eq_of_eq_mul_left ha0' hGp
have ht : b / G = s := by
rw [hs]
exact Nat.mul_div_cancel_left s (Nat.pos_of_ne_zero hG0)
rw [hx, ht]
have hb2 : b = a.gcd b * (e * s) :=
calc b = G * s := hs
_ = a.gcd b * e * s := by rw [he]
_ = a.gcd b * (e * s) := by ring
have hes : e * s ≠ 0 := by
intro h
rw [h, Nat.mul_zero] at hb2
exact hb0' hb2
refine ⟨Nat.pos_of_ne_zero hes, ?_, ?_, ?_⟩
· have h1 := hlt b hb a ha
rw [Nat.gcd_comm b a] at h1
have h2 : a.gcd b * (e * s) < a.gcd b * B.card := by
rw [← hb2, Nat.mul_comm]; exact h1
exact Nat.lt_of_mul_lt_mul_left h2
· intro h
exact hpb (hb2 ▸ Dvd.dvd.mul_left h _)
· rw [hGp]; ring
have hcardsum : (B.filter (fun a => p ∣ a)).card + (B.filter (fun b => ¬ p ∣ b)).card = B.card := by
rw [← Finset.card_union_of_disjoint (Finset.disjoint_filter_filter_not B B (fun a => p ∣ a)),
Finset.filter_union_filter_not_eq]
have hinjX : Set.InjOn (fun a => (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a)
(B.filter (fun a => p ∣ a) : Finset ℕ) := by
intro a ha a' ha' h
obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
obtain ⟨haB', hpa'⟩ := Finset.mem_filter.mp ha'
have h1 := (hprod a haB hpa b0 hb0 hpb0)
have h2 := (hprod a' haB' hpa' b0 hb0 hpb0).2.2.2
simp only at h
rw [← h] at h2
have hq : 0 < (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a :=
Nat.pos_of_ne_zero (by
intro hz
have := h1.1
rw [hz, Nat.zero_mul] at this
exact lt_irrefl 0 this)
exact Nat.eq_of_mul_eq_mul_right hq (h1.2.2.2.trans h2.symm)
have hinjT : Set.InjOn (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id)
(B.filter (fun b => ¬ p ∣ b) : Finset ℕ) := by
intro b hb b' hb' h
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
obtain ⟨hbB', hpb'⟩ := Finset.mem_filter.mp hb'
simp only at h
rw [← Nat.div_mul_cancel (hGb b hbB hpb), ← Nat.div_mul_cancel (hGb b' hbB' hpb'), h]
refine key B.card p
((B.filter (fun a => p ∣ a)).image (fun a => (B.filter (fun b => ¬ p ∣ b)).gcd id * p / a))
((B.filter (fun b => ¬ p ∣ b)).image (fun b => b / (B.filter (fun b => ¬ p ∣ b)).gcd id))
hp.pos hpn ?_ ?_ ?_ ?_
· intro x hx t ht
obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp ht
obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
have h := hprod a haB hpa b hbB hpb
exact ⟨h.1, h.2.1, h.2.2.1⟩
· exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨ha0, hpa0⟩)⟩
· exact ⟨_, Finset.mem_image_of_mem _ (Finset.mem_filter.mpr ⟨hb0, hpb0⟩)⟩
· rw [Finset.card_image_of_injOn hinjX, Finset.card_image_of_injOn hinjT, hcardsum]
intro B h0 hne hgcd hnp hnp1 hle hpp
by_contra hcon
have hn : 0 < B.card := hne.card_pos
have hnq : (0 : ℚ) < B.card := by exact_mod_cast hn
have hlt : ∀ a ∈ B, ∀ b ∈ B, a < B.card * a.gcd b := by
intro a ha b hb
rcases (hle a ha b hb).lt_or_eq with h | h
· exact h
· exfalso
apply hcon
refine ⟨a, ha, b, hb, ?_⟩
rw [le_div_iff₀ hnq]
have h2 : a.gcd b * B.card ≤ a := by rw [Nat.mul_comm]; exact h.ge
exact_mod_cast h2
have hA : ∀ p : ℕ, p.Prime → B.card ≤ 2 * p →
∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b → a = p * a.gcd b := by
intro p hp hnp2 a ha hpa b hb hpb
have ha0 : a ≠ 0 := fun h => h0 (h ▸ ha)
have hg0 : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (Nat.pos_of_ne_zero ha0)
obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b
have hpg : ¬ p ∣ a.gcd b := fun h => hpb (h.trans (Nat.gcd_dvd_right a b))
have hpx : p ∣ x := by
have h1 : p ∣ a.gcd b * x := hx ▸ hpa
exact (hp.dvd_mul.mp h1).resolve_left hpg
obtain ⟨t, ht⟩ := hpx
have hlt' := hlt a ha b hb
have hxn : x < B.card := by
have h3 : a.gcd b * x < a.gcd b * B.card := by
rw [← hx, Nat.mul_comm]; exact hlt'
exact Nat.lt_of_mul_lt_mul_left h3
have ht1 : t = 1 := by
have hx0 : x ≠ 0 := by
rintro rfl
rw [Nat.mul_zero] at hx
exact ha0 hx
have ht0 : t ≠ 0 := by
rintro rfl
rw [Nat.mul_zero] at ht
exact hx0 ht
by_contra hne1
have ht2 : 2 ≤ t := by omega
have h4 : p * 2 ≤ p * t := Nat.mul_le_mul_left p ht2
omega
calc a = a.gcd b * x := hx
_ = p * a.gcd b := by rw [ht, ht1]; ring
rcases hsmooth B h0 hne hgcd hnp hnp1 hle hpp with h | ⟨p, hp, hnp2, a, ha, hpa⟩
· exact hcon h
· have hpn : p < B.card := by
have h1 := hpp a ha p 1 hp (by rwa [pow_one])
rwa [pow_one] at h1
have hexb : ∃ b ∈ B, ¬ p ∣ b := by
by_contra h
push Not at h
have h1 : p ∣ B.gcd id := Finset.dvd_gcd (fun b hb => h b hb)
rw [hgcd] at h1
exact hp.one_lt.ne' (Nat.dvd_one.mp h1)
exact hlarge B h0 hlt p hp hpn (hA p hp hnp2) ⟨a, ha, hpa⟩ hexbAnnexes (2), in full
Untrusted contributor text — an annex (D-31): an informal argument, not a proof.
Untrusted: annex (D-31), by t1001-402-r2c, drafted with claude-fable-5-1 (Claude Code agent 402-R2-c); Lean fast-checked on POST /check (AXLE lean-4.33.1), 2026-10-01T12:39:47Z, licence CC-BY-4.0. Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1/annex/3ba21d75d8e00b9e7480a2564cd6cac91b4067ada622eef004be90e67232d5ae.md.
Erdős 402, hole erdos-402--h3-v2--h1: the general "few or almost all" lemma for every prime, and the duality reduction to the "few" side. Both checked in Lean (block below, re-checked from this text on POST /check, lean-4.33.1, no sorry, no axioms beyond Mathlib's). Generalises annex 6a64518f9cd863c9abea3114b518f3172f4c73c6a187eb928b43db35f77c0002 (primes p ≥ n/2) and uses the dual set of annex abe3e5f7aae6540a75a47ba0421ff62ac6c95f4bce427ba0df7a06c398575b87.
Setting. B a finite nonempty set of positive integers, N a number with a < N·gcd(a,b) for all a, b in B (a "strict counterexample" is the case N = |B| = n). p a prime; u = number of multiples of p in B, v = number of non-multiples.
Theorem A (R2c.few_or_most). Let M be any positive integer divisible by every m ≥ 1 with m·p < N (e.g. M = lcm(1..k), k = ⌊(N−1)/p⌋). Then u·v < N·M. No condition p ≥ √N and no condition on p-adic valuations is needed.
Proof. If u = 0 or v = 0 there is nothing to show. Let C be the non-multiples, G = gcd(C). Take a with p | a and b in C, g = gcd(a,b), a = g·x, b = g·y. Then x < N, y < N, and p | x since p does not divide g; write x = p·m. From m·p = x < N, m | M, say M = m·m'. Hence a = g·p·m divides p·M·b, and this for every b in C, so a | p·M·G. Put e_a = p·M·G / a and s_b = b / G: positive integers, a ↦ e_a injective on the multiples, b ↦ s_b injective on C. From a·e_a·s_b = p·M·b one gets e_a·s_b = m'·y < M·N. A set of u distinct positive integers has an element ≥ u, likewise v; so u·v ≤ max e · max s < N·M.
Corollaries with N = n = u + v. (A1) If n ≤ (k+1)·p and M is a positive common multiple of 1..k then u < 2M or v < 2M. (k = 1: u·v < u + v, so u = 1 or v = 1: the n ≤ 2p case.) (A2) If 9 ≤ n ≤ 3p then u ≤ 2 or v ≤ 2. Sharpness: exhaustive search over all B ⊆ [1..26] with N ≤ 10 and all primes ≤ 13 finds u·v/(N·M) as large as 6/7 (B = {2,4,5,6,10}, N = 7, p = 5), so the bound cannot be improved by more than a small constant in general.
Theorem B (R2c.dual_package). Let L = lcm(B), B* = {L/a : a in B}. Then |B*| = |B|, 0 not in B*, gcd(B*) = 1; every prime power dividing an element of B* divides an element of B; (L/a)·gcd(a,b) = b·gcd(L/a, L/b), so "all quotients ≤ n" passes from B to B* and a pair with n·gcd(x,y) ≤ x in B* gives one in B; and if p divides an element of B but p² divides none, then p | L/a exactly when p does not divide a, so u(B*) = v(B), v(B*) = u(B).
Theorem B' (R2c.wlog_few). Fix n and a prime p. Suppose every B satisfying the hypotheses of this hole in ℕ form (0 not in B, |B| = n, gcd 1, a ≤ n·gcd(a,b), all prime powers dividing elements < n), with p dividing an element, p² dividing none, and 2u ≤ n, has a pair with n·gcd(a,b) ≤ a. Then the same holds without "2u ≤ n". (When p² ≥ n, "p² divides none" follows from the prime-power hypothesis.) So at one prime p ≥ √n a prover may assume the "few multiples" side of Theorem A: u < 2M once n ≥ 4M.
What duality does not give. If p² divides an element, p | L/a iff v_p(a) < v_p(L): the multiples of p in B* are the elements of non-maximal p-valuation and the counts do not swap. The reduction is for one prime at a time: dualising to make p "few" may make another prime q "almost all".
What remains open. Theorem A bounds min(u, v) but the hole needs a contradiction from "few": for n/3 ≤ p < n/2 the case u ≤ 2 leaves the configuration B = {2p} ∪ T of 402-R1-a's notes; for smaller p the bound 2·lcm(1..k) grows like e^{n/p} and is only useful for p ≥ n/ log n roughly. The literature closes the gap with primes in short intervals; nothing here replaces that.
Lean (three statements plus two corollaries; helper facts are inner haves so each can be inlined):
import Mathlib
/-- A ("few or almost all", exact form). B a set of positive integers, all quotients
a / gcd(a,b) < N, p any prime, M any positive common multiple of the m with m * p < N.
Then (#multiples of p) * (#non-multiples of p) < N * M. No hypothesis on p-adic valuations. -/
theorem R2c.few_or_most (B : Finset ℕ) (N p M : ℕ) (h0 : 0 ∉ B) (hne : B.Nonempty)
(hp : p.Prime) (hM0 : 0 < M) (hM : ∀ m : ℕ, 0 < m → m * p < N → m ∣ M)
(hs : ∀ a ∈ B, ∀ b ∈ B, a < N * Nat.gcd a b) :
(B.filter (fun a => p ∣ a)).card * (B.filter (fun b => ¬ p ∣ b)).card < N * M := by
have key : ∀ (Y : Finset ℕ) (hY : Y.Nonempty), 0 ∉ Y → Y.card ≤ Y.max' hY := by
intro Y hY h0
have hsub : Y ⊆ Finset.Icc 1 (Y.max' hY) := by
intro y hy
rw [Finset.mem_Icc]
exact ⟨Nat.pos_of_ne_zero (fun e => h0 (e ▸ hy)), Y.le_max' y hy⟩
have := Finset.card_le_card hsub
simpa using this
have hpos : ∀ a ∈ B, 0 < a := fun a ha => Nat.pos_of_ne_zero (fun e => h0 (e ▸ ha))
have hN : 0 < N := by
obtain ⟨a, ha⟩ := hne
have := hs a ha a ha
exact Nat.pos_of_ne_zero (by rintro rfl; simp at this)
have hNM : 0 < N * M := Nat.mul_pos hN hM0
rcases Finset.eq_empty_or_nonempty (B.filter (fun a => p ∣ a)) with hU | hU
· rw [hU]; simpa using hNM
rcases Finset.eq_empty_or_nonempty (B.filter (fun b => ¬ p ∣ b)) with hC | hC
· rw [hC]; simpa using hNM
generalize hG : (B.filter (fun b => ¬ p ∣ b)).gcd id = G
have hGb : ∀ b ∈ B, ¬ p ∣ b → G ∣ b := by
intro b hb hpb
rw [← hG]
exact Finset.gcd_dvd (f := id) (Finset.mem_filter.mpr ⟨hb, hpb⟩)
have hG0 : 0 < G := by
obtain ⟨b, hb⟩ := hC
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
exact Nat.pos_of_dvd_of_pos (hGb b hbB hpb) (hpos b hbB)
-- the pair analysis
have hpair : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b →
a ∣ p * M * b ∧ ∀ e s : ℕ, a * e * s = p * M * b → e * s < N * M := by
intro a ha hpa b hb hpb
have hg0 : 0 < a.gcd b := Nat.gcd_pos_of_pos_left b (hpos a ha)
obtain ⟨x, hx⟩ := Nat.gcd_dvd_left a b
obtain ⟨y, hy⟩ := Nat.gcd_dvd_right a b
have hpg : ¬ p ∣ a.gcd b := fun h => hpb (h.trans (Nat.gcd_dvd_right a b))
have hpx : p ∣ x := by
have h1 : p ∣ a.gcd b * x := hx ▸ hpa
exact (hp.dvd_mul.mp h1).resolve_left hpg
obtain ⟨m, hm⟩ := hpx
have hxN : x < N := by
have h1 := hs a ha b hb
have h3 : a.gcd b * x < a.gcd b * N := by
rw [← hx, Nat.mul_comm]; exact h1
exact Nat.lt_of_mul_lt_mul_left h3
have hyN : y < N := by
have h1 := hs b hb a ha
rw [Nat.gcd_comm b a] at h1
have h3 : a.gcd b * y < a.gcd b * N := by
rw [← hy, Nat.mul_comm]; exact h1
exact Nat.lt_of_mul_lt_mul_left h3
have hx0 : 0 < x := Nat.pos_of_ne_zero (by
rintro rfl
rw [Nat.mul_zero] at hx
exact (hpos a ha).ne' hx)
have hm0 : 0 < m := Nat.pos_of_ne_zero (by
rintro rfl
rw [Nat.mul_zero] at hm
exact hx0.ne' hm)
have hmM : m ∣ M := hM m hm0 (by rw [Nat.mul_comm, ← hm]; exact hxN)
obtain ⟨m', hm'⟩ := hmM
have hm'0 : 0 < m' := Nat.pos_of_ne_zero (by
rintro rfl
rw [Nat.mul_zero] at hm'
exact hM0.ne' hm')
have ea : a = a.gcd b * (p * m) := by rw [← hm]; exact hx
refine ⟨⟨m' * y, ?_⟩, ?_⟩
· calc p * M * b = p * (m * m') * (a.gcd b * y) := by rw [← hm', ← hy]
_ = a.gcd b * (p * m) * (m' * y) := by ring
_ = a * (m' * y) := by rw [← ea]
· intro e s hes
have h1 : (a.gcd b * p * m) * (e * s) = (a.gcd b * p * m) * (m' * y) := by
calc (a.gcd b * p * m) * (e * s) = (a.gcd b * (p * m)) * e * s := by ring
_ = a * e * s := by rw [← ea]
_ = p * M * b := hes
_ = p * (m * m') * (a.gcd b * y) := by rw [← hm', ← hy]
_ = (a.gcd b * p * m) * (m' * y) := by ring
have h2 : e * s = m' * y :=
Nat.eq_of_mul_eq_mul_left (Nat.mul_pos (Nat.mul_pos hg0 hp.pos) hm0) h1
have h3 : m' ≤ M := Nat.le_of_dvd hM0 ⟨m, by rw [hm', Nat.mul_comm]⟩
rw [h2, Nat.mul_comm N M]
calc m' * y ≤ M * y := Nat.mul_le_mul_right y h3
_ < M * N := Nat.mul_lt_mul_of_pos_left hyN hM0
-- every multiple of p divides p * M * G
have hdiv : ∀ a ∈ B, p ∣ a → a ∣ p * M * G := by
intro a ha hpa
have h1 : a ∣ (B.filter (fun b => ¬ p ∣ b)).gcd (fun b => p * M * id b) := by
apply Finset.dvd_gcd
intro b hb
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
exact (hpair a ha hpa b hbB hpb).1
rw [Finset.gcd_mul_left, hG] at h1
simpa using h1
have hprod : ∀ a ∈ B, p ∣ a → ∀ b ∈ B, ¬ p ∣ b →
(p * M * G / a) * (b / G) < N * M ∧ a * (p * M * G / a) = p * M * G ∧
0 < p * M * G / a ∧ 0 < b / G := by
intro a ha hpa b hb hpb
have e1 : a * (p * M * G / a) = p * M * G := Nat.mul_div_cancel' (hdiv a ha hpa)
have e2 : G * (b / G) = b := Nat.mul_div_cancel' (hGb b hb hpb)
have hPos : 0 < p * M * G := Nat.mul_pos (Nat.mul_pos hp.pos hM0) hG0
refine ⟨(hpair a ha hpa b hb hpb).2 _ _ ?_, e1, ?_, ?_⟩
· rw [e1, Nat.mul_assoc (p * M), e2]
· exact Nat.pos_of_ne_zero (by
intro h
rw [h, Nat.mul_zero] at e1
exact hPos.ne e1)
· exact Nat.pos_of_ne_zero (by
intro h
rw [h, Nat.mul_zero] at e2
exact (hpos b hb).ne e2)
obtain ⟨a0, ha0⟩ := hU
obtain ⟨b0, hb0⟩ := hC
obtain ⟨ha0B, hpa0⟩ := Finset.mem_filter.mp ha0
obtain ⟨hb0B, hpb0⟩ := Finset.mem_filter.mp hb0
have hinjX : Set.InjOn (fun a => p * M * G / a) (B.filter (fun a => p ∣ a) : Finset ℕ) := by
intro a ha a' ha' h
obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
obtain ⟨haB', hpa'⟩ := Finset.mem_filter.mp ha'
have h1 := hprod a haB hpa b0 hb0B hpb0
have h2 := (hprod a' haB' hpa' b0 hb0B hpb0).2.1
simp only at h
rw [← h] at h2
exact Nat.eq_of_mul_eq_mul_right h1.2.2.1 (h1.2.1.trans h2.symm)
have hinjT : Set.InjOn (fun b => b / G) (B.filter (fun b => ¬ p ∣ b) : Finset ℕ) := by
intro b hb b' hb' h
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
obtain ⟨hbB', hpb'⟩ := Finset.mem_filter.mp hb'
simp only at h
rw [← Nat.div_mul_cancel (hGb b hbB hpb), ← Nat.div_mul_cancel (hGb b' hbB' hpb'), h]
have hXn : ((B.filter (fun a => p ∣ a)).image (fun a => p * M * G / a)).Nonempty :=
⟨_, Finset.mem_image_of_mem _ ha0⟩
have hTn : ((B.filter (fun b => ¬ p ∣ b)).image (fun b => b / G)).Nonempty :=
⟨_, Finset.mem_image_of_mem _ hb0⟩
have hX0 : 0 ∉ (B.filter (fun a => p ∣ a)).image (fun a => p * M * G / a) := by
intro h
obtain ⟨a, ha, e⟩ := Finset.mem_image.mp h
obtain ⟨haB, hpa⟩ := Finset.mem_filter.mp ha
exact (hprod a haB hpa b0 hb0B hpb0).2.2.1.ne' e
have hT0 : 0 ∉ (B.filter (fun b => ¬ p ∣ b)).image (fun b => b / G) := by
intro h
obtain ⟨b, hb, e⟩ := Finset.mem_image.mp h
obtain ⟨hbB, hpb⟩ := Finset.mem_filter.mp hb
exact (hprod a0 ha0B hpa0 b hbB hpb).2.2.2.ne' e
have hmx := Finset.max'_mem _ hXn
have hmt := Finset.max'_mem _ hTn
obtain ⟨a1, ha1, ea1⟩ := Finset.mem_image.mp hmx
obtain ⟨b1, hb1, eb1⟩ := Finset.mem_image.mp hmt
obtain ⟨ha1B, hpa1⟩ := Finset.mem_filter.mp ha1
obtain ⟨hb1B, hpb1⟩ := Finset.mem_filter.mp hb1
have hfin := (hprod a1 ha1B hpa1 b1 hb1B hpb1).1
rw [ea1, eb1] at hfin
have c1 := key _ hXn hX0
have c2 := key _ hTn hT0
rw [Finset.card_image_of_injOn hinjX] at c1
rw [Finset.card_image_of_injOn hinjT] at c2
exact lt_of_le_of_lt (Nat.mul_le_mul c1 c2) hfin
/-- B (dual package). For a nonempty set B of positive integers, the dual set
B* = {lcm(B)/a} has the same size, no zero, gcd 1; prime powers dividing its elements divide
elements of B; the quotient hypotheses transfer; a good pair of B* gives a good pair of B; and
for a prime p dividing an element of B but with p² dividing none, the multiples of p in B* are
exactly the images of the non-multiples in B (the two counts swap). -/
theorem R2c.dual_package (B : Finset ℕ) (n : ℕ) (hne : B.Nonempty) (h0 : 0 ∉ B) :
(B.image (fun a => B.lcm id / a)).card = B.card ∧
(B.image (fun a => B.lcm id / a)).Nonempty ∧
0 ∉ B.image (fun a => B.lcm id / a) ∧
(B.image (fun a => B.lcm id / a)).gcd id = 1 ∧
(∀ x ∈ B.image (fun a => B.lcm id / a), ∀ q k : ℕ, q.Prime → q ^ k ∣ x → ∃ a ∈ B, q ^ k ∣ a) ∧
((∀ a ∈ B, ∀ b ∈ B, a ≤ n * Nat.gcd a b) →
∀ x ∈ B.image (fun a => B.lcm id / a), ∀ y ∈ B.image (fun a => B.lcm id / a),
x ≤ n * Nat.gcd x y) ∧
((∃ x ∈ B.image (fun a => B.lcm id / a), ∃ y ∈ B.image (fun a => B.lcm id / a),
n * Nat.gcd x y ≤ x) → ∃ a ∈ B, ∃ b ∈ B, n * Nat.gcd a b ≤ a) ∧
(∀ p : ℕ, p.Prime → (∃ a ∈ B, p ∣ a) → (∀ a ∈ B, ¬ p ^ 2 ∣ a) →
(∀ a ∈ B, (p ∣ B.lcm id / a ↔ ¬ p ∣ a)) ∧
((B.image (fun a => B.lcm id / a)).filter (fun x => p ∣ x)).card
= (B.filter (fun a => ¬ p ∣ a)).card ∧
((B.image (fun a => B.lcm id / a)).filter (fun x => ¬ p ∣ x)).card
= (B.filter (fun a => p ∣ a)).card) := by
-- E2 of 402-R1-b
have dual_quot : ∀ L a a' b b' : ℕ, a * a' = L → b * b' = L → 0 < a →
a' * Nat.gcd a b = b * Nat.gcd a' b' := by
intro L a a' b b' ha hb h0
have h1 : Nat.gcd a' b' * (a * b) = L * Nat.gcd a b := by
rw [← Nat.gcd_mul_right]
have e1 : a' * (a * b) = L * b := by rw [← ha]; ring
have e2 : b' * (a * b) = L * a := by rw [← hb]; ring
rw [e1, e2, Nat.gcd_mul_left, Nat.gcd_comm b a]
have h2 : a * (a' * Nat.gcd a b) = a * (b * Nat.gcd a' b') := by
rw [← mul_assoc, ha, ← h1]; ring
exact Nat.eq_of_mul_eq_mul_left h0 h2
-- a prime power dividing an lcm divides an element
have ppl : ∀ (q k : ℕ), q.Prime → ∀ S : Finset ℕ, 0 ∉ S → S.Nonempty → q ^ k ∣ S.lcm id →
∃ a ∈ S, q ^ k ∣ a := by
intro q k hq S
induction S using Finset.induction_on with
| empty => intro _ h; exact absurd h (by simp)
| insert x S hx ih =>
intro hS0 _ hdvd
have hx0 : x ≠ 0 := fun e => hS0 (e ▸ Finset.mem_insert_self x S)
have hS0' : 0 ∉ S := fun h => hS0 (Finset.mem_insert_of_mem h)
rcases Finset.eq_empty_or_nonempty S with hSe | hSn
· subst hSe
refine ⟨x, Finset.mem_insert_self _ _, ?_⟩
simpa using hdvd
· have hl0 : S.lcm id ≠ 0 := by
intro h
rw [Finset.lcm_eq_zero_iff] at h
obtain ⟨z, hz, e⟩ := h
have e' : z = 0 := e
exact hS0' (e' ▸ hz)
rw [Finset.lcm_insert] at hdvd
have hdvd' : q ^ k ∣ Nat.lcm x (S.lcm id) := hdvd
rw [hq.pow_dvd_iff_le_factorization (Nat.lcm_ne_zero hx0 hl0),
Nat.factorization_lcm hx0 hl0, Finsupp.sup_apply] at hdvd'
rcases le_sup_iff.mp hdvd' with h | h
· exact ⟨x, Finset.mem_insert_self _ _, (hq.pow_dvd_iff_le_factorization hx0).mpr h⟩
· obtain ⟨a, ha, hda⟩ := ih hS0' hSn ((hq.pow_dvd_iff_le_factorization hl0).mpr h)
exact ⟨a, Finset.mem_insert_of_mem ha, hda⟩
generalize hLdef : B.lcm id = L
have hdvd : ∀ a ∈ B, a ∣ L := fun a ha => hLdef ▸ Finset.dvd_lcm (f := id) ha
have hL0 : L ≠ 0 := by
intro h
rw [← hLdef, Finset.lcm_eq_zero_iff] at h
obtain ⟨z, hz, e⟩ := h
have e' : z = 0 := e
exact h0 (e' ▸ hz)
have hLpos : 0 < L := Nat.pos_of_ne_zero hL0
have hmul : ∀ a ∈ B, a * (L / a) = L := fun a ha => Nat.mul_div_cancel' (hdvd a ha)
have hapos : ∀ a ∈ B, 0 < a := fun a ha => Nat.pos_of_ne_zero (fun e => h0 (e ▸ ha))
have hqpos : ∀ a ∈ B, 0 < L / a := by
intro a ha
exact Nat.pos_of_ne_zero (by
intro h
have := hmul a ha
rw [h, Nat.mul_zero] at this
exact hL0 this.symm)
have hinj : Set.InjOn (fun a => L / a) (B : Set ℕ) := by
intro a ha b hb hab
simp only at hab
have e1 := hmul a ha
have e2 := hmul b hb
rw [hab] at e1
exact Nat.eq_of_mul_eq_mul_right (hqpos b hb) (e1.trans e2.symm)
-- quotient identity: (L/a) * gcd a b = b * gcd (L/a) (L/b)
have hid : ∀ a ∈ B, ∀ b ∈ B, (L / a) * Nat.gcd a b = b * Nat.gcd (L / a) (L / b) :=
fun a ha b hb => dual_quot L a (L / a) b (L / b) (hmul a ha) (hmul b hb) (hapos a ha)
have hgpos : ∀ a ∈ B, ∀ b ∈ B, 0 < Nat.gcd a b := fun a ha b _ =>
Nat.gcd_pos_of_pos_left _ (hapos a ha)
have hgpos' : ∀ a ∈ B, ∀ b ∈ B, 0 < Nat.gcd (L / a) (L / b) := fun a ha b _ =>
Nat.gcd_pos_of_pos_left _ (hqpos a ha)
refine ⟨Finset.card_image_of_injOn hinj, hne.image _, ?_, ?_, ?_, ?_, ?_, ?_⟩
· intro h
obtain ⟨a, ha, e⟩ := Finset.mem_image.mp h
exact (hqpos a ha).ne' e
· generalize hd : (B.image (fun a => L / a)).gcd id = d
have hdd : ∀ a ∈ B, d ∣ L / a := by
intro a ha
rw [← hd]
exact Finset.gcd_dvd (f := id) (Finset.mem_image_of_mem _ ha)
obtain ⟨a0, ha0⟩ := hne
have hdL : d ∣ L := (hdd a0 ha0).trans (Nat.div_dvd_of_dvd (hdvd a0 ha0))
have hdpos : 0 < d := Nat.pos_of_dvd_of_pos hdL hLpos
have hall : ∀ a ∈ B, id a ∣ L / d := by
intro a ha
obtain ⟨k, hk⟩ := hdd a ha
have e : L = d * (a * k) := by
have := hmul a ha
rw [hk] at this
rw [← this]; ring
have : L / d = a * k := by rw [e]; exact Nat.mul_div_cancel_left _ hdpos
rw [this]; exact Dvd.intro _ rfl
have hLdvd : L ∣ L / d := by
have h := Finset.lcm_dvd hall
rwa [hLdef] at h
have hpos' : 0 < L / d := Nat.div_pos (Nat.le_of_dvd hLpos hdL) hdpos
have hle : L ≤ L / d := Nat.le_of_dvd hpos' hLdvd
by_contra hne1
have h2 : 2 ≤ d := by omega
have := Nat.div_lt_self hLpos h2
omega
· intro x hx q k hq hqx
obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
have h1 : q ^ k ∣ B.lcm id := hLdef ▸ hqx.trans (Nat.div_dvd_of_dvd (hdvd a ha))
exact ppl q k hq B h0 hne h1
· intro hle x hx y hy
obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp hy
have e := hid a ha b hb
have h1 := hle b hb a ha
rw [Nat.gcd_comm b a] at h1
have h2 : L / a * Nat.gcd a b ≤ n * Nat.gcd (L / a) (L / b) * Nat.gcd a b := by
rw [e]
calc b * Nat.gcd (L / a) (L / b) ≤ n * Nat.gcd a b * Nat.gcd (L / a) (L / b) :=
Nat.mul_le_mul_right _ h1
_ = n * Nat.gcd (L / a) (L / b) * Nat.gcd a b := by ring
exact Nat.le_of_mul_le_mul_right h2 (hgpos a ha b hb)
· rintro ⟨x, hx, y, hy, hxy⟩
obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp hy
refine ⟨b, hb, a, ha, ?_⟩
have e := hid a ha b hb
have h2 : n * Nat.gcd b a * Nat.gcd (L / a) (L / b) ≤ b * Nat.gcd (L / a) (L / b) := by
rw [← e, Nat.gcd_comm b a]
calc n * Nat.gcd a b * Nat.gcd (L / a) (L / b) = n * Nat.gcd (L / a) (L / b) * Nat.gcd a b := by ring
_ ≤ L / a * Nat.gcd a b := Nat.mul_le_mul_right _ hxy
exact Nat.le_of_mul_le_mul_right h2 (hgpos' a ha b hb)
· intro p hp ⟨a1, ha1, hpa1⟩ hsq
have hpL : p ∣ L := hpa1.trans (hdvd a1 ha1)
have hsqL : ¬ p ^ 2 ∣ L := by
intro h
obtain ⟨a, ha, hda⟩ := ppl p 2 hp B h0 hne (hLdef ▸ h)
exact hsq a ha hda
have hiff : ∀ a ∈ B, (p ∣ L / a ↔ ¬ p ∣ a) := by
intro a ha
constructor
· intro h1 h2
apply hsqL
rw [← hmul a ha, pow_two]
exact Nat.mul_dvd_mul h2 h1
· intro h
have h1 : p ∣ a * (L / a) := by rw [hmul a ha]; exact hpL
exact (hp.dvd_mul.mp h1).resolve_left h
refine ⟨hiff, ?_, ?_⟩
· have e : (B.image (fun a => L / a)).filter (fun x => p ∣ x)
= (B.filter (fun a => ¬ p ∣ a)).image (fun a => L / a) := by
ext x
simp only [Finset.mem_filter, Finset.mem_image]
constructor
· rintro ⟨⟨a, ha, rfl⟩, h⟩
exact ⟨a, ⟨ha, (hiff a ha).mp h⟩, rfl⟩
· rintro ⟨a, ⟨ha, h⟩, rfl⟩
exact ⟨⟨a, ha, rfl⟩, (hiff a ha).mpr h⟩
rw [e]
exact Finset.card_image_of_injOn (hinj.mono (by
intro a ha
exact (Finset.mem_filter.mp (Finset.mem_coe.mp ha)).1))
· have e : (B.image (fun a => L / a)).filter (fun x => ¬ p ∣ x)
= (B.filter (fun a => p ∣ a)).image (fun a => L / a) := by
ext x
simp only [Finset.mem_filter, Finset.mem_image]
constructor
· rintro ⟨⟨a, ha, rfl⟩, h⟩
exact ⟨a, ⟨ha, by_contra (fun h' => h ((hiff a ha).mpr h'))⟩, rfl⟩
· rintro ⟨a, ⟨ha, h⟩, rfl⟩
exact ⟨⟨a, ha, rfl⟩, fun h' => (hiff a ha).mp h' h⟩
rw [e]
exact Finset.card_image_of_injOn (hinj.mono (by
intro a ha
exact (Finset.mem_filter.mp (Finset.mem_coe.mp ha)).1))
/-- A1. Card form: n = |B| ≤ (k+1)·p, M a positive common multiple of 1..k. Then fewer than
2M elements are multiples of p, or fewer than 2M are not. -/
theorem R2c.few_or_most_card (B : Finset ℕ) (p k M : ℕ) (h0 : 0 ∉ B) (hne : B.Nonempty)
(hp : p.Prime) (hM0 : 0 < M) (hM : ∀ m : ℕ, 0 < m → m ≤ k → m ∣ M)
(hk : B.card ≤ (k + 1) * p)
(hs : ∀ a ∈ B, ∀ b ∈ B, a < B.card * Nat.gcd a b) :
(B.filter (fun a => p ∣ a)).card < 2 * M ∨ (B.filter (fun b => ¬ p ∣ b)).card < 2 * M := by
have h := R2c.few_or_most B B.card p M h0 hne hp hM0 (by
intro m hm0 hmp
apply hM m hm0
by_contra hcon
push Not at hcon
have : (k + 1) * p ≤ m * p := Nat.mul_le_mul_right p hcon
omega) hs
have hsum : (B.filter (fun a => p ∣ a)).card + (B.filter (fun b => ¬ p ∣ b)).card = B.card := by
rw [← Finset.card_union_of_disjoint (Finset.disjoint_filter_filter_not B B (fun a => p ∣ a)),
Finset.filter_union_filter_not_eq]
rw [← hsum] at h
by_contra hcon
push Not at hcon
nlinarith [hcon.1, hcon.2, Nat.mul_le_mul hcon.1 hcon.2]
/-- A2. k = 2 (n ≤ 3p, n ≥ 9): at most two multiples of p, or at most two non-multiples. -/
theorem R2c.few_or_most_third (B : Finset ℕ) (p : ℕ) (h0 : 0 ∉ B)
(hp : p.Prime) (h9 : 9 ≤ B.card) (hk : B.card ≤ 3 * p)
(hs : ∀ a ∈ B, ∀ b ∈ B, a < B.card * Nat.gcd a b) :
(B.filter (fun a => p ∣ a)).card ≤ 2 ∨ (B.filter (fun b => ¬ p ∣ b)).card ≤ 2 := by
have hne : B.Nonempty := Finset.card_pos.mp (by omega)
have h := R2c.few_or_most B B.card p 2 h0 hne hp (by norm_num) (by
intro m hm0 hmp
have hm : m ≤ 2 := by
by_contra hcon
push Not at hcon
have : 3 * p ≤ m * p := Nat.mul_le_mul_right p hcon
omega
interval_cases m
· exact one_dvd 2
· exact dvd_rfl) hs
have hsum : (B.filter (fun a => p ∣ a)).card + (B.filter (fun b => ¬ p ∣ b)).card = B.card := by
rw [← Finset.card_union_of_disjoint (Finset.disjoint_filter_filter_not B B (fun a => p ∣ a)),
Finset.filter_union_filter_not_eq]
rw [← hsum] at h h9
by_contra hcon
push Not at hcon
obtain ⟨u, hu⟩ : ∃ u, (B.filter (fun a => p ∣ a)).card = u + 3 := ⟨_, (Nat.sub_add_cancel hcon.1).symm⟩
obtain ⟨v, hv⟩ : ∃ v, (B.filter (fun b => ¬ p ∣ b)).card = v + 3 := ⟨_, (Nat.sub_add_cancel hcon.2).symm⟩
rw [hu, hv] at h h9
nlinarith [Nat.zero_le (u * v)]
/-- B'. WLOG "few multiples". Fix n and a prime p. If every admissible B (hole hypotheses, p
divides an element, p² divides none) with at most n/2 multiples of p has a good pair, then every
admissible B has one. -/
theorem R2c.wlog_few (n p : ℕ) (hp : p.Prime)
(H : ∀ B : Finset ℕ, 0 ∉ B → B.Nonempty → B.card = n → B.gcd id = 1 →
(∀ a ∈ B, ∀ b ∈ B, a ≤ n * Nat.gcd a b) →
(∀ a ∈ B, ∀ q k : ℕ, q.Prime → q ^ k ∣ a → q ^ k < n) →
(∃ a ∈ B, p ∣ a) → (∀ a ∈ B, ¬ p ^ 2 ∣ a) →
2 * (B.filter (fun a => p ∣ a)).card ≤ n →
∃ a ∈ B, ∃ b ∈ B, n * Nat.gcd a b ≤ a) :
∀ B : Finset ℕ, 0 ∉ B → B.Nonempty → B.card = n → B.gcd id = 1 →
(∀ a ∈ B, ∀ b ∈ B, a ≤ n * Nat.gcd a b) →
(∀ a ∈ B, ∀ q k : ℕ, q.Prime → q ^ k ∣ a → q ^ k < n) →
(∃ a ∈ B, p ∣ a) → (∀ a ∈ B, ¬ p ^ 2 ∣ a) →
∃ a ∈ B, ∃ b ∈ B, n * Nat.gcd a b ≤ a := by
intro B h0 hne hcard hgcd hle hpp hex hsq
by_cases hfew : 2 * (B.filter (fun a => p ∣ a)).card ≤ n
· exact H B h0 hne hcard hgcd hle hpp hex hsq hfew
· obtain ⟨d1, d2, d3, d4, d5, d6, d7, d8⟩ := R2c.dual_package B n hne h0
obtain ⟨hiff, c1, c2⟩ := d8 p hp hex hsq
have hsum : (B.filter (fun a => p ∣ a)).card + (B.filter (fun b => ¬ p ∣ b)).card = B.card := by
rw [← Finset.card_union_of_disjoint (Finset.disjoint_filter_filter_not B B (fun a => p ∣ a)),
Finset.filter_union_filter_not_eq]
have hexb : ∃ b ∈ B, ¬ p ∣ b := by
by_contra h
push Not at h
have h1 : p ∣ B.gcd id := Finset.dvd_gcd (fun b hb => h b hb)
rw [hgcd] at h1
exact hp.one_lt.ne' (Nat.dvd_one.mp h1)
obtain ⟨b, hb, hpb⟩ := hexb
apply d7
apply H _ d3 d2 (d1.trans hcard) d4 (d6 hle)
· intro x hx q k hq hqx
obtain ⟨a, ha, hda⟩ := d5 x hx q k hq hqx
exact hpp a ha q k hq hda
· exact ⟨_, Finset.mem_image_of_mem _ hb, (hiff b hb).mpr hpb⟩
· intro x hx hpx
obtain ⟨a, ha, hda⟩ := d5 x hx p 2 hp hpx
exact hsq a ha hda
· rw [c1]; omegaUntrusted contributor text — an annex (D-31): an informal argument, not a proof.
Untrusted: annex (D-31), by t1001-402a, 2026-10-01T11:51:00Z, licence CC-BY-4.0. Rendered from targets/erdos-402/nodes/erdos-402--h3-v2--h1/annex/6a64518f9cd863c9abea3114b518f3172f4c73c6a187eb928b43db35f77c0002.md.
Large primes cannot divide an element of a strict counterexample (erdos-402--h3-v2--h1).
Setting. B is a set of n positive integers with gcd 1, and a ≤ n·gcd(a, b) for all a, b in B (the node's hypotheses). Suppose the conclusion fails; then every quotient is strictly small: a < n·gcd(a, b) for all a, b in B (if a = n·gcd(a, b) the pair (a, b) answers).
Claim. Under the strict inequality, no prime p with n ≤ 2p divides any element of B.
Proof. Let p be such a prime and suppose p divides some element. By the node's prime-power hypothesis p < n. Let B_p be the elements divisible by p and C the others; C is nonempty because gcd(B) = 1.
Step 1. For a in B_p and b in C, a = p·gcd(a, b). Indeed a / gcd(a, b) is a multiple of p (p does not divide gcd(a, b), which divides b), it is positive and below n ≤ 2p, so it is p.
Step 2. Hence for a in B_p the number d_a = a / p equals gcd(a, b) for every b in C, so d_a divides G = gcd(C). Write G = d_a·e_a and b = G·s_b. Then e_a = G·p / a, the map a ↦ e_a is injective on B_p, the map b ↦ s_b is injective on C, and b = gcd(a, b)·e_a·s_b. The strict inequality for the pair (b, a) gives e_a·s_b < n; also e_a·s_b > 0, and p does not divide e_a·s_b because it does not divide b.
Step 3 (counting). Let X = {e_a} and T = {s_b}, with u = |X| = |B_p| ≥ 1, v = |T| = |C| ≥ 1, u + v = n. A set of u distinct positive integers has an element ≥ u, so some x0 ≥ u and t0 ≥ v, and u·v ≤ x0·t0 < n = u + v. So u = 1 or v = 1. If u = 1, the n − 1 numbers x0·t (t in T) are distinct, lie in {1, …, n − 1} and avoid p, which lies in that range: n − 1 ≤ n − 2, absurd. If v = 1, the same with the n − 1 numbers x·t0. ∎
Remarks. (i) The hypothesis n ≤ 2p is used only in Step 1. (ii) In the extremal sets {1, …, n} and {L/1, …, L/n} (L = lcm(1..n)) a prime p in (n/2, n] divides exactly one element, respectively all but one; these are the cases u = 1 and v = 1, which survive only because there a quotient equals n. (iii) Bertrand's postulate gives a prime p with n/2 ≤ p < n for n ≥ 4, so the extremal sets always contain such a multiple: the remaining statement (the hole of the skeleton) is that B has a pair with a = n·gcd(a, b) or an element with a prime factor ≥ n/2. What is left to prove is therefore: a set of n ≥ 2 positive integers, gcd 1, all of whose prime factors are below n/2, has a quotient a / gcd(a, b) ≥ n. (iv) The next step in the same direction is primes in [n/3, n/2): there a / gcd(a, b) is p or 2p for a in B_p, b in C, and the two-block counting above becomes a three-way one. This is the direction of Szegedy's and Zaharescu's proofs for large n; it is not carried out here.
The skeleton submitted with this annex proves the Claim in Lean inside the assembly and leaves the single hole described in (iii), stated as a disjunction so that it keeps the parent's hypotheses (and its witness B = {1, …, 10}).
How to read this page
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).