Equations in central binomial coefficients

TheoremAllen's theorem on central binomial products#●ready to prove

Let \(x\) and \(b\) be positive integers and let \(a\) be a nonnegative integer. Then \(\binom{2(a+b)}{a+b} = \binom{2a}{a}\binom{x+2b}{b}\) if and only if \(x = 1\) and \(a = 1\).

public theorem_wanted centralBinom_add_eq_centralBinom_mul_choose_iff (x a b : ℕ) (hx : 0 < x)
    (hb : 0 < b) :
    (a + b).centralBinom = a.centralBinom * (x + 2 * b).choose b ↔ x = 1 ∧ a = 1
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Theorem 1.

TheoremAllen's inequality for central binomial products#●ready to prove

Let \(x\) and \(b\) be positive integers and let \(a\) be a nonnegative integer with \(a \le x\). Then \(\binom{2(a+b)}{a+b} \le \binom{2a}{a}\binom{x+2b}{b}\), and equality holds if and only if \(x = 1\) and \(a = 1\).

public theorem_wanted centralBinom_add_le_centralBinom_mul_choose_of_le (x a b : ℕ) (hx : 0 < x)
    (hb : 0 < b) (hax : a ≤ x) :
    (a + b).centralBinom ≤ a.centralBinom * (x + 2 * b).choose b ∧
      ((a + b).centralBinom = a.centralBinom * (x + 2 * b).choose b ↔ x = 1 ∧ a = 1)
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Proposition 1.

TheoremCentral binomial products with \(a + b \le 10\)#●ready to prove

Let \(x\), \(a\), \(b\) be positive integers with \(a + b \le 10\). Then \(\binom{2(a+b)}{a+b} = \binom{2a}{a}\binom{x+2b}{b}\) if and only if \(x = 1\) and \(a = 1\).

public theorem_wanted centralBinom_add_eq_centralBinom_mul_choose_iff_of_le_ten (x a b : ℕ)
    (hx : 0 < x) (ha : 0 < a) (hb : 0 < b) (hk : a + b ≤ 10) :
    (a + b).centralBinom = a.centralBinom * (x + 2 * b).choose b ↔ x = 1 ∧ a = 1
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 1.

TheoremCentral binomial products in the case \(x = a - 1\)#●ready to prove

Let \(a\) and \(b\) be natural numbers with \(4 < 2a \le a + b\). Then \(\binom{2(a+b)}{a+b} \ne \binom{2a}{a}\binom{a+2b-1}{b}\), so the equation \(\binom{2(a+b)}{a+b} = \binom{2a}{a}\binom{x+2b}{b}\) has no solution with \(x = a - 1\).

public theorem_wanted centralBinom_add_ne_centralBinom_mul_choose_sub_one (a b : ℕ)
    (ha : 4 < 2 * a) (hab : 2 * a ≤ a + b) :
    (a + b).centralBinom ≠ a.centralBinom * (a + 2 * b - 1).choose b
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 2.

TheoremCentral binomial products in the case \(x = a - 2\)#●ready to prove

Let \(a\) and \(b\) be natural numbers with \(4 < 2a \le a + b\). Then \(\binom{2(a+b)}{a+b} \ne \binom{2a}{a}\binom{a+2b-2}{b}\), so the equation \(\binom{2(a+b)}{a+b} = \binom{2a}{a}\binom{x+2b}{b}\) has no solution with \(x = a - 2\).

public theorem_wanted centralBinom_add_ne_centralBinom_mul_choose_sub_two (a b : ℕ)
    (ha : 4 < 2 * a) (hab : 2 * a ≤ a + b) :
    (a + b).centralBinom ≠ a.centralBinom * (a + 2 * b - 2).choose b
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 3.

TheoremCentral binomial products in the case \(x = a - 3\)#●ready to prove

Let \(a\) and \(b\) be natural numbers with \(4 < 2a \le a + b\). Then \(\binom{2(a+b)}{a+b} \ne \binom{2a}{a}\binom{a+2b-3}{b}\), so the equation \(\binom{2(a+b)}{a+b} = \binom{2a}{a}\binom{x+2b}{b}\) has no solution with \(x = a - 3\).

public theorem_wanted centralBinom_add_ne_centralBinom_mul_choose_sub_three (a b : ℕ)
    (ha : 4 < 2 * a) (hab : 2 * a ≤ a + b) :
    (a + b).centralBinom ≠ a.centralBinom * (a + 2 * b - 3).choose b
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 4.

TheoremHanson's theorem on a prime factor above \(3m/2\) in consecutive integers#●ready to prove

Let \(m\) and \(n\) be natural numbers with \(0 < m < n\). The product \(n(n+1)\cdots(n+m-1)\) has a prime divisor \(p\) with \(p > 3m/2\) if and only if \((n, m)\) is none of the pairs \((3, 2)\), \((8, 2)\) and \((6, 5)\) (the products \(3 \cdot 4\), \(8 \cdot 9\) and \(6 \cdot 7 \cdot 8 \cdot 9 \cdot 10\)).

public theorem_wanted exists_prime_dvd_prod_consecutive_gt_three_halves_iff (n m : ℕ)
    (hm : 0 < m) (hmn : m < n) :
    (∃ p, p.Prime ∧ p ∣ ∏ i ∈ range m, (n + i) ∧ 3 * m < 2 * p) ↔
      (n, m) ≠ (3, 2) ∧ (n, m) ≠ (8, 2) ∧ (n, m) ≠ (6, 5)
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 5, quoting Hanson.

TheoremStănică's bounds for the binomial coefficient \(\binom{mn}{rn}\)#●ready to prove

Let \(m\), \(n\) and \(r\) be natural numbers with \(1 \le r < m\) and \(n \ge 1\), and put

\[B = \frac{m^{mn + 1/2}}{(m-r)^{(m-r)n + 1/2}\, r^{rn + 1/2}}.\]

Then

\[\frac{e^{-1/(8n)}}{\sqrt{2\pi}\,\sqrt{n}}\, B < \binom{mn}{rn} < \frac{1}{\sqrt{2\pi}\,\sqrt{n}}\, B.\]
public theorem_wanted choose_mul_mul_bounds (m n r : ℕ) (hr : 1 ≤ r) (hrm : r < m)
    (hn : 1 ≤ n) :
    Real.exp (-(1 / (8 * (n : ℝ)))) / (Real.sqrt (2 * Real.pi) * Real.sqrt n) *
          ((m : ℝ) ^ (m * n) * Real.sqrt m /
            (((m - r : ℕ) : ℝ) ^ ((m - r) * n) * Real.sqrt ((m - r : ℕ) : ℝ) *
              ((r : ℝ) ^ (r * n) * Real.sqrt r))) <
        ((m * n).choose (r * n) : ℝ) ∧
      ((m * n).choose (r * n) : ℝ) <
        1 / (Real.sqrt (2 * Real.pi) * Real.sqrt n) *
          ((m : ℝ) ^ (m * n) * Real.sqrt m /
            (((m - r : ℕ) : ℝ) ^ ((m - r) * n) * Real.sqrt ((m - r : ℕ) : ℝ) *
              ((r : ℝ) ^ (r * n) * Real.sqrt r)))
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 6, quoting Stănică.

TheoremCentral binomial products with \(a \ge b \ge 3\)#●ready to prove

Let \(x\), \(a\), \(b\) be natural numbers with \(x \ge 1\) and \(3 \le b \le a\). Then \(\binom{2(a+b)}{a+b} \ne \binom{2a}{a}\binom{x+2b}{b}\).

public theorem_wanted centralBinom_add_ne_of_half_le_of_three_le (x a b : ℕ) (hx : 0 < x)
    (hab : a + b ≤ 2 * a) (hb : 3 ≤ b) :
    (a + b).centralBinom ≠ a.centralBinom * (x + 2 * b).choose b
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 7.

TheoremCentral binomial products with \(x \ge 2\) and \(a \ge b\)#●ready to prove

Let \(x\), \(a\), \(b\) be natural numbers with \(x \ge 2\) and \(1 \le b \le a\). Then \(\binom{2(a+b)}{a+b} \ne \binom{2a}{a}\binom{x+2b}{b}\).

public theorem_wanted centralBinom_add_ne_of_half_le_of_two_le (x a b : ℕ) (hx : 2 ≤ x)
    (hb : 0 < b) (hab : a + b ≤ 2 * a) :
    (a + b).centralBinom ≠ a.centralBinom * (x + 2 * b).choose b
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 8.

TheoremA prime factor above \(9m/5\) in a product of consecutive integers#●ready to prove

Let \(m\) and \(n\) be natural numbers with \(2 < m < n\) and \(n + m \ge 150\). Then the product \(n(n+1)\cdots(n+m-1)\) has a prime divisor \(p\) with \(p > 9m/5\).

public theorem_wanted exists_prime_dvd_prod_consecutive_gt_nine_fifths (n m : ℕ) (hm : 2 < m)
    (hmn : m < n) (h150 : 150 ≤ n + m) :
    ∃ p, p.Prime ∧ p ∣ ∏ i ∈ range m, (n + i) ∧ 9 * m < 5 * p
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 9, quoting Shanta and Shorey.

TheoremA prime factor above \(4.42m\) in a product of consecutive integers#●ready to prove

Let \(m\) and \(n\) be natural numbers with \(m > 3\), \(n > 4m\) and \(n + m \ge 150\). Then the product \(n(n+1)\cdots(n+m-1)\) has a prime divisor \(p\) with \(p > 4.42\,m\).

public theorem_wanted exists_prime_dvd_prod_consecutive_gt_four_point_four_two (n m : ℕ)
    (hm : 3 < m) (hmn : 4 * m < n) (h150 : 150 ≤ n + m) :
    ∃ p, p.Prime ∧ p ∣ ∏ i ∈ range m, (n + i) ∧ 442 * m < 100 * p
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 10, quoting Nair and Shorey.

TheoremCentral binomial products in the balanced range#●ready to prove

Let \(a\) and \(b\) be positive integers, let \(x \ge 2\) be an integer, and put \(k = a + b\). If \(k \ge 75\), \(a \le \tfrac{9}{10}k\) and \(b \le \tfrac{4}{5}k\), then \(\binom{2k}{k} \ne \binom{2a}{a}\binom{x+2b}{b}\).

public theorem_wanted centralBinom_add_ne_of_balanced (x a b : ℕ) (hx : 2 ≤ x) (ha : 0 < a)
    (hb : 0 < b) (hk : 75 ≤ a + b) (ha9 : 10 * a ≤ 9 * (a + b)) (hb8 : 5 * b ≤ 4 * (a + b)) :
    (a + b).centralBinom ≠ a.centralBinom * (x + 2 * b).choose b
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 11.

TheoremNo large solutions of the central binomial product equation with a dominant central factor#●ready to prove

For natural numbers \(a\), \(b\), \(x\) with \(b \ge 1\), \(x \ge 2\), \(a + b \ge 150\) and \(a \ge \frac{171}{121} x\), we have \(\binom{2(a+b)}{a+b} \ne \binom{2a}{a}\binom{x+2b}{b}\).

public theorem_wanted centralBinom_add_ne_of_large_a (x a b : ℕ) (hx : 2 ≤ x) (hb : 0 < b)
    (hk : 150 ≤ a + b) (ha : 171 * x ≤ 121 * a) :
    (a + b).centralBinom ≠ a.centralBinom * (x + 2 * b).choose b
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Lemma 12.

TheoremCentral binomial products with \(x = 1\)#●ready to prove

Let \(a\) and \(b\) be positive integers. Then \(\binom{2(a+b)}{a+b} = \binom{2a}{a}\binom{1+2b}{b}\) if and only if \(a = 1\).

public theorem_wanted centralBinom_add_eq_centralBinom_mul_choose_one_iff (a b : ℕ) (ha : 0 < a)
    (hb : 0 < b) :
    (a + b).centralBinom = a.centralBinom * (1 + 2 * b).choose b ↔ a = 1
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Proposition 2.

TheoremNo large solutions of the central binomial product equation with shift at least two#●ready to prove

For natural numbers \(a\), \(b\), \(x\) with \(a \ge 1\), \(b \ge 1\), \(x \ge 2\) and \(a + b \ge 150\), we have \(\binom{2(a+b)}{a+b} \ne \binom{2a}{a}\binom{x+2b}{b}\).

public theorem_wanted centralBinom_add_ne_of_two_le_of_large (x a b : ℕ) (hx : 2 ≤ x)
    (ha : 0 < a) (hb : 0 < b) (hk : 150 ≤ a + b) :
    (a + b).centralBinom ≠ a.centralBinom * (x + 2 * b).choose b
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Proposition 3.

TheoremCentral binomial products with \(x \ge 2\) and \(a + b < 150\)#●ready to prove

Let \(x\), \(a\), \(b\) be natural numbers with \(a \ge 1\), \(b \ge 1\), \(x \ge 2\) and \(x < a + b < 150\). Then \(\binom{2(a+b)}{a+b} \ne \binom{2a}{a}\binom{x+2b}{b}\).

public theorem_wanted centralBinom_add_ne_of_two_le_of_small (x a b : ℕ) (hx : 2 ≤ x)
    (ha : 0 < a) (hb : 0 < b) (hxk : x < a + b) (hk : a + b < 150) :
    (a + b).centralBinom ≠ a.centralBinom * (x + 2 * b).choose b
Sources
  • Meaghan Allen, Solvability of \(\binom{2k}{k} = \binom{2a}{a}\binom{x+2b}{b}\), INTEGERS 26 (2026), Article A26, Proposition 4.
17 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.