Let Xbeanemptyset.ObservethatcardXisempty. Onecancheckthateverybinaryrelationwhichisnatural.pdf

FORMALIZED MATHEMATICS Volume 12, Number 2, 2004 University of Bia?ystok Fundamental Theorem of Arithmetic 1 Artur Korni?owicz University of Bia?ystok Piotr Rudnicki University of Alberta Edmonton Summary. We formalize the notion of the prime-power factorization of a natural number and prove the Fundamental Theorem of Arithmetic. We prove also how prime-power factorization can be used to compute: products, quotients, powers, greatest common divisors and least common multiples. MML Identifier: NAT 3. The notation and terminology used in this paper are introduced in the following papers: [25], [27], [12], [7], [3], [4], [1], [24], [13], [2], [19], [18], [28], [8], [9], [6], [16], [15], [11], [26], [22], [23], [10], [14], [20], [5], [21], and [17]. 1. Preliminaries We follow the rules: a, b, n denote natural numbers, r denotes a real number, and f denotes a finite sequence of elements of R. Let X be an empty set. Observe that cardX is empty. One can check that every binary relation which is natural-yielding is also real-yielding. Let us mention that there exists a finite sequence which is natural-yielding. Let a be a non empty natural number and let b be a natural number. Observe that ab is non empty. One can verify that every prime number is non empty. In the sequel p denotes a prime number. One can verify that Prime is infinite. The following propositions are true: 1A. Korni?owicz has been supported by a post-doctoral fellowship at Shinshu University, Nagano, Japan. P. Rudnicki has been supported by NSERC Grant OGP9207. 179 c? 2004 University of Bia?ystok ISSN 1426–2630 180 artur korni?owicz and piotr rudnicki (1) For all natural numbers a, b, c, d such that a | c and b | d holds a ·b | c ·d. (2) If 1 a, then b ? ab. (3) If a 6= 0, then n | na. (4) For all natural numbers i, j, m, n such that i j and mj | n holds mi+1 | n. (5) If p | ab, then p | a. (6) For every prime number a such that a | pb holds a = p. (7) For every finite sequence f of elements of N such that