Computational proof: every integer larger than 1 has a prime divisor
Deduced from first principles
Deduced from first principles
Axiom schemes
Axiom schemes
Order
Order
In[]:=
equal[n_,m_]:=Hold[Equal][n,m]
In[]:=
greaterEqual[n_,m_]:=Hold[GreaterEqual][n,m]
Axiom OrdRefl. For any integer n ≥ 0, we have
In[]:=
AxiomOrdRefl[n_]:=greaterEqual[n,n]
Axiom OrdAntiSym. Given two integers n ≥ 0 and m ≥ 0. If n ≥ m and m ≥ n then n == m.
In[]:=
AxiomOrdAntiSym[{Verbatim[Hold[GreaterEqual]][n_,m_],Verbatim[Hold[GreaterEqual]][m_,n_]}]:=equal[n,m]
Axiom OrdTrans. Given three integers n ≥ 0, m ≥ 0 and k ≥ 0. If n ≥ m and m ≥ k then n ≥ k.
In[]:=
AxiomOrdTrans[{Verbatim[Hold[GreaterEqual]][n_,m_],Verbatim[Hold[GreaterEqual]][m_,k_]}]:=greaterEqual[n,k]
Divisibility
Divisibility
In[]:=
divisible[n_,m_]:=Hold[Divisible][n,m]
Axiom DivZero. The zero is divisible by every number.
In[]:=
AxiomDivZero[n_]:=divisible[0,n]
Axiom DivAdd. If n is divisible by m then n+m is divisible by m.
In[]:=
AxiomDivAdd[Verbatim[Hold[Divisible]][n_,m_]]:=divisible[n+m,m]
Axiom DivInv. If the proposition divisible[n, m] holds, then it was derived from Axioms DivZero and DivAdd.
In[]:=
AxiomDivInv[Verbatim[Hold[Divisible]][n_,m_]]:=If[n<m,equal[n,0],divisible[n-m,m]]
Minimum nontrivial divisor
Minimum nontrivial divisor
In[]:=
MinDiv[n_]:=Divisors[n][[2]]
In[]:=
minDiv[n_]:=If[n≥2,Hold[MinDiv][n],$Aborted]
Axiom MinDivDiv. For any integer n ≥ 2, we have that n is divisible by MinDiv[n].
In[]:=
AxiomMinDivDiv[Verbatim[Hold[GreaterEqual]][n_,2]]:=divisible[n,minDiv[n]]
Axiom MinDivMin. For any integer n ≥ 2 and any integer d ≥ 2, if n is divisible by d then d ≥ MinDiv[n].
In[]:=
AxiomMinDivMin[Verbatim[Hold[GreaterEqual]][n_,2],Verbatim[Hold[GreaterEqual]][d_,2],Verbatim[Hold[Divisible]][n_,d_]]:=greaterEqual[d,minDiv[n]]
Axiom MinDivNonTriv. For any integer n ≥ 2, if n is divisible by d then MinDiv[n] ≥ 2.
In[]:=
AxiomMinDivNonTriv[Verbatim[Hold[GreaterEqual]][n_,2]]:=greaterEqual[minDiv[n],2]
Prime number
Prime number
In[]:=
primeQ[p_]:=Hold[PrimeQ][p]
Axiom PrimeIntro. Let p ≥ 2 be an integer. If p is equal to its minimum nontrivial divisor, then p is prime.
In[]:=
AxiomPrimeIntro[Verbatim[Hold[GreaterEqual]][p_,2],Verbatim[Hold[Equal]][p_,Hold[MinDiv][p_]]]:=primeQ[p]
Axiom PrimeElim1. Let p be an integer. If p is prime then p ≥ 2.
In[]:=
AxiomPrimeElim1[Verbatim[Hold[PrimeQ]][p_]]:=greaterEqual[p,2]
Axiom PrimeElim2. Let p be an integer. If p is prime then p is equal to its minimum nontrivial divisor.
In[]:=
AxiomPrimeElim2[Verbatim[Hold[PrimeQ]][p_]]:=equal[p,minDiv[p]]
Auxiliary results
Auxiliary results
Successive additions and divisibility
Successive additions and divisibility
Theorem DivAdd. Let n ≥ 0, m > 0 and k ≥ 0 be integers. If n is divisible by m then n + m*k is divisible by m.
In[]:=
ThmDivAdd[Verbatim[Hold[Divisible]][n_,m_],k_]:=divisible[n+m*k,m]
An instance of Theorem 2
In[]:=
ThmDivAdd[divisible[6,3],2]
Out[]=
Hold[Divisible][12,3]
Proof
Proof
We proceed by induction on k.
base case
For k == 0 we obtain the thesis from the premise
In[]:=
ThmDivAdd[divisible[n,m],0]
Out[]=
Hold[Divisible][n,m]
induction step
Assume that k ≥ 1
In[]:=
P1=greaterEqual[k,1]
Out[]=
Hold[GreaterEqual][k,1]
Consider the premise
In[]:=
P2=divisible[n,m]
Out[]=
Hold[Divisible][n,m]
Assume that theorem holds when k is substituted by of k – 1 (notice that his is possible because of P1).
In[]:=
P3=ThmDivAdd[P2,k-1]
Out[]=
Hold[Divisible][(-1+k)m+n,m]
Now, apply axiom DivAdd
In[]:=
P4=AxiomDivAdd[P3]
Out[]=
Hold[Divisible][m+(-1+k)m+n,m]
Simplify P4
In[]:=
P4//FullSimplify
Out[]=
Hold[Divisible][km+n,m]
Thus, we obtained the desired result
In[]:=
ThmDivAdd[divisible[n,m],k]
Out[]=
Hold[Divisible][km+n,m]
In[]:=
ClearAll[P1,P2,P3,P4]
Qed
Qed
Transitivity of division
Transitivity of division
Statement
Statement
Theorem DivTrans. Let n ≥ 0, m > 0 and k > 0 be integers. If n is divisible by m and m is divisible by k then n is divisible by k.
In[]:=
ThmDivTrans[{Verbatim[Hold[Divisible]][n_,m_],Verbatim[Hold[Divisible]][m_,k_]}]:=divisible[n,k]
An instance of this theorem
In[]:=
ThmDivTrans[{divisible[12,4],divisible[4,2]}]
Out[]=
Hold[Divisible][12,2]
Proof
Proof
We proceed by induction on n.
base case
For n == 0, we obtain the thesis by an invocation of axiom DivZero
In[]:=
AxiomDivZero[k]
Out[]=
Hold[Divisible][0,k]
Induction step
Assume that n ≥ 1
In[]:=
P1=greaterEqual[n,1]
Out[]=
Hold[GreaterEqual][n,1]
Consider the premises
Define
and consider the cases corresponding to n < m
case I: n < m is true
Assume
Notice the contradiction
Therefore, this case is impossible.
case II: n < m is false
Notice that
Hence, the assumption
is well-defined, i.e., –m + n is a nonnegative integer.
Remember that we assumed
Notice that
Indeed,
Hence, we can apply the induction hypothesis
Notice that m/k is an integer, since P3 holds.
Now we apply Theorem DivAdd
and we obtain the desired result
Qed
Qed
Division and order
Division and order
Statement
Statement
Theorem DivOrd. Let n ≥ 1 and m > 0 be integers. If n is divisible by m then n is greater or equal to m.
An instance of this theorem
Proof
Proof
We proceed by reductio ad absurdum.
Suppose that n ≥ m is false, i.e., n < m holds.
Consider the premise
Apply axiom DivInv
Apply the premise n < m
Moreover, we have the premise n ≥ 1
ultimately, we obtain a contradiction
Qed
Qed
Main result
Main result
Statement
Statement
Theorem DivPrim. For every integer n ≥ 2, the minimum nontrivial divisor of n is prime.
Proof
Proof
From the premise n ≥ 2,
we have MinDiv[n] ≥ 2 because of Axiom MinDivNonTriv.
Furthermore, MinDiv[MinDiv[n]] ≥ 2.
We have that MinDiv[n] is divisible my MinDiv[MinDiv[n]], because of Axiom MinDivDiv
Moreover, we have that n is divisible my MinDiv[n], because of Axiom MinDivDiv
Ultimately, n is divisible by MinDiv[MinDiv[n]] because of theorem DivTrans.
Hence, MinDiv[MinDiv[n]] ≥ MinDiv[n].
Applying Theorem DivOrd we obtain MinDiv[n] ≥ MinDiv[MinDiv[n]].
Consider the following fact
which can be verified by computation in the Wolfram Language
Apply transitivity of the order
Using the Theorem DivOrder we obtain
Applying anti-symmetry of the order (axiom OrdAntiSym), we conclude that MinDiv[n] == MinDiv[MinDiv[n]].
Therefore, the minimum nontrivial divisor of n is prime, in virtue of axiom PrimeIntro.
Qed
Qed