:: Pythagorean triples
:: by Freek Wiedijk
::
:: Received August 26, 2001
:: Copyright (c) 2001-2026 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, NEWTON;
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;
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 Nat;
reserve i,i9 for Integer;
definition
let m,n be Nat;
redefine pred m,n are_coprime means :: redefines are_coprime (INT_2, definition)
for k being Nat st k divides m & k divides n holds k = 1;
compatibility by EULER_2:23;
end;
definition
let m,n be Nat;
redefine pred m,n are_coprime means :: redefines are_coprime (PYTHTRIP, redefinition) → are_coprime (INT_2, definition)
for p being Prime holds not (p divides m & p divides n);
compatibility
proof
hereby
assume
A1: m,n are_coprime;
let p be Prime;
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 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 being Element of NAT such that
A4: p is prime and
A5: p divides k by INT_2:31;
reconsider p9 = p as Prime 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;
cluster even square for 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;
cluster odd square for 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 being Element of NAT 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 mod 4 by NAT_D:61
.= 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 mod 4 by NAT_D:61
.= 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 NAT_D:66
.= (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 being Element of NAT 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;
set M = max(m,m9 + 1);
reconsider M as Element of NAT by ORDINAL1:def 12;
take M;
let n;
assume
A6: n >= M;
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,ORDINAL1:def 12;
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 being Element of NAT 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 Nat;
b is even
proof
assume b is odd;
then reconsider b9 = b as odd Nat;
a9^2 + b9^2 = c^2 by A1;
hence contradiction;
end;
then reconsider b9 = b as even Nat;
a9^2 + b9^2 = c^2 by A1;
then reconsider c9 = c as odd 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;
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 being Element of NAT 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 being Element of NAT st a^2 + b^2 = c^2 & X = { a,b,c } by Def4;
hence thesis;
end;
end;
definition
::$N Formula for Pythagorean Triples
::$L https://en.wikipedia.org/wiki/Pythagorean_triple Formula for Pythagorean Triples
redefine mode Pythagorean_triple means :: redefines Pythagorean_triple (PYTHTRIP, definition)
:Def5:
ex k,m,n being Element of NAT 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 being Element of NAT 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 being Element of NAT 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 being Element of NAT
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 being Element of NAT 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 being Element of NAT 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;
given k,m,n being Element of NAT 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,ORDINAL1:def 12;
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 :: redefines simplified (PYTHTRIP, definition)
:Def8:
ex m,n being Element of NAT st m in X & n in X & m,n are_coprime;
compatibility
proof
hereby
assume
A1: X is simplified;
consider a,b,c being Element of NAT 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;
given m,n being Element of NAT 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 b,c,n as Element of NAT by ORDINAL1:def 12;
ex k,m,w being Element of NAT st m <= w &
{a,b,c} = { k*(w^2 - m^2), k*(2*m*w), k*(w^2 + m^2) }
proof
take k = 1, m = 1, w = 2*n;
thus thesis by A2;
end;
then reconsider X = { a,b,c } as Pythagorean_triple by 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;