TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)

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.

$\mathbb{Q}$ is countably infinite

Statement

$\mathbb{Q} \approx \mathbb{N}$ (Equinumerous sets, $A \approx B$ and $A \preceq B$ ): the rationals are countably infinite (Finite, countably infinite, countable, uncountable).

No choice principle is used. The one place where a reader expects a choice, "pick a representative $a/b$ of each rational", is exactly where Every rational has a positive-denominator representative applies: every rational has a representative with positive denominator, so the map $(a,b) \mapsto [(a,b)]$ defined on $\mathbb{Z} \times \mathbb{Z}_{>0}$ is already surjective onto $\mathbb{Q}$ , and countability follows from a surjection without ever selecting a representative. The same device handles $\mathbb{Z}$ , which is a surjective image of $\mathbb{N} \times \mathbb{N}$ by construction (The integers as equivalence classes of pairs of naturals).

Facts & Assumptions

Given: $\mathbb{Z} = (\mathbb{N} \times \mathbb{N})/\sim$ with quotient map $(a,b) \mapsto [(a,b)]$ (The integers as equivalence classes of pairs of naturals), and $\mathbb{Q}$ the set of classes $[(a,b)]$ of pairs of integers with $b \ne 0$ (The rationals as equivalence classes of pairs of integers). Write $\mathbb{Z}_{>0} = \{\, b \in \mathbb{Z} : b > 0 \,\}$ (Order on the integers).

[L1]

Finite, countably infinite, at most countable, uncountable (Finite, countably infinite, countable, uncountable).

[L2]

Bijections, injections, surjections, composition; $\approx$ and $\preceq$ (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A \preceq B$ ).

[L3]

A nonempty $X$ is at most countable iff there is a surjection $\mathbb{N} \to X$ ; and from such a surjection $s$ the map $x \mapsto \min\{\, k : s(k) = x \,\}$ is an injection $X \to \mathbb{N}$ (A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$ ).

[L4]

There is a bijection $\beta : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ ( $\mathbb{N} \times \mathbb{N} \approx \mathbb{N}$ ).

[L5]

A product of two at most countable sets is at most countable (A product of two at most countable sets is at most countable); a subset of an at most countable set is at most countable (Every subset of an at most countable set is at most countable).

[L6]

Every rational is $[(a,b)]$ for some integers $a$ and $b$ with $b > 0$ (Every rational has a positive-denominator representative).

[L7]

$\mathbb{N}$ embeds injectively in $\mathbb{Z}$ by $n \mapsto [(n,0)]$ (The naturals embed in the integers) and $\mathbb{Z}$ embeds injectively in $\mathbb{Q}$ by $k \mapsto [(k,1)]$ (The integers embed in the rationals).

[L8]

$\preceq$ in both directions gives $\approx$ (The Schröder-Bernstein theorem).

[L9]

The relation of Order on the integers is a total order on $\mathbb{Z}$ compatible with the ring structure (The integers form a totally ordered ring), and $\mathbb{Z}_{>0} \ne \varnothing$ : on representatives $0 < [(a,b)]$ holds exactly when $b < a$ in $\mathbb{N}$ (Order on the integers), and $0 < 1$ in $\mathbb{N}$ , since $1 = \sigma(0) \ne 0$ (The von Neumann naturals form a Peano system) while $0 < n$ for every nonzero natural $n$ (claim 4 of On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ ); so the integer $[(1,0)]$ is positive.

Proof

technique · direct

1.1

The quotient map $\pi : \mathbb{N} \times \mathbb{N} \to \mathbb{Z}$ , $\pi(a,b) = [(a,b)]$ , is surjective, since every integer is by definition such a class; hence $\pi \circ \beta : \mathbb{N} \to \mathbb{Z}$ is a surjection, and $\mathbb{Z} \ne \varnothing$ , so $\mathbb{Z}$ is at most countable by [L3].

givenL2L3L4

1.2

The composite $\iota : \mathbb{N} \to \mathbb{Q}$ , $n \mapsto [([(n,0)],1)]$ , of the two embeddings of [L7] is injective, so $\mathbb{N} \preceq \mathbb{Q}$ .

L2L7

2.1

$\mathbb{Z}_{>0}$ is a subset of $\mathbb{Z}$ , hence at most countable by [L5], and it is nonempty by [L9]; therefore $\mathbb{Z} \times \mathbb{Z}_{>0}$ is at most countable by [L5] and nonempty, so [L3] provides a surjection $u : \mathbb{N} \to \mathbb{Z} \times \mathbb{Z}_{>0}$ .

step 1.1L3L5L9

3.1

The map $\rho : \mathbb{Z} \times \mathbb{Z}_{>0} \to \mathbb{Q}$ , $\rho(a,b) = [(a,b)]$ , is well defined because $b > 0$ gives $b \ne 0$ , and it is surjective by [L6]; hence $\rho \circ u : \mathbb{N} \to \mathbb{Q}$ is a surjection, $\mathbb{Q}$ is at most countable, and [L3] turns that surjection into an injection $j : \mathbb{Q} \to \mathbb{N}$ , so $\mathbb{Q} \preceq \mathbb{N}$ .

step 2.1givenL2L3L6

4.1

From $\mathbb{N} \preceq \mathbb{Q}$ and $\mathbb{Q} \preceq \mathbb{N}$ , the Schröder-Bernstein theorem [L8] yields a bijection $\mathbb{Q} \to \mathbb{N}$ ; hence $\mathbb{Q} \approx \mathbb{N}$ and $\mathbb{Q}$ is countably infinite.

step 1.2step 3.1L1L8∎

Remarks

Why Schröder-Bernstein rather than a count. The usual last line is "countable, and infinite because $\mathbb{N}$ injects into it". Turning that into a proof requires knowing that a set containing an injective copy of $\mathbb{N}$ is not finite, which is the pigeonhole principle, The pigeonhole principle on $\mathbb{N}$ , proved earlier on this page. That route is now available, but it is a detour: The Schröder-Bernstein theorem gets the bijection directly from the two injections already in hand, and it is choice free, so nothing is lost.
Lowest terms are not needed and are not available. A frequent presentation injects $\mathbb{Q}$ into $\mathbb{Z} \times \mathbb{N}$ by sending each rational to its representative in lowest terms. That map needs greatest common divisors, which are not available at this point in the reading order; they are developed later on the divisibility-and-GCD page. Working with a surjection instead of an injection avoids that later dependency. Working with a surjection instead of an injection avoids the issue entirely: repetitions in an enumeration are harmless (A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$ ).
The proof shows in passing that $\mathbb{Z} \approx \mathbb{N}$ , by the same two-injection argument applied to [L7] and step 1.1, and that $\mathbb{Q} \times \mathbb{Q}$ , $\mathbb{Q}^3$ and so on are countable (A product of two at most countable sets is at most countable). The contrast with $\mathbb{R}$ is uncountable (Cantor's nested intervals, 1874) is the point of the page: adding all limits of rational approximations to $\mathbb{Q}$ changes the size of the set, not merely its arithmetic.

Depends on

Used by

…and 5 more results.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 67 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)
J. Lebl, Basic Analysis: Introduction to Real Analysis, basic set theory (standard reference, not scraped)
Countable set (Wikipedia) (standard reference, not scraped)
Rational number (Wikipedia) (standard reference, not scraped)
T. Tao, Analysis I, 3rd ed., §8.1 (standard reference, not scraped)

Q\mathbb{Q}Q is countably infinite