set g = seq_n^ 3;
set f = seq_n^ 2;
now not seq_n^ 2 in Big_Omega (seq_n^ 3)assume
seq_n^ 2
in Big_Omega (seq_n^ 3)
;
contradictionthen consider s being
Element of
Funcs (
NAT,
REAL)
such that A1:
s = seq_n^ 2
and A2:
ex
d being
Real ex
N being
Element of
NAT st
(
d > 0 & ( for
n being
Element of
NAT st
n >= N holds
(
d * ((seq_n^ 3) . n) <= s . n &
s . n >= 0 ) ) )
;
consider d being
Real,
N being
Element of
NAT such that A3:
d > 0
and A4:
for
n being
Element of
NAT st
n >= N holds
(
d * ((seq_n^ 3) . n) <= s . n &
s . n >= 0 )
by A2;
A5:
N + 2
> 1
+ 0
by XREAL_1:8;
ex
n being
Element of
NAT st
(
n >= N &
d * ((seq_n^ 3) . n) > s . n )
proof
take n =
max (
N,
[/((N + 2) / d)\]);
( n is set & n is Element of NAT & n >= N & d * ((seq_n^ 3) . n) > s . n )
A6:
n >= N
by XXREAL_0:25;
A7:
n is
Integer
by XXREAL_0:16;
A8:
[/((N + 2) / d)\] >= (N + 2) / d
by INT_1:def 7;
(N + 2) * (d ") > 0 * (d ")
by A3, XREAL_1:68;
then A9:
n > 0
by A8, XXREAL_0:25;
reconsider n =
n as
Element of
NAT by A6, A7, INT_1:3;
A10:
((seq_n^ 2) . n) * (n to_power (- 2)) =
(n to_power 2) * (n to_power (- 2))
by A9, Def3
.=
n to_power (2 + (- 2))
by A9, POWER:27
.=
1
by POWER:24
;
A11:
n to_power (- 2) > 0
by A9, POWER:34;
A12:
d * n >= d * [/((N + 2) / d)\]
by A3, XREAL_1:64, XXREAL_0:25;
d * [/((N + 2) / d)\] >= d * ((N + 2) / d)
by A3, A8, XREAL_1:64;
then
d * n >= ((N + 2) / d) * d
by A12, XXREAL_0:2;
then A13:
d * n >= N + 2
by A3, XCMPLX_1:87;
(d * ((seq_n^ 3) . n)) * (n to_power (- 2)) =
(d * (n to_power 3)) * (n to_power (- 2))
by A9, Def3
.=
d * ((n to_power 3) * (n to_power (- 2)))
.=
d * (n to_power (3 + (- 2)))
by A9, POWER:27
.=
d * n
by POWER:25
;
then
(d * ((seq_n^ 3) . n)) * (n to_power (- 2)) > ((seq_n^ 2) . n) * (n to_power (- 2))
by A5, A10, A13, XXREAL_0:2;
hence
(
n is
set &
n is
Element of
NAT &
n >= N &
d * ((seq_n^ 3) . n) > s . n )
by A1, A11, XREAL_1:64, XXREAL_0:25;
verum
end; hence
contradiction
by A4;
verum end;
hence
not seq_n^ 2 in Big_Omega (seq_n^ 3)
; verum