Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### 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;

Back to top