Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

**Freek Wiedijk**- University of Nijmegen

- A Pythagorean triple is a set of positive integers $\{ a,b,c \}$ with $a^2 + b^2 = c^2$. We prove that every Pythagorean triple is of the form $$a = n^2 - m^2 \qquad b = 2mn \qquad c = n^2 + m^2$$ or is a multiple of such a triple. Using this characterization we show that for every $n > 2$ there exists a Pythagorean triple $X$ with $n\in X$. Also we show that even the set of {\em simplified\/} Pythagorean triples is infinite.

- Relative Primeness
- Squares
- Distributive Law for HCF
- Unbounded Sets are Infinite
- Pythagorean Triples

- [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek.
The ordinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Grzegorz Bancerek.
Sequences of ordinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Agata Darmochwal.
Finite sets.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Yoshinori Fujisawa, Yasushi Fuwa, and Hidetaka Shimizu.
Public-key cryptography and Pepin's test for the primality of Fermat numbers.
*Journal of Formalized Mathematics*, 10, 1998. - [7]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [8]
Rafal Kwiatek and Grzegorz Zwara.
The divisibility of integers and integer relatively primes.
*Journal of Formalized Mathematics*, 2, 1990. - [9]
Piotr Rudnicki and Andrzej Trybulec.
Abian's fixed point theorem.
*Journal of Formalized Mathematics*, 9, 1997. - [10]
Andrzej Trybulec.
Domains and their Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [11]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [12]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [13]
Andrzej Trybulec and Czeslaw Bylinski.
Some properties of real numbers operations: min, max, square, and square root.
*Journal of Formalized Mathematics*, 1, 1989. - [14]
Michal J. Trybulec.
Integers.
*Journal of Formalized Mathematics*, 2, 1990. - [15]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]