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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-prime-number/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-prime-number-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

p\ \text{prime}

After

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

Conditions: none

Rule: mko_prime_def · Uses: G1, mko_prime_def

Leaf basis: mko_prime_def + def_unfold

By the MKO's definition, a prime must satisfy two conditions together: p≥2, and p has no natural divisor other than 1 and p. To refute, one failed condition suffices; to confirm, every possible nontrivial divisor must be excluded.



S02 · impliesBefore

d\mid n,\ n>0

After

1\le d\le n

Conditions: n>0

Rule: L_div_bound · Uses: mko_dvd_def, L_div_bound

Leaf basis: mul_zero + order_basics + exists_elim

A divisor of a positive number lies between 1 and the number itself, by Lemma L_div_bound (proved in S02.1 and S02.2). This makes 'list every divisor' a finite task.



S03 · impliesBefore

p=0,\ p=1

After

0,\ 1\ \text{not prime}

Conditions: none

Rule: mko_prime_def · Uses: S01, S02, G3

Leaf basis: mko_prime_def + order_basics + mul_zero

Neither 2≤0 nor 2≤1 holds, so 0 and 1 are not prime. Note: by S02 the only divisor of 1 is 1 (1≤d≤1), so 1 actually passes the condition 'divisors are only 1 and itself'; it is excluded solely by 2≤p. 0 fails both conditions: 0=2·0, so 2∣0 with 2∉{1,0}.



S04 · impliesBefore

p=2

After

2\ \text{prime}

Conditions: none

Rule: mko_prime_def · Uses: S01, S02

Leaf basis: mko_prime_def + case_analysis + order_basics

2≥2. If d∣2, then 1≤d≤2 by S02, and the only naturals from 1 to 2 are 1 and 2, so d=1 or d=2. Both conditions hold, so 2 is prime (N22 is an independent check).



S05 · impliesBefore

91=7\cdot 13

After

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

Conditions: none

Rule: mko_prime_def · Uses: S01, mko_dvd_def, G3

Leaf basis: mko_prime_def + exists_intro + numeric_evaluation

7·13=91 (N1), so 7∣91 with witness 13. 7≠1 and 7≠91, so the divisor condition fails and 91 is not prime; 7 is a compositeness witness (MKO paragraph 2).



S06 · impliesBefore

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

After

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

Conditions: none

Rule: rem_test · Uses: S05, rem_test

Leaf basis: rem_test + numeric_evaluation

91 leaves remainder 1 on division by 2, 3 and 5 (N2 to N4), so by rem_test none of them divides 91. Declaring 91 prime after testing only these three would be wrong, since S05 found the divisor 7. Finding no factor in an incomplete list of candidates is not a proof of primality (MKO paragraph 2).



S07 · impliesBefore

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

After

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

Conditions: none

Rule: L_div_bound · Uses: S01, S02, G3

Leaf basis: exists_elim + order_basics + case_analysis

97≥2 holds. For the divisor condition argue by contradiction: suppose d∣97 with d≠1 and d≠97, and take a witness 97=dk. By S02, 1≤d≤97, and excluding 1 and 97 gives 2≤d≤96. Also k≥1 (S02.1); if k=1 then d=97, which is excluded; so k≥2.



S08 · impliesBefore

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

After

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

Conditions: d\ge 2; k\ge 2

Rule: L_small_factor · Uses: S07, L_small_factor

Leaf basis: order_basics + mul_comm + exists_intro

By Lemma L_small_factor (proved in S08.1 and S08.2), the smaller member m of the factor pair also divides 97, and m²≤97. This is the reason one only needs to check up to the square root, stated with exact integer comparisons.



S09 · impliesBefore

m^2\le 97

After

2\le m\le 9

Conditions: none

Rule: order_basics · Uses: S08, G2

Leaf basis: order_basics + numeric_evaluation + contradiction

If m≥10, then m²≥100>97 (N5), contradicting m²≤97; so m≤9. And 9²=81≤97 (N6), so 9 is the largest integer with m²≤97. This uses exact integer squares, not a floating-point √97.



S10 · case_splitBefore

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

After

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

Conditions: none

Rule: rem_test · Uses: S09, rem_test

Leaf basis: rem_test + case_analysis + numeric_evaluation

Compute the remainder of 97 on division by each m: m=2 gives 1, 3 gives 1, 4 gives 1, 5 gives 2, 6 gives 1, 7 gives 6, 8 gives 1, 9 gives 7 (N7 to N14). None is 0, so by rem_test none of 2 to 9 divides 97. This contradicts 'some m with 2≤m≤9 divides 97' from S08 and S09.



S11 · impliesBefore

\text{assumption of S07 leads to a contradiction}

After

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

Conditions: none

Rule: contradiction · Uses: S07, S10

Leaf basis: contradiction + quantifier_negation + mko_prime_def

The hypothesis of S07, 'some d∣97 with d∉{1,97}', leads to the contradiction in S10, so it is false: every divisor of 97 is 1 or 97. Together with 97≥2, the definition makes 97 prime. N15 is an independent check with a built-in primality test.



S12 · impliesBefore

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

After

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

Conditions: none

Rule: L_small_factor · Uses: S05, S08, G2

Leaf basis: order_basics + rem_test + numeric_evaluation

Apply the same bound to 91: 9²=81≤91<100=10² (N18, N19), so the composite 91 must have a divisor between 2 and 9; the complete search finds m=7 (91 leaves remainder 0 on division by 7, N17), in agreement with S05. Contrast S06: testing only 2, 3, 5 is an incomplete search, which is how 7 was missed.



S13 · impliesBefore

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

After

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

Conditions: p\neq 2

Rule: mko_prime_def · Uses: S01, S04, mko_dvd_def

Leaf basis: mko_prime_def + exists_intro + forall_intro

An even p=2j has the divisor 2 (witness j). If p≠2, then 2≠1 and 2≠p, so the divisor condition fails and p is not prime. With S04, 2 is the only even prime (N21 is a finite check over the even numbers 4 to 120 and supports only those points).







## Substeps and lemmas

S02.1 · impliesBefore

n=dk,\ n>0

After

d\ge 1,\ k\ge 1

Conditions: n>0

Rule: mul_zero · Uses: mko_dvd_def, mul_zero

Leaf basis: mul_zero + contradiction

If d=0 or k=0, then n=dk=0, contradicting n>0. So d≠0 and k≠0, and a nonzero natural is at least 1.



S02.2 · impliesBefore

k\ge 1,\ d\ge 0

After

n=dk\ge d\cdot 1=d

Conditions: none

Rule: order_basics · Uses: S02.1, order_basics

Leaf basis: order_basics + mul_one

k≥1 and d≥0, so dk≥d·1=d, that is d≤n. S02.1 and S02.2 together prove Lemma L_div_bound.



S08.1 · impliesBefore

n=dk

After

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

Conditions: none

Rule: exists_intro · Uses: mko_dvd_def, mul_comm

Leaf basis: exists_intro + mul_comm + case_analysis

n=d·k gives d∣n (witness k); by commutativity n=k·d gives k∣n (witness d). m is one of d and k, so m∣n; and since d, k≥2, m≥2.



S08.2 · impliesBefore

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

After

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

Conditions: none

Rule: order_basics · Uses: order_basics

Leaf basis: order_basics + mul_comm

Multiplying m≤d by the nonnegative m gives m·m≤d·m; multiplying m≤k by the nonnegative d gives d·m≤d·k. Chaining gives m²≤n. S08.1 and S08.2 together prove Lemma L_small_factor.







## 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 primeThe 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 enoughThe 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 boundMKO 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-prime-number-01.json)