let n be Nat; ( 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
; 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 b = 1 * ((2 * 1) * (2 * n)), c = 1 * (((2 * n) ^2) + (1 ^2)), n = n as Element of NAT by ORDINAL1:def 12;
ex k, m, w being Element of NAT st
( m <= w & {a,b,c} = {(k * ((w ^2) - (m ^2))),(k * ((2 * m) * w)),(k * ((w ^2) + (m ^2)))} )
proof
take k = 1;
ex m, w being Element of NAT st
( m <= w & {a,b,c} = {(k * ((w ^2) - (m ^2))),(k * ((2 * m) * w)),(k * ((w ^2) + (m ^2)))} )
take m = 1;
ex w being Element of NAT st
( m <= w & {a,b,c} = {(k * ((w ^2) - (m ^2))),(k * ((2 * m) * w)),(k * ((w ^2) + (m ^2)))} )
take w = 2
* n;
( m <= w & {a,b,c} = {(k * ((w ^2) - (m ^2))),(k * ((2 * m) * w)),(k * ((w ^2) + (m ^2)))} )
thus
(
m <= w &
{a,b,c} = {(k * ((w ^2) - (m ^2))),(k * ((2 * m) * w)),(k * ((w ^2) + (m ^2)))} )
by A2;
verum
end;
then reconsider X = {a,b,c} as Pythagorean_triple by Def5;
take
X
; ( not X is degenerate & X is simplified & 4 * n in X )
( a <> 0 & b <> 0 )
by A1;
hence
not 0 in X
by ENUMSET1:def 1; ORDINAL1:def 16 ( X is simplified & 4 * n in X )
a - c = - 2
;
then a gcd c =
(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,c are_coprime
;
( a in X & c in X )
by ENUMSET1:def 1;
hence
X is simplified
by A3; 4 * n in X
thus
4 * n in X
by ENUMSET1:def 1; verum