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.