let f be eventually-nonnegative Real_Sequence; :: thesis: ( ex b being Element of NAT st
( b >= 2 & f is_smooth_wrt b ) implies f is smooth )
given b being Element of NAT such that A1: b >= 2 and
A2: f is_smooth_wrt b ; :: thesis: f is smooth
A3: f is eventually-nondecreasing by A2, Def19;
then consider N3 being Element of NAT such that
A4: for n being Element of NAT st n >= N3 holds
f . n <= f . (n + 1) by Def8;
f taken_every b in Big_Oh f by A2, Def19;
then consider t being Element of Funcs NAT ,REAL such that
A5: f taken_every b = t 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, N2 being Element of NAT such that
A7: c > 0 and
A8: for n being Element of NAT st n >= N2 holds
( t . n <= c * (f . n) & t . n >= 0 ) by A6;
set N = max N2,N3;
A9: max N2,N3 >= N2 by XXREAL_0:25;
A10: max N2,N3 >= N3 by XXREAL_0:25;

now

let a be Element of NAT ; :: thesis: ( a >= 2 implies f is_smooth_wrt a )
set i = [/(log b,a)\];
A11: [/(log b,a)\] >= log b,a by INT_1:def 5;
A12: b > 1 by A1, XXREAL_0:2;
A13: b <> 1 by A1;
assume A14: a >= 2 ; :: thesis: f is_smooth_wrt a
then a > 1 by XXREAL_0:2;
then log b,a > log b,1 by A12, POWER:65;
then log b,a > 0 by A1, A13, POWER:59;
then reconsider i = [/(log b,a)\] as Element of NAT by A11, INT_1:16;
reconsider i1 = b |^ i as Element of NAT ;

A15: now

let n be Element of NAT ; :: thesis: ( n >= max N2,N3 implies ( (f taken_every a) . n <= (c |^ i) * (f . n) & (f taken_every a) . n >= 0 ) )
defpred S₁[ Element of NAT ] means f . ((b |^ $1) * n) <= (c |^ $1) * (f . n);
a >= 1 by A14, XXREAL_0:2;
then A16: a * n >= 1 * n by XREAL_1:66;
b to_power (log b,a) <= b to_power i by A12, A11, PRE_FF:10;
then a <= b |^ i by A1, A13, POWER:def 3;
then A17: a * n <= i1 * n by XREAL_1:66;
assume A18: n >= max N2,N3 ; :: thesis: ( (f taken_every a) . n <= (c |^ i) * (f . n) & (f taken_every a) . n >= 0 )
then A19: n >= N2 by A9, XXREAL_0:2;
then A20: t . n <= c * (f . n) by A8;

A21: now

assume f . n < 0 ; :: thesis: contradiction
then c * (f . n) < c * 0 by A7, XREAL_1:70;
hence contradiction by A8, A19, A20; :: thesis: verum

end;

A22: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
set m = (b |^ k) * n;
assume A23: f . ((b |^ k) * n) <= (c |^ k) * (f . n) ; :: thesis: S₁[k + 1]
reconsider m = (b |^ k) * n as Element of NAT ;
c * (f . m) <= c * ((c |^ k) * (f . n)) by A7, A23, XREAL_1:66;
then c * (f . m) <= (c * (c |^ k)) * (f . n) ;
then c * (f . m) <= ((c to_power 1) * (c to_power k)) * (f . n) by POWER:30;
then A24: c * (f . m) <= (c to_power (k + 1)) * (f . n) by A7, POWER:32;
m >= N2

proof

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

suppose k = 0 ; :: thesis: m >= N2

then (b |^ k) * n = (b to_power 0 ) * n
.= 1 * n by POWER:29
.= n ;
hence m >= N2 by A9, A18, XXREAL_0:2; :: thesis: verum

end;

suppose k > 0 ; :: thesis: m >= N2

then b to_power k > 1 by A12, POWER:40;
then (b |^ k) * n >= 1 * n by XREAL_1:66;
hence m >= N2 by A19, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then (f taken_every b) . m <= c * (f . m) by A5, A8;
then A25: f . (b * m) <= c * (f . m) by Def18;
f . ((b |^ (k + 1)) * n) = f . ((b to_power (k + 1)) * n)
.= f . (((b to_power 1) * (b to_power k)) * n) by A1, POWER:32
.= f . ((b * (b |^ k)) * n) by POWER:30
.= f . (b * ((b |^ k) * n)) ;
hence S₁[k + 1] by A25, A24, XXREAL_0:2; :: thesis: verum

end;

f . ((b |^ 0 ) * n) = f . ((b to_power 0 ) * n)
.= f . (1 * n) by POWER:29
.= 1 * (f . n)
.= (c to_power 0 ) * (f . n) by POWER:29 ;
then A26: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A26, A22);
then f . ((b |^ i) * n) <= (c |^ i) * (f . n) ;
then A27: (f taken_every i1) . n <= (c |^ i) * (f . n) by Def18;
A28: n >= N3 by A10, A18, XXREAL_0:2;
then a * n >= N3 by A16, XXREAL_0:2;
then f . (a * n) <= f . (i1 * n) by A4, A17, Th1;
then (f taken_every a) . n <= f . (i1 * n) by Def18;
then (f taken_every a) . n <= (f taken_every i1) . n by Def18;
hence (f taken_every a) . n <= (c |^ i) * (f . n) by A27, XXREAL_0:2; :: thesis: (f taken_every a) . n >= 0
f . n <= f . (a * n) by A4, A28, A16, Th1;
hence (f taken_every a) . n >= 0 by A21, Def18; :: thesis: verum

end;

c |^ i = c to_power i ;
then ( f taken_every a is Element of Funcs NAT ,REAL & c |^ i > 0 ) by A7, FUNCT_2:11, POWER:39;
then f taken_every a in Big_Oh f by A15;
hence f is_smooth_wrt a by A3, Def19; :: thesis: verum

end;

hence f is smooth by Def20; :: thesis: verum