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

assume t in Big_Theta f ; :: thesis: contradiction
then consider s being Element of Funcs NAT ,REAL such that
A3: s = t and
A4: 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
A5: c > 0 and
A6: d > 0 and
A7: for n being Element of NAT st n >= N holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) by A4;
consider N0 being Element of NAT such that
A8: for n being Element of NAT st n >= N0 holds
f . n <= f . (n + 1) by ASYMPT_0:def 8;
set N1 = max ([/(c / d)\] + 1),(max N,N0);
A9: ( max ([/(c / d)\] + 1),(max N,N0) >= [/(c / d)\] + 1 & max ([/(c / d)\] + 1),(max N,N0) >= max N,N0 ) by XXREAL_0:25;
( max N,N0 >= N & max N,N0 >= N0 ) by XXREAL_0:25;
then A10: ( max ([/(c / d)\] + 1),(max N,N0) >= N & max ([/(c / d)\] + 1),(max N,N0) >= N0 ) by A9, XXREAL_0:2;
max ([/(c / d)\] + 1),(max N,N0) is Integer by XXREAL_0:16;
then reconsider N1 = max ([/(c / d)\] + 1),(max N,N0) as Element of NAT by A9, INT_1:16;
thus contradiction :: thesis: verum

proof

per cases ( N1 mod 2 = 1 or N1 mod 2 = 0 ) by NAT_D:12;

suppose A11: N1 mod 2 = 1 ; :: thesis: contradiction

then s . N1 = N1 by A1, A3;
then N1 <= c * (f . N1) by A7, A10;
then A12: N1 / c <= f . N1 by A5, XREAL_1:81;
A13: c " > 0 by A5;
A14: [/(c / d)\] + 1 > [/(c / d)\] + 0 by XREAL_1:10;
[/(c / d)\] >= c / d by INT_1:def 5;
then [/(c / d)\] + 1 > c / d by A14, XXREAL_0:2;
then N1 > c / d by A9, XXREAL_0:2;
then N1 * (c " ) > (c " ) * (c / d) by A13, XREAL_1:70;
then N1 / c > (c " ) * (c / d) ;
then N1 / c > (c " ) * (c * (1 / d)) ;
then N1 / c > ((c " ) * c) * (1 / d) ;
then N1 / c > 1 * (1 / d) by A5, XCMPLX_0:def 7;
then A15: f . N1 > 1 / d by A12, XXREAL_0:2;
f . (N1 + 1) >= f . N1 by A8, A10;
then A16: f . (N1 + 1) > 1 / d by A15, XXREAL_0:2;
(N1 + 1) mod 2 = (1 + (1 mod 2)) mod 2 by A11, EULER_2:8
.= (1 + 1) mod 2 by NAT_D:14
.= 0 by NAT_D:25 ;
then A17: t . (N1 + 1) = 1 by A1;
N1 + 1 > N1 + 0 by XREAL_1:10;
then N1 + 1 > N by A10, XXREAL_0:2;
then A18: d * (f . (N1 + 1)) <= 1 by A3, A7, A17;
d * (1 / d) < d * (f . (N1 + 1)) by A6, A16, XREAL_1:70;
hence contradiction by A6, A18, XCMPLX_1:107; :: thesis: verum

end;

suppose A19: N1 mod 2 = 0 ; :: thesis: contradiction

then (N1 + 1) mod 2 = (0 + (1 mod 2)) mod 2 by EULER_2:8
.= (0 + 1) mod 2 by NAT_D:14
.= 1 by NAT_D:14 ;
then A20: s . (N1 + 1) = N1 + 1 by A1, A3;
A21: N1 + 1 > N1 + 0 by XREAL_1:10;
then N1 + 1 > N by A10, XXREAL_0:2;
then N1 + 1 <= c * (f . (N1 + 1)) by A7, A20;
then A22: (N1 + 1) / c <= f . (N1 + 1) by A5, XREAL_1:81;
A23: c " > 0 by A5;
A24: [/(c / d)\] + 1 > [/(c / d)\] + 0 by XREAL_1:10;
[/(c / d)\] >= c / d by INT_1:def 5;
then [/(c / d)\] + 1 > c / d by A24, XXREAL_0:2;
then N1 > c / d by A9, XXREAL_0:2;
then N1 + 1 > c / d by A21, XXREAL_0:2;
then (N1 + 1) * (c " ) > (c " ) * (c / d) by A23, XREAL_1:70;
then (N1 + 1) / c > (c " ) * (c / d) ;
then (N1 + 1) / c > (c " ) * (c * (1 / d)) ;
then (N1 + 1) / c > ((c " ) * c) * (1 / d) ;
then (N1 + 1) / c > 1 * (1 / d) by A5, XCMPLX_0:def 7;
then A25: f . (N1 + 1) > 1 / d by A22, XXREAL_0:2;
N1 + 1 > N0 by A10, A21, XXREAL_0:2;
then f . ((N1 + 1) + 1) >= f . (N1 + 1) by A8;
then A26: f . (N1 + 2) > 1 / d by A25, XXREAL_0:2;
(N1 + 2) mod 2 = (0 + (2 mod 2)) mod 2 by A19, EULER_2:8
.= (0 + 0 ) mod 2 by NAT_D:25
.= 0 by NAT_D:26 ;
then A27: t . (N1 + 2) = 1 by A1;
N1 + 2 > N1 + 0 by XREAL_1:10;
then N1 + 2 > N by A10, XXREAL_0:2;
then A28: d * (f . (N1 + 2)) <= 1 by A3, A7, A27;
d * (1 / d) < d * (f . (N1 + 2)) by A6, A26, XREAL_1:70;
hence contradiction by A6, A28, XCMPLX_1:107; :: thesis: verum

end;

end;

end;

end;