:: Pythagorean triples :: by Freek Wiedijk :: :: Received August 26, 2001 :: Copyright (c) 2001-2018 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; definitions ORDINAL1, INT_1, INT_2, ABIAN; equalities SQUARE_1, RELAT_1, ORDINAL1, CARD_1; expansions INT_1, INT_2, ABIAN; theorems SQUARE_1, NAT_1, INT_2, WSIERP_1, EULER_2, ABIAN, EULER_1, INT_1, ENUMSET1, FINSET_1, TARSKI, RELAT_1, FUNCT_1, ORDINAL1, ZFMISC_1, XBOOLE_0, XCMPLX_1, NEWTON, XREAL_1, COMPLEX1, XXREAL_0, PREPOWER, NAT_D, AFINSQ_1; schemes NAT_1; 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 for k be Nat st k divides m & k divides n holds k = 1; compatibility proof hereby assume m,n are_coprime; then A1: m gcd n = 1; let k be Nat; assume k divides m & k divides n; then k divides 1 by A1,NAT_D:def 5; hence k = 1 by WSIERP_1:15; end; assume for k be Nat st k divides m & k divides n holds k = 1; then A2: for k be Nat st k divides m & k divides n holds k divides 1; 1 divides m & 1 divides n by NAT_D:6; hence m gcd n = 1 by A2,NAT_D:def 5; end; end; definition let m,n be Nat; redefine pred m,n are_coprime means for p being prime Nat holds not (p divides m & p divides n); compatibility proof hereby assume A1: m,n are_coprime; let p be prime Nat; assume p divides m & p divides n; then p = 1 by A1; hence contradiction by INT_2:def 4; end; assume A2: for p being prime Nat holds not (p divides m & p divides n); let k be Nat; assume A3: k divides m & k divides n; per cases by NAT_1:25; suppose k = 0; then m = 0 & n = 0 by A3; hence thesis by A2,INT_2:28,NAT_D:6; end; suppose k = 1; hence thesis; end; suppose k > 1; then k >= 1+1 by NAT_1:13; then consider p such that A4: p is prime and A5: p divides k by INT_2:31; reconsider p9 = p as prime Element of NAT by A4; p9 divides m & p9 divides n by A3,A5,NAT_D:4; hence thesis by A2; end; end; end; begin :: squares definition let n be Number; attr n is square means :Def3: ex m being Nat st n = m^2; end; registration cluster square -> natural for Number; coherence; end; registration let n be Nat; cluster n^2 -> square; coherence; end; registration cluster even square for Element of NAT; existence proof take 0; 0 = 2*0^2; hence thesis; end; end; registration cluster odd square for Element of NAT; existence proof take 1; 1^2 = 2*0 + 1; hence thesis; end; end; registration cluster even square for Integer; existence proof take the even square Element of NAT; thus thesis; end; end; registration cluster odd square for Integer; existence proof take the odd square Element of NAT; thus thesis; end; end; registration let m,n be square object; cluster m*n -> square; coherence proof consider n9 being Nat such that A1: n = n9^2 by Def3; consider m9 being Nat such that A2: m = m9^2 by Def3; m*n = (m9*n9)^2 by A2,A1; hence thesis; end; end; theorem Th1: m*n is square & m,n are_coprime implies m is square & n is square proof defpred P[Nat] means for m,n st m*n = \$1 & m*n is square & m,n are_coprime holds m is square & n is square; A1: for mn being Nat st for k being Nat st k < mn holds P[k] holds P[mn] proof let mn be Nat; assume A2: for k be Nat st k < mn for m,n st m*n = k & m*n is square & m,n are_coprime holds m is square & n is square; let m,n; assume A3: m*n = mn; assume m*n is square; then consider mn9 being Nat such that A4: mn = mn9^2 by A3; assume A5: m,n are_coprime; then A6: m gcd n = 1^2; per cases by A3,NAT_1:25; suppose A7: m*n = 0; hereby per cases by A7,XCMPLX_1:6; suppose m = 0^2; hence thesis by A6,NEWTON:52; end; suppose n = 0^2; hence thesis by A6,NEWTON:52; end; end; end; suppose m*n = 1^2; hence thesis by NAT_1:15; end; suppose A8: mn > 1; then mn >= 1 + 1 by NAT_1:13; then consider p9 such that A9: p9 is prime and A10: p9 divides mn by INT_2:31; reconsider p = p9 as prime Element of NAT by A9; p divides mn9 by A4,A10,NEWTON:80; then consider mn99 be Nat such that A11: mn9 = p*mn99 by NAT_D:def 3; A12: p > 1 by INT_2:def 4; then p*p > p by XREAL_1:155; then A13: p*p > 1 by A12,XXREAL_0:2; A14: n > 0 by A3,A8; A15: p <> 0 by INT_2:def 4; A16: m > 0 by A3,A8; hereby per cases by A3,A10,NEWTON:80; suppose A17: p divides m; then A18: not p divides n by A5; consider m9 be Nat such that A19: m = p*m9 by A17,NAT_D:def 3; p*(m9*n) = p*(p*(mn99*mn99)) by A3,A4,A11,A19; then m9*n = p*(mn99*mn99) by A15,XCMPLX_1:5; then p divides m9*n; then p divides m9 by A18,NEWTON:80; then consider m99 be Nat such that A20: m9 = p*m99 by NAT_D:def 3; reconsider m99 as Element of NAT by ORDINAL1:def 12; A21: m99 <> 0 by A3,A8,A19,A20; p*(p*(m99*n)) = p*(p*(mn99*mn99)) by A3,A4,A11,A19,A20; then p*(m99*n) = p*(mn99*mn99) by A15,XCMPLX_1:5; then A22: m99*n = mn99^2 by A15,XCMPLX_1:5; m = (p*p)*m99 by A19,A20; then m99 divides m; then m99 gcd n = 1 by A6,WSIERP_1:16; then A23: m99,n are_coprime; m = (p*p)*m99 by A19,A20; then 1*m99 < m by A13,A21,XREAL_1:98; then A24: m99*n < mn by A3,A14,A21,XREAL_1:98; then m99 is square by A2,A22,A23; then consider m999 being Nat such that A25: m99 = m999^2; m = (p*m999)^2 by A19,A20,A25; hence thesis by A2,A24,A22,A23; end; suppose A26: p divides n; then A27: not p divides m by A5; consider n9 be Nat such that A28: n = p*n9 by A26,NAT_D:def 3; p*(m*n9) = p*(p*(mn99*mn99)) by A3,A4,A11,A28; then m*n9 = p*(mn99*mn99) by A15,XCMPLX_1:5; then p divides m*n9; then p divides n9 by A27,NEWTON:80; then consider n99 be Nat such that A29: n9 = p*n99 by NAT_D:def 3; reconsider n99 as Element of NAT by ORDINAL1:def 12; A30: n99 <> 0 by A3,A8,A28,A29; p*(p*(m*n99)) = p*(p*(mn99*mn99)) by A3,A4,A11,A28,A29; then p*(m*n99) = p*(mn99*mn99) by A15,XCMPLX_1:5; then A31: m*n99 = mn99^2 by A15,XCMPLX_1:5; n = (p*p)*n99 by A28,A29; then n99 divides n; then m gcd n99 = 1 by A6,WSIERP_1:16; then A32: m,n99 are_coprime; n = (p*p)*n99 by A28,A29; then 1*n99 < n by A13,A30,XREAL_1:98; then A33: m*n99 < mn by A3,A16,A30,XREAL_1:98; then n99 is square by A2,A31,A32; then consider n999 being Nat such that A34: n99 = n999^2; n = (p*n999)^2 by A28,A29,A34; hence thesis by A2,A33,A31,A32; end; end; end; end; for mn being Nat holds P[mn] from NAT_1:sch 4(A1); hence thesis; end; registration let i be Integer; cluster i^2 -> integer; coherence; end; registration let i be even Integer; cluster i^2 -> even; coherence; end; registration let i be odd Integer; cluster i^2 -> odd; coherence; end; theorem i is even iff i^2 is even; theorem Th3: i is even implies i^2 mod 4 = 0 proof given i9 such that A1: i = 2*i9; i^2 = 4*(i9^2) + 0 by A1; hence i^2 mod 4 = (0 qua Integer) mod 4 by EULER_1:12 .= 0 by NAT_D:24; end; theorem Th4: i is odd implies i^2 mod 4 = 1 proof assume i is odd; then consider i9 such that A1: i = 2*i9 + 1 by ABIAN:1; i^2 = 4*(i9^2 + i9) + 1 by A1; hence i^2 mod 4 = (1 qua Integer) mod 4 by EULER_1:12 .= 1 by NAT_D:24; end; registration let m,n be odd square Integer; cluster m + n -> non square; coherence proof reconsider n99 = n as Element of NAT by ORDINAL1:def 12; reconsider m99 = m as Element of NAT by ORDINAL1:def 12; consider m9 being Nat such that A1: m = m9^2 by Def3; A2: m9 is odd by A1; consider n9 being Nat such that A3: n = n9^2 by Def3; A4: n9 is odd by A3; A5: (m99 + n99) mod 4 = ((m99 mod 4) + (n99 mod 4)) mod 4 by EULER_2:6 .= (1 + (n99 mod 4)) mod 4 by A1,A2,Th4 .= (1 + 1) mod 4 by A3,A4,Th4 .= 2 by NAT_D:24; hereby assume m + n is square; then consider mn9 being Nat such that A6: m + n = mn9^2; mn9 is even by A6; hence contradiction by A5,A6,Th3; end; end; end; theorem Th5: m^2 = n^2 implies m = n proof assume A1: m^2 = n^2; per cases by A1,SQUARE_1:40; suppose m = n; hence thesis; end; suppose A2: m = -n; then m = -0; hence thesis by A2; end; end; theorem Th6: m divides n iff m^2 divides n^2 proof defpred P[Nat] means for n holds \$1 divides n iff \$1^2 divides n^2; A1: for m being Nat st for k being Nat st k < m holds P[k] holds P[m] proof let m be Nat; assume A2: for k being Nat st k < m for n holds k divides n iff k^2 divides n ^2; let n; hereby assume m divides n; then consider k9 be Nat such that A3: n = m*k9 by NAT_D:def 3; n^2 = (m^2)*(k9^2) by A3; hence m^2 divides n^2; end; assume A4: m^2 divides n^2; per cases by NAT_1:25; suppose m = 0; then n^2 = 0 by A4; then n = 0 by XCMPLX_1:6; hence thesis by NAT_D:6; end; suppose m = 1; hence thesis by NAT_D:6; end; suppose A5: m > 1; consider k9 be Nat such that A6: n^2 = (m^2)*k9 by A4,NAT_D:def 3; m >= 1 + 1 by A5,NAT_1:13; then consider p9 such that A7: p9 is prime and A8: p9 divides m by INT_2:31; reconsider p = p9 as prime Element of NAT by A7; consider m9 be Nat such that A9: m = p*m9 by A8,NAT_D:def 3; reconsider m9 as Element of NAT by ORDINAL1:def 12; m^2 = (m*m9)*p by A9; then p divides m^2; then p divides n^2 by A4,NAT_D:4; then p divides n by NEWTON:80; then consider n9 be Nat such that A10: n = p*n9 by NAT_D:def 3; A11: p > 1 by INT_2:def 4; then A12: p^2 > 0 by SQUARE_1:12; reconsider n9 as Element of NAT by ORDINAL1:def 12; (p^2)*(n9^2) = (p^2)*((m9^2)*k9) by A9,A10,A6; then n9^2 = (m9^2)*k9 by A12,XCMPLX_1:5; then A13: m9^2 divides n9^2; p*m9 > 1*m9 by A5,A9,A11,XREAL_1:98; then m9 divides n9 by A2,A9,A13; then consider k be Nat such that A14: n9 = m9*k by NAT_D:def 3; n = m*k by A9,A10,A14; hence thesis; end; end; for m being Nat holds P[m] from NAT_1:sch 4(A1); hence thesis; end; begin :: distributive law for gcd theorem Th7: m divides n or k = 0 iff k*m divides k*n proof hereby assume A1: m divides n or k = 0; per cases by A1; suppose m divides n; then consider k9 be Nat such that A2: n = m*k9 by NAT_D:def 3; k*n = (k*m)*k9 by A2; hence k*m divides k*n; end; suppose k = 0; hence k*m divides k*n; end; end; assume A3: k*m divides k*n; now consider k9 be Nat such that A4: k*n = k*m*k9 by A3,NAT_D:def 3; assume A5: k <> 0; k*n = k*(m*k9) by A4; then n = m*k9 by A5,XCMPLX_1:5; hence m divides n; end; hence thesis; end; theorem Th8: (k*m) gcd (k*n) = k*(m gcd n) proof per cases; suppose A1: k <> 0; k divides k*m & k divides k*n; then k divides (k*m) gcd (k*n) by NAT_D:def 5; then consider k9 be Nat such that A2: (k*m) gcd (k*n) = k*k9 by NAT_D:def 3; reconsider k9 as Element of NAT by ORDINAL1:def 12; now k*k9 divides k*m by A2,NAT_D:def 5; hence k9 divides m by A1,Th7; k*k9 divides k*n by A2,NAT_D:def 5; hence k9 divides n by A1,Th7; let p be Nat; reconsider p9=p as Element of NAT by ORDINAL1:def 12; assume p divides m & p divides n; then k*p9 divides k*m & k*p9 divides k*n by Th7; then k*p divides k*k9 by A2,NAT_D:def 5; then p9 divides k9 by A1,Th7; hence p divides k9; end; hence thesis by A2,NAT_D:def 5; end; suppose k = 0; hence thesis by NEWTON:52; end; end; begin :: unbounded sets are infinite theorem Th9: for X being set st for m ex n st n >= m & n in X holds X is infinite proof let X be set; A1: now let f be Function; defpred P[Nat] means ex m st for n st n >= m holds not n in f.:\$1; A2: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume ex m st for n st n >= m holds not n in f.:k; then consider m such that A3: for n st n >= m holds not n in f.:k; Segm(k + 1) = Segm k \/ { k } by AFINSQ_1:2; then A4: f.:(k + 1) = f.:k \/ Im(f,k) by RELAT_1:120; per cases; suppose A5: k in dom f & f.k in NAT; then reconsider m9 = f.k as Element of NAT; take max(m,m9 + 1); let n; assume A6: n >= max(m,m9 + 1); then A7: not n in f.:k by A3,XXREAL_0:30; n >= m9 + 1 by A6,XXREAL_0:30; then n <> m9 by NAT_1:13; then A8: not n in { m9 } by TARSKI:def 1; f.:(k + 1) = f.:k \/ { m9 } by A4,A5,FUNCT_1:59; hence thesis by A7,A8,XBOOLE_0:def 3; end; suppose A9: k in dom f & not f.k in NAT; take m; set m9 = f.k; let n; n <> m9 by A9; then A10: not n in { m9 } by TARSKI:def 1; assume n >= m; then A11: not n in f.:k by A3; f.:(k + 1) = f.:k \/ { m9 } by A4,A9,FUNCT_1:59; hence thesis by A11,A10,XBOOLE_0:def 3; end; suppose not k in dom f; then A12: dom f misses { k } by ZFMISC_1:50; take m; let n; assume A13: n >= m; Im(f,k) = f.:(dom f /\ { k }) by RELAT_1:112 .= f.:{} by A12,XBOOLE_0:def 7 .= {}; hence thesis by A3,A4,A13; end; end; A14: P[0] proof take 0; let n such that n >= 0; thus thesis; end; thus for k being Nat holds P[k] from NAT_1:sch 2(A14,A2); end; now assume X is finite; then consider f being Function such that A15: rng f = X and A16: dom f in omega by FINSET_1:def 1; reconsider k = dom f as Element of NAT by A16; f.:k = X by A15,RELAT_1:113; hence ex m st for n st n >= m holds not n in X by A1; end; hence thesis; end; begin :: Pythagorean triples theorem a,b are_coprime implies a is odd or b is odd; theorem Th11: 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 proof assume A1: a^2 + b^2 = c^2; assume A2: a,b are_coprime; assume a is odd; then reconsider a9 = a as odd Element of NAT; b is even proof assume b is odd; then reconsider b9 = b as odd Element of NAT; a9^2 + b9^2 = c^2 by A1; hence contradiction; end; then reconsider b9 = b as even Element of NAT; a9^2 + b9^2 = c^2 by A1; then reconsider c9 = c as odd Element of NAT; 2 divides c9-a9 by ABIAN:def 1; then consider i such that A3: c9 - a9 = 2*i; c^2 >= a^2 + 0 by A1,XREAL_1:6; then c >= a by SQUARE_1:16; then 2*i >= 2*0 by A3,XREAL_1:48; then i >= 0 by XREAL_1:68; then reconsider m9 = i as Element of NAT by INT_1:3; consider n9 being Nat such that A4: c9 + a9 = 2*n9 by ABIAN:def 2; consider k9 being Nat such that A5: b9 = 2*k9 by ABIAN:def 2; reconsider n9,k9 as Element of NAT by ORDINAL1:def 12; A6: n9*m9 = ((c + a)/2)*((c - a)/2) by A4,A3 .= (b/2)^2 by A1 .= k9^2 by A5; A7: n9 + m9 = c by A4,A3; A8: n9,m9 are_coprime proof let p be prime Nat; assume that A9: p divides n9 and A10: p divides m9; reconsider p as prime Element of NAT by ORDINAL1:def 12; p divides c by A7,A9,A10,NAT_D:8; then A11: p divides c*c by NAT_D:9; p divides -m9 by A10,INT_2:10; then A12: p divides (n9 + -m9) by A9,WSIERP_1:4; then p divides a*a by A4,A3,NAT_D:9; then A13: p divides -(a*a) by INT_2:10; b*b = c*c + -(a*a) by A1; then p divides (b*b qua Integer) by A13,A11,WSIERP_1:4; then p divides b by NEWTON:80; hence contradiction by A2,A4,A3,A12; end; then n9 is square by A6,Th1; then consider n be Nat such that A14: n9 = n^2; m9 is square by A8,A6,Th1; then consider m be Nat such that A15: m9 = m^2; reconsider m,n as Element of NAT by ORDINAL1:def 12; take m,n; n9 - m9 = a by A4,A3; then m^2 <= n^2 by A14,A15,XREAL_1:49; hence m <= n by SQUARE_1:16; thus a = n^2 - m^2 by A4,A3,A14,A15; b^2 = (2^2)*(n*m)^2 by A5,A6,A14,A15,SQUARE_1:9 .= (2*m*n)^2; hence b = 2*m*n by Th5; thus thesis by A4,A3,A14,A15; end; theorem 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 :Def4: ex a,b,c st a^2 + b^2 = c^2 & it = { a,b,c }; existence proof take { 0,0,0 }; take 0,0,0; thus 0^2 + 0^2 = 0^2; thus thesis; end; end; reserve X for Pythagorean_triple; registration cluster -> finite for Pythagorean_triple; coherence proof let X; ex a,b,c st a^2 + b^2 = c^2 & X = { a,b,c } by Def4; hence thesis; end; end; definition ::\$N Formula for Pythagorean Triples redefine mode Pythagorean_triple means :Def5: ex k,m,n st m <= n & it = { k* (n^2 - m^2), k*(2*m*n), k*(n^2 + m^2) }; compatibility proof let X be Subset of NAT; hereby assume X is Pythagorean_triple; then consider a,b,c such that A1: a^2 + b^2 = c^2 and A2: X = { a,b,c } by Def4; set k = a gcd b; A3: k divides a by NAT_D:def 5; A4: k divides b by NAT_D:def 5; per cases; suppose k = 0; then A5: a = 0 & b = 0 by A3,A4; thus ex k,m,n st m <= n & X = { k*(n^2 - m^2), k*(2*m*n), k*(n^2 + m^2 ) } proof take 0,0,0; thus thesis by A1,A2,A5,XCMPLX_1:6; end; end; suppose A6: k <> 0; then A7: k*k <> 0 by XCMPLX_1:6; consider a9 be Nat such that A8: a = k*a9 by A3,NAT_D:def 3; consider b9 be Nat such that A9: b = k*b9 by A4,NAT_D:def 3; reconsider a9,b9 as Element of NAT by ORDINAL1:def 12; k*(a9 gcd b9) = k*1 by A8,A9,Th8; then a9 gcd b9 = 1 by A6,XCMPLX_1:5; then A10: a9,b9 are_coprime; c^2 = (k^2)*(a9^2 + b9^2) by A1,A8,A9; then k^2 divides c^2; then k divides c by Th6; then consider c9 be Nat such that A11: c = k*c9 by NAT_D:def 3; reconsider c9 as Element of NAT by ORDINAL1:def 12; k^2*(a9^2 + b9^2) = k^2*c9^2 by A1,A8,A9,A11; then A12: a9^2 + b9^2 = c9^2 by A7,XCMPLX_1:5; thus ex k,m,n st m <= n & X = { k*(n^2 - m^2), k*(2*m*n), k*(n^2 + m^2 ) } proof per cases by A10; suppose a9 is odd; then consider m,n such that A13: m <= n & a9 = n^2 - m^2 & b9 = 2*m*n & c9 = n^2 + m^2 by A12,A10 ,Th11; take k,m,n; thus thesis by A2,A8,A9,A11,A13; end; suppose b9 is odd; then consider m,n such that A14: m <= n & b9 = n^2 - m^2 & a9 = 2*m*n & c9 = n^2 + m^2 by A12,A10 ,Th11; take k,m,n; thus thesis by A2,A8,A9,A11,A14,ENUMSET1:58; end; end; end; end; assume ex k,m,n st m <= n & X = { k*(n^2 - m^2), k*(2*m*n), k*(n^2 + m^2 ) }; then consider k,m,n such that A15: m <= n and A16: X = { k*(n^2 - m^2), k*(2*m*n), k*(n^2 + m^2) }; m^2 <= n^2 by A15,SQUARE_1:15; then reconsider a9 = n^2 - m^2 as Element of NAT by INT_1:3,XREAL_1:48; set c9 = n^2 + m^2; set b9 = 2*m*n; (k*a9)^2 + (k*b9)^2 = (k*c9)^2; hence thesis by A16,Def4; end; end; notation let X; synonym X is degenerate for X is with_zero; end; theorem n > 2 implies ex X st X is non degenerate & n in X proof assume A1: n > 2; per cases; suppose n is even; then consider m being Nat such that A2: n = 2*m; reconsider m as Element of NAT by ORDINAL1:def 12; set c = 1*(m^2 + 1^2); set b = 1*(2*1*m); 2*m > 2*1 by A1,A2; then A3: m > 1 by XREAL_1:64; then m^2 > 1^2 by SQUARE_1:16; then m^2 - 1^2 > 0 by XREAL_1:50; then reconsider a = 1*(m^2 - 1^2) as Element of NAT by INT_1:3; reconsider X = { a,b,c } as Pythagorean_triple by A3,Def5; take X; a <> 0 by A3,SQUARE_1:16; hence not 0 in X by A1,A2,ENUMSET1:def 1; thus thesis by A2,ENUMSET1:def 1; end; suppose n is odd; then consider i such that A4: n = 2*i + 1 by ABIAN:1; A5: 2*i >= 2*1 by A1,A4,INT_1:7; then i >= 1 by XREAL_1:68; then reconsider m = i as Element of NAT by INT_1:3; reconsider a = 1*((m + 1)^2 - m^2) as Element of NAT by A4; set b = 1*(2*m*(m + 1)); set c = 1*((m + 1)^2 + m^2); m <= m + 1 by NAT_1:11; then reconsider X = { a,b,c } as Pythagorean_triple by Def5; take X; a = 2*m + 1 & c = m^2 + 2*m + m^2 + 1; hence not 0 in X by A5,ENUMSET1:def 1; thus thesis by A4,ENUMSET1:def 1; end; end; definition ::\$CD let X; attr X is simplified means 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 :Def8: ex m,n st m in X & n in X & m,n are_coprime; compatibility proof hereby assume A1: X is simplified; consider a,b,c such that A2: a^2 + b^2 = c^2 and A3: X = { a,b,c } by Def4; take a,b; thus a in X by A3,ENUMSET1:def 1; thus b in X by A3,ENUMSET1:def 1; now let k be Nat; reconsider k1=k as Element of NAT by ORDINAL1:def 12; assume A4: k divides a & k divides b; then k1^2 divides a^2 & k1^2 divides b^2 by Th6; then k^2 divides c^2 by A2,NAT_D:8; then k1 divides c by Th6; then for n st n in X holds k1 divides n by A3,A4,ENUMSET1:def 1; hence k = 1 by A1; end; hence a,b are_coprime; end; assume ex m,n st m in X & n in X & m,n are_coprime; then consider m,n such that A5: m in X & n in X and A6: m,n are_coprime; let k; assume for n st n in X holds k divides n; then A7: k divides m & k divides n by A5; m gcd n = 1 by A6; then k divides 1 by A7,NAT_D:def 5; hence thesis by WSIERP_1:15; end; end; theorem Th14: n > 0 implies ex X st X is non degenerate & X is simplified & 4* n in X proof set b = 1*(2*1*(2*n)); set c = 1*((2*n)^2 + 1^2); assume A1: n > 0; then n >= 0 + 1 by NAT_1:13; then A2: n + n > 0 + 1 by XREAL_1:8; then (2*n)^2 > 1^2 by SQUARE_1:16; then (2*n)^2 - 1^2 > 0 by XREAL_1:50; then reconsider a = 1*((2*n)^2 - 1^2) as Element of NAT by INT_1:3; reconsider X = { a,b,c } as Pythagorean_triple by A2,Def5; take X; a <> 0 & b <> 0 by A1; hence not 0 in X by ENUMSET1:def 1; a - c = -2; then a gcd c = 1*((2*n)^2 + 1^2) gcd -2 by PREPOWER:97 .= |.1*((2*n)^2 + 1^2).| gcd |.-2.| by INT_2:34 .= |.1*((2*n)^2 + 1^2).| gcd |.2.| by COMPLEX1:52 .= (2*(2*n^2) + 1) gcd 2 by INT_2:34 .= 1 gcd 2 by EULER_1:16 .= 1 by WSIERP_1:8; then A3: a,c are_coprime; a in X & c in X by ENUMSET1:def 1; hence X is simplified by A3; thus thesis by ENUMSET1:def 1; end; registration cluster non degenerate simplified for Pythagorean_triple; existence proof consider X such that A1: X is non degenerate & X is simplified and 4*1 in X by Th14; take X; thus thesis by A1; end; end; theorem { 3,4,5 } is non degenerate simplified Pythagorean_triple proof 3^2 + 4^2 = 5^2; then reconsider X = { 3,4,5 } as Pythagorean_triple by Def4; 3 gcd 4 = 3 gcd (4 - 3) by PREPOWER:97 .= 1 by WSIERP_1:8; then A1: 4 in X & 3,4 are_coprime by ENUMSET1:def 1; not 0 in X & 3 in X by ENUMSET1:def 1; hence thesis by A1,Def8,ORDINAL1:def 16; end; theorem { X: X is non degenerate & X is simplified } is infinite proof set T = { X: X is non degenerate & X is simplified }; for m ex n st n >= m & n in union T proof let m; set m9 = m + 1; set n = 4*m9; take n; consider X such that A1: X is non degenerate & X is simplified and A2: 4*m9 in X by Th14; n + 0 = 1*m9 + 3*m9; then A3: n >= m9 + 0 by XREAL_1:6; m9 >= m by NAT_1:11; hence n >= m by A3,XXREAL_0:2; X in T by A1; hence thesis by A2,TARSKI:def 4; end; then A4: union T is infinite by Th9; now let X be set; assume X in T; then ex X9 being Pythagorean_triple st X = X9 & X9 is non degenerate & X9 is simplified; hence X is finite; end; hence thesis by A4,FINSET_1:7; end;