let s be 4 _or_greater Nat; for x being non zero s -gonal number st s <> 2 holds
Polygon (s,(IndexPoly (s,x))) = x
let x be non zero s -gonal number ; ( s <> 2 implies Polygon (s,(IndexPoly (s,x))) = x )
assume
s <> 2
; Polygon (s,(IndexPoly (s,x))) = x
then A1:
s - 2 <> 0
;
A2:
0 <= (((8 * s) - 16) * x) + ((s - 4) ^2)
by Th35;
set qq = sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2));
set w = IndexPoly (s,x);
A3: ((IndexPoly (s,x)) ^2) * (s - 2) =
(((((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) ^2) / (((2 * s) - 4) ^2)) * (s - 2)
by XCMPLX_1:76
.=
(((((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) ^2) / ((4 * (s - 2)) * (s - 2))) * (s - 2)
.=
((((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) ^2) + ((s - 4) ^2)) + ((2 * (sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2)))) * (s - 4))) / (4 * (s - 2))
by XCMPLX_1:92, A1
;
A4: (IndexPoly (s,x)) * (s - 4) =
((((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) + s) - 4) * (s - 4)) / ((2 * s) - 4)
by XCMPLX_1:74
.=
(2 * (((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) * (s - 4)) + ((s - 4) ^2))) / (2 * (2 * (s - 2)))
by XCMPLX_1:91
.=
(2 * (((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) * (s - 4)) + ((s - 4) ^2))) / (4 * (s - 2))
;
A5:
(sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) ^2 = (((8 * s) - 16) * x) + ((s - 4) ^2)
by SQUARE_1:def 2, A2;
Polygon (s,(IndexPoly (s,x))) =
((((((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) ^2) + ((s - 4) ^2)) + ((2 * (sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2)))) * (s - 4))) - (2 * (((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) * (s - 4)) + ((s - 4) ^2)))) / (4 * (s - 2))) / 2
by XCMPLX_1:120, A3, A4
.=
(((((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) ^2) + ((s - 4) ^2)) + ((2 * (sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2)))) * (s - 4))) - (2 * (((sqrt ((((8 * s) - 16) * x) + ((s - 4) ^2))) * (s - 4)) + ((s - 4) ^2)))) / ((4 * (s - 2)) * 2)
by XCMPLX_1:78
.=
x
by A1, XCMPLX_1:89, A5
;
hence
Polygon (s,(IndexPoly (s,x))) = x
; verum