:: ASYMPT_1 semantic presentation
E1:
for b1 being Nat holds
not ( b1 >= 2 & not 2 to_power b1 > b1 + 1 )
theorem :: ASYMPT_1:1
proof
let c
1, c
2 be
Real_Sequence;
assume that E2:
( c
1 . 0
= 0 & ( for b
1 being
Nat holds
( b
1 > 0 implies c
1 . b
1 = ((((12 * (b1 to_power 3)) * (log 2,b1)) - (5 * (b1 ^2 ))) + ((log 2,b1) ^2 )) + 36 ) ) )
and E3:
( c
2 . 0
= 0 & ( for b
1 being
Nat holds
( b
1 > 0 implies c
2 . b
1 = (b1 to_power 3) * (log 2,b1) ) ) )
;
c
1 is
eventually-positive
proof
take
3
;
:: according to ASYMPT_0:def 6
let c
3 be
Nat;
assume E4:
c
3 >= 3
;
then
c
3 > 1
by XREAL_1:2;
then E5:
c
3 to_power 3
> c
3 to_power 2
by POWER:44;
E6:
c
3 to_power 2
> 0
by E4, POWER:39;
E7:
log 2,c
3 >= log 2,3
by E4, PRE_FF:12;
log 2,3
> log 2,2
by POWER:65;
then
log 2,3
> 1
by POWER:60;
then
log 2,c
3 > 1
by E7, XREAL_1:2;
then
(c3 to_power 3) * (log 2,c3) > (c3 to_power 2) * 1
by E5, E6, REAL_2:199;
then
12
* ((c3 to_power 3) * (log 2,c3)) > 5
* (c3 to_power 2)
by E6, REAL_2:199;
then
(12 * (c3 to_power 3)) * (log 2,c3) > (5 * (c3 ^2 )) + 0
by POWER:53;
then E8:
((12 * (c3 to_power 3)) * (log 2,c3)) - (5 * (c3 ^2 )) > 0
by XREAL_1:22;
(log 2,c3) ^2 >= 0
by SQUARE_1:72;
then
(((12 * (c3 to_power 3)) * (log 2,c3)) - (5 * (c3 ^2 ))) + ((log 2,c3) ^2 ) > 0
+ 0
by E8, XREAL_1:10;
then
((((12 * (c3 to_power 3)) * (log 2,c3)) - (5 * (c3 ^2 ))) + ((log 2,c3) ^2 )) + 36
> 0
+ 0
by XREAL_1:10;
hence
c
1 . c
3 > 0
by E2, E4;
end;
then reconsider c
3 = c
1 as
eventually-positive Real_Sequence ;
c
2 is
eventually-positive
then reconsider c
4 = c
2 as
eventually-positive Real_Sequence ;
take
c
3
;
take
c
4
;
ex b
1 being
Real_Sequence st
( b
1 . 0
= 0 & ( for b
2 being
Nat holds
( b
2 > 0 implies b
1 . b
2 = ((12 * (b2 to_power 3)) * (log 2,b2)) - (5 * (b2 ^2 )) ) ) )
then consider c
5 being
Real_Sequence such that E4:
( c
5 . 0
= 0 & ( for b
1 being
Nat holds
( b
1 > 0 implies c
5 . b
1 = ((12 * (b1 to_power 3)) * (log 2,b1)) - (5 * (b1 ^2 )) ) ) )
;
c
5 is
eventually-positive
proof
take
3
;
:: according to ASYMPT_0:def 6
let c
6 be
Nat;
assume E5:
c
6 >= 3
;
then
c
6 > 1
by XREAL_1:2;
then E6:
c
6 to_power 3
> c
6 to_power 2
by POWER:44;
E7:
c
6 to_power 2
> 0
by E5, POWER:39;
E8:
log 2,c
6 >= log 2,3
by E5, PRE_FF:12;
log 2,3
> log 2,2
by POWER:65;
then
log 2,3
> 1
by POWER:60;
then
log 2,c
6 > 1
by E8, XREAL_1:2;
then
(c6 to_power 3) * (log 2,c6) > (c6 to_power 2) * 1
by E6, E7, REAL_2:199;
then
12
* ((c6 to_power 3) * (log 2,c6)) > 5
* (c6 to_power 2)
by E7, REAL_2:199;
then
(12 * (c6 to_power 3)) * (log 2,c6) > (5 * (c6 ^2 )) + 0
by POWER:53;
then
((12 * (c6 to_power 3)) * (log 2,c6)) - (5 * (c6 ^2 )) > 0
by XREAL_1:22;
hence
c
5 . c
6 > 0
by E4, E5;
end;
then reconsider c
6 = c
5 as
eventually-positive Real_Sequence ;
ex b
1 being
Real_Sequence st
( b
1 . 0
= 0 & ( for b
2 being
Nat holds
( b
2 > 0 implies b
1 . b
2 = ((log 2,b2) ^2 ) + 36 ) ) )
then consider c
7 being
Real_Sequence such that E5:
( c
7 . 0
= 0 & ( for b
1 being
Nat holds
( b
1 > 0 implies c
7 . b
1 = ((log 2,b1) ^2 ) + 36 ) ) )
;
c
7 is
eventually-positive
then reconsider c
8 = c
7 as
eventually-positive Real_Sequence ;
set c
9 =
max c
6,c
8;
for b
1 being
Nat holds c
3 . b
1 = (c6 . b1) + (c8 . b1)
proof
let c
10 be
Nat;
thus
c
3 . c
10 = (c6 . c10) + (c8 . c10)
proof
per cases
not ( not c
10 = 0 & not c
10 > 0 )
;
suppose
c
10 = 0
;
hence
c
3 . c
10 = (c6 . c10) + (c8 . c10)
by E2, E4, E5;
end;
suppose E6:
c
10 > 0
;
end;
end;
end;
end;
then E6:
Big_Oh c
3 =
Big_Oh (c6 + c8)
by SEQ_1:11
.=
Big_Oh (max c6,c8)
by ASYMPT_0:9
;
4 =
2
^2
.=
2
to_power 2
by POWER:53
;
then E7:
log 2,4 =
2
* (log 2,2)
by POWER:63
.=
2
* 1
by POWER:60
.=
2
;
E8:
for b
1 being
Nat holds
not ( b
1 >= 4 & not 7
* (b1 ^2 ) > c
8 . b
1 )
proof
defpred S
1[
Nat] means 7
* (a1 ^2 ) > c
8 . a
1;
E9:
S
1[4]
proof
c
8 . 4 =
(2 ^2 ) + 36
by E5, E7
.=
40
;
hence
S
1[4]
;
E10:
for b
1 being
Nat holds
( ( b
1 >= 4 & S
1[b
1] ) implies ( S
1[b
1 + 1] ) )
proof
let c
10 be
Nat;
assume that E11:
c
10 >= 4
and E12:
7
* (c10 ^2 ) > c
8 . c
10
;
E13:
c
8 . c
10 = ((log 2,c10) ^2 ) + 36
by E5, E11;
7
* ((c10 + 1) ^2 ) = (7 * (c10 ^2 )) + ((7 * (2 * c10)) + (7 * 1))
;
then E14:
7
* ((c10 + 1) ^2 ) > (c8 . c10) + ((7 * (2 * c10)) + (7 * 1))
by E12, XREAL_1:8;
E15:
c
8 . (c10 + 1) = ((log 2,(c10 + 1)) ^2 ) + 36
by E5;
c
10 >= 1
by E11, XREAL_1:2;
then
c
10 + c
10 >= c
10 + 1
by XREAL_1:8;
then E16:
log 2,
(c10 + c10) >= log 2,
(c10 + 1)
by PRE_FF:12;
c
10 + 1
>= 4
+ 0
by E11, XREAL_1:10;
then
log 2,
(c10 + 1) >= 2
by E7, PRE_FF:12;
then
(log 2,(c10 + c10)) ^2 >= (log 2,(c10 + 1)) ^2
by E16, SQUARE_1:77;
then E17:
c
8 . (c10 + 1) <= ((log 2,(c10 + c10)) ^2 ) + 36
by E15, XREAL_1:8;
log 2,
(c10 + c10) = log 2,
(2 * c10)
;
then
log 2,
(c10 + c10) = (log 2,c10) + (log 2,2)
by E11, POWER:61;
then E18:
(log 2,(c10 + c10)) ^2 =
((log 2,c10) + 1) ^2
by POWER:60
.=
(((log 2,c10) ^2 ) + (2 * (log 2,c10))) + 1
;
c
10 >= 2
by E11, XREAL_1:2;
then E19:
2
to_power c
10 > c
10 + 1
by E1;
E20:
log 2,c
10 >= 2
by E7, E11, PRE_FF:12;
c
10 + 1
> c
10 + 0
by XREAL_1:10;
then
2
to_power c
10 > c
10
by E19, XREAL_1:2;
then
log 2,
(2 to_power c10) > log 2,c
10
by E11, POWER:65;
then
c
10 * (log 2,2) > log 2,c
10
by POWER:63;
then
c
10 * 1
> log 2,c
10
by POWER:60;
then
14
* c
10 > 2
* (log 2,c10)
by E20, REAL_2:199;
then
((7 * 2) * c10) + 7
> (2 * (log 2,c10)) + 1
by XREAL_1:10;
then
((log 2,c10) ^2 ) + ((2 * (log 2,c10)) + 1) < ((log 2,c10) ^2 ) + ((7 * (2 * c10)) + 7)
by XREAL_1:8;
then
((log 2,(c10 + c10)) ^2 ) + 36
< (((log 2,c10) ^2 ) + ((7 * (2 * c10)) + 7)) + 36
by E18, XREAL_1:8;
then
(c8 . c10) + ((7 * (2 * c10)) + (7 * 1)) > c
8 . (c10 + 1)
by E13, E17, XREAL_1:2;
hence
S
1[c
10 + 1]
by E14, XREAL_1:2;
end;
for b
1 being
Nat holds
( b
1 >= 4 implies S
1[b
1] )
from INT_2:sch 1(E9, E10);
hence
for b
1 being
Nat holds
not ( b
1 >= 4 & not 7
* (b1 ^2 ) > c
8 . b
1 )
;
end;
E9:
for b
1 being
Nat holds
not ( b
1 >= 4 & not c
6 . b
1 > 7
* (b1 ^2 ) )
proof
let c
10 be
Nat;
assume E10:
c
10 >= 4
;
then E11:
c
6 . c
10 = ((12 * (c10 to_power 3)) * (log 2,c10)) - (5 * (c10 ^2 ))
by E4;
c
10 > 1
by E10, XREAL_1:2;
then E12:
c
10 to_power 3
> c
10 to_power 2
by POWER:44;
E13:
c
10 to_power 2
> 0
by E10, POWER:39;
log 2,c
10 >= log 2,4
by E10, PRE_FF:12;
then
log 2,c
10 > 1
by E7, XREAL_1:2;
then
(c10 to_power 3) * (log 2,c10) > (c10 to_power 2) * 1
by E12, E13, REAL_2:199;
then
12
* ((c10 to_power 3) * (log 2,c10)) > 12
* (c10 to_power 2)
by XREAL_1:70;
then
(12 * (c10 to_power 3)) * (log 2,c10) > 12
* (c10 ^2 )
by POWER:53;
then
c
6 . c
10 > (12 * (c10 ^2 )) - (5 * (c10 ^2 ))
by E11, XREAL_1:11;
hence
c
6 . c
10 > 7
* (c10 ^2 )
;
end;
E10:
for b
1 being
Nat holds
not ( b
1 >= 4 & not c
6 . b
1 > c
8 . b
1 )
proof
let c
10 be
Nat;
assume E11:
c
10 >= 4
;
then E12:
c
6 . c
10 > 7
* (c10 ^2 )
by E9;
7
* (c10 ^2 ) > c
8 . c
10
by E8, E11;
hence
c
6 . c
10 > c
8 . c
10
by E12, XREAL_1:2;
end;
E11:
for b
1 being
Nat holds
( b
1 >= 4 implies
(max c6,c8) . b
1 = c
6 . b
1 )
E12:
max c
6,c
8 is
Element of
Funcs NAT ,
REAL
by FUNCT_2:11;
consider c
10 being
Nat such that E13:
for b
1 being
Nat holds
not ( b
1 >= c
10 & not
(max c6,c8) . b
1 > 0 )
by ASYMPT_0:def 6;
now
let c
11 be
Nat;
assume E14:
c
11 >= max 4,c
10
;
E15:
(
max 4,c
10 >= 4 &
max 4,c
10 >= c
10 )
by SQUARE_1:46;
then E16:
( c
11 >= 4 & c
11 >= c
10 )
by E14, XREAL_1:2;
then E17:
(max c6,c8) . c
11 =
c
6 . c
11
by E11
.=
((12 * (c11 to_power 3)) * (log 2,c11)) - (5 * (c11 ^2 ))
by E4, E14, E15
;
c
11 to_power 2
> 0
by E14, E15, POWER:39;
then
c
11 ^2 > 0
by POWER:53;
then
5
* (c11 ^2 ) > 5
* 0
by XREAL_1:70;
then
(max c6,c8) . c
11 <= ((12 * (c11 to_power 3)) * (log 2,c11)) - 0
by E17, REAL_1:92;
then
(max c6,c8) . c
11 <= 12
* ((c11 to_power 3) * (log 2,c11))
;
hence
(max c6,c8) . c
11 <= 12
* (c4 . c11)
by E3, E14, E15;
thus
(max c6,c8) . c
11 >= 0
by E13, E16;
end;
then E14:
max c
6,c
8 in Big_Oh c
4
by E12;
c
3 in Big_Oh c
3
by ASYMPT_0:10;
hence
( c
3 = c
1 & c
4 = c
2 & c
3 in Big_Oh c
4 )
by E6, E14, ASYMPT_0:12;
end;
E2:
for b1 being logbase Real
for b2 being Real_Sequence holds
( ( b2 . 0 = 0 & ( for b3 being Nat holds
( b3 > 0 implies b2 . b3 = log b1,b3 ) ) ) implies ( not b1 > 1 or b2 is eventually-positive ) )
proof
let c
1 be
logbase Real;
let c
2 be
Real_Sequence;
assume that E3:
c
1 > 1
and E4:
( c
2 . 0
= 0 & ( for b
1 being
Nat holds
( b
1 > 0 implies c
2 . b
1 = log c
1,b
1 ) ) )
;
E5:
( c
1 > 0 & c
1 <> 1 )
by ASYMPT_0:def 3;
set c
3 =
[/c1\];
E6:
[/c1\] >= c
1
by INT_1:def 5;
E7:
[/c1\] > 0
by E5, INT_1:def 5;
then reconsider c
4 =
[/c1\] as
Nat by INT_1:16;
now
let c
5 be
Nat;
assume E8:
c
5 >= c
4 + 1
;
c
4 + 1
> c
4 + 0
by XREAL_1:10;
then
c
5 > c
4
by E8, XREAL_1:2;
then E9:
log c
1,c
5 > log c
1,c
4
by E3, E7, POWER:65;
log c
1,c
4 >= log c
1,c
1
by E3, E6, PRE_FF:12;
then
log c
1,c
5 > 0
by E5, POWER:60, E9;
hence
c
2 . c
5 > 0
by E4, E8;
end;
hence
c
2 is
eventually-positive
by ASYMPT_0:def 6;
end;
theorem :: ASYMPT_1:2
proof
let c
1, c
2 be
logbase Real;
let c
3, c
4 be
Real_Sequence;
assume that E3:
c
1 > 1
and E4:
c
2 > 1
and E5:
( c
3 . 0
= 0 & ( for b
1 being
Nat holds
( b
1 > 0 implies c
3 . b
1 = log c
1,b
1 ) ) )
and E6:
( c
4 . 0
= 0 & ( for b
1 being
Nat holds
( b
1 > 0 implies c
4 . b
1 = log c
2,b
1 ) ) )
;
reconsider c
5 = c
3 as
eventually-positive Real_Sequence by E3, E5, E2;
reconsider c
6 = c
4 as
eventually-positive Real_Sequence by E4, E6, E2;
take
c
5
;
take
c
6
;
E7:
( c
1 > 0 & c
1 <> 1 )
by ASYMPT_0:def 3;
E8:
( c
2 > 0 & c
2 <> 1 )
by ASYMPT_0:def 3;
now
let c
7 be
set ;
hereby
assume
c
7 in Big_Oh c
5
;
then consider c
8 being
Element of
Funcs NAT ,
REAL such that E9:
c
7 = c
8
and E10:
ex b
1 being
Realex b
2 being
Nat st
( b
1 > 0 & ( for b
3 being
Nat holds
( b
3 >= b
2 implies ( c
8 . b
3 <= b
1 * (c5 . b3) & c
8 . b
3 >= 0 ) ) ) )
;
consider c
9 being
Real, c
10 being
Nat such that E11:
c
9 > 0
and E12:
for b
1 being
Nat holds
( b
1 >= c
10 implies ( c
8 . b
1 <= c
9 * (c5 . b1) & c
8 . b
1 >= 0 ) )
by E10;
log c
1,c
2 > log c
1,1
by E3, E4, POWER:65;
then
log c
1,c
2 > 0
by E7, POWER:59;
then E13:
c
9 * (log c1,c2) > c
9 * 0
by E11, XREAL_1:70;
now
take c
11 = c
10 + 1;
let c
12 be
Nat;
assume E14:
c
12 >= c
11
;
c
10 + 1
> c
10 + 0
by XREAL_1:10;
then E15:
c
12 > c
10
by E14, XREAL_1:2;
then E16:
c
8 . c
12 <= c
9 * (c5 . c12)
by E12;
c
5 . c
12 =
log c
1,c
12
by E5, E14
.=
(log c1,c2) * (log c2,c12)
by E7, E8, E14, POWER:64
;
then
c
8 . c
12 <= (c9 * (log c1,c2)) * (log c2,c12)
by E16;
hence
c
8 . c
12 <= (c9 * (log c1,c2)) * (c6 . c12)
by E6, E14;
thus
c
8 . c
12 >= 0
by E12, E15;
end;
hence
c
7 in Big_Oh c
6
by E9, E13;
end;
assume
c
7 in Big_Oh c
6
;
then consider c
8 being
Element of
Funcs NAT ,
REAL such that E9:
c
7 = c
8
and E10:
ex b
1 being
Realex b
2 being
Nat st
( b
1 > 0 & ( for b
3 being
Nat holds
( b
3 >= b
2 implies ( c
8 . b
3 <= b
1 * (c6 . b3) & c
8 . b
3 >= 0 ) ) ) )
;
consider c
9 being
Real, c
10 being
Nat such that E11:
c
9 > 0
and E12:
for b
1 being
Nat holds
( b
1 >= c
10 implies ( c
8 . b
1 <= c
9 * (c6 . b1) & c
8 . b
1 >= 0 ) )
by E10;
log c
2,c
1 > log c
2,1
by E3, E4, POWER:65;
then
log c
2,c
1 > 0
by E8, POWER:59;
then E13:
c
9 * (log c2,c1) > c
9 * 0
by E11, XREAL_1:70;
now
take c
11 = c
10 + 1;
let c
12 be
Nat;
assume E14:
c
12 >= c
11
;
c
10 + 1
> c
10 + 0
by XREAL_1:10;
then E15:
c
12 > c
10
by E14, XREAL_1:2;
then E16:
c
8 . c
12 <= c
9 * (c6 . c12)
by E12;
c
6 . c
12 =
log c
2,c
12
by E6, E14
.=
(log c2,c1) * (log c1,c12)
by E7, E8, E14, POWER:64
;
then
c
8 . c
12 <= (c9 * (log c2,c1)) * (log c1,c12)
by E16;
hence
c
8 . c
12 <= (c9 * (log c2,c1)) * (c5 . c12)
by E5, E14;
thus
c
8 . c
12 >= 0
by E12, E15;
end;
hence
c
7 in Big_Oh c
5
by E9, E13;
end;
hence
( c
5 = c
3 & c
6 = c
4 &
Big_Oh c
5 = Big_Oh c
6 )
by TARSKI:2;
end;
:: deftheorem E3 defines seq_a^ ASYMPT_1:def 1 :
E4:
for b1, b2, b3 being Real holds
( ( ) implies ( not b1 > 0 or not b3 > 0 or not b3 <> 1 or b1 to_power b2 = b3 to_power (b2 * (log b3,b1)) ) )
proof
let c
1, c
2, c
3 be
Real;
assume that E5:
c
1 > 0
and E6:
c
3 > 0
and E7:
c
3 <> 1
;
E8:
c
1 to_power c
2 > 0
by E5, POWER:39;
log c
3,
(c1 to_power c2) = c
2 * (log c3,c1)
by E5, E6, E7, POWER:63;
hence
c
1 to_power c
2 = c
3 to_power (c2 * (log c3,c1))
by E6, E7, E8, POWER:def 3;
end;
theorem :: ASYMPT_1:3
proof
let c
1, c
2 be
positive Real;
assume E5:
c
1 < c
2
;
set c
3 =
seq_a^ c
2,1,0;
set c
4 =
seq_a^ c
1,1,0;
hereby
assume
seq_a^ c
2,1,0
in Big_Oh (seq_a^ c1,1,0)
;
then consider c
5 being
Element of
Funcs NAT ,
REAL such that E6:
c
5 = seq_a^ c
2,1,0
and E7:
ex b
1 being
Realex b
2 being
Nat st
( b
1 > 0 & ( for b
3 being
Nat holds
( b
3 >= b
2 implies ( c
5 . b
3 <= b
1 * ((seq_a^ c1,1,0) . b3) & c
5 . b
3 >= 0 ) ) ) )
;
consider c
6 being
Real, c
7 being
Nat such that E8:
c
6 > 0
and E9:
for b
1 being
Nat holds
( b
1 >= c
7 implies ( c
5 . b
1 <= c
6 * ((seq_a^ c1,1,0) . b1) & c
5 . b
1 >= 0 ) )
by E7;
set c
8 =
(log 2,c2) - (log 2,c1);
log 2,c
2 > (log 2,c1) + 0
by E5, POWER:65;
then E10:
(log 2,c2) - (log 2,c1) > 0
by XREAL_1:22;
set c
9 =
[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\];
set c
10 =
max c
7,
[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\];
E11:
(
max c
7,
[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] >= c
7 &
max c
7,
[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] >= [/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] )
by SQUARE_1:46;
(
max c
7,
[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] = c
7 or
max c
7,
[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] = [/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] )
by SQUARE_1:49;
then reconsider c
11 =
max c
7,
[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] as
Nat by E11, INT_1:16;
set c
12 = c
11 + 1;
set c
13 = 2
to_power ((c11 + 1) * (log 2,c1));
E12:
2
to_power ((c11 + 1) * (log 2,c1)) > 0
by POWER:39;
c
11 + 1
> c
11 + 0
by XREAL_1:10;
then E13:
( c
11 + 1
> c
7 & c
11 + 1
> [/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] )
by E11, XREAL_1:2;
[/((log 2,c6) / ((log 2,c2) - (log 2,c1)))\] >= (log 2,c6) / ((log 2,c2) - (log 2,c1))
by INT_1:def 5;
then
c
11 + 1
> (log 2,c6) / ((log 2,c2) - (log 2,c1))
by E13, XREAL_1:2;
then
(c11 + 1) * ((log 2,c2) - (log 2,c1)) > ((log 2,c6) / ((log 2,c2) - (log 2,c1))) * ((log 2,c2) - (log 2,c1))
by E10, XREAL_1:70;
then
(c11 + 1) * ((log 2,c2) - (log 2,c1)) > log 2,c
6
by E10, XCMPLX_1:88;
then
2
to_power ((c11 + 1) * ((log 2,c2) - (log 2,c1))) > 2
to_power (log 2,c6)
by POWER:44;
then
2
to_power (((c11 + 1) * (log 2,c2)) - ((c11 + 1) * (log 2,c1))) > c
6
by E8, POWER:def 3;
then
(2 to_power ((c11 + 1) * (log 2,c2))) / (2 to_power ((c11 + 1) * (log 2,c1))) > c
6
by POWER:34;
then
((2 to_power ((c11 + 1) * (log 2,c2))) / (2 to_power ((c11 + 1) * (log 2,c1)))) * (2 to_power ((c11 + 1) * (log 2,c1))) > c
6 * (2 to_power ((c11 + 1) * (log 2,c1)))
by E12, XREAL_1:70;
then
2
to_power ((c11 + 1) * (log 2,c2)) > c
6 * (2 to_power ((c11 + 1) * (log 2,c1)))
by E12, XCMPLX_1:88;
then
c
2 to_power (c11 + 1) > c
6 * (2 to_power ((c11 + 1) * (log 2,c1)))
by E4;
then E14:
c
2 to_power (c11 + 1) > c
6 * (c1 to_power (c11 + 1))
by E4;
(seq_a^ c2,1,0) . (c11 + 1) <= c
6 * ((seq_a^ c1,1,0) . (c11 + 1))
by E6, E9, E13;
then
c
2 to_power ((1 *