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 ORDINAL1:def 16 :: 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

.= |.(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,1 * (((2 * n) ^2) + (1 ^2)) are_coprime ;

( a in X & 1 * (((2 * n) ^2) + (1 ^2)) in X ) by ENUMSET1:def 1;

hence X is simplified by A3; :: thesis: 4 * n in X

thus 4 * n in X by ENUMSET1:def 1; :: thesis: verum

( 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 ORDINAL1:def 16 :: 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

.= |.(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,1 * (((2 * n) ^2) + (1 ^2)) are_coprime ;

( a in X & 1 * (((2 * n) ^2) + (1 ^2)) in X ) by ENUMSET1:def 1;

hence X is simplified by A3; :: thesis: 4 * n in X

thus 4 * n in X by ENUMSET1:def 1; :: thesis: verum