given x, y, z, t being positive Nat such that A1:
(x ^2) + (2 * (y ^2)) = z ^2
and
A2:
(2 * (x ^2)) + (y ^2) = t ^2
; contradiction
set d = x gcd y;
set x1 = x div (x gcd y);
set y1 = y div (x gcd y);
set z1 = z div (x gcd y);
set t1 = t div (x gcd y);
A3:
x gcd y divides x
by INT_2:def 2;
A4:
x gcd y divides y
by INT_2:def 2;
then A5:
y div (x gcd y) = y / (x gcd y)
by RING_3:6;
A6:
(x gcd y) ^2 divides x ^2
by A3, PYTHTRIP:6;
A7:
(x gcd y) ^2 divides y ^2
by A4, PYTHTRIP:6;
then
(x gcd y) ^2 divides 2 * (y ^2)
by INT_2:2;
then
(x gcd y) ^2 divides z ^2
by A1, A6, NAT_D:8;
then A8:
z div (x gcd y) = z / (x gcd y)
by RING_3:6, PYTHTRIP:6;
(x gcd y) ^2 divides 2 * (x ^2)
by A6, INT_2:2;
then
(x gcd y) ^2 divides t ^2
by A2, A7, NAT_D:8;
then A9:
t div (x gcd y) = t / (x gcd y)
by RING_3:6, PYTHTRIP:6;
A10: ((x div (x gcd y)) ^2) + (2 * ((y div (x gcd y)) ^2)) =
((x ^2) / ((x gcd y) ^2)) + (2 * ((y / (x gcd y)) ^2))
by A5, XCMPLX_1:76
.=
((x ^2) / ((x gcd y) ^2)) + (2 * ((y ^2) / ((x gcd y) ^2)))
by XCMPLX_1:76
.=
(z ^2) / ((x gcd y) ^2)
by A1
.=
(z div (x gcd y)) ^2
by A8, XCMPLX_1:76
;
(2 * ((x div (x gcd y)) ^2)) + ((y div (x gcd y)) ^2) =
(2 * ((x ^2) / ((x gcd y) ^2))) + ((y / (x gcd y)) ^2)
by A5, XCMPLX_1:76
.=
(2 * ((x ^2) / ((x gcd y) ^2))) + ((y ^2) / ((x gcd y) ^2))
by XCMPLX_1:76
.=
(t ^2) / ((x gcd y) ^2)
by A2
.=
(t div (x gcd y)) ^2
by A9, XCMPLX_1:76
;
hence
contradiction
by A10, Th76, Lm12; verum