given x, y, z being positive Integer such that A1: (((4 * x) * y) - x) - y = z ^2 ; :: thesis: contradiction
consider p, k being Nat such that
A2: p = (4 * k) + 3 and
A3: p is prime and
A4: p divides (4 * (x - 1)) + 3 by NUMBER05:3;
reconsider p = p as Prime by A3;
A5: p > 1 by INT_2:def 4;
A6: p - 1 <> 1 by A2;
A7: Euler p = p - 1 by EULER_1:20;
A8: (2 * z) |^ (p - 1) = (2 * z) |^ (2 * ((2 * k) + 1)) by A2
.= ((2 * z) |^ 2) |^ ((2 * k) + 1) by NEWTON:9 ;
A9: (2 * z) |^ 2 = (2 * z) ^2 by WSIERP_1:1;
A10: ((4 * x) - 1) * ((4 * y) - 1) = ((2 * z) ^2) + 1 by A1;
then A11: p divides ((2 * z) ^2) + 1 by A4, INT_2:2;
(2 * z) ^2 , - 1 are_congruent_mod p by A4, A10, INT_2:2;
then ((2 * z) ^2) |^ ((2 * k) + 1),(- 1) |^ ((2 * k) + 1) are_congruent_mod p by GR_CY_3:34;
then A12: (((2 * z) |^ 2) |^ ((2 * k) + 1)) mod p = (- 1) mod p by A9, NAT_D:64
.= p - 1 by NUMBER10:5 ;
2 * z,p are_coprime

proof

let w be Prime; :: according to PYTHTRIP:def 2 :: thesis: ( not R20(w,2 * z) or not R20(w,p) )
assume that
A13: w divides 2 * z and
A14: w divides p ; :: thesis: contradiction
w > 1 by INT_2:def 4;
then w = p by A14, INT_2:def 4;
then p divides (2 * z) ^2 by A13, INT_2:2;
then p divides (((2 * z) ^2) + 1) - ((2 * z) ^2) by A11, INT_5:1;
hence contradiction by A5, WSIERP_1:15; :: thesis: verum

end;

hence contradiction by A6, A7, A8, A12, INT_2:def 4, EULER_2:18; :: thesis: verum