10.6092/issn.1972-5787/385
We discuss the formalization, in the Matita Interactive Theorem Prover, of a few elementary results in number theory about the  Moebius mu function and the Euler phi function.
application/pdf
1972-5787
385
1
en
Cristian Armentano
Journal of Formalized Reasoning
A Page in Number Theory
Text.Serial.Journal
https://jfr.unibo.it/
1
Articles
2008-09-26
2007-10-22
2008-09-23
2016-01-29
1-23
JFR
Cristian Armentano
2008/09/26
10.6092/issn.1972-5787/385
1
University of Bologna
1972-5787
1
en
23
A Page in Number Theory
https://jfr.unibo.it/article/download/385/726
1
A Page in Number Theory
Andrea Asperti, Cristian Armentano
Dipartimento di Scienze dell’Informazione
Università degli Studi di Bologna


We discuss the formalization, in the Matita Interactive Theorem Prover, of a few elementary
results in number theory about the Möbius µ function and the Euler φ function.




1.   INTRODUCTION
The title of the paper must be understood in a strictly literal sense: we discuss
the formalization, in the Matita Interactive Theorem Prover [2, 3], of one page of a
traditional graduate textbook in Number Theory, and precisely the portion of text
spanning from line −9 of page 19 to line −6 of page 20 in Ireland and Rosen’s book
“A Classical Introduction to Modern Number Theory” [10] 1 (see appendix A).
The page is quite dense; the main notions and results are the following:
—definition of the Möbius µ function
—proof of Σd|n µ(d) = 0
—definition of the Dirichlet composition
—proof of the Möbius Inversion Theorem
—definition of the Euler φ function
—proof of Σd|n φ(d) = n
Although the results are relatively elementary, the only formalization we are aware
of is by J.Avigad and other people, in Isabelle, as part of their proof of the prime
number theorem [6] . Intentionally, we did not look at [6] during our development,
since we did not want to be biased in our choices by a previous formalization.
However, a detailed comparison was done after the completion of the work, as
discussed in salient points along the paper. The style of the presentation will strictly
follow the original mathematical text, quoting the source (in framed boxes) and
discussing step by step its formalization. We shall just make a single large detour
concerning iteration and several theorems about its invariance under permutation
of the inputs (under the suitable conditions).
   At the moment we started the work, the mathematical library of Matita already
contained the proof of the Fundamental Theorem of Arithmetic (unicity of the
decomposition in prime factors), Fermat’s Little Theorem and its generalization to
the Euler function, namely the fact that for any a coprime to n, aφ(n) ≡ 1 mod n.
   The results contained in this paper have been presented in a two-hour lesson
given by the first author at the Types Summer School held Bertinoro in August
2007. All the scripts are accessible from the Matita Home Page.

1 Among   the several texts we consulted, we found [10] particularly accessible, only requiring a
familiarity with basic abstract algebra.
                                           Journal of Formal Reasoning Vol. 1, No. 1, 2008, Pages 1–23.
2        ·    A. Asperti and C. Armentano

2.   THE MÖBIUS µ FUNCTION
     “. . . We now introduce a very important arithmetic function, the Möbius
     µ function.
     For n ∈ Z + , µ(1) = 1, µ(n) = 0 if n is not square-free, and µ(p1 p2 . . . pl ) =
     (−1)l , where the pi are distinct positive primes.”
  The above definition of the µ function is essentially based on the composition of
two other functions: the factorization function (already available in Matita), and a
function counting the number of the distinct primes (provided no prime has an order
greater than 1 in the decomposition, otherwise the result is 0). We could formalize
µ as such a composition2 or give a more direct definition, essentially obtained by
a partial evaluation of the former. According to our experience, working with a
direct definition is usually simpler.
The definition relies on the following auxiliary functions of the Matita library :
—(p_ord n p) returns a pair hq, ri, where q is the order (or multiplicity) of p in
 n and r is the remaining, i.e. n = pq r, where p does not divide r (for n = 0 it
 returns the default pair h0, 0i);
—(nth_prime i) is the i-th prime number in progressive order;
—(max_prime_factor n) is the index of the largest prime in n, in the enumeration
 of all primes;
—Z, OZ, oneZ and Zopp are respectively the type of integers, its zero, one, and the
 function taking n to −n.
The definition is straightforward: we start looking for the max prime factor pk in
n, and then call an auxiliary function, defined by primitive recursion over k that
computes the order of pk in n, returns 0 if it is greater than 1 and otherwise recurs
on the remainder, changing the sign of the result.
                                                                                     
let rec moebius aux p n : Z :=
  match p with
  [ O ⇒ oneZ
  | (S p1) ⇒
     match p ord n (nth prime p1) with
     [ (pair q r) ⇒
       match q with
       [ O ⇒ moebius aux p1 r
       | (S q1) ⇒
         match q1 with
         [ O ⇒ Zopp (moebius aux p1 r)
         | (S q2) ⇒ OZ
         ]
       ]
     ]
  ].
                                                                                         

2 This   is the approach in Isabelle, by D.Gray.


Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                                                A Page in Number Theory          ·     3

                                                                                                           
definition moebius n: Z :=
  let p := max prime factor n in moebius aux (S p) n.
                                                                                   
We remind the reader that Matita is based on the same foundational framework
as Coq - the Calculus of Inductive Constructions - thus embedding a notion of
normalization into its logic. As a consequence, all definitions are live and can be
evaluated just normalizing the involved expression.

3. ΣD|N µ(D) = 0
     Proposition. If n > 1, Σd|n µ(d) = 0.
     Proof. If n = pa1 1 pa2 2 . . . pal l , then

                              Σd|n µ(d) = Σ(1 ,...,l ) µ(p11 . . . pl l )
     where the i are zero or one. Thus
                                      l       l
            Σd|n µ(d) = 1 − l + (2 ) − (3 ) + . . . + (−1)l = (1 − 1)l = 0

  Remark 1. The previous proof is standard. For instance, it can also be found
in [9] (Theorem 262, p.235), [11] (Theorem 2.2.5, p.63), [1](Theorem 2.1, p.25).
    Existence and unicity of the decomposition into prime factors has been already
proved in Matita, and we may assume to have the list [a1 ; a2 ; . . . al ] such that n =
pa1 1 pa2 2 . . . pal l . We may also easily (re-)define µ taking as input [a1 ; a2 ; . . . al ], and
prove that if µ(n) 6= 0 then ai is either one or zero (for the square-free condition).
It is also possible to prove that d divides n if and only if d admits a decomposition
of the kind pb11 pb22 . . . pbl l where bi ≤ ai . Notwithstanding all these property, the
equation
                              Σd|n µ(d) = Σ(1 ,...,l ) µ(p11 . . . pl l )                        (1)
is still far away. The pointP is that in order to formalize the statement we would need
a multi-dimensional sum ~x≤~a f (~x) parametric in n, ~a ∈ N n and f : N n → N ,
whose definition is relatively complex, due to the dependent type N n .
The alternative approach followed in [6] is the following. Define the radical
                                                                           P rad(n)
of a number n to be the greatest square free number dividing n. Then d|n µ(d) =
P
   d|rad(d) µ(d). Finally, for some prime factor p of n write
                       X                 X                X
                             µ(d) =            µ(d) +            µ(d)
                       d|rad(d)           d|rad(d),p|d          d|rad(d),p6 |d

and prove that each term in the first sum is canceled by a corresponding term of
the second.
We followed still another route. Let p be a prime factor of n, and assume its order
in n is a, i.e. n = pa r and p 6 |r. Then
                                     Σd|pa r µ(d) = Σd|r Σi≤a µ(pi d)                                (2)
Since p 6 |r then p 6 |d and hence µ(pd) = −µ(d).
Moreover, for any i > 1, µ(pi d) = 0 since it is not square free. Hence, for any d,

                                                         Journal of Formal Reasoning Vol. 1, No. 1, 2008.
4     ·     A. Asperti and C. Armentano

                       Σi≤a µ(pi d) = µ(d) + µ(pd) + Σ2≤i≤a µ(pi d)
                                    = µ(d) − µ(d)
                                    = 0
Formalizing the last row of equations is not particularly problematic. More complex
is the formal proof of equation (2). The problem can be essentially decomposed
into two subproblems:
(1) getting rid of the nested sum;
(2) proving that the sum is invariant under permutation of its addends.
We shall separately discuss the two problems in the following subsections. For the
sake of clarity, we shall stick to sums, but all results may be generalized to products
and, more generally, to arbitrary iterative constructs, provided the iterated function
is commutative, associative, and admits a neutral element. In Matita, all results
have been proved in the generalized form; specific cases are derived by instatiation
(they are still usefull for readibility, and notational purposes).
3.1   Nested Sums
Let us write
                                              X
                                                       g(i)
                                            i<n,p(i)

for the sum of all g(i) where i ranges over all integers less than n which satisfy the
boolean condition p (we shall sometimes omit the bound when it can be inferred by
the condition). We prefer boolean conditions to generic predicates for computability
reasons, but the following discussion can be easily generalized to the formers.
The above function is easily defined in a formal way by induction on n:
                                                                                      
let rec sigma p n p g =
match n with
[ O⇒O
| S k ⇒ match p k with
    [true ⇒ g(k)+(sigma p k p g)
    | false ⇒ (sigma p k p g)
    ]
].
                                                                                         
The following statement reduces a nested sum to a single sum:
                   X       X               X
                                 g(i, j) =     g(k/m, k mod m)                     (3)
                    i<n,p1 (i) j<m,p2 (j)            k <n·m
                                                     p1 (k/m)
                                                   p2 (k mod m)

Formally:
                                                                                         
theorem sigma p2:
∀ n,m: nat.
∀ p1: nat → bool.
∀ p2: nat → nat → bool.
∀ g: nat → nat → nat.
Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                                           A Page in Number Theory           ·     5

sigma p n p1
   (λ x.sigma p m (p2 x) (g x)) =
sigma p (n∗m)
   (λ x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
   (λ x.g (div x m) (mod x m)).
                                                                                       
The only interesting remark, here, is the type of the inner boolean test function p2 ,
that does also depend, in general, on the outer index (a fact that is often transparent
in the usual mathematical notation). The theorem is proved by induction on n and
relies on the following lemma (proved, in turn, by induction over k):
                      X                X                   X
                            g(i) =           g(i + n) +         g(i)
                   i<k+n,p(i)           i<k,p(i+n)                i<k,p(i)

Here is the formal statement:
                                                                                                       
theorem sigma p plus: ∀n,k:nat.∀ p:nat → bool.
∀ g: nat → nat.
  sigma p (k + n) p g
  = sigma p k (λ x.p (x+n)) (λ x.g (x+n)) + sigma p n p g.
                                                                                                       
3.2   Invariance under permutation
The second important result is the invariance of the sum under permutation of its
addends:
                              X                    X
                                     g(h(x)) =           g(x)                (4)
                                x<n1 ,p1 (x)              x<n2 ,p2 (x)

provided h is a bijection from {x < n2 : p2 (x)} to {x < n1 : p1 (x)}. The bijectivity
of h can be formalized in many different ways; we choose to explicitly provide the
inverse function:
                                                                                      
theorem eq sigma p gh:
∀ g: nat → Z.
∀ h,hinv: nat → nat.∀ n1,n2.
∀ p1,p2:nat → bool.
(∀ i . i < n1 → p1 i = true → p2 (h i ) = true) →
(∀ i . i < n1 → p1 i = true → hinv (h i ) = i) →
(∀ i . i < n1 → p1 i = true → h i < n2) →
(∀ j . j < n2 → p2 j = true → p1 (hinv j ) = true) →
(∀ j . j < n2 → p2 j = true → h (hinv j ) = j) →
(∀ j . j < n2 → p2 j = true → hinv j < n) →
  sigma p n1 p1 (λ x.g(h x)) = sigma p n2 (λ x.p2 x) g.
                                                                                                       
  There is an interesting remark to be made here. Consider the same result in the
particular case when the boolean conditions p1 and p2 are true. That implies that
n1 = n2 = n and h must be a permutation of the first n integers. The idea of
proving the result by induction on n does obviously face the difficulty that h is not,
in general, a permutation of the first n − 1 integers. The most elegant solution, in
this case, is to introduce the elementary notion of transposition
                                        
                                          n
                                         m
                                                     Journal of Formal Reasoning Vol. 1, No. 1, 2008.
6     ·      A. Asperti and C. Armentano

between two natural numbers n and m, that is the operation swapping n and m.
This allows us to reduce the problem to the following simpler statement: for all
n, m < k
                            X         X n
                               g(i) =    g(       i)                        (5)
                                             m
                                      i<k           i<k
Still, the previous equation is not entirely trivial, requiring a complete (course of
values) induction on the distance between n and m.
  Somewhat surprisingly, the most general case of conditional sums turns out to be
simpler, since we may take advantage of the boolean condition to get rid of part of
the problems. The key lemma, in this case, is the following, almost trivial remark:
for any a < k such that p(a)
                             X                    X
                                  g(i) = g(a) +         g(i)                      (6)
                                  i<k,p(i)                       i<k
                                                                  p(i)
                                                                 i 6= a

Then, the proof of equation (3) can be done by induction over n2 . If n2 = 0, then
it is easy to prove that p1 (x) must be false for any x < n1 . Suppose n2 = k + 1. If
p2 (k + 1) = false then
                                X                X
                                       g(i) =         g(i)
                                  i<k+1,p2 (i)            i<k,p2 (i)

and the results follows by induction (provided you prove that h and h−1 still define
a bijection in the restricted interval). If p2 (k + 1) = true then
            X                               X
                    g(x) = g(k + 1) +              g(x)
          x<k+1,p2 (x)                            x<k,p2 (x)
                                                    X
                              = g(k + 1) +                 g(h(x))                  by induction
                                               x < n1 , p1 (x)
                                              x 6= h−1 (k + 1)
                                                                 X
                              = g(h(h−1 (k + 1))) +                       g(h(x))
                                                           x < n1 , p1 (x)
                                                          x 6= h−1 (k + 1)
                                      X
                              =                  g(h(x))                            by (5)
                                  x<n1 ,p1 (x)

3.3   A composite statement
It is worth to combine together the two equations 3 and 4:
                     X                X       X
                            g(x) =                   g(h2 (i, j))                                  (7)
                         x<k,p1 (x)           i<n,p21 (i) j<m,p22 (j)

provided h2 is a bijection between
                               {(i, j) < (n, m) : p21 (i) ∧ p22 (i, j)}
and
                                             {x < k : p1 (x)}
Formally:
Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                                    A Page in Number Theory           ·     7

                                                                                                
theorem sigma p knm:
∀ g: nat → nat.
∀ h2:nat → nat → nat.
∀ h11,h12:nat → nat.
∀ k,n,m.
∀ p1,p21:nat → bool.
∀ p22:nat → nat → bool.
(∀ x. x < k → p1 x = true →
  p21 (h11 x) = true ∧ p22 (h11 x) (h12 x) = true
  ∧ h2 (h11 x) (h12 x) = x ∧(h11 x) < n ∧(h12 x) < m) →
(∀ i , j . i < n → j < m
   → p21 i = true → p22 i j = true →
  p1 (h2 i j ) = true ∧ h11 (h2 i j ) = i ∧ h12 (h2 i j ) = j ∧ h2 i j < k) →
sigma p k p1 g = sigma p n p21 (λ x:nat.sigma p m (p22 x) (λ y. g (h2 x y))).
                                                                                    
Starting from 7, equation 2 is now easy to prove: it amounts to check that the
function h1 (d, i) = pi d defines an isomorphism between {(d, i) ≤ (r, a) : d|r} and
{x ≤ pa r : x|pa r} (under the essential assumption that p does not divides r). The
inverse function is just (the symmetric of) p_ord, and the injective nature of p_ord
was a key lemma for the fundamental theorem of arithmetic, already proved in the
library.

4.   DIRICHLET MULTIPLICATION
     “The full significance of the Möbius µ function can be understood most
     clearly when its connection with Dirichlet multiplication is brought to light.
     Let f and g be complex valued functions on Z + . The Dirichlet product of
     f and g is defined by the formula f ⊗ g(n) = Σf (d1 )g(d2 ) where the sum
     is over all pairs (d1 , d2 ) of positive integers such that d1 d2 = n.”
As remarked by the authors themselves a few lines later, the same definition can
be given whenever the codomain of f and g is an any abelian group, preserving
all properties of the multiplication. For the sake of simplicity, we consider Z itself.
This is our definition in Matita.
                                                                                       
definition dirichlet product f g n: Z :=
 sigma p (S n) (λ d.divides b d n) (λ d. ( f d)∗(g (div n d ))).
                                                                                    
Up to our knowledge, there is no explicit definition of the Dirichlet composition in
[6], although it is implicitly used in most of their results.

     “This product is associative, as one can see by checking that f ⊗(g⊗h)(n) =
     (f ⊗ g) ⊗ h(n) = Σf (d1 )g(d2 )h(d3 ) where the sum is over all 3-tuples
     (d1 , d2 , d3 ) of positive integers such that d1 d2 d3 = n.”
The associativity property looks absolutely trivial. Unfortunately, its formalization
is not. The gap between the simple mathematical remark behind the previous
“proof”, and the actual complexity of its formal counterpart is one of the most
astonishing points in the formalization of these results in number theory. Avigad
and his coauthors experienced a similar puzzling sensation:

                                              Journal of Formal Reasoning Vol. 1, No. 1, 2008.
8      ·      A. Asperti and C. Armentano

        “This type of “reindexing” is often so transparent in mathematical ar-
        guments that when we first came across an instance where we needed it
        [. . . ], it took some thought to identify the relevant principle”. [6]
The point is the following. By definition
                                      f ⊗ g(n) = Σd|n f (d)g(n/d)
Hence
                       f ⊗ (g ⊗ h)(n) =
                              = Σd1 |n f (d1 )g ⊗ h(n/d1 )
                              = Σd1 |n f (d1 )(Σd2 |(n/d1 ) g(d2 )h((n/d1 )/d2 ))
                              = Σd1 |n Σd2 |(n/d1 ) f (d1 )g(d2 )h((n/d1 )/d2 )
while
                          (f ⊗ g) ⊗ h(n) =
                                = Σd1 |n f ⊗ g(d1 )h(n/d1 )
                                = Σd1 |n (Σd2 |d1 f (d2 )g(d1 /d2 ))h(n/d1 )
                                = Σd1 |n Σd2 |d1 f (d2 )g(d1 /d2 ))h(n/d1 )
In order to prove the equivalence of the two summations, we must hence exploit
the bijection between the following sets:
                             A = {(d1 , d2 ) ≤ (n, n) : d1 |n, d2 |(n/d1 )}

                                B = {(d1 , d2 ) ≤ (n, n) : d1 |n, d2 |d1 }
The bijection is easily found: h : A → B and h−1 : B → A are the following
functions
                                         h(d1 , d2 ) = (d1 d2 , d1 )

                                       h−1 (d1 , d2 ) = (d2 , d1 /d2 )
However, checking that they are inverse of each other (on the given domains) require
quite a lot of tedious computations. Even worse, with the results mentioned so far,
we should first get rid of (at least one of the) nested sum, that would furtherly
complicate the notation, mixing the division operations of the Dirichlet product
with that of equation 3. All statements would become quite unreadable. The only
solution is to give still another version of equations 4 and 7, dealing with nested
sums on both sides:
       X           X                    X         X
                            g(i, j) =                     g(h21 (i, j), h22 (i, j)) (8)
      i<n1 ,p11 (i) j<m1 ,p12 (i,j)           i<n2 ,p21 (i) j<m2 ,p22 (i,j)

provided hh21 , h22 i is a bijection between
                                {(i, j) < (n1 , m1 ) : p11 (i) ∧ p12 (i, j)}
and
                                {(i, j) < (n2 , m2 ) : p21 (i) ∧ p22 (i, j)}
(with inverse function hh11 , h12 i). Formally:
Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                                      A Page in Number Theory           ·     9

                                                                                                  
theorem sigma p2 eq:
∀ g: nat → nat → Z.
∀ h11,h12,h21,h22: nat → nat → nat.
∀ n1,m1,n2,m2.
∀ p11,p21:nat → bool.
∀ p12,p22:nat → nat → bool.
(∀ i , j . i < n2 → j < m2 → p21 i = true → p22 i j = true →
  p11 (h11 i j ) = true ∧ p12 (h11 i j ) (h12 i j ) = true
  ∧ h21 (h11 i j ) (h12 i j ) = i ∧ h22 (h11 i j ) (h12 i j ) = j
  ∧ h11 i j < n1 ∧h12 i j < m1) →
(∀ i , j . i < n2 → j < m2 → p11 i = true → p12 i j = true →
  p21 (h21 i j ) = true ∧ p22 (h21 i j ) (h22 i j ) = true
  ∧ h11 (h21 i j ) (h22 i j ) = i ∧ h12 (h21 i j ) (h22 i j ) = j
  ∧ h21 i j < n2 ∧h22 i j < m2) →
sigma p n1 p11 (λ x:nat .sigma p m1 (p12 x) (λ y. g x y)) =
sigma p n2 p21 (λ x:nat .sigma p m2 (p22 x) (λ y. g (h11 x y) (h12 x y ))).
                                                                                                  

5.   THE INVERSION THEOREM
     “Define the function T by T (1) = 1 and T (n) = 0 for n > 1. Then
     f ⊗ T = T ⊗ f = f .”
                          X
            f ⊗ T (n) =         f (d)T (n/d)                       by def. of µ
                          d|n
                                               X
                       = f (n)T (n/n) +            f (d)T (n/d)    by eq. 6
                                            d<n,d|n
                                    X
                       = f (n) +         0
                                  d<n,d|n
                       = f (n)
The proof that T ⊗ f = f is slightly more involved. The best solution is to prove
once and for all the commutativity of the Dirichlet composition. It is interesting
to observe that, from the mathematical point of view, such a property is so evident
that the authors do not even care to mention it! For the formal proof you have to
exploit the permutation mapping d in n/d between divisors of n.
A second remark to do is about extensionality. Matita is based on the Calculus of
Inductive Constructions, which is not an extensional theory. So, by the fact that
for any n, f ⊗ T (n) = f (n) we are not authorized to conclude that f ⊗ T = f , but
we must stumble along with the former, weaker equivalence.
     “Define I by I(n) = 1 for all n. Then f ⊗ I(n) = I ⊗ f (n) = Σd|n f (d).”

Prove f ⊗ I(n) = f (n) and then use commutativity for the other equality. Again,
proving directly I ⊗ f (n) = f (n) is far more complex.
     “Lemma. I ⊗ µ = µ ⊗ I = T.
     Proof. µ ⊗ I(1) = µ(1)I(1) = 1. If n > 1, µ ⊗ I(n) = Σd|n µ(d) = 0.

This is easy.
                                                Journal of Formal Reasoning Vol. 1, No. 1, 2008.
10     ·     A. Asperti and C. Armentano

     “Theorem (Möbius Inversion Theorem).
     Let F (n) = Σd|n f (d). Then f (n) = Σd|n µ(d)F (n/d).
     Proof. F = f ⊗ I. Thus F ⊗ µ = (f ⊗ I) ⊗ µ = f ⊗ (I ⊗ µ) = f ⊗ T = f .
     This shows that f (n) = F ⊗ µ(n) = Σd|n µ(d)F (n/d).

The formal proof essentially follows the same line, but is not as elegant, mostly
due to extensionality problems. Let us write ∼   = for the extensional equivalence of
functions, i.e. f ∼
                  = g iff ∀n.f (n) = g(n). For instance, if we only know F ∼
                                                                           = f ⊗ I we
cannot just rewrite F ⊗ µ into (f ⊗ I) ⊗ µ, since rewriting only works with Leibniz
(intensional) equality. The right way to proceed, here, is to prove first prove the
congruence of ⊗ with respect to extensional equality, namely
                             f∼
                              = f0 → g ∼
                                       = g0 → f ⊗ g ∼
                                                    = f 0 ⊗ g0
The complete Matita proof can be found in Appendix B.
   P
6.    D|N φ(D) = N

     “. . . The Möbius inversions has many applications. We shall use it to
     obtain formula for yet another arithmetic function, the Euler φ function.
     For n ∈ Z + , φ(n) is defined to be the number of integers between 1 and
     n relative prime to n. For example, φ(1) = 1, φ(5) = 4, φ(6) = 2 and
     φ(9) = 6. If p is a prime, it is clear that φ(p) = p − 1.”

The Euler φ function (sometimes called totient function) can be simply expressed
in terms of our sum operation as follows:
                                                      n
                                                      X
                                        φ(n) =              1
                                                   gcd(i,n)=1

where gcd(m, n) is the greatest common divisor of m and n.
Since the gcd function already belongs to the Matita library, the previous definition
can be directly translated into its formal counterpart:
                                                                                     
definition totient n: nat :=
 sigma p n (λ m. eqb (gcd m n) 1) (λ m.1).
                                                                                      
Note that, for simplicity, the sum stops at n − 1, so we do not count n as one of
the possible integers relative prime to itself: if n = 1, our sum correctly returns 1,
while if n > 1, gcd(n, n) = 1 is obviously false.
                    P
    Proposition. d|n φ(d) = n.
    Proof. Consider the n rational numbers n1 , n2 , n3 , ..., n−1  n
                                                                n , n . Reduce each
    to lowest terms; i.e., express each number as quotient of relative prime
    integers. The denominators will all be divisors of n. If d|n, exactly φ(d) of
    our numbers
           P      will have d in the denominator after reducing to lowest terms.
    Thus d|n φ(d) = n.

Before describing the formal version of this proof, let us try to make the previous
proof a bit more explicit.
Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                                   A Page in Number Theory           ·     11

Let us define Pd as the number of fractions having, after the reduction, d in the
denominator. We have to prove that ∀d, d|n.Pd = φ(d).
It is clear that after reducing to lowest terms, we obtain fractions in the form dpii ,
where di |n and gcd(pi , di ) = 1. Let x be a divisor of n; at least Px integers will
be less or equal than n, and relative prime to it (that is the numerators of those
fractions having x in the denominator), and so Px ≥ φ(x).
On the other hand, after the reduction there can’t be any other fraction with
denominator x, apart from those already considered. Suppose, towards obtaining
a contradiction, that there’s another fraction xk , where gcd(k, x) = 1, and k isn’t
any of the Px numerators introduced before. We are sure that k ≤ x, because none
of the initial fractions was greater than 1. Since x|n, and n > 0 by hypothesis,
                                      k∗l
∃l > 0.n = x ∗ l. So the fraction x∗l     = k∗l
                                              n is one of the n fraction before the
reduction to lowest terms, because k ∗l ≤ x∗l, that is k ∗l ≤ n. This fact guarantees
that l must be one of the Px numerator achieved after reducing to lowest terms all
the fractions. So then Px ≤ φ(x).
Since Px ≥ φ(x) and Px ≤ φ(x), we have Px = φ(x). It is now easy to obtain the
thesis of the theorem.
6.1   The formal proof
The formal proof strongly relies on sigma_p properties. By unfolding φ with its
definition we obtain
                            X          X
                                              1=n                          (9)
                            d<n+1,d|n i<d,gcd(i,d)=1

It is clear how these nested sums represent the scenario of the fractions reduced
to their lowest terms. The outer one is indexed over divisors of n, that is all the
possible denominators. For each outer index d0 , the inner sum ranges over the
possible numerators of fractions having, after the reduction, d0 in the denominator.
Inner indexes, in fact, must be relative prime to d0 , and less than it (here we have
a little difference with the “handwritten” proof, since we don’t work with nn , but
we consider n0 instead, according to the definition of totient introduced before).
Our first problem is that the upper bound d of the inner sum depends on (in
this case, is) the index of the outer one, while the library theorems dealing with
nested sums (in particular, equation 7) do not consider this possibility. Instead of
generalizing those results, in this case it is simpler to change the bound adjusting
the boolean predicate of the inner sum (in order to maintain the same semantics)
in the following way
                     X          X                X         X
                                        1=                        1              (10)
                 d<n+1,d|n i<d,gcd(i,d)=1    d<n+1,d|n    i < n + 1,
                                                         gcd(i, d) = 1
                                                             i<d

The previous transformation, as straightforward as it may seem, actually relies on
a couple of technical lemmas, whose proof is yet another tedious exercise.
The first one states that you may extend the bound, provided the boolean condition



                                              Journal of Formal Reasoning Vol. 1, No. 1, 2008.
 12     ·     A. Asperti and C. Armentano

 is false:
                                     X                  X
                                             g(i) =              g(i)                    (11)
                                  i<m,p(i)            i<n,p(i)

if n ≤ m and p(i) = false for n ≤ i < m.
                                                                                               
 theorem false to eq sigma p:
 ∀ n,m:nat.n \le m →
 ∀ p:nat → bool.
 ∀ g: nat → nat.
 (∀ i :nat. n \le i → i < m → p i = false) →
   sigma p m p g = sigma p n p g.
                                                                              
The second one states that you may change the boolean condition (and the body
of the sum), provided they have the same semantics on the given interval:
                            X              X
                                 g1 (i) =      g2 (i)                     (12)
                                i<n,p1 (i)            i<n,p2 (i)

if p1 (i) = p2 (i) for any i < n, and g1 (i) = g2 (i) for any i < n satisfying p1 (i):
                                                                                               
 theorem eq sigma p1: ∀p1,p2:nat → bool.
 ∀ g1,g2: nat → nat.∀ n.
 (∀ x. x < n → p1 x = p2 x) →
 (∀ x. x < n → p1 x = true → g1 x = g2 x) →
   sigma p n p1 g1 = sigma p n p2 g2.
                                                                                               
Using equation 10 we are left to prove
                              X        X
                                                              1=n                        (13)
                                  d<n+1,d|n    i<n+1
                                              gcd(i, d) = 1
                                                 i<d

 Let now t be the constant true boolean predicate; by induction over n it is very
 easy to prove that
                                       X
                                 n=         1
                                               j<n,t(j)

 so that 13 can be rewritten as
                          X                  X                     X
                                                        1=                 1
                            d<n+1,d|n    i<n+1                j<n+1,t(j)
                                        gcd(i, d) = 1
                                           i<d

 As described before, the nested sums allow us to represent reduced fractions. In
 this way its useful to think that the right dummy sum is indexed over the initial
 numerators (before reduction numerators are all the values in [0, n[). The aim is
 to complete the proof using theorem 7, finding a bijection between the couples of
 indexes in the nested sums and the indexes in the right, dummy sum. The variables
 of theorem 7 must be instantiated as follows:
 —g = (λx.1)
 Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                                         A Page in Number Theory           ·     13

—p1 = (λx.true)
—p21 = (λd.d|n)
—p22 = (λm, d.m < d ∧ gcd(m, d) = 1)
—h2 = (λd, i.i ∗ (n/d))
—h11 = (λj.n/(gcd(j, n)))
—h12 = (λj.j/(gcd(j, n)))
Let us also define sets A1 and A2 in this way:
                         A1 = {(d, i) < (n + 1, n + 1)|p21 (d) ∧ p22 (d, i)}
                         A2 = {j|p1 (j)} = [0, n[
Each couple (a, b) ∈ A1 represents the fraction ab after the reduction, while each
element in A2 simply represents the numerator of one of the initial fractions (having
n in the denominator) before the reduction. It is easy to see that h2 , applied to a
couple (x, y) ∈ A1 , returns the numerator of fraction xy before the reduction, while
h11 and h12 , applied to an element w ∈ A2 , return, respectively, the denominator
and the numerator of the fraction wn after the reduction. This bijection between A1
and A2 is formalized in the two main hypothesis of theorem 7, and can be proved
using simple properties of gcd and divides listed in appendix C.
6.2     Isabelle proof
We shall now have a look at the proof of d|n φ(d) = 0 in Isabelle Library3 , making
                                          P
a comparison with our proof in Matita, and trying to show how these two different
works share the same basic ideas.
   While our proof is based on properties of sums, this one has a more set-theoretic
flavor. Even φ is defined as the cardinality of a particular set, in the following way:
                         φ(p) = |{x ∈ N.1 ≤ x ≤ p ∧ gcd(p, x) = 1}|                            (14)
The complete proof is composed of 23 elementary lemmas. We shall not see all
them in detail but we shall just describe the main ideas of the proof, emphasizing
the connections with the classic one introduced at the beginning of section 6.
  Given n ∈ N + , the proof starts with a few initial definitions:
—S = {x ∈ Z.1 ≤ x ≤ n}
—I = {d ∈ Z.1 ≤ d ∧ d|n}
—∀d ∈ I.A(d) = {k ∈ S.gcd(k, n) = d}
—∀d ∈ I.B(d) = {m ∈ N.1 ≤ m ≤ (n/d) ∧ gcd(m, (n/d)) = 1}
—f : I → N.f = {λx : I.n/x}
Even if they are not described explicitly in the original work, it is very useful to
also define the following functions, for d ∈ I:
                                    rd (k) = k/d : A(d) → N

3 Thecomplete proof is a part of Avigad’s work, and can be found at
http://www.andrew.cmu.edu/user/avigad/isabelle/NumberTheory/EulerPhi.html



                                                    Journal of Formal Reasoning Vol. 1, No. 1, 2008.
14     ·     A. Asperti and C. Armentano

The two lemmas A_inj_prop and image_A_eq_B state, respectively, the following
results:
                                 ∀d ∈ I, rd is injective on A(d)                 (15)
                                 ∀d ∈ I, rd (A(d)) = B(d)                        (16)
It is very easy to see that the family of sets A(i) (with i ∈ I) is a partition of S,
and so
                                        X
                                  |S| =    |A(i)|                                (17)
                                               i∈I

Hence, we have:
                        |S|
                    n = P
                      = Pd∈I |A(d)|      by property 17
                      = Pd∈I |rd (A(d))| by injectivity of rd on A(d)
                      =   d∈I |B(d)|     by property 16
There is a clear relationship between sets B(i) and the reduction to lowest terms
described in the paper proof; for each divisor d of n, B(d) contains all and only
the possible numerators of reduced fractions, having nd in the denominator. In fact
a generic element x ∈ B(d) must be, by definition of B(d), less or equal than nd
(because all the considered fractions are not greater than 1), and relative prime to
it (because these fractions are reduced to lowest terms).
   We also see a clear connection with the nested sums 9 in Matita proof. In both
cases the outer sum ranges over the possible divisors of n, and the inner sum gives a
particular representation of the possible numerators in the reduced fractions. There
is just a little difference: while our proof considers the divisors of n as possible
denominators, in this proof the authors, given d|n, work with nd as denominator.
   Of course, this is not a real difference because, if d ranges over the set of the
possible natural divisor of n, nd ranges over the same set.
   The remaining part of Isabelle proof is essentially meant to formalize this obvious
equivalence.
   Given d|n, according to definition 14 we have
                                               n
                                   |B(d)| = φ( )
                                               d
So, by definition of f :
                                        X n
                                   n =      φ( )                                  (18)
                                               d
                                        d∈I
                                        X
                                     =      φ(f (d))                              (19)
                                               d∈I

Two more lemmas I_inj_prop and f_image_I_eq_I prove, respectively:
                                        f is injective on I                      (20)
                                        f (I) = I                                (21)
Now 19 becomes

Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                                       A Page in Number Theory         ·     15
                             P
                         n =          φ(d) by property 20
                             Pd∈f (I)
                           = Pd∈I φ(d)     by property 21
                           =  d|n φ(d)
that is the thesis of the theorem.

7.   CONCLUSIONS
In this paper we described the formalization, in the Matita interactive theorem
prover, of a few elementary results in number theory about the Möbius µ func-
tion, the Inversion Theorem, and the Euler φ function. Although our work and
that of Avigad et al. [6] are the only published formalisations of the mathematics
in question, some of the problems and of the techniques used for their solutions
frequently occur in different mathematical domains. For instance, Dirichlet con-
volution is meant to equip a certain function space with ring properties, and has
strong similarities with polynomial multiplication
                                              n
                                              X
                              p · q = (n 7→         pk · qn−k )
                                              k=0

where the computation of the n − th coefficient requires a sum of addends indexed
over all possible pairs (k, j) such that k + j = n.
Formal proofs of the convolution of polynomials can e.g. be found in [14] or [7]. The
latter proof is by a brute force induction; details of the former proof are not given in
the paper, but the following remark confirms the complexity of issue, independently
from the underlying proof assistant in use:
      “We would like to remark that proving the associativity of this convo-
      lution product presented a technical challenge as it turned out to be ex-
      tremely tedious for the authors of [13]”.
Coming to the resources required for our work, it is clear that the amount of time
invested largely depends by the skill of the authors; moreover, most of the time
is usually spent not on the results themselves, but in integrating the library with
the needed lemmas or, even worse, revising, cleaning or generalizing already proved
statements (hence, with no clear trace, in size, of the work that was done). So,
any measure must be taken with the due caution. As a really rough estimation,
our whole contribution to the Matita library was likely to be around 4-5000 lines of
script code, for an effort in time of about 150-200 hours. That makes 2-3 minutes
per (script) line, and an average of 250-300 minutes for each line of the source math-
ematical text. The former datum is particularly impressive, and it is obviously the
main obstacle towards a larger diffusion of automatic provers in the mathematical
community. Most of the research effort in the area of formalized reasoning is fi-
nally aimed to reduce this cost; hence, inspite of the fact that its measure is clearly
very sensible to the nature of the mathematical text being formalized, this value
provides an interesting estimate of the state of the art.
   Similarly, it is not so easy to compare the dimension of our development with
that in [6] due to the different organization of the subjects. This is a tentative
reconstruction:

                                                Journal of Formal Reasoning Vol. 1, No. 1, 2008.
16     ·     A. Asperti and C. Armentano

                 Content         Isabelle                    Matita
                 Möbius         Mu                          moebius.ma
                 lemma           526 lines                   365 lines
                 Dirichlet       Theory Inversion (up to     dirichlet product.ma
                 convolution     mu_inversion_nat1)          520 lines
                 Inversion       714 lines                   inversion.ma
                 theorem                                     100 lines
                 Euler φ         EulerPhi (up to             totient1.ma
                 lemma           big_prop1)                  241 lines
                                 389 lines
                 Total           1629 lines                  1226 lines

                                    Fig. 1.   Matita vs. Isabelle


All “reindexing” operations for sums are contained in the file iter_p_gen, which
is 1632 lines long, but this should be compared with the 2351 lines of Isabelle’s
“Finite Sets” Theory (integrated by 200 additional lines of Avigad’s “FiniteLib”
Theory).
   The above comparison is not meant to draw conclusions about the relative ef-
ficiency of the underlying proof assistants, but only to emphasize the substantial
similarity of the two developments, that in turns presumably reflects the overall
amount of work required for writing them. At the current state of the art, the com-
plexity of formalizing the results discussed in this paper is not likely to be sensibly
reduced by any of the already available tools.
   More interesting is the comparison of the formal proof with the original mathe-
matical version. Ireland and Rosen [10] need precisely one page (36 lines) to present
all results discussed in this paper. This gives a “De Bruijn” factor of 34 for Matita
(45 for Isabelle). Even admitting that the page we considered is unusually dense,
the increase in the length of the formal version is much higher than the value of 3-4,
that looks typical of other mathematical subjects (see Wiedijk’s analysis). Growing
factors much higher than usual have been also testified in other parts of the formal
proof of the prime number theorem in Isabelle:
      “In many cases, the increase in length is dramatic: the three and a half
      pages of text associated with the proof of the error estimate translate to
      about 1600 lines, or 37 pages, of proof scripts and the five pages of text
      associated with the final part of the proof translate to about 4000 lines,
      or 89 pages of proof scripts.” [6]
Even recognizing the extreme conciseness of mathematics, we should not make the
mistake to consider it as an intrinsic quality of its language. Since the age of 6,
humans are trained 5/6 hours a week to learn the idiom of mathematics and its
methods. This training is, for most people, quite hard, and not natural at all.
The compactness of the mathematical notation and the flashing effectiveness of its
arguments must be attributed, first of all, to the interpretative ability of the human
mind and the suitable, intensive training he received (possibly joined, in a few cases,
with some geometric intuition). It is well known that imitating the intellectual
capabilities of humans is one of the most difficult tasks for computing machines,
hence it is not evident at all that the traditional mathematical language and its

Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                                  A Page in Number Theory           ·     17

explanatory style, explicitly meant for inter-human communication, should also
turn out to be immediately suitable or reusable for human-computer communication
or, even worse, for purely automatic elaboration.
   It is often heard that mathematicians would not use interactive provers for the
reason that the language and techniques adopted but the current tools are too
far from their working practice. However, computer scientists normally talk with
machines in artificial languages explicitly devised to this aim, and quite far from
natural language, or any other scientific idiom. Surely, it is much easier for a
human to learn the commands of an interactive prover, than for a machine the
cryptic arguments of mathematics. In fact, the large majority of mathematicians
are not attracted by mathematical provers since the huge cost of the formalization
is not counterbalanced by the additional features (comprising automatic checking)
offered by the current tools. If we wish to convince mathematicians of the interest
of tools supporting the automation of formal reasoning, the only possibility it to
produce, soon or later, a genuinely new result. The flyspeck project, aimed to
formalize the proof of the Kepler Conjecture [8, 12], partly goes in this direction
(even if the proof has not been devised with the help of the computer, that would be
the crucial step). A more close-to-hand goal would consist to give a new, original
proof of a known result, or to find a new, unexpected relation between different
notions. From this point of view, the weaknesses of the current systems could even
turn out to be an unexpected feature, forcing the user to look for workarounds, or
more elementary arguments. As remarked in [6]:
     The need to rewrite proofs in such a way may be frustrating, but the task
     can also be oddly enjoyable: it poses interesting puzzles, and enables
     one to better understand the relationship of the advanced mathematical
     methods to the elementary substitutes.
The authors arrive to regret that, with the progress of the systems and their libraries
this re-founding work will gradually be less demanding, losing “one good reason for
investing time in such exercises.”
  Actually, it is only desirable that interactive provers will provide in the future
more and more functionalities to support that work of re-invention of mathematics
that is the real novelty of the formal approach.

References
 [1] T.M.Apostol. Introduction to Analytic Number Theory. Springer Verlag, 1976.
 [2] A.Asperti, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli. Crafting a Proof Assistant.
     Proceedings of Types 2006: Types for Proofs and Programs. Nottingham, UK,
     April 18-21, 2006. LNCS 4502, pp. 18-32, 2007. Springer Verlag.
 [3] A.Asperti, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli. User Interaction with the
     Matita Proof Assistant. Journal of Automated Reasoning, Special Issue on
     User Interfaces for Theorem Proving, V.39, N.2, August 2007. Springer Verlag.
 [4] A.Asperti, F.Guidi, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli. A Content Based
     Mathematical Search Engine: Whelp. Proceedings of TYPES 2004 conference:
     Types for Proofs and Programs. Paris, France, December 15-18, 2004. LNCS
     3839, Springer Berlin.

                                             Journal of Formal Reasoning Vol. 1, No. 1, 2008.
18     ·     A. Asperti and C. Armentano

 [5] J.Avigad. Notes on a formalization of the prime number theorem. Carnegie
     Mellon Technical Report CMU-PHIL-163, 2004.
 [6] J.Avigad, K.Donnelly, D.Gray, P.Raff. A formally verified proof of the prime
     number theorem. To appear in the ACM Transactions on Computational Logic.
 [7] C.Ballarin. Computer Algebra and Theorem Proving. PhD Thesis. University
     of Cambridge, Computer Laboratory Technical Report n.473, 1999.
 [8] T.C.Hales. Formalizing the Proof of the Kepler Conjecture. Proceedings of
     the 17th International Conference on Theorem Proving in Higher Order Log-
     ics (TPHOLs 2004), Park City, Utah, USA, September 14-17, 2004. K.Slind,
     A.Bunker, G.Gopalakrishnan (Eds.) LNCS 3223 Springer 2004.
 [9] G.H.Hardy, E.M.Wright. An Introduction to the Theory of Numbers. Oxford
     at the Clarendon Press, 1975 (4th edition).
[10] K.Ireland, M.Rosen. A Classical Introduction to Modern Number Theory.
     Graduate Texts in Mathematics. Springer Verlag.
[11] G.J.O. Jameson. The Prime Number Theorem. London Mathematical Society.
     Student Texts 53. Cambridge University Press. 2003.
[12] D.Mackenzie. What in the Name of Euclid Is Going On Here? Science, Vol.
     307. no. 5714, pp. 1402 - 1403. March 2005.
[13] P.Rudnicki, A.Trybulec. Multivariate Polynomials with Arbitrary Number of
     Variables. Formalized Mathematics, 8, 317-332, 1999.
[14] P.Rudnicki, C.Schwarzweller, A.Trybulec. Commutative Algebra in the Mizar
     System, Journal of Symbolic Computation, vol. 32, pp. 143-169, 2001.




Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                        A Page in Number Theory          ·     19

A.   IRELAND AND ROSEN’S SOURCE PAGES




                                  Journal of Formal Reasoning Vol. 1, No. 1, 2008.
20     ·     A. Asperti and C. Armentano




Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                                        A Page in Number Theory          ·     21

B.   PROOF OF THE MÖBIUS INVERSION THEOREM
set "baseuri" "cic:/matita/Z/inversion".

include "Z/dirichlet_product.ma".
include "Z/moebius.ma".

(* moebius inversion theorem *)
theorem inversion: \forall f:nat \to Z.\forall n:nat.O < n \to
dirichlet_product moebius (sigma_div f) n = f n.
intros.
rewrite > commutative_dirichlet_product
  [apply (trans_eq ? ? (dirichlet_product (dirichlet_product f (\lambda n.Zone)) moebius n))
    [unfold dirichlet_product.
     apply eq_sigma_p1;intros
      [reflexivity
      |apply eq_f2
        [apply sym_eq.
         unfold sigma_div.
         apply dirichlet_product_one_r.
         apply (divides_b_true_to_lt_O ? ? H H2)
        |reflexivity
        ]
      ]
    |rewrite > associative_dirichlet_product
      [apply (trans_eq ? ? (dirichlet_product f (sigma_div moebius) n))
        [unfold dirichlet_product.
         apply eq_sigma_p1;intros
          [reflexivity
          |apply eq_f2
            [reflexivity
            |unfold sigma_div.
             apply dirichlet_product_one_l.
             apply (lt_times_n_to_lt x)
              [apply (divides_b_true_to_lt_O ? ? H H2)
              |rewrite > divides_to_div
                [assumption
                |apply (divides_b_true_to_divides ? ? H2)
                ]
              ]
            ]
          ]
        |apply (trans_eq ? ? (dirichlet_product f is_one n))
          [unfold dirichlet_product.
           apply eq_sigma_p1;intros
            [reflexivity
            |apply eq_f2
              [reflexivity
              |apply sigma_div_moebius.
               apply (lt_times_n_to_lt x)
                [apply (divides_b_true_to_lt_O ? ? H H2)
                |rewrite > divides_to_div
                  [assumption
                  |apply (divides_b_true_to_divides ? ? H2)
                  ]
                ]
              ]
            ]
          |apply dirichlet_product_is_one_r
          ]
        ]
      |assumption
      ]
    ]
  |assumption
  ]
qed.




                                                  Journal of Formal Reasoning Vol. 1, No. 1, 2008.
22     ·     A. Asperti and C. Armentano

C.    SOME USEFUL LEMMAS
This appendix contains the list of all lemmas used in our development concerning
properties of division, modulus, gcd, order and divide. The interest of such a listing
is to give a more precise idea of the degree of granularity of the formal proof. The
list of lemmas has been obtained automatically using the indexing functionalities
provided by Matita (see [4]).
C.1 division and modulus
 le_div            ∀n, m.O < n → m/n ≤ m
 div_n_n           ∀n.O < n → n/n = 1
 div_mod           ∀n, m.O < m → n = (n/m) ∗ m + (n mod m)
 div_plus_times ∀m, q, r : nat.r < m → (q ∗ m + r)/m = q
C.2 divides
 divides_n_n                         ∀n.n|n
 divides_to_mod_O                    ∀n, m.O < n → n|m → (m mod n) = O
 trans_divides                       ∀n, m, p.n|m → m|p → n|p
 divides_to_le                       ∀n, m.O < m → n|m → n ≤ m
 divides_to_lt_O                     ∀n, m.O < m → n|m → O < n
 divides_to_div                      ∀n, m.n|m → m/n ∗ n = m
 div_div                             ∀n, d : nat.O < n → d|n → n/(n/d) = d
 eq_times_div_div_times              ∀a, b, c : nat.O < b → c|b → a ∗ (b/c) = (a ∗ b)/c
C.3   divides b
divides is a binary property, while divides_b is its (computable) characteristic
function. We need a few lemmas relating them:
  divides_b_true_to_divides
     ∀n, m.divides b n m = true → n|m
  divides_b_false_to_not_divides
     ∀n, m.divides b n m = false → n 6 |m
  divides_to_divides_b_true
     ∀n, m.O < n → n|m → divides b n m = true
  not_divides_to_divides_b_false
     ∀n, m : nat.O < n → n 6 |m → divides b n m = false
  divides_b_true_to_lt_O
     ∀n, m.O < n → divides b m n = true → O < m
  divides_b_div_true
     ∀d, n.O < n → divides b d n = true → divides b (n/d) n = true
C.4   ord
Let us recall that (p_ord n p) returns a pair hq, ri such that n = pq r and p does
not divide r. The functions ord and ord_rem are respectively the first and second
projection of p_ord.




Journal of Formal Reasoning Vol. 1, No. 1, 2008.
                                            A Page in Number Theory           ·     23

 p_ord_exp1
    ∀p, n, q, r.O < p → p 6 |r → n = pq ∗ r → p ord n p = hq, ri
 not_divides_to_p_ord_O
    ∀n, i.(nth prime i) 6 |n → p ord n (nth prime i) = hO, ni
 p_ord_to_not_eq_O
    ∀n, i, q, r.1 < n → p ord n (nth prime i) = hq, ri → r 6= O
 divides_to_le_ord
    ∀p, n, m : nat.O < n → O < m → prime p → n|m → ord n p ≤ ord m p
 exp_ord
    ∀p, n.1 < p → O < n → n = p( ord n p) ∗ (ord rem n p)
 lt_O_ord_rem
    ∀p, n.1 < p → O < n → O < ord rem n p
C.5   max prime factor
The max_prime_factor function has been abbreviated here as mpf for editorial
reasons.
 divides_mpf_n
     ∀n.1 < n → nth prime(mpf n)|n
 divides_to_mpf1
     ∀n, m.O < n → O < m → n|m → mpf n ≤ mpf m
 p_ord_to_lt_mpf1
     ∀n, p, q, r.O < n →
        mpf n ≤ i → hq, ri = p ord n (nth prime i) → 1 < r → mpf r < i
 lt_mpf_to_not_divides
     ∀n, i.O < n → n = 1 ∨ mpf n < i → (nth prime i 6 |n)
 eq_p_mpf
     ∀n, p, r.O < n → O < r →
        r = 1 ∨ (mpf r) < i → i = mpf (r ∗ (nth prime i)n )

C.6   greatest common divisor (gcd)
 divides_gcd_n
    ∀n, m.gcd n m|n
 divides_gcd_m
    ∀n, m.gcd n m|m
 sym_gcd
    ∀n, m : nat.gcd n m = gcd m n
 eq_gcd_times_times_times_gcd
    ∀a, b, c : nat.(gcd (c ∗ a) (c ∗ b)) = c ∗ (gcd a b)
 eq_gcd_div_div_div_gcd
    ∀a, b, m : nat.O < m → m|a → m|b → gcd (a/m) (b/m) = (gcd a b)/m
 divides_times_to_divides_div_gcd
    ∀a, b, c : nat.a|(b ∗ c) → (a/(gcd a b))|c




                                       Journal of Formal Reasoning Vol. 1, No. 1, 2008.
