let p be Prime; :: thesis: for n, s being Nat st Sum (canFS (NatDivisors p)) = n |^ s & 2 <= s & s <= 10 & not ( s = 2 & p = 3 ) & not ( s = 3 & p = 7 ) & not ( s = 5 & p = 31 ) holds
( s = 7 & p = 127 )
let n, s be Nat; :: thesis: ( Sum (canFS (NatDivisors p)) = n |^ s & 2 <= s & s <= 10 & not ( s = 2 & p = 3 ) & not ( s = 3 & p = 7 ) & not ( s = 5 & p = 31 ) implies ( s = 7 & p = 127 ) )
assume A1: ( Sum (canFS (NatDivisors p)) = n |^ s & 2 <= s & s <= 10 ) ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )
A2: n = 2 by Th21, A1;
A3: p <> 1 by INT_2:def 4;
NatDivisors p = {1,p} by LATSTONE:26;
then ( canFS (NatDivisors p) = <*1,p*> or canFS (NatDivisors p) = <*p,1*> ) by A3, POLYVIE1:1;
then A4: Sum (canFS (NatDivisors p)) = 1 + p by RVSUM_1:77;
A5: n |^ (1 + 1) = (2 |^ 1) * 2 by A2, NEWTON:6;
then A6: n |^ (2 + 1) = 4 * 2 by A2, NEWTON:6;
then A7: n |^ (3 + 1) = 8 * 2 by A2, NEWTON:6;
then A8: n |^ (4 + 1) = 16 * 2 by A2, NEWTON:6;
then A9: n |^ (5 + 1) = 32 * 2 by A2, NEWTON:6;
then A10: n |^ (6 + 1) = 64 * 2 by A2, NEWTON:6;
then A11: n |^ (7 + 1) = 128 * 2 by A2, NEWTON:6;
then A12: n |^ (8 + 1) = 256 * 2 by A2, NEWTON:6;
then A13: n |^ (9 + 1) = 512 * 2 by A2, NEWTON:6;
not not s = 0 & ... & not s = 10 by A1;

per cases then ( s = 2 or s = 3 or s = 4 or s = 5 or s = 6 or s = 7 or s = 8 or s = 9 or s = 10 ) by A1;

suppose A14: s = 2 ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )

then n |^ s = 4 by A5;
hence ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) ) by A14, A4, A1; :: thesis: verum

end;

suppose A15: s = 3 ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )

then n |^ s = 8 by A6;
hence ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) ) by A15, A4, A1; :: thesis: verum

end;

suppose s = 4 ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )

then n |^ s = 16 by A7;
hence ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) ) by A4, A1, XPRIMES0:15; :: thesis: verum

end;

suppose A16: s = 5 ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )

then n |^ s = 32 by A8;
hence ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) ) by A4, A1, A16; :: thesis: verum

end;

suppose s = 6 ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )

then n |^ s = 64 by A9;
hence ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) ) by A4, A1, XPRIMES0:63; :: thesis: verum

end;

suppose A17: s = 7 ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )

then n |^ s = 128 by A10;
hence ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) ) by A4, A1, A17; :: thesis: verum

end;

suppose s = 8 ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )

then n |^ s = 256 by A11;
hence ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) ) by A4, A1, XPRIMES0:255; :: thesis: verum

end;

suppose s = 9 ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )

then n |^ s = 512 by A12;
hence ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) ) by A4, A1, XPRIMES0:511; :: thesis: verum

end;

suppose s = 10 ; :: thesis: ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) )

then n |^ s = 1024 by A13;
hence ( ( s = 2 & p = 3 ) or ( s = 3 & p = 7 ) or ( s = 5 & p = 31 ) or ( s = 7 & p = 127 ) ) by A4, A1, XPRIMES0:1023; :: thesis: verum

end;

end;