let s be non zero Nat; :: thesis: for x being non zero s -gonal number st s >= 4 holds
(((8 * s) - 16) * x) + ((s - 4) ^2) is square
let x be non zero s -gonal number ; :: thesis: ( s >= 4 implies (((8 * s) - 16) * x) + ((s - 4) ^2) is square )
assume A1: s >= 4 ; :: thesis: (((8 * s) - 16) * x) + ((s - 4) ^2) is square
consider n being Nat such that
A2: x = Polygon (s,n) by Def4;
A3: (((8 * s) - 16) * x) + ((s - 4) ^2) = (((2 * n) * (s - 2)) - (s - 4)) ^2 by A2;
n <> 0 by A2;
then A4: 2 * n >= 1 by Th1;
s >= 0 + 4 by A1;
then A5: s - 4 >= 0 by XREAL_1:19;
s - 2 >= s - 4 by XREAL_1:13;
then (2 * n) * (s - 2) >= 0 + (1 * (s - 4)) by A4, A5, XREAL_1:66;
then ((2 * n) * (s - 2)) - (s - 4) in NAT by INT_1:3, XREAL_1:19;
hence (((8 * s) - 16) * x) + ((s - 4) ^2) is square by A3; :: thesis: verum