let a, b, k be Nat; :: thesis: for p being Prime st p = (4 * k) + 3 & p divides (a ^2) + (b ^2) holds
( p divides a & p divides b )
let p be Prime; :: thesis: ( p = (4 * k) + 3 & p divides (a ^2) + (b ^2) implies ( p divides a & p divides b ) )
assume that
A1: p = (4 * k) + 3 and
A2: p divides (a ^2) + (b ^2) ; :: thesis: ( p divides a & p divides b )
assume A3: ( not p divides a or not p divides b ) ; :: thesis: contradiction
A4: a |^ 2 = a ^2 by WSIERP_1:1;
A5: b |^ 2 = b ^2 by WSIERP_1:1;

A6: now :: thesis: ( not p divides a implies not p divides b )

assume A7: not p divides a ; :: thesis: not p divides b
assume A8: p divides b ; :: thesis: contradiction
b divides b ^2 ;
then p divides b ^2 by A8, INT_2:9;
then p divides ((a ^2) + (b ^2)) - (b ^2) by A2, INT_5:1;
hence contradiction by A4, A7, NAT_3:5; :: thesis: verum

end;

A9: now :: thesis: ( not p divides b implies not p divides a )

assume A10: not p divides b ; :: thesis: not p divides a
assume A11: p divides a ; :: thesis: contradiction
a divides a ^2 ;
then p divides a ^2 by A11, INT_2:9;
then p divides ((a ^2) + (b ^2)) - (a ^2) by A2, INT_5:1;
hence contradiction by A5, A10, NAT_3:5; :: thesis: verum

end;

A12: Euler p = p - 1 by EULER_1:20;
A13: ((4 * k) + 1) + 2 > 0 + 2 by XREAL_1:6;

per cases ( ( a = 0 & b = 0 ) or ( a <> 0 & b = 0 ) or ( a = 0 & b <> 0 ) or ( a <> 0 & b <> 0 ) ) ;

suppose ( a = 0 & b = 0 ) ; :: thesis: contradiction

hence contradiction by A3, INT_2:12; :: thesis: verum

end;

suppose ( ( a <> 0 & b = 0 ) or ( a = 0 & b <> 0 ) ) ; :: thesis: contradiction

hence contradiction by A2, A3, A4, A5, NAT_3:5, INT_2:12; :: thesis: verum

end;

suppose A14: ( a <> 0 & b <> 0 ) ; :: thesis: contradiction

( a,p are_coprime & b,p are_coprime ) by A3, A6, A9, Th4;
then ( (a |^ (p - 1)) mod p = 1 & (b |^ (p - 1)) mod p = 1 ) by A12, A14, EULER_2:18, INT_2:def 4;
then ((a |^ (p - 1)) + (b |^ (p - 1))) mod p = (1 + 1) mod p by NAT_D:66
.= 2 by A1, A13, NAT_D:24 ;
then A15: not p divides (a |^ (p - 1)) + (b |^ (p - 1)) by INT_1:62;
A16: a |^ (p - 1) = a |^ (2 * ((2 * k) + 1)) by A1
.= (a |^ 2) |^ ((2 * k) + 1) by NEWTON:9 ;
A17: b |^ (p - 1) = b |^ (2 * ((2 * k) + 1)) by A1
.= (b |^ 2) |^ ((2 * k) + 1) by NEWTON:9 ;
(a |^ 2) + (b |^ 2) divides ((a |^ 2) |^ ((2 * k) + 1)) + ((b |^ 2) |^ ((2 * k) + 1)) by NEWTON01:35;
hence contradiction by A2, A4, A5, A15, A16, A17, INT_2:9; :: thesis: verum

end;

end;