\input utility.tdf \input common.tdf \input divides.tdf \centerline{\bf{Divisibility is Transitive}} $\nats$ is the set of natural numbers. \chap{1. Divisibility} First define divisibility as follows: $a$ divides $b$ if and only if for some natural number $k$, $b$ is the product of $k$ and $a$. \noindent{}Definition: \prop 1.1 $((a \divides b) \Iff \Some k \in \nats (b = k \cdot a))$ \By D That divisibility is transitive is stated in the \noindent{}Theorem: \prop 1.2 $(a \divides b \And b \divides c \c a \divides c)$ \lineb Proof: We begin by taking the two hypotheses as givens: \note 1 $(a\divides b)$ \By G \note 2 $(b \divides c)$ \By G \lineb Then we let $k_1$ and $k_2$ be natural numbers asserted to exist by Definition 1.1. \note 3 $(k_1 \ident \an k \in \nats (b = k \cdot a))$ \By S \note 4 $(k_2 \ident \an k \in \nats (c = k \cdot b))$ \By S \lineb And then we let $k$ be their product, \note 5 $(k \ident (k_2 \cdot k_1))$ \By S \lineb and run down the fact that it is also a natural number: \note 6 $(\true \c \Some k \in \nats (b = k \cdot a)$ \By 1.1;.1 \linec $\c k_1 \in \nats)$ \By .3 \note 7 $(\true \c \Some k \in \nats (c = k \cdot b)$ \By 1.1;.2 \linec $\c k_2 \in \nats$ \By .4 \linec $\c k_2\cdot k_1 \in \nats$ \By 040.44;.6 \linec $\c k \in \nats)$ \By .5 \lineb We then use the definitions of $k_1$ and $k_2$ again to establish that $k$ satisfies Definition 1.1. \note 8 $(\true \c \Some k \in \nats (b = k \cdot a)$ \By 1.1;.1 \linec $\c b = k_1 \cdot a)$ \By .3 \note 9 $ (\true \c \Some k \in \nats (c = k \cdot b)$ \By 1.1;.2 \linec $\c c = k_2 \cdot b$ \By .4 \lined $ \ident k_2 \cdot (k_1 \cdot a)$ \By .8 \lined $\ident (k_2 \cdot k_1) \cdot a$ \By 039.7 \lined $\ident k \cdot a$ \By .5 \linec $\c a \divides c)$ \By 1.1; .7 \Bye .9 H .1, .2 \lineb The references 039.7 and 040.44 are to 39.7 and 40.44 respectively in the common notions file. \end