let k be Nat; :: thesis: for i, j being Integer
for p being Prime st p = (4 * k) + 3 & p divides (i ^2) + (j ^2) holds
( p divides i & p divides j )
let i, j be Integer; :: thesis: for p being Prime st p = (4 * k) + 3 & p divides (i ^2) + (j ^2) holds
( p divides i & p divides j )
let p be Prime; :: thesis: ( p = (4 * k) + 3 & p divides (i ^2) + (j ^2) implies ( p divides i & p divides j ) )
assume A1: ( p = (4 * k) + 3 & p divides (i ^2) + (j ^2) ) ; :: thesis: ( p divides i & p divides j )
A2: i ^2 = (- i) ^2 ;
A3: j ^2 = (- j) ^2 ;

per cases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( i < 0 & j < 0 ) ) ;

suppose ( i >= 0 & j >= 0 ) ; :: thesis: ( p divides i & p divides j )

then ( i in NAT & j in NAT ) by INT_1:3;
hence ( p divides i & p divides j ) by A1, Lm17; :: thesis: verum

end;

suppose ( i >= 0 & j < 0 ) ; :: thesis: ( p divides i & p divides j )

then ( i in NAT & - j in NAT ) by INT_1:3;
then ( p divides i & p divides - j ) by A1, A3, Lm17;
hence ( p divides i & p divides j ) by INT_2:10; :: thesis: verum

end;

suppose ( i < 0 & j >= 0 ) ; :: thesis: ( p divides i & p divides j )

then ( - i in NAT & j in NAT ) by INT_1:3;
then ( p divides - i & p divides j ) by A1, A2, Lm17;
hence ( p divides i & p divides j ) by INT_2:10; :: thesis: verum

end;

suppose ( i < 0 & j < 0 ) ; :: thesis: ( p divides i & p divides j )

then ( - i in NAT & - j in NAT ) by INT_1:3;
then ( p divides - i & p divides - j ) by A1, A2, A3, Lm17;
hence ( p divides i & p divides j ) by INT_2:10; :: thesis: verum

end;

end;