CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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.

A rational root of $x^{k} = m$ is an integer: if $k \geq 1$ , $m \in Z$ , $x \in Q$ and $x^{k}$ is the image of $m$ , then $x$ is the image of an integer

Statement

$Q$ is a field (The rationals form a field, Field), so $(Q, \cdot, 1)$ is a commutative monoid and natural powers $x^{k}$ are defined in it by Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ . Write $j : Z \to Q$ , $j (u) = [(u, 1)]$ , for the embedding of The integers embed in the rationals.

Let $k \in N$ with $k \geq 1$ , let $m \in Z$ , and let $x \in Q$ satisfy

$x^{k} = j (m) .$

Then $x = j (z)$ for some $z \in Z$ .

Facts & Assumptions

Given: $k \in N$ with $k \geq 1$ , $m \in Z$ , and $x \in Q$ with $x^{k} = j (m)$ .

[L1]

A rational is a class $[(u, w)]$ with $u, w \in Z$ , $w \neq 0$ , and $[(u, w)] = [(u^{'}, w^{'})]$ exactly when $u w^{'} = u^{'} w$ (The rationals as equivalence classes of pairs of integers).

[L2]

$[(u, w)] \cdot [(u^{'}, w^{'})] = [(u u^{'}, w w^{'})]$ , $0 = [(0, 1)]$ , $1 = [(1, 1)]$ , and $[(u, w)] \neq 0$ exactly when $u \neq 0$ (Arithmetic on the rationals).

[L3]

$Q$ is a field: multiplication is associative and commutative on all of $Q$ with $y \cdot 1 = y$ and $y \cdot 0 = 0$ (The rationals form a field, Field), so $(Q, \cdot, 1)$ is a commutative monoid (Semigroup and monoid).

[L4]

$g^{0} = e$ and $g^{σ (t)} = g^{t} \cdot g$ in a monoid (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ ).

[L5]

$j (u) = [(u, 1)]$ is injective and preserves addition and multiplication (The integers embed in the rationals).

[L6]

For $d : = \gcd (u, w) \neq 0$ there are unique $u / d$ and $w / d$ with $u = d (u / d)$ , $w = d (w / d)$ , and $\gcd (u / d, w / d) = 1$ (If $d = \gcd (a, b)$ is nonzero then $a / d$ and $b / d$ are coprime, Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ , Coprime integers: $\gcd (a, b) = 1$ ).

[L7]

$\gcd (u, w) \geq 1$ unless $u = w = 0$ ( $\gcd$ is symmetric and unchanged by signs: $\gcd (a, b) = \gcd (b, a) = \gcd (∣ a ∣, ∣ b ∣)$ ; moreover $\gcd (a, 0) = ∣ a ∣$ , $\gcd (a, 1) = 1$ , $\gcd (a, a) = ∣ a ∣$ , and $\gcd (a, b) \geq 1$ unless $a = b = 0$ , Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ).

[L8]

If $\gcd (u, w) = 1$ then the set of common divisors of $u$ and $w$ is exactly ${1, - 1}$ ( $a$ and $b$ are coprime if and only if $a x + b y = 1$ for some integers $x, y$ ; and in that case the only common divisors of $a$ and $b$ are $1$ and $- 1$ , $(Z, \cdot, 1)$ is a commutative monoid whose group of units is ${1, - 1}$ ; equivalently $u ∣ 1$ holds exactly for $u = 1$ and $u = - 1$ ).

[L9]

If $q$ is prime and $q ∣ u v$ then $q ∣ u$ or $q ∣ v$ (Euclid's lemma: if $p$ is prime and $p ∣ a b$ then $p ∣ a$ or $p ∣ b$ ).

[L10]

Every integer $> 1$ has a prime divisor, and every prime $q$ satisfies $q > 1$ (Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime, Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L11]

Divisibility is reflexive and transitive, $d ∣ u$ implies $d ∣ u c$ , and $d ∣ u$ means $u = d c$ for some $c$ (Divisibility is reflexive and transitive on $Z$ , and is linear: if $d ∣ a$ and $d ∣ b$ then $d ∣ a x + b y$ for all integers $x, y$ ; also $d ∣ a$ implies $d ∣ a c$ , $- d ∣ a$ and $d ∣ - a$ , Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L12]

Induction on $N$ (The principle of mathematical induction); every natural $\neq 0$ is a successor (Every nonzero natural number is a successor); $m < n$ exactly when $σ (m) \leq n$ , and $1 = σ (0)$ (Discreteness: $σ (n)$ is the immediate successor, The natural numbers $N$ (von Neumann), Order on the natural numbers).

[L14]

$u ∣ 1$ exactly when $u = 1$ or $u = - 1$ ( $(Z, \cdot, 1)$ is a commutative monoid whose group of units is ${1, - 1}$ ; equivalently $u ∣ 1$ holds exactly for $u = 1$ and $u = - 1$ ).

[L13]

A product of two nonzero integers is nonzero (The integers have no zero divisors; multiplicative cancellation); $Z$ is a commutative ring whose order is total, antisymmetric and transitive (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals, The integers form a totally ordered ring, Order on the integers); $ι : N \to Z$ is injective and order preserving with image the nonnegative integers (The naturals embed in the integers).

Proof

technique · direct

1.1

$0 < 1$ in $Z$ , and every integer $y > 0$ satisfies $y \geq 1$ : $y = ι (t)$ with $t \neq 0$ , so $1 = σ (0) \leq t$ and $ι$ preserves the order.

L12L13

1.2

For integers $u, w$ with $w \neq 0$ and every $t \in N$ : $w^{t} \neq 0$ and $[(u, w)]^{t} = [(u^{t}, w^{t})]$ , powers on the left in $Q$ and on the right in $Z$ . The set of $t$ for which this holds contains $0$ , since $w^{0} = 1 \neq 0$ and $[(u, w)]^{0} = 1 = [(1, 1)] = [(u^{0}, w^{0})]$ ; and if it holds at $t$ then $w^{σ (t)} = w^{t} w \neq 0$ and $[(u, w)]^{σ (t)} = [(u^{t}, w^{t})] \cdot [(u, w)] = [(u^{t} u, w^{t} w)] = [(u^{σ (t)}, w^{σ (t)})]$ . Induction finishes it.

L1L2L4L12L13

1.3

Suppose first $x = 0$ . Since $k \geq 1$ , write $k = σ (t)$ ; then $x^{k} = x^{t} \cdot 0 = 0 = j (0)$ , so $j (m) = j (0)$ and $m = 0$ by injectivity of $j$ ; and $x = 0 = j (0)$ is the image of an integer.

L3L4L5L12

1.4

Suppose instead $x \neq 0$ , and write $x = [(a, b)]$ with $b \neq 0$ ; then $a \neq 0$ . If $b < 0$ , replace $(a, b)$ by $(- a, - b)$ , which represents the same rational because $a (- b) = (- a) b$ ; so we may assume $b > 0$ .

L1L2L13choose

2.1

For a prime $q$ , an integer $u$ and $t \geq 1$ : if $q ∣ u^{t}$ then $q ∣ u$ . Let $S$ be the set of $t$ for which this implication holds; $0 \in S$ vacuously, since $t \geq 1$ fails there. Suppose $t \in S$ and $q ∣ u^{σ (t)} = u^{t} u$ . By [L9] either $q ∣ u^{t}$ or $q ∣ u$ ; in the second case we are done, and in the first, if $t \geq 1$ then $t \in S$ gives $q ∣ u$ , while if $t = 0$ then $u^{t} = 1$ and $q ∣ 1$ is impossible for a prime, since $q > 1 > 0 > - 1$ would then be contradicted. So $σ (t) \in S$ and $S = N$ .

step 1.1L4L9L10L12L13L14

2.2

Put $d : = \gcd (a, b)$ ; since $a \neq 0$ we have $d \geq 1 > 0$ , so $d \neq 0$ . Put $a_{1} : = a / d$ and $b_{1} : = b / d$ , so that $a = d a_{1}$ , $b = d b_{1}$ and $\gcd (a_{1}, b_{1}) = 1$ .

step 1.1step 1.4L6L7L13

3.1

$a_{1} \neq 0$ and $b_{1} > 0$ : if $a_{1} = 0$ then $a = 0$ , and if $b_{1} \leq 0$ then $b = d b_{1} \leq 0$ , both contrary to step 1.4. Moreover $[(a, b)] = [(a_{1}, b_{1})]$ , because $a b_{1} = (d a_{1}) b_{1} = a_{1} (d b_{1}) = a_{1} b$ .

step 1.4step 2.2L1L13

4.1

By step 1.2, $x^{k} = [(a_{1}, b_{1})]^{k} = [(a_{1}^{k}, b_{1}^{k})]$ , and this equals $j (m) = [(m, 1)]$ , so $a_{1}^{k} \cdot 1 = m b_{1}^{k}$ , that is $a_{1}^{k} = m b_{1}^{k}$ .

step 1.2step 3.1L1L5L13

5.1

Suppose $b_{1} > 1$ and fix a prime $q$ with $q ∣ b_{1}$ . Since $k \geq 1$ , write $k = σ (t)$ ; then $b_{1}^{k} = b_{1}^{t} b_{1}$ , so $b_{1} ∣ b_{1}^{k}$ and hence $q ∣ b_{1}^{k}$ by transitivity. Then $q ∣ m b_{1}^{k} = a_{1}^{k}$ , so $q ∣ a_{1}$ by step 2.1.

step 2.1step 4.1L4L10L11L12

6.1

So $q$ is a common divisor of $a_{1}$ and $b_{1}$ , which are coprime, hence $q = 1$ or $q = - 1$ by [L8] and [L14]; but $q > 1 > 0 > - 1$ , a contradiction. Therefore $b_{1} \leq 1$ , and $b_{1} > 0$ gives $b_{1} \geq 1$ , so $b_{1} = 1$ .

step 1.1step 2.2step 3.1step 5.1L8L10L13L14

7.1

Hence $x = [(a_{1}, 1)] = j (a_{1})$ is the image of an integer; together with step 1.3 this covers both cases.

step 1.3step 3.1step 6.1L5∎

Remarks

The instances live on the companion page. No rational squares to $3$ or to $6$ , and none cubes to $2$ : each is this corollary followed by ruling out the finitely many integer candidates by size, and all three are worked out in No rational squares to $3$ or to $6$ , and none cubes to $2$ : three instances of the rational-root corollary ↗.
The argument lives inside $Q$ and never enters $R$ . No $n$ -th root is asserted to exist; the hypothesis is that a rational $x$ already satisfies $x^{k} = j (m)$ , and the conclusion is about its denominator. The powers are monoid powers of Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ in $(Q, \cdot, 1)$ , not Integer powers $a^{m}$ , which is stated in the ambient ordered field.
This is a second route to a fact the library already had. The published FALSE: some rational number squares to 2 refutes "some rational number squares to $2$ " by parity alone, on the construction pages, long before primes existed here. The case $k = 2$ , $m = 2$ of this corollary gives the same conclusion by a different argument, and the two agree: a rational squaring to $2$ would have to be an integer $z$ with $z^{2} = 2$ , and $1 < 2 < 4$ leaves no candidate.
Where primality is used. Exactly once, in step 2.1, through Euclid's lemma: if $p$ is prime and $p ∣ a b$ then $p ∣ a$ or $p ∣ b$ : a prime dividing a power divides the base. For a composite divisor the step fails, which is why the classical proof cannot be run with an arbitrary common factor in place of a prime.

Depends on

Used by

No rational squares to 3 or to 6, and none cubes to 2: three instances of the rational-root corollary Example

Dependency tree · two levels

73 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

Rational root theorem (Wikipedia) (standard reference, not scraped)
University of Toronto MAT 246 solutions: Rational roots (standard reference, not scraped)

A rational root of xk=mxk=m is an integer: if k≥1k≥1, m∈Zm∈Z, x∈Qx∈Q and xkxk is the image of mm, then xx is the image of an integer