let s be non zero Nat; :: thesis: for x being non zero s -gonal number st s >= 4 holds
IndexPoly (s,x) in NAT
let x be non zero s -gonal number ; :: thesis: ( s >= 4 implies IndexPoly (s,x) in NAT )
assume A1: s >= 4 ; :: thesis: IndexPoly (s,x) in NAT
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;
A4: s - 2 <> 0 by A1;
n <> 0 by A2;
then A5: 2 * n >= 1 by Th1;
s >= 0 + 4 by A1;
then A6: s - 4 >= 0 by XREAL_1:19;
s - 2 >= s - 4 by XREAL_1:13;
then A7: (2 * n) * (s - 2) >= 0 + (1 * (s - 4)) by A5, A6, XREAL_1:66;
IndexPoly (s,x) = (((((2 * n) * (s - 2)) - (s - 4)) + s) - 4) / ((2 * s) - 4) by SQUARE_1:22, A7, A3, XREAL_1:19
.= ((2 * n) * (s - 2)) / (2 * (s - 2))
.= (2 * n) / 2 by A4, XCMPLX_1:91
.= n ;
hence IndexPoly (s,x) in NAT by ORDINAL1:def 12; :: thesis: verum