let m be Nat; Sum ((sqr (x_r-seq m)) ") <= Sum (sqr (cosec (x_r-seq m)))
set f = x_r-seq m;
set f1 = sqr (cosec (x_r-seq m));
set f2 = (sqr (x_r-seq m)) " ;
A1:
len (x_r-seq m) = m
by Th19;
A2:
len (cosec (x_r-seq m)) = len (x_r-seq m)
by Lm15;
A3:
len (sqr (x_r-seq m)) = len (x_r-seq m)
by RVSUM_1:143;
now for n being Nat st n in Seg m holds
((sqr (x_r-seq m)) ") . n <= (sqr (cosec (x_r-seq m))) . nlet n be
Nat;
( n in Seg m implies ((sqr (x_r-seq m)) ") . n <= (sqr (cosec (x_r-seq m))) . n )assume
n in Seg m
;
((sqr (x_r-seq m)) ") . n <= (sqr (cosec (x_r-seq m))) . nthen A4:
( 1
<= n &
n <= m )
by FINSEQ_1:1;
then A5:
n in dom (x_r-seq m)
by A1, FINSEQ_3:25;
A6:
(sqr (cosec (x_r-seq m))) . n = ((cosec (x_r-seq m)) . n) ^2
by VALUED_1:11;
A7:
(cosec (x_r-seq m)) . n = cosec ((x_r-seq m) . n)
by A5, Def4;
A8:
((sqr (x_r-seq m)) ") . n = ((sqr (x_r-seq m)) . n) "
by VALUED_1:10;
A9:
(sqr (x_r-seq m)) . n = ((x_r-seq m) . n) ^2
by VALUED_1:11;
A10:
(x_r-seq m) . n < PI / 2
by A4, Th21;
A11:
0 < (x_r-seq m) . n
by A4, Th21;
A12:
((sin . ((x_r-seq m) . n)) ^2) " = (cosec ((x_r-seq m) . n)) ^2
by XCMPLX_1:204;
PI / 2
< PI / 1
by XREAL_1:76;
then
(x_r-seq m) . n < PI
by A10, XXREAL_0:2;
then
(x_r-seq m) . n in ].0,PI.[
by A11, XXREAL_1:4;
then A13:
0 < sin ((x_r-seq m) . n)
by COMPTRIG:7;
sin . ((x_r-seq m) . n) <= (x_r-seq m) . n
by A11, Th17;
then
(sin . ((x_r-seq m) . n)) ^2 <= ((x_r-seq m) . n) ^2
by A13, XREAL_1:66;
hence
((sqr (x_r-seq m)) ") . n <= (sqr (cosec (x_r-seq m))) . n
by A6, A7, A8, A9, A12, A13, XREAL_1:85;
verum end;
hence
Sum ((sqr (x_r-seq m)) ") <= Sum (sqr (cosec (x_r-seq m)))
by A1, A2, A3, RVSUM_1:82; verum