This document is a section of formal elementary number theory leading up to a complete proof of the fundamental theorem of arithmetic. On the way to this result a large number of simple facts about integer division, prime numbers, greatest common divisors, and the product function, $\prod_{i=1}^{m}a(i)$, are developed. The entire section is written in the formal logic of PL/CV2, and the proof was checked by the PL/CV2 Proof Checker on an IBM 370/168. Readers familiar with the syntax of a high level programming language, like PL/I, and accustomed to highly symbolic mathematical proofs should be able to read this document as a specimen of extremely formal and rigorous mathematics. The following remarks about PL/CV2 notation will simplify reading. 1. The PROCESS line indicates the beginning of PL/I executable text, the THEOREM line indicates the beginning of purely declarative text. 2. All proof text is written between PL/I comment delimiters of the form //.../ or /#...#/ depending on context. 3. For the built-in PL/I functions ABS, MOD, SIGN, MAX, MIN, EXP, DIVISION (/) only the properties of the functions are listed, in Section 0 called BUILT-IN FUNCTIONS. No proofs of these properties are supplied (because the operations are provided by the system). Thus proved propositions appear starting in Section 1 (at line 0036). 4. In the listing the negation sign is written ^, thus B ^= 0 reads "B not equal to zero". The PL/I symbol for "or" is the vertical bar, thus line 0037 TRI : B less than 0|B=0|B greater than 0 is labeled by TRI (for trichotomy) and means B is less than or equal to 0 or greater than 0. The justification... BY ARITH... indicates that the conclusion follows from simple arithmetic reasoning, provided by the system, from the list of hypotheses. 5. Every PL/CV2 procedure, such as LOG at line 0049, begins with an ASSUME statement, telling what is assumed about the input, and with an ATTAIN statement telling what will be proved about it. Also every procedure is proved to terminate. In the case of recursive procedures, the termination proof begins with the line ARBITRARY (integer variable) WHERE (conditon) (see line 0053). It is proved that this integer variable decreases on any recursive call.