Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-26
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

(n+1) Cn=(2nn)

Statement

For every n∈N, in N,

(n+1) Cn=(2nn).

Facts & Assumptions

Given: a natural number n.

[F1]

Cn+(2nn+1)=(2nn) in N (Cn+(2nn+1)=(2nn)).

[L2]

m!≠0 for every m∈N, and σ(m)!=m!⋅σ(m) (The factorial n! and the falling factorial nk‾, defined by recursion in N).

[L4]

For all x,y,k∈N with k≠0: if x⋅k=y⋅k then x=y (Cancellation for multiplication by a nonzero factor).

[L5]

For all x,y,k∈N: if x+k=y+k then x=y (Addition is cancellative).

Proof

technique · direct
1.1L1L2L3L4algebra

First, (n+1)(2nn+1)=n(2nn) in N. For n=0 both sides are 0, since (01)=0 by [L3]. For n≥1 one has n+1≤2n and 2n−(n+1)=n−1, so [L1] gives (2nn+1) (n+1)! (n−1)!=(2n)! and (2nn) n! n!=(2n)!; writing (n+1)!=(n+1)⋅n! and the second factor n!=n⋅(n−1)! by [L2], the two left sides read (n+1)(2nn+1)⋅n! (n−1)! and n(2nn)⋅n! (n−1)!, and cancelling the nonzero factor n! (n−1)! by [L2] and [L4] gives the identity.

2.1F1L3L5step 1.1algebra∎

Multiply [F1] by n+1: (n+1)Cn+(n+1)(2nn+1)=(n+1)(2nn). By step 1.1 the second summand on the left is n(2nn), and the right-hand side is n(2nn)+(2nn), so cancelling the common summand n(2nn) by [L5] gives (n+1)Cn=(2nn). At n=0 this reads C0=(00)=1.

Remarks

  • The quotient form. The identity is an identity of natural numbers. Reading each natural number as its canonical natural in R (The canonical natural ι(n)=n⋅1F of a field) and dividing by the nonzero real n+1 turns it into the familiar Cn=1n+1(2nn). The multiplicative form is the one proved, and it is the form in which no division and no embedding is needed; it also says at once that n+1 divides the central binomial coefficient, which the quotient form presupposes.

  • What the proof actually uses. Only the reflection identity and factorial bookkeeping. The Catalan number is never manipulated as a formula: it enters as the count it was defined to be and leaves as a factor of a binomial coefficient.

Depends on

Used by

Dependency tree · two levels

37 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources