let p, q be Prime; :: thesis: for n being Nat holds
( not (p * (p + 1)) + (q * (q + 1)) = n * (n + 1) or ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )
let n be Nat; :: thesis: ( not (p * (p + 1)) + (q * (q + 1)) = n * (n + 1) or ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )
assume (p * (p + 1)) + (q * (q + 1)) = n * (n + 1) ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )
then A1: p * (p + 1) = (n - q) * ((n + q) + 1) ;

A2: now :: thesis: not n <= q

assume n <= q ; :: thesis: contradiction
then n - q <= q - q by XREAL_1:9;
then n - q <= 0 ;
hence contradiction by A1; :: thesis: verum

end;

then A3: n - q > q - q by XREAL_1:9;
A4: n - q in NAT by A2, INT_1:5;
p divides p * (p + 1) ;

per cases then ( p divides n - q or p divides (n + q) + 1 ) by A1, INT_5:7;

suppose p divides n - q ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

then A5: p <= n - q by A3, INT_2:27;
then A6: p + 1 <= (n - q) + 1 by XREAL_1:6;
p * (p + 1) <= (n - q) * (p + 1) by A5, XREAL_1:64;
then (n + q) + 1 <= p + 1 by A1, A3, XREAL_1:68;
then (n + q) + 1 <= (n - q) + 1 by A6, XXREAL_0:2;
then n + q <= n - q by XREAL_1:8;
hence ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) ) by XREAL_1:6; :: thesis: verum

end;

suppose p divides (n + q) + 1 ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

then consider k being Nat such that
A7: (n + q) + 1 = p * k by NAT_D:def 3;
A8: p * (p + 1) = (n - q) * (p * k) by A1, A7;
(((n - q) * k) * p) / p = (n - q) * k by XCMPLX_1:89;
then A9: p + 1 = k * (n - q) by A8, XCMPLX_1:89;
( k = 0 or k >= 0 + 1 ) by NAT_1:13;

per cases then ( k = 0 or k = 1 or k > 1 ) by XXREAL_0:1;

suppose k = 0 ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

hence ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) ) by A7; :: thesis: verum

end;

suppose k = 1 ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

hence ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) ) by A7, A9; :: thesis: verum

end;

suppose k > 1 ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

then A10: k + 1 > 1 + 1 by XREAL_1:8;
A11: 2 * q = ((k * p) - 1) - (n - q) by A7
.= ((k * ((k * (n - q)) - 1)) - 1) - (n - q) by A9
.= (k + 1) * (((k - 1) * (n - q)) - 1) ;
then k + 1 divides 2 * q ;

per cases then ( k + 1 = q or k + 1 = 2 * q ) by A10, GR_CY_3:1, XPRIMES1:2;

suppose A12: k + 1 = q ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

A13: (2 * q) / q = 2 by XCMPLX_1:89;
1 < q by INT_2:def 4;
then 1 + 1 <= q by NAT_1:13;
then A14: q - 2 in NAT by INT_1:5;
2 = ((k - 1) * (n - q)) - 1 by A12, A11, A13, XCMPLX_1:89;

per cases then ( ( q - 2 = 1 & n - q = 3 ) or ( q - 2 = 3 & n - q = 1 ) ) by A12, A14, A4, Th26, XPRIMES1:3;

suppose ( q - 2 = 1 & n - q = 3 ) ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

then ( q = 3 & n = 6 ) ;
hence ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) ) by A9, A12; :: thesis: verum

end;

suppose ( q - 2 = 3 & n - q = 1 ) ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

then ( q = 5 & n = 6 ) ;
hence ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) ) by A9, A12; :: thesis: verum

end;

end;

end;

suppose A15: k + 1 = 2 * q ; :: thesis: ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) )

then (k + 1) * 1 = (k + 1) * (((k - 1) * (n - q)) - 1) by A11;
then 1 = ((k - 1) * (n - q)) - 1 by XCMPLX_1:5;
then (2 * (q - 1)) * (n - q) = 2 * 1 by A15;
then (q - 1) * (n - q) = 1 ;
then ( q - 1 = 1 & n - q = 1 ) by A4, NAT_1:15;
then ( q = 2 & n = 3 ) ;
hence ( ( p = 2 & q = 2 & n = 3 ) or ( p = 5 & q = 3 & n = 6 ) or ( p = 3 & q = 5 & n = 6 ) ) by A9, A15; :: thesis: verum

end;

end;

end;

end;

end;

end;