set g = seq_n^ 1;
let f be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds f . n = Step1 n ) implies ex s being eventually-positive Real_Sequence st
( s = f & f is eventually-nondecreasing & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & not s is smooth ) )
assume A1: for n being Element of NAT holds f . n = Step1 n ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = f & f is eventually-nondecreasing & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & not s is smooth )
f is eventually-positive

proof

take 1 ; :: according to ASYMPT_0:def 6 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not f . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not f . n <= 0 )
assume n >= 1 ; :: thesis: not f . n <= 0
then A2: ex m being Element of NAT st
( m ! <= n & n < (m + 1) ! & Step1 n = m ! ) by Def9;
f . n = Step1 n by A1;
hence not f . n <= 0 by A2, NEWTON:23; :: thesis: verum

end;

then reconsider f = f as eventually-positive Real_Sequence ;

now

let k be Element of NAT ; :: thesis: f . k <= f . (k + 1)
thus f . k <= f . (k + 1) :: thesis: verum

proof

per cases ( k = 0 or k > 0 ) ;

suppose A3: k = 0 ; :: thesis: f . k <= f . (k + 1)

A4: f . (0 + 1) = Step1 1 by A1;
f . 0 = Step1 0 by A1
.= 0 by Def9 ;
hence f . k <= f . (k + 1) by A3, A4; :: thesis: verum

end;

suppose k > 0 ; :: thesis: f . k <= f . (k + 1)

then consider n1 being Element of NAT such that
A5: n1 ! <= k and
A6: k < (n1 + 1) ! and
A7: Step1 k = n1 ! by Def9;
A8: k + 1 <= (n1 + 1) ! by A6, INT_1:20;
A9: k <= k + 1 by NAT_1:11;
A10: f . k = n1 ! by A1, A7;

per cases ( k + 1 < (n1 + 1) ! or k + 1 = (n1 + 1) ! ) by A8, XXREAL_0:1;

suppose A11: k + 1 < (n1 + 1) ! ; :: thesis: f . k <= f . (k + 1)

n1 ! <= k + 1 by A9, A5, XXREAL_0:2;
then Step1 (k + 1) = n1 ! by A11, Def9;
hence f . k <= f . (k + 1) by A1, A10; :: thesis: verum

end;

suppose A12: k + 1 = (n1 + 1) ! ; :: thesis: f . k <= f . (k + 1)

A13: (n1 + 1) ! > 0 by NEWTON:23;
n1 + 2 > 0 + 1 by XREAL_1:10;
then 1 * ((n1 + 1) !) < (n1 + 2) * ((n1 + 1) !) by A13, XREAL_1:70;
then A14: k + 1 < ((n1 + 1) + 1) ! by A12, NEWTON:21;
f . (k + 1) = Step1 (k + 1) by A1
.= (n1 + 1) ! by A12, A14, Def9 ;
hence f . k <= f . (k + 1) by A10, Lm51, NAT_1:11; :: thesis: verum

end;

end;

end;

end;

end;

end;

then A15: for k being Element of NAT st k >= 0 holds
f . k <= f . (k + 1) ;
A16: 1 = 2 - 1 ;

A17: now

set h = f taken_every 2;
assume f is smooth ; :: thesis: contradiction
then f is_smooth_wrt 2 by ASYMPT_0:def 20;
then f taken_every 2 in Big_Oh f by ASYMPT_0:def 19;
then consider t being Element of Funcs (NAT,REAL) such that
A18: t = f taken_every 2 and
A19: 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
c > 0 and
A20: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A19;
set n2 = max ((max (N,3)),([/c\] + 1));
A21: max ((max (N,3)),([/c\] + 1)) >= max (N,3) by XXREAL_0:25;
max (N,3) >= N by XXREAL_0:25;
then A22: max ((max (N,3)),([/c\] + 1)) >= N by A21, XXREAL_0:2;
A23: max ((max (N,3)),([/c\] + 1)) >= [/c\] + 1 by XXREAL_0:25;
A24: max ((max (N,3)),([/c\] + 1)) is Integer by XXREAL_0:16;
A25: max (N,3) >= 3 by XXREAL_0:25;
then A26: max ((max (N,3)),([/c\] + 1)) >= 3 by A21, XXREAL_0:2;
reconsider n2 = max ((max (N,3)),([/c\] + 1)) as Element of NAT by A21, A24, INT_1:16;
set n1 = (n2 !) - 1;
A27: n2 > 2 by A26, XXREAL_0:2;
then A28: n2 ! >= 2 by Lm51, NEWTON:20;
then A29: (n2 !) - 1 >= 1 by A16, XREAL_1:11;
set n3 = n2 - 1;
1 + 1 <= n2 by A26, XXREAL_0:2;
then A30: 1 <= n2 - 1 by XREAL_1:21;
A31: n2 - 1 >= 1 by A16, A27, XREAL_1:11;
reconsider n1 = (n2 !) - 1 as Element of NAT by A29, INT_1:16;
A32: t . n1 = f . (2 * n1) by A18, ASYMPT_0:def 18;
n2 ! > n2 by A26, Lm53;
then n2 ! >= n2 + 1 by INT_1:20;
then n1 >= n2 by XREAL_1:21;
then n1 >= N by A22, XXREAL_0:2;
then A33: t . n1 <= c * (f . n1) by A20;
n2 < n2 + 1 by NAT_1:13;
then n2 * (n2 !) < (n2 + 1) * (n2 !) by A28, XREAL_1:70;
then A34: n2 * (n2 !) < (n2 + 1) ! by NEWTON:21;
(n2 !) + 2 <= (n2 !) + (n2 !) by A28, XREAL_1:8;
then A35: n2 ! <= (2 * (n2 !)) - (2 * 1) by XREAL_1:21;
A36: (n2 !) - 1 < (n2 !) - 0 by XREAL_1:17;
then A37: 2 * n1 < 2 * (n2 !) by XREAL_1:70;
reconsider n3 = n2 - 1 as Element of NAT by A31, INT_1:16;
n3 ! >= 1 by A31, Lm51, NEWTON:19;
then 1 * 1 <= (n2 - 1) * (n3 !) by A30, Lm20;
then n2 * 1 <= ((n2 - 1) * (n3 !)) * n2 by XREAL_1:66;
then n2 <= (n2 - 1) * ((n3 !) * (n3 + 1)) ;
then n2 <= (n2 - 1) * (n2 !) by NEWTON:21;
then A38: (n2 !) + n2 <= ((n2 !) * 1) + ((n2 - 1) * (n2 !)) by XREAL_1:8;
A39: n3 + 1 = n2 + 0 ;
then n2 * (n3 !) = n2 ! by NEWTON:21;
then n2 * (n3 !) <= (n2 * (n2 !)) - n2 by A38, XREAL_1:21;
then n3 ! <= (n2 * ((n2 !) - 1)) / (n2 * 1) by A21, A25, XREAL_1:79;
then A40: n3 ! <= ((n2 !) - 1) / 1 by A21, A25, XCMPLX_1:92;
A41: [/c\] >= c by INT_1:def 5;
[/c\] + 1 > [/c\] + 0 by XREAL_1:10;
then [/c\] + 1 > c by A41, XXREAL_0:2;
then A42: n2 > c by A23, XXREAL_0:2;
A43: n3 ! > 0 by NEWTON:23;
2 * (n2 !) <= n2 * (n2 !) by A27, XREAL_1:66;
then 2 * (n2 !) < (n2 + 1) ! by A34, XXREAL_0:2;
then A44: 2 * n1 < (n2 + 1) ! by A37, XXREAL_0:2;
A45: f . (2 * n1) = Step1 (2 * n1) by A1
.= (n3 + 1) ! by A28, A44, A35, Def9
.= n2 * (n3 !) by NEWTON:21 ;
f . n1 = Step1 n1 by A1
.= n3 ! by A29, A36, A39, A40, Def9 ;
hence contradiction by A33, A32, A45, A42, A43, XREAL_1:70; :: thesis: verum

end;

take f ; :: thesis: ( f = f & f is eventually-nondecreasing & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & not f is smooth )

now

let n be Element of NAT ; :: thesis: f . n <= (seq_n^ 1) . n
thus f . n <= (seq_n^ 1) . n :: thesis: verum

proof

per cases ( n = 0 or n > 0 ) ;

suppose A46: n = 0 ; :: thesis: f . n <= (seq_n^ 1) . n

f . 0 = Step1 0 by A1
.= 0 by Def9 ;
hence f . n <= (seq_n^ 1) . n by A46, Def3; :: thesis: verum

end;

suppose A47: n > 0 ; :: thesis: f . n <= (seq_n^ 1) . n

then A48: (seq_n^ 1) . n = n to_power 1 by Def3
.= n by POWER:30 ;
ex n1 being Element of NAT st
( n1 ! <= n & n < (n1 + 1) ! & Step1 n = n1 ! ) by A47, Def9;
hence f . n <= (seq_n^ 1) . n by A1, A48; :: thesis: verum

end;

end;

end;

end;

hence ( f = f & f is eventually-nondecreasing & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & not f is smooth ) by A15, A17, ASYMPT_0:def 8; :: thesis: verum