:: PYTHTRIP semantic presentation
begin
definition
let m, n be Nat;
redefine pred m,n are_relative_prime means :Def1: :: PYTHTRIP:def 1
for k being Nat st k divides m & k divides n holds
k = 1;
compatibility
( m,n are_relative_prime iff for k being Nat st k divides m & k divides n holds
k = 1 )
proof
hereby ::_thesis: ( ( for k being Nat st k divides m & k divides n holds
k = 1 ) implies m,n are_relative_prime )
assume m,n are_relative_prime ; ::_thesis: for k being Nat st k divides m & k divides n holds
k = 1
then A1: m gcd n = 1 by INT_2:def_3;
let k be Nat; ::_thesis: ( k divides m & k divides n implies k = 1 )
assume ( k divides m & k divides n ) ; ::_thesis: k = 1
then k divides 1 by A1, NAT_D:def_5;
hence k = 1 by WSIERP_1:15; ::_thesis: verum
end;
assume for k being Nat st k divides m & k divides n holds
k = 1 ; ::_thesis: m,n are_relative_prime
then A2: for k being 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; :: according to INT_2:def_3 ::_thesis: verum
end;
end;
:: deftheorem Def1 defines are_relative_prime PYTHTRIP:def_1_:_
for m, n being Nat holds
( m,n are_relative_prime iff for k being Nat st k divides m & k divides n holds
k = 1 );
definition
let m, n be Nat;
redefine pred m,n are_relative_prime means :Def2: :: PYTHTRIP:def 2
for p being prime Nat holds
( not p divides m or not p divides n );
compatibility
( m,n are_relative_prime iff for p being prime Nat holds
( not p divides m or not p divides n ) )
proof
hereby ::_thesis: ( ( for p being prime Nat holds
( not p divides m or not p divides n ) ) implies m,n are_relative_prime )
assume A1: m,n are_relative_prime ; ::_thesis: for p being prime Nat st p divides m holds
not p divides n
let p be prime Nat; ::_thesis: ( p divides m implies not p divides n )
assume ( p divides m & p divides n ) ; ::_thesis: contradiction
then p = 1 by A1, Def1;
hence contradiction by INT_2:def_4; ::_thesis: verum
end;
assume A2: for p being prime Nat holds
( not p divides m or not p divides n ) ; ::_thesis: m,n are_relative_prime
let k be Nat; :: according to PYTHTRIP:def_1 ::_thesis: ( k divides m & k divides n implies k = 1 )
assume A3: ( k divides m & k divides n ) ; ::_thesis: k = 1
percases ( k = 0 or k = 1 or k > 1 ) by NAT_1:25;
suppose k = 0 ; ::_thesis: k = 1
then ( m = 0 & n = 0 ) by A3, INT_2:3;
hence k = 1 by A2, INT_2:28, NAT_D:6; ::_thesis: verum
end;
suppose k = 1 ; ::_thesis: k = 1
hence k = 1 ; ::_thesis: verum
end;
suppose k > 1 ; ::_thesis: 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 Element of NAT by A4;
( p9 divides m & p9 divides n ) by A3, A5, NAT_D:4;
hence k = 1 by A2; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def2 defines are_relative_prime PYTHTRIP:def_2_:_
for m, n being Nat holds
( m,n are_relative_prime iff for p being prime Nat holds
( not p divides m or not p divides n ) );
begin
definition
let n be number ;
attrn is square means :Def3: :: PYTHTRIP:def 3
ex m being Nat st n = m ^2 ;
end;
:: deftheorem Def3 defines square PYTHTRIP:def_3_:_
for n being number holds
( n is square iff ex m being Nat st n = m ^2 );
registration
cluster square -> natural for set ;
coherence
for b1 being number st b1 is square holds
b1 is natural
proof
let n be number ; ::_thesis: ( n is square implies n is natural )
assume n is square ; ::_thesis: n is natural
then ex m being Nat st n = m ^2 by Def3;
hence n is natural ; ::_thesis: verum
end;
end;
registration
let n be Nat;
clustern ^2 -> square ;
coherence
n ^2 is square by Def3;
end;
registration
cluster epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer even square for Element of NAT ;
existence
ex b1 being Element of NAT st
( b1 is even & b1 is square )
proof
take 0 ; ::_thesis: ( 0 is even & 0 is square )
0 = 2 * (0 ^2) ;
hence ( 0 is even & 0 is square ) ; ::_thesis: verum
end;
end;
registration
cluster epsilon-transitive epsilon-connected ordinal natural V24() V25() ext-real non negative integer odd square for Element of NAT ;
existence
ex b1 being Element of NAT st
( b1 is odd & b1 is square )
proof
take 1 ; ::_thesis: ( 1 is odd & 1 is square )
1 ^2 = (2 * 0) + 1 ;
hence ( 1 is odd & 1 is square ) ; ::_thesis: verum
end;
end;
registration
clusterV24() V25() ext-real integer even square for set ;
existence
ex b1 being Integer st
( b1 is even & b1 is square )
proof
set n = the even square Element of NAT ;
take the even square Element of NAT ; ::_thesis: ( the even square Element of NAT is even & the even square Element of NAT is square )
thus ( the even square Element of NAT is even & the even square Element of NAT is square ) ; ::_thesis: verum
end;
end;
registration
clusterV24() V25() ext-real integer odd square for set ;
existence
ex b1 being Integer st
( b1 is odd & b1 is square )
proof
set n = the odd square Element of NAT ;
take the odd square Element of NAT ; ::_thesis: ( the odd square Element of NAT is odd & the odd square Element of NAT is square )
thus ( the odd square Element of NAT is odd & the odd square Element of NAT is square ) ; ::_thesis: verum
end;
end;
registration
let m, n be square number ;
clusterm * n -> square ;
coherence
m * n is square
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 m * n is square ; ::_thesis: verum
end;
end;
theorem Th1: :: PYTHTRIP:1
for m, n being Element of NAT st m * n is square & m,n are_relative_prime holds
( m is square & n is square )
proof
let m, n be Element of NAT ; ::_thesis: ( m * n is square & m,n are_relative_prime implies ( m is square & n is square ) )
defpred S1[ Nat] means for m, n being Element of NAT st m * n = $1 & m * n is square & m,n are_relative_prime holds
( m is square & n is square );
A1: for mn being Nat st ( for k being Nat st k < mn holds
S1[k] ) holds
S1[mn]
proof
let mn be Nat; ::_thesis: ( ( for k being Nat st k < mn holds
S1[k] ) implies S1[mn] )
assume A2: for k being Nat st k < mn holds
for m, n being Element of NAT st m * n = k & m * n is square & m,n are_relative_prime holds
( m is square & n is square ) ; ::_thesis: S1[mn]
let m, n be Element of NAT ; ::_thesis: ( m * n = mn & m * n is square & m,n are_relative_prime implies ( m is square & n is square ) )
assume A3: m * n = mn ; ::_thesis: ( not m * n is square or not m,n are_relative_prime or ( m is square & n is square ) )
assume m * n is square ; ::_thesis: ( not m,n are_relative_prime or ( m is square & n is square ) )
then consider mn9 being Nat such that
A4: mn = mn9 ^2 by A3, Def3;
assume A5: m,n are_relative_prime ; ::_thesis: ( m is square & n is square )
then A6: m gcd n = 1 ^2 by INT_2:def_3;
percases ( m * n = 0 or m * n = 1 ^2 or mn > 1 ) by A3, NAT_1:25;
supposeA7: m * n = 0 ; ::_thesis: ( m is square & n is square )
hereby ::_thesis: verum
percases ( m = 0 ^2 or n = 0 ^2 ) by A7, XCMPLX_1:6;
suppose m = 0 ^2 ; ::_thesis: ( m is square & n is square )
hence ( m is square & n is square ) by A6, NEWTON:52; ::_thesis: verum
end;
suppose n = 0 ^2 ; ::_thesis: ( m is square & n is square )
hence ( m is square & n is square ) by A6, NEWTON:52; ::_thesis: verum
end;
end;
end;
end;
suppose m * n = 1 ^2 ; ::_thesis: ( m is square & n is square )
hence ( m is square & n is square ) by NAT_1:15; ::_thesis: verum
end;
supposeA8: mn > 1 ; ::_thesis: ( m is square & n is square )
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 being 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 ::_thesis: verum
percases ( p divides m or p divides n ) by A3, A10, NEWTON:80;
supposeA17: p divides m ; ::_thesis: ( m is square & n is square )
then A18: not p divides n by A5, Def2;
consider m9 being 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 by NAT_D:def_3;
then p divides m9 by A18, NEWTON:80;
then consider m99 being Nat such that
A20: m9 = p * m99 by NAT_D:def_3;
reconsider m99 = 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 by NAT_D:def_3;
then m99 gcd n = 1 by A6, WSIERP_1:16;
then A23: m99,n are_relative_prime by INT_2:def_3;
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 by Def3;
m = (p * m999) ^2 by A19, A20, A25;
hence ( m is square & n is square ) by A2, A24, A22, A23; ::_thesis: verum
end;
supposeA26: p divides n ; ::_thesis: ( m is square & n is square )
then A27: not p divides m by A5, Def2;
consider n9 being 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 by NAT_D:def_3;
then p divides n9 by A27, NEWTON:80;
then consider n99 being Nat such that
A29: n9 = p * n99 by NAT_D:def_3;
reconsider n99 = 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 by NAT_D:def_3;
then m gcd n99 = 1 by A6, WSIERP_1:16;
then A32: m,n99 are_relative_prime by INT_2:def_3;
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 by Def3;
n = (p * n999) ^2 by A28, A29, A34;
hence ( m is square & n is square ) by A2, A33, A31, A32; ::_thesis: verum
end;
end;
end;
end;
end;
end;
for mn being Nat holds S1[mn] from NAT_1:sch_4(A1);
hence ( m * n is square & m,n are_relative_prime implies ( m is square & n is square ) ) ; ::_thesis: verum
end;
registration
let i be Integer;
clusteri ^2 -> integer ;
coherence
i ^2 is integer ;
end;
registration
let i be even Integer;
clusteri ^2 -> even ;
coherence
i ^2 is even ;
end;
registration
let i be odd Integer;
clusteri ^2 -> odd ;
coherence
not i ^2 is even ;
end;
theorem :: PYTHTRIP:2
for i being Integer holds
( i is even iff i ^2 is even ) ;
theorem Th3: :: PYTHTRIP:3
for i being Integer st i is even holds
(i ^2) mod 4 = 0
proof
let i be Integer; ::_thesis: ( i is even implies (i ^2) mod 4 = 0 )
given i9 being Integer such that A1: i = 2 * i9 ; :: according to INT_1:def_3,ABIAN:def_1 ::_thesis: (i ^2) mod 4 = 0
i ^2 = (4 * (i9 ^2)) + 0 by A1;
hence (i ^2) mod 4 = 0 mod 4 by EULER_1:12
.= 0 by NAT_D:24 ;
::_thesis: verum
end;
theorem Th4: :: PYTHTRIP:4
for i being Integer st i is odd holds
(i ^2) mod 4 = 1
proof
let i be Integer; ::_thesis: ( i is odd implies (i ^2) mod 4 = 1 )
assume i is odd ; ::_thesis: (i ^2) mod 4 = 1
then consider i9 being Integer 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 EULER_1:12
.= 1 by NAT_D:24 ;
::_thesis: verum
end;
registration
let m, n be odd square Integer;
clusterm + n -> non square ;
coherence
not m + n is square
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 ::_thesis: verum
assume m + n is square ; ::_thesis: contradiction
then consider mn9 being Nat such that
A6: m + n = mn9 ^2 by Def3;
mn9 is even by A6;
hence contradiction by A5, A6, Th3; ::_thesis: verum
end;
end;
end;
theorem Th5: :: PYTHTRIP:5
for m, n being Element of NAT st m ^2 = n ^2 holds
m = n
proof
let m, n be Element of NAT ; ::_thesis: ( m ^2 = n ^2 implies m = n )
assume A1: m ^2 = n ^2 ; ::_thesis: m = n
percases ( m = n or m = - n ) by A1, SQUARE_1:40;
suppose m = n ; ::_thesis: m = n
hence m = n ; ::_thesis: verum
end;
supposeA2: m = - n ; ::_thesis: m = n
then m = - 0 ;
hence m = n by A2; ::_thesis: verum
end;
end;
end;
theorem Th6: :: PYTHTRIP:6
for m, n being Element of NAT holds
( m divides n iff m ^2 divides n ^2 )
proof
let m, n be Element of NAT ; ::_thesis: ( m divides n iff m ^2 divides n ^2 )
defpred S1[ Nat] means for n being Element of NAT holds
( $1 divides n iff $1 ^2 divides n ^2 );
A1: for m being Nat st ( for k being Nat st k < m holds
S1[k] ) holds
S1[m]
proof
let m be Nat; ::_thesis: ( ( for k being Nat st k < m holds
S1[k] ) implies S1[m] )
assume A2: for k being Nat st k < m holds
for n being Element of NAT holds
( k divides n iff k ^2 divides n ^2 ) ; ::_thesis: S1[m]
let n be Element of NAT ; ::_thesis: ( m divides n iff m ^2 divides n ^2 )
hereby ::_thesis: ( m ^2 divides n ^2 implies m divides n )
assume m divides n ; ::_thesis: m ^2 divides n ^2
then consider k9 being 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 by NAT_D:def_3; ::_thesis: verum
end;
assume A4: m ^2 divides n ^2 ; ::_thesis: m divides n
percases ( m = 0 or m = 1 or m > 1 ) by NAT_1:25;
suppose m = 0 ; ::_thesis: m divides n
then n ^2 = 0 by A4, INT_2:3;
then n = 0 by XCMPLX_1:6;
hence m divides n by NAT_D:6; ::_thesis: verum
end;
suppose m = 1 ; ::_thesis: m divides n
hence m divides n by NAT_D:6; ::_thesis: verum
end;
supposeA5: m > 1 ; ::_thesis: m divides n
consider k9 being 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 being Nat such that
A9: m = p * m9 by A8, NAT_D:def_3;
reconsider m9 = m9 as Element of NAT by ORDINAL1:def_12;
m ^2 = (m * m9) * p by A9;
then p divides m ^2 by NAT_D:def_3;
then p divides n ^2 by A4, NAT_D:4;
then p divides n by NEWTON:80;
then consider n9 being 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 = 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 by NAT_D:def_3;
p * m9 > 1 * m9 by A5, A9, A11, XREAL_1:98;
then m9 divides n9 by A2, A9, A13;
then consider k being Nat such that
A14: n9 = m9 * k by NAT_D:def_3;
n = m * k by A9, A10, A14;
hence m divides n by NAT_D:def_3; ::_thesis: verum
end;
end;
end;
for m being Nat holds S1[m] from NAT_1:sch_4(A1);
hence ( m divides n iff m ^2 divides n ^2 ) ; ::_thesis: verum
end;
begin
theorem Th7: :: PYTHTRIP:7
for m, n, k being Element of NAT holds
( ( m divides n or k = 0 ) iff k * m divides k * n )
proof
let m, n, k be Element of NAT ; ::_thesis: ( ( m divides n or k = 0 ) iff k * m divides k * n )
hereby ::_thesis: ( not k * m divides k * n or m divides n or k = 0 )
assume A1: ( m divides n or k = 0 ) ; ::_thesis: k * m divides k * n
percases ( m divides n or k = 0 ) by A1;
suppose m divides n ; ::_thesis: k * m divides k * n
then consider k9 being 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 by NAT_D:def_3; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: k * m divides k * n
hence k * m divides k * n ; ::_thesis: verum
end;
end;
end;
assume A3: k * m divides k * n ; ::_thesis: ( m divides n or k = 0 )
now__::_thesis:_(_k_<>_0_implies_m_divides_n_)
consider k9 being Nat such that
A4: k * n = (k * m) * k9 by A3, NAT_D:def_3;
assume A5: k <> 0 ; ::_thesis: m divides n
k * n = k * (m * k9) by A4;
then n = m * k9 by A5, XCMPLX_1:5;
hence m divides n by NAT_D:def_3; ::_thesis: verum
end;
hence ( m divides n or k = 0 ) ; ::_thesis: verum
end;
theorem Th8: :: PYTHTRIP:8
for k, m, n being Element of NAT holds (k * m) gcd (k * n) = k * (m gcd n)
proof
let k, m, n be Element of NAT ; ::_thesis: (k * m) gcd (k * n) = k * (m gcd n)
percases ( k <> 0 or k = 0 ) ;
supposeA1: k <> 0 ; ::_thesis: (k * m) gcd (k * n) = k * (m gcd n)
( k divides k * m & k divides k * n ) by NAT_D:9;
then k divides (k * m) gcd (k * n) by NAT_D:def_5;
then consider k9 being Nat such that
A2: (k * m) gcd (k * n) = k * k9 by NAT_D:def_3;
reconsider k9 = k9 as Element of NAT by ORDINAL1:def_12;
now__::_thesis:_(_k9_divides_m_&_k9_divides_n_&_(_for_p_being_Nat_st_p_divides_m_&_p_divides_n_holds_
p_divides_k9_)_)
k * k9 divides k * m by A2, NAT_D:def_5;
hence k9 divides m by A1, Th7; ::_thesis: ( k9 divides n & ( for p being Nat st p divides m & p divides n holds
p divides k9 ) )
k * k9 divides k * n by A2, NAT_D:def_5;
hence k9 divides n by A1, Th7; ::_thesis: for p being Nat st p divides m & p divides n holds
p divides k9
let p be Nat; ::_thesis: ( p divides m & p divides n implies p divides k9 )
reconsider p9 = p as Element of NAT by ORDINAL1:def_12;
assume ( p divides m & p divides n ) ; ::_thesis: p divides k9
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 ; ::_thesis: verum
end;
hence (k * m) gcd (k * n) = k * (m gcd n) by A2, NAT_D:def_5; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: (k * m) gcd (k * n) = k * (m gcd n)
hence (k * m) gcd (k * n) = k * (m gcd n) by NEWTON:52; ::_thesis: verum
end;
end;
end;
begin
theorem Th9: :: PYTHTRIP:9
for X being set st ( for m being Element of NAT ex n being Element of NAT st
( n >= m & n in X ) ) holds
X is infinite
proof
let X be set ; ::_thesis: ( ( for m being Element of NAT ex n being Element of NAT st
( n >= m & n in X ) ) implies X is infinite )
A1: now__::_thesis:_for_f_being_Function
for_k_being_Element_of_NAT_holds_S1[k]
let f be Function; ::_thesis: for k being Element of NAT holds S1[k]
defpred S1[ Element of NAT ] means ex m being Element of NAT st
for n being Element of NAT st n >= m holds
not n in f .: $1;
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume ex m being Element of NAT st
for n being Element of NAT st n >= m holds
not n in f .: k ; ::_thesis: S1[k + 1]
then consider m being Element of NAT such that
A3: for n being Element of NAT st n >= m holds
not n in f .: k ;
k + 1 = succ k by NAT_1:38
.= k \/ {k} by ORDINAL1:def_1 ;
then A4: f .: (k + 1) = (f .: k) \/ (Im (f,k)) by RELAT_1:120;
percases ( ( k in dom f & f . k in NAT ) or ( k in dom f & not f . k in NAT ) or not k in dom f ) ;
supposeA5: ( k in dom f & f . k in NAT ) ; ::_thesis: S1[k + 1]
then reconsider m9 = f . k as Element of NAT ;
take max (m,(m9 + 1)) ; ::_thesis: for n being Element of NAT st n >= max (m,(m9 + 1)) holds
not n in f .: (k + 1)
let n be Element of NAT ; ::_thesis: ( n >= max (m,(m9 + 1)) implies not n in f .: (k + 1) )
assume A6: n >= max (m,(m9 + 1)) ; ::_thesis: not n in f .: (k + 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 not n in f .: (k + 1) by A7, A8, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA9: ( k in dom f & not f . k in NAT ) ; ::_thesis: S1[k + 1]
take m ; ::_thesis: for n being Element of NAT st n >= m holds
not n in f .: (k + 1)
set m9 = f . k;
let n be Element of NAT ; ::_thesis: ( n >= m implies not n in f .: (k + 1) )
n <> f . k by A9;
then A10: not n in {(f . k)} by TARSKI:def_1;
assume n >= m ; ::_thesis: not n in f .: (k + 1)
then A11: not n in f .: k by A3;
f .: (k + 1) = (f .: k) \/ {(f . k)} by A4, A9, FUNCT_1:59;
hence not n in f .: (k + 1) by A11, A10, XBOOLE_0:def_3; ::_thesis: verum
end;
suppose not k in dom f ; ::_thesis: S1[k + 1]
then A12: dom f misses {k} by ZFMISC_1:50;
take m ; ::_thesis: for n being Element of NAT st n >= m holds
not n in f .: (k + 1)
let n be Element of NAT ; ::_thesis: ( n >= m implies not n in f .: (k + 1) )
assume A13: n >= m ; ::_thesis: not n in f .: (k + 1)
Im (f,k) = f .: ((dom f) /\ {k}) by RELAT_1:112
.= f .: {} by A12, XBOOLE_0:def_7
.= {} ;
hence not n in f .: (k + 1) by A3, A4, A13; ::_thesis: verum
end;
end;
end;
A14: S1[ 0 ]
proof
take 0 ; ::_thesis: for n being Element of NAT st n >= 0 holds
not n in f .: 0
let n be Element of NAT ; ::_thesis: ( n >= 0 implies not n in f .: 0 )
assume n >= 0 ; ::_thesis: not n in f .: 0
thus not n in f .: 0 ; ::_thesis: verum
end;
thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A14, A2); ::_thesis: verum
end;
now__::_thesis:_(_X_is_finite_implies_ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_n_>=_m_holds_
not_n_in_X_)
assume X is finite ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
not n in X
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 being Element of NAT st
for n being Element of NAT st n >= m holds
not n in X by A1; ::_thesis: verum
end;
hence ( ( for m being Element of NAT ex n being Element of NAT st
( n >= m & n in X ) ) implies X is infinite ) ; ::_thesis: verum
end;
begin
theorem Th10: :: PYTHTRIP:10
for a, b being Element of NAT holds
( not a,b are_relative_prime or a is odd or b is odd )
proof
let a, b be Element of NAT ; ::_thesis: ( not a,b are_relative_prime or a is odd or b is odd )
assume A1: a,b are_relative_prime ; ::_thesis: ( a is odd or b is odd )
assume a is even ; ::_thesis: b is odd
then A2: 2 divides a by PEPIN:22;
assume b is even ; ::_thesis: contradiction
then 2 divides b by PEPIN:22;
hence contradiction by A1, A2, Def1; ::_thesis: verum
end;
theorem Th11: :: PYTHTRIP:11
for a, b, c being Element of NAT st (a ^2) + (b ^2) = c ^2 & a,b are_relative_prime & a is odd holds
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
let a, b, c be Element of NAT ; ::_thesis: ( (a ^2) + (b ^2) = c ^2 & a,b are_relative_prime & 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) ) )
assume A1: (a ^2) + (b ^2) = c ^2 ; ::_thesis: ( not a,b are_relative_prime or not a is odd or ex m, n being Element of NAT st
( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) )
assume A2: a,b are_relative_prime ; ::_thesis: ( not a is odd or ex m, n being Element of NAT st
( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) ) )
assume a is odd ; ::_thesis: ex m, n being Element of NAT st
( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) )
then reconsider a9 = a as odd Element of NAT ;
b is even
proof
assume b is odd ; ::_thesis: contradiction
then reconsider b9 = b as odd Element of NAT ;
(a9 ^2) + (b9 ^2) = c ^2 by A1;
hence contradiction ; ::_thesis: verum
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 being Integer such that
A3: c9 - a9 = 2 * i by INT_1:def_3;
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 Element of NAT such that
A4: c9 + a9 = 2 * n9 by ABIAN:def_2;
consider k9 being Element of NAT such that
A5: b9 = 2 * k9 by ABIAN:def_2;
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_relative_prime
proof
let p be prime Nat; :: according to PYTHTRIP:def_2 ::_thesis: ( not p divides n9 or not p divides m9 )
assume that
A9: p divides n9 and
A10: p divides m9 ; ::_thesis: contradiction
reconsider p = 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 by A13, A11, WSIERP_1:4;
then p divides b by NEWTON:80;
hence contradiction by A2, A4, A3, A12, Def2; ::_thesis: verum
end;
then n9 is square by A6, Th1;
then consider n being Nat such that
A14: n9 = n ^2 by Def3;
m9 is square by A8, A6, Th1;
then consider m being Nat such that
A15: m9 = m ^2 by Def3;
reconsider m = m, n = n as Element of NAT by ORDINAL1:def_12;
take m ; ::_thesis: ex n being Element of NAT st
( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) )
take n ; ::_thesis: ( m <= n & a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) )
n9 - m9 = a by A4, A3;
then m ^2 <= n ^2 by A14, A15, XREAL_1:49;
hence m <= n by SQUARE_1:16; ::_thesis: ( a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) )
thus a = (n ^2) - (m ^2) by A4, A3, A14, A15; ::_thesis: ( b = (2 * m) * n & c = (n ^2) + (m ^2) )
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; ::_thesis: c = (n ^2) + (m ^2)
thus c = (n ^2) + (m ^2) by A4, A3, A14, A15; ::_thesis: verum
end;
theorem :: PYTHTRIP:12
for a, n, m, b, c being Element of NAT st a = (n ^2) - (m ^2) & b = (2 * m) * n & c = (n ^2) + (m ^2) holds
(a ^2) + (b ^2) = c ^2 ;
definition
mode Pythagorean_triple -> Subset of NAT means :Def4: :: PYTHTRIP:def 4
ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & it = {a,b,c} );
existence
ex b1 being Subset of NAT ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & b1 = {a,b,c} )
proof
take {0,0,0} ; ::_thesis: ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & {0,0,0} = {a,b,c} )
take 0 ; ::_thesis: ex b, c being Element of NAT st
( (0 ^2) + (b ^2) = c ^2 & {0,0,0} = {0,b,c} )
take 0 ; ::_thesis: ex c being Element of NAT st
( (0 ^2) + (0 ^2) = c ^2 & {0,0,0} = {0,0,c} )
take 0 ; ::_thesis: ( (0 ^2) + (0 ^2) = 0 ^2 & {0,0,0} = {0,0,0} )
thus (0 ^2) + (0 ^2) = 0 ^2 ; ::_thesis: {0,0,0} = {0,0,0}
thus {0,0,0} = {0,0,0} ; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines Pythagorean_triple PYTHTRIP:def_4_:_
for b1 being Subset of NAT holds
( b1 is Pythagorean_triple iff ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & b1 = {a,b,c} ) );
registration
cluster -> finite for Pythagorean_triple ;
coherence
for b1 being Pythagorean_triple holds b1 is finite
proof
let X be Pythagorean_triple ; ::_thesis: X is finite
ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & X = {a,b,c} ) by Def4;
hence X is finite ; ::_thesis: verum
end;
end;
definition
redefine mode Pythagorean_triple means :Def5: :: PYTHTRIP:def 5
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
for b1 being Subset of NAT holds
( b1 is Pythagorean_triple iff ex k, m, n being Element of NAT st
( m <= n & b1 = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) )
proof
let X be Subset of NAT; ::_thesis: ( X is Pythagorean_triple iff 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)))} ) )
hereby ::_thesis: ( 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)))} ) implies X is Pythagorean_triple )
assume X is Pythagorean_triple ; ::_thesis: 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)))} )
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: a gcd b divides a by NAT_D:def_5;
A4: a gcd b divides b by NAT_D:def_5;
percases ( a gcd b = 0 or a gcd b <> 0 ) ;
suppose a gcd b = 0 ; ::_thesis: 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)))} )
then A5: ( a = 0 & b = 0 ) by A3, A4, INT_2:3;
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)))} ) ::_thesis: verum
proof
take 0 ; ::_thesis: ex m, n being Element of NAT st
( m <= n & X = {(0 * ((n ^2) - (m ^2))),(0 * ((2 * m) * n)),(0 * ((n ^2) + (m ^2)))} )
take 0 ; ::_thesis: ex n being Element of NAT st
( 0 <= n & X = {(0 * ((n ^2) - (0 ^2))),(0 * ((2 * 0) * n)),(0 * ((n ^2) + (0 ^2)))} )
take 0 ; ::_thesis: ( 0 <= 0 & X = {(0 * ((0 ^2) - (0 ^2))),(0 * ((2 * 0) * 0)),(0 * ((0 ^2) + (0 ^2)))} )
thus ( 0 <= 0 & X = {(0 * ((0 ^2) - (0 ^2))),(0 * ((2 * 0) * 0)),(0 * ((0 ^2) + (0 ^2)))} ) by A1, A2, A5, XCMPLX_1:6; ::_thesis: verum
end;
end;
supposeA6: a gcd b <> 0 ; ::_thesis: 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)))} )
then A7: (a gcd b) * (a gcd b) <> 0 by XCMPLX_1:6;
consider a9 being Nat such that
A8: a = (a gcd b) * a9 by A3, NAT_D:def_3;
consider b9 being Nat such that
A9: b = (a gcd b) * b9 by A4, NAT_D:def_3;
reconsider a9 = a9, b9 = b9 as Element of NAT by ORDINAL1:def_12;
(a gcd b) * (a9 gcd b9) = (a gcd b) * 1 by A8, A9, Th8;
then a9 gcd b9 = 1 by A6, XCMPLX_1:5;
then A10: a9,b9 are_relative_prime by INT_2:def_3;
c ^2 = ((a gcd b) ^2) * ((a9 ^2) + (b9 ^2)) by A1, A8, A9;
then (a gcd b) ^2 divides c ^2 by NAT_D:def_3;
then a gcd b divides c by Th6;
then consider c9 being Nat such that
A11: c = (a gcd b) * c9 by NAT_D:def_3;
reconsider c9 = c9 as Element of NAT by ORDINAL1:def_12;
((a gcd b) ^2) * ((a9 ^2) + (b9 ^2)) = ((a gcd b) ^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)))} ) ::_thesis: verum
proof
percases ( a9 is odd or b9 is odd ) by A10, Th10;
suppose a9 is odd ; ::_thesis: 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)))} )
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 a gcd b ; ::_thesis: ex m, n being Element of NAT st
( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )
take m ; ::_thesis: ex n being Element of NAT st
( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )
take n ; ::_thesis: ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )
thus ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) by A2, A8, A9, A11, A13; ::_thesis: verum
end;
suppose b9 is odd ; ::_thesis: 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)))} )
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 a gcd b ; ::_thesis: ex m, n being Element of NAT st
( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )
take m ; ::_thesis: ex n being Element of NAT st
( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )
take n ; ::_thesis: ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} )
thus ( m <= n & X = {((a gcd b) * ((n ^2) - (m ^2))),((a gcd b) * ((2 * m) * n)),((a gcd b) * ((n ^2) + (m ^2)))} ) by A2, A8, A9, A11, A14, ENUMSET1:58; ::_thesis: verum
end;
end;
end;
end;
end;
end;
assume 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)))} ) ; ::_thesis: X is Pythagorean_triple
then consider 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 a = k * a9;
set c9 = (n ^2) + (m ^2);
set b9 = (2 * m) * n;
set b = k * ((2 * m) * n);
set c = k * ((n ^2) + (m ^2));
((k * a9) ^2) + ((k * ((2 * m) * n)) ^2) = (k * ((n ^2) + (m ^2))) ^2 ;
hence X is Pythagorean_triple by A16, Def4; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Pythagorean_triple PYTHTRIP:def_5_:_
for b1 being Subset of NAT holds
( b1 is Pythagorean_triple iff ex k, m, n being Element of NAT st
( m <= n & b1 = {(k * ((n ^2) - (m ^2))),(k * ((2 * m) * n)),(k * ((n ^2) + (m ^2)))} ) );
definition
let X be Pythagorean_triple ;
attrX is degenerate means :Def6: :: PYTHTRIP:def 6
0 in X;
end;
:: deftheorem Def6 defines degenerate PYTHTRIP:def_6_:_
for X being Pythagorean_triple holds
( X is degenerate iff 0 in X );
theorem :: PYTHTRIP:13
for n being Element of NAT st n > 2 holds
ex X being Pythagorean_triple st
( not X is degenerate & n in X )
proof
let n be Element of NAT ; ::_thesis: ( n > 2 implies ex X being Pythagorean_triple st
( not X is degenerate & n in X ) )
assume A1: n > 2 ; ::_thesis: ex X being Pythagorean_triple st
( not X is degenerate & n in X )
percases ( n is even or n is odd ) ;
suppose n is even ; ::_thesis: ex X being Pythagorean_triple st
( not X is degenerate & n in X )
then consider m being Element of NAT such that
A2: n = 2 * m by ABIAN:def_2;
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,(1 * ((2 * 1) * m)),(1 * ((m ^2) + (1 ^2)))} as Pythagorean_triple by A3, Def5;
take X ; ::_thesis: ( not X is degenerate & n in X )
a <> 0 by A3, SQUARE_1:16;
hence not 0 in X by A1, A2, ENUMSET1:def_1; :: according to PYTHTRIP:def_6 ::_thesis: n in X
thus n in X by A2, ENUMSET1:def_1; ::_thesis: verum
end;
suppose n is odd ; ::_thesis: ex X being Pythagorean_triple st
( not X is degenerate & n in X )
then consider i being Integer 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,(1 * ((2 * m) * (m + 1))),(1 * (((m + 1) ^2) + (m ^2)))} as Pythagorean_triple by Def5;
take X ; ::_thesis: ( not X is degenerate & n in X )
( a = (2 * m) + 1 & 1 * (((m + 1) ^2) + (m ^2)) = (((m ^2) + (2 * m)) + (m ^2)) + 1 ) ;
hence not 0 in X by A5, ENUMSET1:def_1; :: according to PYTHTRIP:def_6 ::_thesis: n in X
thus n in X by A4, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
definition
let X be Pythagorean_triple ;
attrX is simplified means :Def7: :: PYTHTRIP:def 7
for k being Element of NAT st ( for n being Element of NAT st n in X holds
k divides n ) holds
k = 1;
end;
:: deftheorem Def7 defines simplified PYTHTRIP:def_7_:_
for X being Pythagorean_triple holds
( X is simplified iff for k being Element of NAT st ( for n being Element of NAT st n in X holds
k divides n ) holds
k = 1 );
definition
let X be Pythagorean_triple ;
redefine attr X is simplified means :Def8: :: PYTHTRIP:def 8
ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime );
compatibility
( X is simplified iff ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime ) )
proof
hereby ::_thesis: ( ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime ) implies X is simplified )
assume A1: X is simplified ; ::_thesis: ex a, b being Element of NAT st
( a in X & b in X & a,b are_relative_prime )
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 = a; ::_thesis: ex b being Element of NAT st
( a in X & b in X & a,b are_relative_prime )
take b = b; ::_thesis: ( a in X & b in X & a,b are_relative_prime )
thus a in X by A3, ENUMSET1:def_1; ::_thesis: ( b in X & a,b are_relative_prime )
thus b in X by A3, ENUMSET1:def_1; ::_thesis: a,b are_relative_prime
now__::_thesis:_for_k_being_Nat_st_k_divides_a_&_k_divides_b_holds_
k_=_1
let k be Nat; ::_thesis: ( k divides a & k divides b implies k = 1 )
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
assume A4: ( k divides a & k divides b ) ; ::_thesis: k = 1
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 being Element of NAT st n in X holds
k1 divides n by A3, A4, ENUMSET1:def_1;
hence k = 1 by A1, Def7; ::_thesis: verum
end;
hence a,b are_relative_prime by Def1; ::_thesis: verum
end;
assume ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime ) ; ::_thesis: X is simplified
then consider m, n being Element of NAT such that
A5: ( m in X & n in X ) and
A6: m,n are_relative_prime ;
let k be Element of NAT ; :: according to PYTHTRIP:def_7 ::_thesis: ( ( for n being Element of NAT st n in X holds
k divides n ) implies k = 1 )
assume for n being Element of NAT st n in X holds
k divides n ; ::_thesis: k = 1
then A7: ( k divides m & k divides n ) by A5;
m gcd n = 1 by A6, INT_2:def_3;
then k divides 1 by A7, NAT_D:def_5;
hence k = 1 by WSIERP_1:15; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines simplified PYTHTRIP:def_8_:_
for X being Pythagorean_triple holds
( X is simplified iff ex m, n being Element of NAT st
( m in X & n in X & m,n are_relative_prime ) );
theorem Th14: :: PYTHTRIP:14
for n being Element of NAT st n > 0 holds
ex X being Pythagorean_triple st
( not X is degenerate & X is simplified & 4 * n in X )
proof
let n be Element of NAT ; ::_thesis: ( n > 0 implies ex X being Pythagorean_triple st
( not X is degenerate & X is simplified & 4 * n in X ) )
set b = 1 * ((2 * 1) * (2 * n));
set c = 1 * (((2 * n) ^2) + (1 ^2));
assume A1: n > 0 ; ::_thesis: ex X being Pythagorean_triple st
( not X is degenerate & X is simplified & 4 * n in X )
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,(1 * ((2 * 1) * (2 * n))),(1 * (((2 * n) ^2) + (1 ^2)))} as Pythagorean_triple by A2, Def5;
take X ; ::_thesis: ( not X is degenerate & X is simplified & 4 * n in X )
( a <> 0 & 1 * ((2 * 1) * (2 * n)) <> 0 ) by A1;
hence not 0 in X by ENUMSET1:def_1; :: according to PYTHTRIP:def_6 ::_thesis: ( X is simplified & 4 * n in X )
a - (1 * (((2 * n) ^2) + (1 ^2))) = - 2 ;
then a gcd (1 * (((2 * n) ^2) + (1 ^2))) = (1 * (((2 * n) ^2) + (1 ^2))) gcd (- 2) by PREPOWER:97
.= (abs (1 * (((2 * n) ^2) + (1 ^2)))) gcd (abs (- 2)) by INT_2:34
.= (abs (1 * (((2 * n) ^2) + (1 ^2)))) gcd (abs 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,1 * (((2 * n) ^2) + (1 ^2)) are_relative_prime by INT_2:def_3;
( a in X & 1 * (((2 * n) ^2) + (1 ^2)) in X ) by ENUMSET1:def_1;
hence X is simplified by A3, Def8; ::_thesis: 4 * n in X
thus 4 * n in X by ENUMSET1:def_1; ::_thesis: verum
end;
registration
cluster finite non degenerate simplified for Pythagorean_triple ;
existence
ex b1 being Pythagorean_triple st
( not b1 is degenerate & b1 is simplified )
proof
consider X being Pythagorean_triple such that
A1: ( not X is degenerate & X is simplified ) and
4 * 1 in X by Th14;
take X ; ::_thesis: ( not X is degenerate & X is simplified )
thus ( not X is degenerate & X is simplified ) by A1; ::_thesis: verum
end;
end;
theorem :: PYTHTRIP:15
{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_relative_prime ) by ENUMSET1:def_1, INT_2:def_3;
( not 0 in X & 3 in X ) by ENUMSET1:def_1;
hence {3,4,5} is non degenerate simplified Pythagorean_triple by A1, Def6, Def8; ::_thesis: verum
end;
theorem :: PYTHTRIP:16
{ X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is infinite
proof
set T = { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ;
for m being Element of NAT ex n being Element of NAT st
( n >= m & n in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } )
proof
let m be Element of NAT ; ::_thesis: ex n being Element of NAT st
( n >= m & n in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } )
set m9 = m + 1;
set n = 4 * (m + 1);
take 4 * (m + 1) ; ::_thesis: ( 4 * (m + 1) >= m & 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } )
consider X being Pythagorean_triple such that
A1: ( not X is degenerate & X is simplified ) and
A2: 4 * (m + 1) in X by Th14;
(4 * (m + 1)) + 0 = (1 * (m + 1)) + (3 * (m + 1)) ;
then A3: 4 * (m + 1) >= (m + 1) + 0 by XREAL_1:6;
m + 1 >= m by NAT_1:11;
hence 4 * (m + 1) >= m by A3, XXREAL_0:2; ::_thesis: 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) }
X in { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } by A1;
hence 4 * (m + 1) in union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } by A2, TARSKI:def_4; ::_thesis: verum
end;
then A4: union { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is infinite by Th9;
now__::_thesis:_for_X_being_set_st_X_in__{__X_where_X_is_Pythagorean_triple_:_(_not_X_is_degenerate_&_X_is_simplified_)__}__holds_
X_is_finite
let X be set ; ::_thesis: ( X in { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } implies X is finite )
assume X in { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } ; ::_thesis: X is finite
then ex X9 being Pythagorean_triple st
( X = X9 & not X9 is degenerate & X9 is simplified ) ;
hence X is finite ; ::_thesis: verum
end;
hence { X where X is Pythagorean_triple : ( not X is degenerate & X is simplified ) } is infinite by A4, FINSET_1:7; ::_thesis: verum
end;