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 )

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

per cases
( n is even or n is odd )
;

end;

suppose
n is even
; :: thesis: ex X being Pythagorean_triple st

( not X is degenerate & n in X )

( not X is degenerate & n in X )

then consider m being Nat such that

A2: n = 2 * m ;

reconsider m = 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,(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 ORDINAL1:def 16 :: thesis: n in X

thus n in X by A2, ENUMSET1:def 1; :: thesis: verum

end;A2: n = 2 * m ;

reconsider m = 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,(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 ORDINAL1:def 16 :: thesis: n in X

thus n in X by A2, ENUMSET1:def 1; :: thesis: verum

suppose
n is odd
; :: thesis: ex X being Pythagorean_triple st

( not X is degenerate & n in X )

( 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 ORDINAL1:def 16 :: thesis: n in X

thus n in X by A4, ENUMSET1:def 1; :: thesis: verum

end;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 ORDINAL1:def 16 :: thesis: n in X

thus n in X by A4, ENUMSET1:def 1; :: thesis: verum