let f be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n > 0 holds
f . n = n to_power (log (2,n)) ) implies ex s being eventually-positive Real_Sequence st
( s = f & not s is smooth ) )
assume A1: for n being Element of NAT st n > 0 holds
f . n = n to_power (log (2,n)) ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = f & not s is smooth )
A2: f is eventually-positive

proof

take 1 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not f . b₁ <= 0 )
let n be Nat; :: thesis: ( not 1 <= n or not f . n <= 0 )
A3: n in NAT by ORDINAL1:def 12;
assume A4: n >= 1 ; :: thesis: not f . n <= 0
then f . n = n to_power (log (2,n)) by A1, A3;
hence not f . n <= 0 by A4, POWER:34; :: thesis: verum

end;

set g = f taken_every 2;
reconsider f = f as eventually-positive Real_Sequence by A2;
take f ; :: thesis: ( f = f & not f is smooth )

now :: thesis: not f is smooth

assume f is smooth ; :: thesis: contradiction
then f is_smooth_wrt 2 ;
then consider t being Element of Funcs (NAT,REAL) such that
A5: t = f taken_every 2 and
A6: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A7: c > 0 and
A8: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A6;
A9: sqrt c > 0 by A7, SQUARE_1:25;
set N0 = [/((sqrt c) / (sqrt 2))\];
reconsider N2 = max (N,[/((sqrt c) / (sqrt 2))\]) as Integer by XXREAL_0:16;
set N1 = max (N2,2);
A10: max (N2,2) >= N2 by XXREAL_0:25;
N2 >= [/((sqrt c) / (sqrt 2))\] by XXREAL_0:25;
then A11: max (N2,2) >= [/((sqrt c) / (sqrt 2))\] by A10, XXREAL_0:2;
A12: max (N2,2) is Integer by XXREAL_0:16;
N2 >= N by XXREAL_0:25;
then A13: max (N2,2) >= N by A10, XXREAL_0:2;
max (N2,2) >= 2 by XXREAL_0:25;
then reconsider N1 = max (N2,2) as Element of NAT by A12, INT_1:3;
set n = N1 + 1;
A14: (N1 + 1) to_power (log (2,(N1 + 1))) > 0 by POWER:34;
A15: 2 * (N1 + 1) > 2 * 0 by XREAL_1:68;
A16: sqrt 2 <> 0 by SQUARE_1:25;
A17: sqrt 2 > 0 by SQUARE_1:25;
A18: [/((sqrt c) / (sqrt 2))\] >= (sqrt c) / (sqrt 2) by INT_1:def 7;
A19: N1 + 1 > N1 + 0 by XREAL_1:8;
then N1 + 1 > [/((sqrt c) / (sqrt 2))\] by A11, XXREAL_0:2;
then N1 + 1 > (sqrt c) / (sqrt 2) by A18, XXREAL_0:2;
then (N1 + 1) * (sqrt 2) > ((sqrt c) / (sqrt 2)) * (sqrt 2) by A17, XREAL_1:68;
then (N1 + 1) * (sqrt 2) > sqrt c by A16, XCMPLX_1:87;
then ((N1 + 1) * (sqrt 2)) ^2 > (sqrt c) ^2 by A9, SQUARE_1:16;
then ((N1 + 1) ^2) * ((sqrt 2) ^2) > c by A7, SQUARE_1:def 2;
then A20: 2 * ((N1 + 1) ^2) > c by SQUARE_1:def 2;
(2 * ((N1 + 1) ^2)) * ((N1 + 1) to_power (log (2,(N1 + 1)))) = ((2 * (N1 + 1)) * (N1 + 1)) * ((N1 + 1) to_power (log (2,(N1 + 1))))
.= ((2 * (N1 + 1)) * (2 to_power (log (2,(N1 + 1))))) * ((N1 + 1) to_power (log (2,(N1 + 1)))) by POWER:def 3
.= (2 * (N1 + 1)) * ((2 to_power (log (2,(N1 + 1)))) * ((N1 + 1) to_power (log (2,(N1 + 1)))))
.= (2 * (N1 + 1)) * ((2 * (N1 + 1)) to_power (log (2,(N1 + 1)))) by POWER:30
.= ((2 * (N1 + 1)) to_power 1) * ((2 * (N1 + 1)) to_power (log (2,(N1 + 1)))) by POWER:25
.= (2 * (N1 + 1)) to_power (1 + (log (2,(N1 + 1)))) by A15, POWER:27
.= (2 * (N1 + 1)) to_power ((log (2,2)) + (log (2,(N1 + 1)))) by POWER:52
.= (2 * (N1 + 1)) to_power (log (2,(2 * (N1 + 1)))) by POWER:53 ;
then (2 * (N1 + 1)) to_power (log (2,(2 * (N1 + 1)))) > c * ((N1 + 1) to_power (log (2,(N1 + 1)))) by A14, A20, XREAL_1:68;
then f . (2 * (N1 + 1)) > c * ((N1 + 1) to_power (log (2,(N1 + 1)))) by A1, A15;
then t . (N1 + 1) > c * ((N1 + 1) to_power (log (2,(N1 + 1)))) by A5, ASYMPT_0:def 15;
then A21: t . (N1 + 1) > c * (f . (N1 + 1)) by A1;
N1 + 1 > N by A13, A19, XXREAL_0:2;
hence contradiction by A8, A21; :: thesis: verum

end;

hence ( f = f & not f is smooth ) ; :: thesis: verum