:: Pythagorean triples
:: by Freek Wiedijk
::
:: Received August 26, 2001
:: Copyright (c) 2001-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, INT_1, NAT_1, ARYTM_3, INT_2, CARD_1,
XXREAL_0, ORDINAL1, SQUARE_1, ABIAN, RELAT_1, ARYTM_1, FINSET_1, FUNCT_1,
XBOOLE_0, COMPLEX1, TARSKI, PYTHTRIP;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, FINSET_1, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, XXREAL_0, INT_1, INT_2, NAT_1, NAT_D, SQUARE_1, ABIAN,
PEPIN, DOMAIN_1, RELAT_1, FUNCT_1;
constructors DOMAIN_1, REAL_1, NAT_1, NAT_D, LIMFUNC1, ABIAN, PEPIN, VALUED_1;
registrations ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, NEWTON,
ABIAN, XBOOLE_0, RELAT_1;
requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
begin :: relative primeness
reserve a,b,c,k,k9,m,n,n9,p,p9 for Element of NAT;
reserve i,i9 for Integer;
definition
let m,n be Nat;
redefine pred m,n are_coprime means
:: PYTHTRIP:def 1
for k be Nat st k divides m & k divides n holds k = 1;
end;
definition
let m,n be Nat;
redefine pred m,n are_coprime means
:: PYTHTRIP:def 2
for p being prime Nat holds not (p divides m & p divides n);
end;
begin :: squares
definition
let n be object;
attr n is square means
:: PYTHTRIP:def 3
ex m being Nat st n = m^2;
end;
registration
cluster square -> natural for object;
end;
registration
let n be Nat;
cluster n^2 -> square;
end;
registration
cluster even square for Element of NAT;
end;
registration
cluster odd square for Element of NAT;
end;
registration
cluster even square for Integer;
end;
registration
cluster odd square for Integer;
end;
registration
let m,n be square object;
cluster m*n -> square;
end;
theorem :: PYTHTRIP:1
m*n is square & m,n are_coprime implies m is square & n is square;
registration
let i be Integer;
cluster i^2 -> integer;
end;
registration
let i be even Integer;
cluster i^2 -> even;
end;
registration
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;
registration
let m,n be odd square Integer;
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 gcd
theorem :: PYTHTRIP:7
m divides n or k = 0 iff k*m divides k*n;
theorem :: PYTHTRIP:8
(k*m) gcd (k*n) = k*(m gcd 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_coprime implies a is odd or b is odd;
theorem :: PYTHTRIP:11
a^2 + b^2 = c^2 & a,b are_coprime & 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;
registration
cluster -> finite for Pythagorean_triple;
end;
definition
::$N Formula for Pythagorean Triples
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_coprime;
end;
theorem :: PYTHTRIP:14
n > 0 implies ex X st X is non degenerate & X is simplified & 4* n in X;
registration
cluster non degenerate simplified for 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;