let p be Prime; :: thesis: ( (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square iff p = 3 )
set x = (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4);
thus ( (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square implies p = 3 ) :: thesis: ( p = 3 implies (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square )

proof

given n being Nat such that A1: (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) = n ^2 ; :: according to PYTHTRIP:def 3 :: thesis: p = 3
A2: p |^ 2 = p ^2 by WSIERP_1:1;
A3: p |^ 3 = (p ^2) * p by POLYEQ_5:2;
A4: p |^ 4 = ((p * p) * p) * p by POLYEQ_5:3
.= (p ^2) * (p ^2) ;
((((4 + (4 * p)) + (4 * (p ^2))) + (4 * (p |^ 3))) + (4 * (p |^ 4))) - (((4 * (p |^ 4)) + (4 * (p |^ 3))) + (p ^2)) = (4 + (4 * p)) + (3 * (p ^2)) ;
then ((2 * (p ^2)) + p) ^2 < (2 * n) ^2 by A1, A2, A3, A4, XREAL_1:47;
then A5: (2 * (p ^2)) + p < 2 * n by XREAL_1:66;
((((2 * (p ^2)) + p) + 2) ^2) - ((((4 + (4 * p)) + (4 * (p ^2))) + (4 * (p |^ 3))) + (4 * (p |^ 4))) = 5 * (p ^2) by A3, A4;
then (2 * n) ^2 < (((2 * (p ^2)) + p) + 2) ^2 by A1, A2, XREAL_1:47;
then 2 * n < ((2 * (p ^2)) + p) + 2 by XREAL_1:66;
then (2 * n) ^2 = (((2 * (p ^2)) + p) + 1) ^2 by A5, Th1;
then (p + 1) * (p - 3) = 0 by A1, A2, A3, A4;
then ( p + 1 = 0 or p - 3 = 0 ) ;
hence p = 3 ; :: thesis: verum

end;

thus ( p = 3 implies (((1 + p) + (p |^ 2)) + (p |^ 3)) + (p |^ 4) is square ) by Lm8, Lm9, Lm10, Lm11; :: thesis: verum