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;
then consider N3 being Nat such that
A4: for n being Nat st n >= N3 holds
f . n <= f . (n + 1) ;
f taken_every b in Big_Oh f by A2;
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;
reconsider N = max (N2,N3) as Element of NAT by ORDINAL1:def 12;
A9: N >= N2 by XXREAL_0:25;
A10: N >= N3 by XXREAL_0:25;

now :: thesis: for a being Element of NAT st a >= 2 holds
f is_smooth_wrt a

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 7;
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:57;
then log (b,a) > 0 by A1, A13, POWER:51;
then reconsider i = [/(log (b,a))\] as Element of NAT by A11, INT_1:3;
reconsider i1 = b |^ i as Element of NAT ;

A15: now :: thesis: for n being Element of NAT st n >= N holds
( (f taken_every a) . n <= (c |^ i) * (f . n) & (f taken_every a) . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= N implies ( (f taken_every a) . n <= (c |^ i) * (f . n) & (f taken_every a) . n >= 0 ) )
defpred S₁[ 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:64;
b to_power (log (b,a)) <= b to_power i by A12, A11, PRE_FF:8;
then a <= b |^ i by A1, A13, POWER:def 3;
then A17: a * n <= i1 * n by XREAL_1:64;
assume A18: n >= N ; :: 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 :: thesis: not f . n < 0

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

end;

A22: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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 by ORDINAL1:def 12;
c * (f . m) <= c * ((c |^ k) * (f . n)) by A7, A23, XREAL_1:64;
then c * (f . m) <= (c * (c |^ k)) * (f . n) ;
then c * (f . m) <= ((c to_power 1) * (c to_power k)) * (f . n) ;
then A24: c * (f . m) <= (c to_power (k + 1)) * (f . n) by A7, POWER:27;
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:24
.= 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:35;
then (b |^ k) * n >= 1 * n by XREAL_1:64;
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 Def15;
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:27
.= f . ((b * (b |^ k)) * n)
.= 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:24
.= 1 * (f . n)
.= (c to_power 0) * (f . n) by POWER:24 ;
then A26: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A26, A22);
then f . ((b |^ i) * n) <= (c |^ i) * (f . n) ;
then A27: (f taken_every i1) . n <= (c |^ i) * (f . n) by Def15;
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 Def15;
then (f taken_every a) . n <= (f taken_every i1) . n by Def15;
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, Def15; :: 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:8, POWER:34;
then f taken_every a in Big_Oh f by A15;
hence f is_smooth_wrt a by A3; :: thesis: verum

end;

hence f is smooth ; :: thesis: verum