Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users

### Pythagorean Triples

by
Freek Wiedijk

MML identifier: PYTHTRIP
[ Mizar article, MML identifier index ]

```environ

vocabulary INT_1, ARYTM_3, FILTER_0, ARYTM, SQUARE_1, ORDINAL2, MATRIX_2,
NAT_1, ARYTM_1, FINSET_1, FUNCT_1, RELAT_1, ORDINAL1, BOOLE, ABSVALUE,
INT_2, TARSKI, PYTHTRIP;
notation TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL2, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, INT_1, INT_2, NAT_1, SQUARE_1, ABIAN, PEPIN, DOMAIN_1,
GROUP_1, RELAT_1, FUNCT_1, LIMFUNC1, ORDINAL1;
constructors REAL_1, INT_2, NAT_1, ABIAN, PEPIN, DOMAIN_1, GROUP_1, LIMFUNC1,
MEMBERED;
clusters FINSET_1, SUBSET_1, NAT_LAT, ABIAN, INT_1, NAT_1, XREAL_0, MEMBERED,
NUMBERS, ORDINAL2;
requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;

begin :: relative primeness

reserve a,a',b,b',c,c',k,k',m,m',m'',m''',n,n',n'',n''',mn,mn',mn'',p,p'
for Nat;
reserve i,i' for Integer;

definition
let m,n;
redefine pred m,n are_relative_prime means
:: PYTHTRIP:def 1
for k st k divides m & k divides n holds k = 1;
end;

definition
let m,n;
redefine pred m,n are_relative_prime means
:: PYTHTRIP:def 2
for p being prime Nat holds not (p divides m & p divides n);
end;

begin :: squares

definition
let n be number;
attr n is square means
:: PYTHTRIP:def 3
ex m st n = m^2;
end;

definition
cluster square -> natural number;
end;

definition
let n be Nat;
cluster n^2 -> square;
end;

definition
cluster even square Nat;
end;

definition
cluster odd square Nat;
end;

definition
cluster even square number;
end;

definition
cluster odd square number;
end;

definition
let m,n be square number;
cluster m*n -> square;
end;

theorem :: PYTHTRIP:1
m*n is square & m,n are_relative_prime implies m is square & n is square;

definition
let i be even Integer;
cluster i^2 -> even;
end;

definition
let i be odd Integer;
cluster i^2 -> odd;
end;

theorem :: PYTHTRIP:2
i is even iff i^2 is even;

theorem :: PYTHTRIP:3
i is even implies i^2 mod 4 = 0;

theorem :: PYTHTRIP:4
i is odd implies i^2 mod 4 = 1;

definition
let m,n be odd square number;
cluster m + n -> non square;
end;

theorem :: PYTHTRIP:5
m^2 = n^2 implies m = n;

theorem :: PYTHTRIP:6
m divides n iff m^2 divides n^2;

begin :: distributive law for hcf

theorem :: PYTHTRIP:7
m divides n or k = 0 iff k*m divides k*n;

theorem :: PYTHTRIP:8
(k*m) hcf (k*n) = k*(m hcf n);

begin :: unbounded sets are infinite

theorem :: PYTHTRIP:9
for X being set st for m ex n st n >= m & n in X holds X is infinite;

begin :: Pythagorean triples

theorem :: PYTHTRIP:10
a,b are_relative_prime implies a is odd or b is odd;

theorem :: PYTHTRIP:11
a^2 + b^2 = c^2 & a,b are_relative_prime & a is odd implies
ex m,n st m <= n & a = n^2 - m^2 & b = 2*m*n & c = n^2 + m^2;

theorem :: PYTHTRIP:12
a = n^2 - m^2 & b = 2*m*n & c = n^2 + m^2 implies a^2 + b^2 = c^2;

definition
mode Pythagorean_triple -> Subset of NAT means
:: PYTHTRIP:def 4
ex a,b,c st a^2 + b^2 = c^2 & it = { a,b,c };
end;

reserve X for Pythagorean_triple;

definition
cluster -> finite Pythagorean_triple;
end;

definition
redefine mode Pythagorean_triple means
:: PYTHTRIP:def 5
ex k,m,n st m <= n & it = { k*(n^2 - m^2), k*(2*m*n), k*(n^2 + m^2) };
end;

definition
let X;
attr X is degenerate means
:: PYTHTRIP:def 6
0 in X;
end;

theorem :: PYTHTRIP:13
n > 2 implies ex X st X is non degenerate & n in X;

definition
let X;
attr X is simplified means
:: PYTHTRIP:def 7
for k st for n st n in X holds k divides n holds k = 1;
end;

definition
let X;
redefine attr X is simplified means
:: PYTHTRIP:def 8
ex m,n st m in X & n in X & m,n are_relative_prime;
end;

theorem :: PYTHTRIP:14
n > 0 implies ex X st X is non degenerate & X is simplified & 4*n in X;

definition
cluster non degenerate simplified Pythagorean_triple;
end;

theorem :: PYTHTRIP:15
{ 3,4,5 } is non degenerate simplified Pythagorean_triple;

theorem :: PYTHTRIP:16
{ X: X is non degenerate & X is simplified } is infinite;

```