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
.= |.(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