let m be Nat; Sum (sqr (cot (x_r-seq m))) <= Sum ((sqr (x_r-seq m)) ")
set f = x_r-seq m;
set f1 = sqr (cot (x_r-seq m));
set f2 = (sqr (x_r-seq m)) " ;
A1:
len (x_r-seq m) = m
by Th19;
A2:
len (cot (x_r-seq m)) = len (x_r-seq m)
by Lm14;
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 (cot (x_r-seq m))) . n <= ((sqr (x_r-seq m)) ") . nlet n be
Nat;
( n in Seg m implies (sqr (cot (x_r-seq m))) . n <= ((sqr (x_r-seq m)) ") . n )assume
n in Seg m
;
(sqr (cot (x_r-seq m))) . n <= ((sqr (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 (cot (x_r-seq m))) . n = ((cot (x_r-seq m)) . n) ^2
by VALUED_1:11;
A7:
(cot (x_r-seq m)) . n = cot ((x_r-seq m) . n)
by A5, Def3;
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:
(tan ((x_r-seq m) . n)) " = cot ((x_r-seq m) . n)
by Th15;
A11:
(x_r-seq m) . n < PI / 2
by A4, Th21;
A12:
0 < (x_r-seq m) . n
by A4, Th21;
then A13:
(x_r-seq m) . n in ].((- (PI / 2)) + (PI * 0)),((PI / 2) + (PI * 0)).[
by A11, XXREAL_1:4;
].((- (PI / 2)) + (PI * 0)),((PI / 2) + (PI * 0)).[ in { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum }
;
then
(x_r-seq m) . n in dom tan
by A13, Th16, TARSKI:def 4;
then
tan . ((x_r-seq m) . n) = tan ((x_r-seq m) . n)
by RFUNCT_1:def 1;
then A14:
((tan . ((x_r-seq m) . n)) ^2) " = (cot ((x_r-seq m) . n)) ^2
by A10, XCMPLX_1:204;
(x_r-seq m) . n <= tan . ((x_r-seq m) . n)
by A4, A12, Th18, Th21;
then
((x_r-seq m) . n) ^2 <= (tan . ((x_r-seq m) . n)) ^2
by A12, XREAL_1:66;
hence
(sqr (cot (x_r-seq m))) . n <= ((sqr (x_r-seq m)) ") . n
by A6, A7, A8, A9, A12, A14, XREAL_1:85;
verum end;
hence
Sum (sqr (cot (x_r-seq m))) <= Sum ((sqr (x_r-seq m)) ")
by A1, A2, A3, RVSUM_1:82; verum