set g = seq_n^ 1;
let f be Real_Sequence; ( ( 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
; 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
then reconsider s = f as eventually-positive Real_Sequence ;
take
s
; ( 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
; ( not s is smooth & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & f is eventually-nondecreasing )
then A16:
for k being Element of NAT st k >= 0 holds
f . k <= f . (k + 1)
;
A17:
1 = 2 - 1
;
hereby ( ( 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
;
contradictionthen
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;
verum
end;
reconsider zz = 0 as Nat ;
take
zz
; ASYMPT_0:def 6 for b1 being set holds
( not zz <= b1 or f . b1 <= f . (b1 + 1) )
let n be Nat; ( 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; verum