let s be non zero Nat; 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 ; ( s >= 4 implies IndexPoly (s,x) in NAT )
assume A1:
s >= 4
; 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; verum