set x = Liouville_constant ;
set a = seq_const 1;
set b = 10;
set c = 2;
A0:
rng (seq_const 1) = {1}
by FUNCOP_1:8;
A1:
1 in 10
by ENUMSET1:def 8, CARD_1:58;
A2:
not 10 is trivial
by NAT_2:28;
reconsider n = 1 as non zero Nat ;
set f = Liouville_seq ((seq_const 1),10);
set pb = powerfact 10;
A3:
Liouville_seq ((seq_const 1),10) is summable
by Th31, A0, A1, ZFMISC_1:31;
for n being Nat holds 0 <= (Liouville_seq ((seq_const 1),10)) . n
by Th33, A2;
then A4:
(Liouville_seq ((seq_const 1),10)) . 1 <= Sum (Liouville_seq ((seq_const 1),10))
by RSSPACE2:3, A3;
A5: (Liouville_seq ((seq_const 1),10)) . 1 =
10 to_power (- 1)
by NEWTON:13, Th39
.=
(1 / 10) to_power 1
by POWER:32
.=
1 / 10
;
set s1 = (Liouville_seq ((seq_const 1),10)) ^\ 2;
set s2 = (powerfact 10) ^\ 2;
A6: (powerfact 10) . 0 =
1 / (10 to_power (0 !))
by DefPower
.=
1 / 10
by NEWTON:12
;
A7: (powerfact 10) . 1 =
1 / (10 to_power (1 !))
by DefPower
.=
1 / 10
by NEWTON:13
;
A8: (Partial_Sums (powerfact 10)) . (0 + 1) =
((Partial_Sums (powerfact 10)) . 0) + ((powerfact 10) . (0 + 1))
by SERIES_1:def 1
.=
((powerfact 10) . 0) + ((powerfact 10) . (0 + 1))
by SERIES_1:def 1
;
Sum (powerfact 10) =
((Partial_Sums (powerfact 10)) . 1) + (Sum ((powerfact 10) ^\ (1 + 1)))
by Th26, SERIES_1:15
.=
(2 / 10) + (Sum ((powerfact 10) ^\ 2))
by A6, A7, A8
;
then A9:
Sum ((powerfact 10) ^\ 2) = (Sum (powerfact 10)) - (2 / 10)
;
Sum (powerfact 10) <= 10 / (10 - 1)
by Th26;
then A10:
Sum ((powerfact 10) ^\ 2) <= (10 / (10 - 1)) - (2 / 10)
by A9, XREAL_1:9;
A11:
(powerfact 10) ^\ 2 is summable
by Th26, SERIES_1:12;
for n being Nat holds
( 0 <= ((Liouville_seq ((seq_const 1),10)) ^\ 2) . n & ((Liouville_seq ((seq_const 1),10)) ^\ 2) . n <= ((powerfact 10) ^\ 2) . n )
proof
let n be
Nat;
( 0 <= ((Liouville_seq ((seq_const 1),10)) ^\ 2) . n & ((Liouville_seq ((seq_const 1),10)) ^\ 2) . n <= ((powerfact 10) ^\ 2) . n )
A12:
((Liouville_seq ((seq_const 1),10)) ^\ 2) . n = (Liouville_seq ((seq_const 1),10)) . (n + 2)
by NAT_1:def 3;
(Liouville_seq ((seq_const 1),10)) . (n + 2) <= ((2 - 1) (#) (powerfact 10)) . (n + 2)
by Th34, A0, ZFMISC_1:7, CARD_1:50;
then
(Liouville_seq ((seq_const 1),10)) . (n + 2) <= (2 - 1) * ((powerfact 10) . (n + 2))
by VALUED_1:6;
hence
(
0 <= ((Liouville_seq ((seq_const 1),10)) ^\ 2) . n &
((Liouville_seq ((seq_const 1),10)) ^\ 2) . n <= ((powerfact 10) ^\ 2) . n )
by Th33, A2, A12, NAT_1:def 3;
verum
end;
then A13:
Sum ((Liouville_seq ((seq_const 1),10)) ^\ 2) <= Sum ((powerfact 10) ^\ 2)
by SERIES_1:20, A11;
A14: Sum (Liouville_seq ((seq_const 1),10)) =
((Partial_Sums (Liouville_seq ((seq_const 1),10))) . 1) + (Sum ((Liouville_seq ((seq_const 1),10)) ^\ (1 + 1)))
by A3, SERIES_1:15
.=
(((Partial_Sums (Liouville_seq ((seq_const 1),10))) . 0) + ((Liouville_seq ((seq_const 1),10)) . (0 + 1))) + (Sum ((Liouville_seq ((seq_const 1),10)) ^\ (1 + 1)))
by SERIES_1:def 1
.=
(((Liouville_seq ((seq_const 1),10)) . 0) + ((Liouville_seq ((seq_const 1),10)) . (0 + 1))) + (Sum ((Liouville_seq ((seq_const 1),10)) ^\ (1 + 1)))
by SERIES_1:def 1
.=
(0 + ((Liouville_seq ((seq_const 1),10)) . 1)) + (Sum ((Liouville_seq ((seq_const 1),10)) ^\ (1 + 1)))
by DefLio
.=
(1 / 10) + (Sum ((Liouville_seq ((seq_const 1),10)) ^\ 2))
by A5
;
Sum ((Liouville_seq ((seq_const 1),10)) ^\ 2) <= (10 / (10 - 1)) - (2 / 10)
by A13, A10, XXREAL_0:2;
then
(1 / 10) + (Sum ((Liouville_seq ((seq_const 1),10)) ^\ 2)) <= (1 / 10) + ((10 / (10 - 1)) - (2 / 10))
by XREAL_1:7;
hence
( 1 / 10 < Liouville_constant & Liouville_constant <= (10 / 9) - (1 / 10) )
by A4, A5, A14, XXREAL_0:1; verum