:: Pythagorean triples :: by Freek Wiedijk :: :: Received August 26, 2001 :: Copyright (c) 2001-2021 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, QUANTAL1; 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 Number; attr n is square means :: PYTHTRIP:def 3 ex m being Nat st n = m^2; end; registration cluster square -> natural for Number; 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; notation let X; synonym X is degenerate for X is with_zero; end; theorem :: PYTHTRIP:13 n > 2 implies ex X st X is non degenerate & n in X; definition ::$CD 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;