A1:
5 = 6 - 1
;
let c be Real; ( c > 6 implies c ^2 < 2 to_power c )
assume A2:
c > 6
; c ^2 < 2 to_power c
set i0 = [\c/];
set i1 = [/c\];
per cases
( [\c/] = [/c\] or not [\c/] = [/c\] )
;
suppose
not
[\c/] = [/c\]
;
c ^2 < 2 to_power cthen 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;
verum end; end;