let x, y, z be Nat; ( x,y are_coprime & (x |^ 2) + (y |^ 2) = z |^ 4 & x is odd implies 7 divides x * y )
assume that
A1:
x,y are_coprime
and
A2:
(x |^ 2) + (y |^ 2) = z |^ 4
; ( not x is odd or 7 divides x * y )
per cases
( 7 divides y or not 7 divides y )
;
suppose A3:
not 7
divides y
;
( not x is odd or 7 divides x * y )set c =
z |^ 2;
A4:
(
x |^ 2
= x ^2 &
y |^ 2
= y ^2 )
by NEWTON:81;
A5:
z |^ 2
= z ^2
by NEWTON:81;
A6:
z |^ (2 + 2) = (z |^ 2) ^2
by NEWTON:8;
assume
x is
odd
;
7 divides x * ythen consider n,
m being
Element of
NAT such that
n <= m
and A7:
x = (m ^2) - (n ^2)
and A8:
y = (2 * n) * m
and A9:
z ^2 = (m ^2) + (n ^2)
by A1, A2, A4, A5, A6, PYTHTRIP:11;
A10:
not 7
divides m
by A3, A8, INT_2:2;
y = n * (2 * m)
by A8;
then A11:
not 7
divides n
by A3, INT_2:2;
A12:
(
(z ^2) mod 7
= 0 or
(z ^2) mod 7
= 1 or
(z ^2) mod 7
= 2 or
(z ^2) mod 7
= 4 )
by NUMBER02:49;
A13:
(
(m ^2) mod 7
= ((m mod 7) * (m mod 7)) mod 7 &
(n ^2) mod 7
= ((n mod 7) * (n mod 7)) mod 7 )
by NAT_D:67;
A14:
((m ^2) + (n ^2)) mod 7
= (((m ^2) mod 7) + ((n ^2) mod 7)) mod 7
by NAT_D:66;
A15:
(
((1 * 7) + 2) mod 7
= 2 &
((2 * 7) + 2) mod 7
= 2 &
((3 * 7) + 4) mod 7
= 4 &
((5 * 7) + 1) mod 7
= 1 )
by NUMBER02:16;
( not not
m mod (6 + 1) = 0 & ... & not
m mod (6 + 1) = 6 & not not
n mod (6 + 1) = 0 & ... & not
n mod (6 + 1) = 6 )
by NUMBER03:11;
then
(((m ^2) mod 7) - ((n ^2) mod 7)) mod 7
= 0
by A9, A10, A11, A12, A13, A14, A15, NAT_D:24, INT_1:62;
then
((m ^2) - (n ^2)) mod 7
= 0
by INT_6:7;
then
7
divides x
by A7, INT_1:62;
hence
7
divides x * y
by INT_2:2;
verum end;