## Divisibility is Transitive

####

This example is taken from the elementary number theory of the natural numbers.
It contains just one definition and one theorem.
The definition is that of divisibility. The big V is an
existence quantifier. The definition states that a divides
b if and only if there is a natural number k which multiplied by a yields b.
The theorem states that divisibility is transitive.

Notes 1 and 2 of the proof state the hypotheses of the theorem as
givens. Givens are justified with a G. Note 3 is an assignment statement.
Assignment statements are justified with an S. It sets k₁ to a natural
number which multiplied by a yields b.
Similarly in Note 4 we pick a k₂ which multiplied by b yields c.
In Note 5 we let k be the product of k₁ and k₂
and in Notes 6 and 7 we verify that k is also a natural number.
The proof of Note 6 appeals to
Definition 1.1 and to Note 1.
Checking Note 6 requires a reference to Theorem 40.44 in
the Common Notions file
which says that the product of two natural numbers is a natural number.

Note 9 then uses the associativity of multiplication and the
k defined in Note 5 to get c equal to k times a. The reference to the associativity
of multiplication is 039.7 and refers to Theorem 39.7 of in the common notions file.
The H followed by .1 and .2 in the
QED reference forms an inference from the two givens to Note 9, which constitutes
the theorem to be proven.