Prime natural numbers: proving 97 prime and 91 composite, and excluding 0 and 1

Goal and scope

From the MKO's definition (p is prime ⇔ 2≤p and every natural divisor d of p satisfies d=1 or d=p): (1) explain why 0 and 1 are not prime; (2) prove that 2 is prime; (3) prove that 91 is composite with the witness 7, and show that testing only 2, 3, 5 misjudges it; (4) prove 'if n=dk with d, k≥2 then min(d,k)²≤n', and use it to prove that 97 is prime by checking only 2 to 9; (5) prove that 2 is the only even prime.

Works in the natural numbers including 0, with natural divisibility and exact integer comparisons (MKO assumptions a1 and a2), never a floating-point square root. The square-root bound comes from a lemma proved here. Uniqueness of prime factorization, the infinitude of primes and primality certificates for large integers are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• order_basics
• division_algorithm
• mul_zero
• numeric_evaluation

• G1 — p and d are natural numbers including 0; divisibility follows the natural-divisibility MKO, with natural witnesses (MKO assumption a1).
• G2 — Factors are checked with natural divisibility and exact integer comparisons, not approximate square roots or floating-point division (MKO assumption a2).
• G3 — Candidates: 0, 1, 2, 91, 97, and even numbers greater than 2.

• p — the candidate natural number
• d\mid p — d divides p
• m=\min(d,k) — the smaller member of a factor pair
• n\bmod m — the remainder of n on division by m

Rules and sources

• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• mko_prime_def · cited — A natural number p is prime exactly when 2≤p and every natural divisor d of p satisfies d=1 or d=p. Neither 0 nor 1 is prime. · mko-prime-number
• mko_dvd_def · cited — For natural numbers a and b, a∣b exactly when there is a natural number k such that b=a·k. · mko-natural-divisibility
• rem_test · prerequisite — For a natural n and a positive natural m: m∣n ⇔ n leaves remainder 0 on division by m (a consequence of uniqueness in the division algorithm).
• L_div_bound · lemma — If d∣n with n>0 and n=dk, then d≥1, k≥1 and d≤n.
• L_small_factor · lemma — If n=d·k with d≥2 and k≥2, then m=min(d,k) satisfies 2≤m, m∣n and m²≤n.

Main derivation

p\ \text{prime}

2\le p\ \land\ \forall d\in\mathbb{N}\,(d\mid p\Rightarrow d=1\lor d=p)

d\mid n,\ n>0

1\le d\le n

p=0,\ p=1

0,\ 1\ \text{not prime}

p=2

2\ \text{prime}

91=7\cdot 13

7\mid 91,\ 7\notin\{1,91\};\ 91\ \text{not prime}

91\bmod 2=91\bmod 3=91\bmod 5=1

2,3,5\nmid 91,\ \text{yet}\ 91\ \text{is composite}

d\mid 97,\ d\neq 1,\ d\neq 97

97=dk,\ 2\le d\le 96,\ k\ge 2

97=dk,\ d\ge 2,\ k\ge 2

m=\min(d,k):\ 2\le m,\ m\mid 97,\ m^2\le 97

m^2\le 97

2\le m\le 9

m\in\{2,3,4,5,6,7,8,9\}

97\bmod m\in\{1,1,1,2,1,6,1,7\}\neq 0,\ \text{so}\ m\nmid 97

\text{assumption of S07 leads to a contradiction}

\forall d\,(d\mid 97\Rightarrow d=1\lor d=97);\ 97\ \text{prime}

91,\ 9^2\le 91<10^2

\text{the complete search}\ 2\le m\le 9\ \text{finds}\ 7

p=2j,\ p\ge 2,\ p\neq 2

2\mid p,\ 2\notin\{1,p\};\ p\ \text{not prime}

Substeps and lemmas

n=dk,\ n>0

d\ge 1,\ k\ge 1

k\ge 1,\ d\ge 0

n=dk\ge d\cdot 1=d

n=dk

d\mid n,\ k\mid n,\ \text{so}\ m\mid n

m\le d,\ m\le k,\ m\ge 0

m^2=m\cdot m\le d\cdot m\le d\cdot k=n

Reverse audits

• S13 · premise_audit · S01, S04, mko_dvd_def — The general argument holds for every even p≠2; the finite check N21 is not part of the proof.
• S12 · premise_audit · S05, L_small_factor — The lemma guarantees a divisor within the bound for a composite number; this step only contrasts a complete search with a partial one.
• S11 · sufficient_goal_reduction · S07, S10, contradiction, mko_prime_def — Goal G: 97 is prime. Sufficient condition H: 97≥2 and no nontrivial divisor; H⇒G by the definition. H is proved by contradiction, without using G as a premise; N15 is only a cross-check, not part of the proof.
• S10 · premise_audit · S09, rem_test, case_analysis — The eight cases exhaust every m with 2≤m≤9; this is a complete check, not a sample.
• S09 · premise_audit · S08, order_basics, G2 — The bound must cover every m with m²≤97; 9 is neither too small nor too large.
• S08.2 · premise_audit · order_basics — Multiplying by a nonnegative number preserves ≤; the lemma itself is not used.
• S08.1 · premise_audit · mko_dvd_def, mul_comm, exists_intro — Only commutativity and witnesses are used; the lemma itself is not used.
• S08 · premise_audit · S07, L_small_factor — The lemma needs d and k both at least 2, which S07 provides.
• S07 · premise_audit · S02, exists_elim — These are the hypothesis of the proof by contradiction and its direct consequences; the hypothesis is discharged only in S11.
• S06 · premise_audit · S05, rem_test — This step only shows the inadequacy of a partial check; it does not change the conclusion of S05.
• S05 · premise_audit · S01, mko_dvd_def, numeric_evaluation — Refutation needs only one nontrivial divisor.
• S04 · premise_audit · S01, S02, case_analysis — The divisor range 1 to 2 is exhausted; no candidate is missed.
• S03 · premise_audit · S01, S02, mul_zero — Refutation needs one failed condition; this also shows which condition is decisive for 1.
• S02.2 · premise_audit · order_basics, mul_one — Multiplying by a nonnegative number preserves ≤; the lemma itself is not used.
• S02.1 · premise_audit · mul_zero, contradiction — Only multiplication by zero is used; the lemma itself is not used.
• S02 · premise_audit · L_div_bound — It needs n>0; for n=0 every d divides 0 and there is no bound (S03).
• S01 · premise_audit · G1, mko_prime_def — This step only unfolds the definition and derives nothing new.

Error controls and negative controls

1 is not prime

The misconception the MKO names: listing 1 as a prime. The only divisor of 1 is indeed 1, but the definition also requires 2≤p, so 1 is not prime (S03). 0 fails even the divisor condition, since 2∣0.

Testing a few small factors is not enough

The other misconception the MKO names: declaring a number prime after testing a few small factors. 91 is not divisible by 2, 3 or 5, yet it equals 7·13 (S06). Confirming primality requires excluding every possible nontrivial divisor; Lemma L_small_factor narrows the range to m²≤n, but every m in that range must be checked (S10, S12).

Use exact integer comparisons for the square-root bound

MKO assumption a2 rules out approximate square roots. Here the bound 9 is fixed exactly by m²≤97 and 10²=100>97; deciding the bound from a rounded floating-point √n could skip a candidate near perfect squares.

• 1 is prime because its only divisors are 1 and itself → reject — The definition requires 2≤p, which 1 fails.
• 91 is not divisible by 2, 3 or 5, so 91 is prime → reject — 91=7·13; a partial check is not a proof.
• To prove 97 prime one must try division by every integer from 2 to 96 → reject — Lemma L_small_factor proves that a nontrivial divisor forces one with 2≤m≤9, so checking 2 to 9 suffices.
• 0 is prime because 0 has no divisors → reject — Every natural divides 0 (for example 0=2·0), and 2≤0 fails.
• All primes are odd → reject — 2 is prime (S04) and even.

Result and limitations

0 and 1 are not prime (2≤p fails; 1 is excluded even though its only divisor is 1); 2 is prime and the only even prime; 91=7·13 is composite, and testing only 2, 3, 5 misses 7; by min(d,k)²≤n only 2 to 9 need checking, and 97 leaves a nonzero remainder on division by each of them, so 97 is prime.

• rem_test is used as a prerequisite; its proof is in the natural-divisibility guide.
• Trying only the primes 2, 3, 5, 7 among 2 to 9 would also suffice, but that needs the extra fact 'the smallest nontrivial divisor is prime', which this guide neither uses nor proves.
• N15, N16 and N22 use the checker's built-in primality test as independent cross-checks only; N21 is a finite-range check.

Verification and source binding

22 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 0bde7a02304dff72bf0e31bb574cf7cb0d9d60df1744fb45c6915cc88cba7bb7
• original source SHA-256: 0bde7a02304dff72bf0e31bb574cf7cb0d9d60df1744fb45c6915cc88cba7bb7
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)