The abstract of the Mizar article:

Pythagorean Triples

by

Freek Wiedijk

Received August 26, 2001

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;