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 ) )
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 & n >= 0 + 1 ) by NAT_1:13;
then A2: n + n > 0 + 1 by XREAL_1:10;
then (2 * n) ^2 > 1 ^2 by SQUARE_1:78;
then ((2 * n) ^2 ) - (1 ^2 ) > 0 by XREAL_1:52;
then reconsider a = 1 * (((2 * n) ^2 ) - (1 ^2 )) as Element of NAT by INT_1:16;
set b = 1 * ((2 * 1) * (2 * n));
set c = 1 * (((2 * n) ^2 ) + (1 ^2 ));
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 )
A4: a <> 0 ;
1 * ((2 * 1) * (2 * n)) <> 0 by A1;
hence not 0 in X by A4, ENUMSET1:def 1; :: according to PYTHTRIP:def 6 :: thesis: ( X is simplified & 4 * n in X )
A5: a in X by ENUMSET1:def 1;
A6: 1 * (((2 * n) ^2 ) + (1 ^2 )) in X by ENUMSET1:def 1;
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:111
.= (abs (1 * (((2 * n) ^2 ) + (1 ^2 )))) gcd (abs (- 2)) by INT_2:51
.= (abs (1 * (((2 * n) ^2 ) + (1 ^2 )))) gcd (abs 2) by COMPLEX1:138
.= ((2 * (2 * (n ^2 ))) + 1) gcd 2 by INT_2:51
.= 1 gcd 2 by EULER_1:17
.= 1 by WSIERP_1:13 ;
then a,1 * (((2 * n) ^2 ) + (1 ^2 )) are_relative_prime by INT_2:def 4;
hence X is simplified by A5, A6, Def8; :: thesis: 4 * n in X
thus 4 * n in X by ENUMSET1:def 1; :: thesis: verum