A1: 5 = 6 - 1 ;
let c be Real; :: thesis: ( c > 6 implies c ^2 < 2 to_power c )
assume A2: c > 6 ; :: thesis: c ^2 < 2 to_power c
set i0 = [\c/];
set i1 = [/c\];
per cases ( [\c/] = [/c\] or not [\c/] = [/c\] ) ;
suppose [\c/] = [/c\] ; :: thesis: c ^2 < 2 to_power c
then c is Integer by INT_1:34;
then reconsider c = c as Element of NAT by A2, INT_1:3;
c + 0 < c + 1 by XREAL_1:8;
then A3: c ^2 < (c + 1) ^2 by SQUARE_1:16;
(c + 1) ^2 < 2 to_power c by A2, Lm8;
hence c ^2 < 2 to_power c by A3, XXREAL_0:2; :: thesis: verum
end;
suppose not [\c/] = [/c\] ; :: thesis: c ^2 < 2 to_power c
then A4: [\c/] + 1 = [/c\] by INT_1:41;
then A5: [\c/] = [/c\] - 1 ;
A6: [/c\] >= c by INT_1:def 7;
then reconsider i1 = [/c\] as Element of NAT by A2, INT_1:3;
i1 > 6 by A2, A6, XXREAL_0:2;
then A7: [\c/] > 5 by A1, A5, XREAL_1:9;
then reconsider i0 = [\c/] as Element of NAT by INT_1:3;
i0 <= c by INT_1:def 6;
then A8: 2 to_power i0 <= 2 to_power c by PRE_FF:8;
i1 >= c by INT_1:def 7;
then A9: i1 ^2 >= c ^2 by A2, SQUARE_1:15;
i0 >= 5 + 1 by A7, INT_1:7;
then i1 ^2 < 2 to_power i0 by A4, Lm8;
then c ^2 < 2 to_power i0 by A9, XXREAL_0:2;
hence c ^2 < 2 to_power c by A8, XXREAL_0:2; :: thesis: verum
end;
end;