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 & not s is smooth & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & f is eventually-nondecreasing ) )
assume A1: for n being Element of NAT holds f . n = Step1 n ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = f & not s is smooth & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & f is eventually-nondecreasing )
f is eventually-positive
proof
take 1 ; :: according to ASYMPT_0:def 4 :: thesis: for b1 being set holds
( not 1 <= b1 or not f . b1 <= 0 )
let n be Nat; :: thesis: ( not 1 <= n or not f . n <= 0 )
A2: n in NAT by ORDINAL1:def 12;
assume n >= 1 ; :: thesis: not f . n <= 0
then A3: ex m being Element of NAT st
( m ! <= n & n < (m + 1) ! & Step1 n = m ! ) by Def6;
f . n = Step1 n by A1, A2;
hence not f . n <= 0 by A3, NEWTON:17; :: thesis: verum
end;
then reconsider s = f as eventually-positive Real_Sequence ;
take s ; :: thesis: ( s = f & not s is smooth & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & f is eventually-nondecreasing )
thus s = f ; :: thesis: ( not s is smooth & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & f is eventually-nondecreasing )
now :: thesis: for k being Element of NAT holds f . k <= f . (k + 1)
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 A4: k = 0 ; :: thesis: f . k <= f . (k + 1)
A5: f . (0 + 1) = Step1 1 by A1;
f . 0 = Step1 0 by A1
.= 0 by Def6 ;
hence f . k <= f . (k + 1) by A4, A5; :: thesis: verum
end;
suppose k > 0 ; :: thesis: f . k <= f . (k + 1)
then consider n1 being Element of NAT such that
A6: n1 ! <= k and
A7: k < (n1 + 1) ! and
A8: Step1 k = n1 ! by Def6;
A9: k + 1 <= (n1 + 1) ! by A7, INT_1:7;
A10: k <= k + 1 by NAT_1:11;
A11: f . k = n1 ! by A1, A8;
per cases ( k + 1 < (n1 + 1) ! or k + 1 = (n1 + 1) ! ) by A9, XXREAL_0:1;
suppose A12: k + 1 < (n1 + 1) ! ; :: thesis: f . k <= f . (k + 1)
n1 ! <= k + 1 by A10, A6, XXREAL_0:2;
then Step1 (k + 1) = n1 ! by A12, Def6;
hence f . k <= f . (k + 1) by A1, A11; :: thesis: verum
end;
suppose A13: k + 1 = (n1 + 1) ! ; :: thesis: f . k <= f . (k + 1)
A14: (n1 + 1) ! > 0 by NEWTON:17;
n1 + 2 > 0 + 1 by XREAL_1:8;
then 1 * ((n1 + 1) !) < (n1 + 2) * ((n1 + 1) !) by A14, XREAL_1:68;
then A15: k + 1 < ((n1 + 1) + 1) ! by A13, NEWTON:15;
f . (k + 1) = Step1 (k + 1) by A1
.= (n1 + 1) ! by A13, A15, Def6 ;
hence f . k <= f . (k + 1) by A11, Lm51, NAT_1:11; :: thesis: verum
end;
end;
end;
end;
end;
end;
then A16: for k being Element of NAT st k >= 0 holds
f . k <= f . (k + 1) ;
A17: 1 = 2 - 1 ;
hereby :: thesis: ( ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & f is eventually-nondecreasing )
set h = f taken_every 2;
assume s is smooth ; :: thesis: contradiction
then s is_smooth_wrt 2 ;
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:3;
set n1 = (n2 !) - 1;
A27: n2 > 2 by A26, XXREAL_0:2;
then A28: n2 ! >= 2 by Lm51, NEWTON:14;
then A29: (n2 !) - 1 >= 1 by A17, XREAL_1:9;
set n3 = n2 - 1;
1 + 1 <= n2 by A26, XXREAL_0:2;
then A30: 1 <= n2 - 1 by XREAL_1:19;
A31: n2 - 1 >= 1 by A17, A27, XREAL_1:9;
reconsider n1 = (n2 !) - 1 as Element of NAT by A29, INT_1:3;
A32: t . n1 = f . (2 * n1) by A18, ASYMPT_0:def 15;
n2 ! > n2 by A26, Lm53;
then n2 ! >= n2 + 1 by INT_1:7;
then n1 >= n2 by XREAL_1:19;
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:68;
then A34: n2 * (n2 !) < (n2 + 1) ! by NEWTON:15;
(n2 !) + 2 <= (n2 !) + (n2 !) by A28, XREAL_1:6;
then A35: n2 ! <= (2 * (n2 !)) - (2 * 1) by XREAL_1:19;
A36: (n2 !) - 1 < (n2 !) - 0 by XREAL_1:15;
then A37: 2 * n1 < 2 * (n2 !) by XREAL_1:68;
reconsider n3 = n2 - 1 as Element of NAT by A31, INT_1:3;
n3 ! >= 1 by A31, Lm51, NEWTON:13;
then 1 * 1 <= (n2 - 1) * (n3 !) by A30, Lm20;
then n2 * 1 <= ((n2 - 1) * (n3 !)) * n2 by XREAL_1:64;
then n2 <= (n2 - 1) * ((n3 !) * (n3 + 1)) ;
then n2 <= (n2 - 1) * (n2 !) by NEWTON:15;
then A38: (n2 !) + n2 <= ((n2 !) * 1) + ((n2 - 1) * (n2 !)) by XREAL_1:6;
A39: n3 + 1 = n2 + 0 ;
then n2 * (n3 !) = n2 ! by NEWTON:15;
then n2 * (n3 !) <= (n2 * (n2 !)) - n2 by A38, XREAL_1:19;
then n3 ! <= (n2 * ((n2 !) - 1)) / (n2 * 1) by A21, A25, XREAL_1:77;
then A40: n3 ! <= ((n2 !) - 1) / 1 by A21, A25, XCMPLX_1:91;
A41: [/c\] >= c by INT_1:def 7;
[/c\] + 1 > [/c\] + 0 by XREAL_1:8;
then [/c\] + 1 > c by A41, XXREAL_0:2;
then A42: n2 > c by A23, XXREAL_0:2;
A43: n3 ! > 0 by NEWTON:17;
2 * (n2 !) <= n2 * (n2 !) by A27, XREAL_1:64;
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, Def6
.= n2 * (n3 !) by NEWTON:15 ;
f . n1 = Step1 n1 by A1
.= n3 ! by A29, A36, A39, A40, Def6 ;
hence contradiction by A33, A32, A45, A42, A43, XREAL_1:68; :: thesis: verum
end;
hereby :: thesis: f is eventually-nondecreasing
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 Def6 ;
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:25 ;
ex n1 being Element of NAT st
( n1 ! <= n & n < (n1 + 1) ! & Step1 n = n1 ! ) by A47, Def6;
hence f . n <= (seq_n^ 1) . n by A1, A48; :: thesis: verum
end;
end;
end;
end;
reconsider zz = 0 as Nat ;
take zz ; :: according to ASYMPT_0:def 6 :: thesis: for b1 being set holds
( not zz <= b1 or f . b1 <= f . (b1 + 1) )
let n be Nat; :: thesis: ( not zz <= n or f . n <= f . (n + 1) )
n in NAT by ORDINAL1:def 12;
hence ( not zz <= n or f . n <= f . (n + 1) ) by A16; :: thesis: verum