hereby :: thesis: ( ex m, n being Element of NAT st

( m in X & n in X & m,n are_coprime ) implies X is simplified )

assume
ex m, n being Element of NAT st ( m in X & n in X & m,n are_coprime ) 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_coprime )

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_coprime )

take b = b; :: thesis: ( a in X & b in X & a,b are_coprime )

thus a in X by A3, ENUMSET1:def 1; :: thesis: ( b in X & a,b are_coprime )

thus b in X by A3, ENUMSET1:def 1; :: thesis: a,b are_coprime

end;( a in X & b in X & a,b are_coprime )

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_coprime )

take b = b; :: thesis: ( a in X & b in X & a,b are_coprime )

thus a in X by A3, ENUMSET1:def 1; :: thesis: ( b in X & a,b are_coprime )

thus b in X by A3, ENUMSET1:def 1; :: thesis: a,b are_coprime

now :: thesis: for k being Nat st k divides a & k divides b holds

k = 1

hence
a,b are_coprime
; :: thesis: verumk = 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; :: thesis: verum

end;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; :: thesis: verum

( m in X & n in X & m,n are_coprime ) ; :: 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_coprime ;

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;

then k divides 1 by A7, NAT_D:def 5;

hence k = 1 by WSIERP_1:15; :: thesis: verum