let f be eventually-nonnegative eventually-nondecreasing Real_Sequence; :: thesis: for t being Real_Sequence st ( for n being Element of NAT holds
( ( n mod 2 = 0 implies t . n = 1 ) & ( n mod 2 = 1 implies t . n = n ) ) ) holds
not t in Big_Theta f
let t be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds
( ( n mod 2 = 0 implies t . n = 1 ) & ( n mod 2 = 1 implies t . n = n ) ) ) implies not t in Big_Theta f )
assume A1: for n being Element of NAT holds
( ( n mod 2 = 0 implies t . n = 1 ) & ( n mod 2 = 1 implies t . n = n ) ) ; :: thesis: not t in Big_Theta f
A2: Big_Theta f = { s where s is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) ) ) } by ASYMPT_0:27;
hereby :: thesis: verum
consider N0 being Nat such that
A3: for n being Nat st n >= N0 holds
f . n <= f . (n + 1) by ASYMPT_0:def 6;
assume t in Big_Theta f ; :: thesis: contradiction
then consider s being Element of Funcs (NAT,REAL) such that
A4: s = t and
A5: ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) ) ) by A2;
consider c, d being Real, N being Element of NAT such that
A6: c > 0 and
A7: d > 0 and
A8: for n being Element of NAT st n >= N holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) by A5;
set N1 = max (([/(c / d)\] + 1),(max (N,N0)));
A9: max (([/(c / d)\] + 1),(max (N,N0))) >= [/(c / d)\] + 1 by XXREAL_0:25;
A10: max (([/(c / d)\] + 1),(max (N,N0))) is Integer by XXREAL_0:16;
A11: max (([/(c / d)\] + 1),(max (N,N0))) >= max (N,N0) by XXREAL_0:25;
max (N,N0) >= N0 by XXREAL_0:25;
then A12: max (([/(c / d)\] + 1),(max (N,N0))) >= N0 by A11, XXREAL_0:2;
max (N,N0) >= N by XXREAL_0:25;
then A13: max (([/(c / d)\] + 1),(max (N,N0))) >= N by A11, XXREAL_0:2;
reconsider N1 = max (([/(c / d)\] + 1),(max (N,N0))) as Element of NAT by A11, A10, INT_1:3;
thus contradiction :: thesis: verum
proof
per cases ( N1 mod 2 = 1 or N1 mod 2 = 0 ) by NAT_D:12;
suppose A14: N1 mod 2 = 1 ; :: thesis: contradiction
A15: [/(c / d)\] >= c / d by INT_1:def 7;
[/(c / d)\] + 1 > [/(c / d)\] + 0 by XREAL_1:8;
then [/(c / d)\] + 1 > c / d by A15, XXREAL_0:2;
then N1 > c / d by A9, XXREAL_0:2;
then N1 * (c ") > (c ") * (c / d) by A6, XREAL_1:68;
then N1 / c > ((c ") * c) * (1 / d) ;
then A16: N1 / c > 1 * (1 / d) by A6, XCMPLX_0:def 7;
A17: f . (N1 + 1) >= f . N1 by A3, A12;
s . N1 = N1 by A1, A4, A14;
then N1 <= c * (f . N1) by A8, A13;
then N1 / c <= f . N1 by A6, XREAL_1:79;
then f . N1 > 1 / d by A16, XXREAL_0:2;
then f . (N1 + 1) > 1 / d by A17, XXREAL_0:2;
then A18: d * (1 / d) < d * (f . (N1 + 1)) by A7, XREAL_1:68;
N1 + 1 > N1 + 0 by XREAL_1:8;
then A19: N1 + 1 > N by A13, XXREAL_0:2;
(N1 + 1) mod 2 = (1 + (1 mod 2)) mod 2 by A14, EULER_2:6
.= (1 + 1) mod 2 by NAT_D:14
.= 0 by NAT_D:25 ;
then t . (N1 + 1) = 1 by A1;
then d * (f . (N1 + 1)) <= 1 by A4, A8, A19;
hence contradiction by A7, A18, XCMPLX_1:106; :: thesis: verum
end;
suppose A20: N1 mod 2 = 0 ; :: thesis: contradiction
then (N1 + 1) mod 2 = (0 + (1 mod 2)) mod 2 by EULER_2:6
.= (0 + 1) mod 2 by NAT_D:14
.= 1 by NAT_D:14 ;
then A21: s . (N1 + 1) = N1 + 1 by A1, A4;
A22: [/(c / d)\] >= c / d by INT_1:def 7;
A23: N1 + 1 > N1 + 0 by XREAL_1:8;
then N1 + 1 > N0 by A12, XXREAL_0:2;
then A24: f . ((N1 + 1) + 1) >= f . (N1 + 1) by A3;
[/(c / d)\] + 1 > [/(c / d)\] + 0 by XREAL_1:8;
then [/(c / d)\] + 1 > c / d by A22, XXREAL_0:2;
then N1 > c / d by A9, XXREAL_0:2;
then N1 + 1 > c / d by A23, XXREAL_0:2;
then (N1 + 1) * (c ") > (c ") * (c / d) by A6, XREAL_1:68;
then (N1 + 1) / c > ((c ") * c) * (1 / d) ;
then A25: (N1 + 1) / c > 1 * (1 / d) by A6, XCMPLX_0:def 7;
N1 + 1 > N by A13, A23, XXREAL_0:2;
then N1 + 1 <= c * (f . (N1 + 1)) by A8, A21;
then (N1 + 1) / c <= f . (N1 + 1) by A6, XREAL_1:79;
then f . (N1 + 1) > 1 / d by A25, XXREAL_0:2;
then f . (N1 + 2) > 1 / d by A24, XXREAL_0:2;
then A26: d * (1 / d) < d * (f . (N1 + 2)) by A7, XREAL_1:68;
N1 + 2 > N1 + 0 by XREAL_1:8;
then A27: N1 + 2 > N by A13, XXREAL_0:2;
(N1 + 2) mod 2 = (0 + (2 mod 2)) mod 2 by A20, EULER_2:6
.= (0 + 0) mod 2 by NAT_D:25
.= 0 by NAT_D:26 ;
then t . (N1 + 2) = 1 by A1;
then d * (f . (N1 + 2)) <= 1 by A4, A8, A27;
hence contradiction by A7, A26, XCMPLX_1:106; :: thesis: verum
end;
end;
end;
end;