let k, m be Nat; ( 1 <= k & k <= m implies (2 / (k * PI)) + (((x_r-seq m) ") . k) = ((x_r-seq (m + 1)) ") . k )
assume that
A1:
1 <= k
and
A2:
k <= m
; (2 / (k * PI)) + (((x_r-seq m) ") . k) = ((x_r-seq (m + 1)) ") . k
set f = x_r-seq m;
set g = x_r-seq (m + 1);
m + 0 <= m + 1
by XREAL_1:6;
then
k <= m + 1
by A2, XXREAL_0:2;
then A3:
(x_r-seq (m + 1)) . k = (k * PI) / ((2 * (m + 1)) + 1)
by A1, Th19;
(x_r-seq m) . k = (k * PI) / ((2 * m) + 1)
by A1, A2, Th19;
then ((2 * m) + 1) / (k * PI) =
((x_r-seq m) . k) "
by XCMPLX_1:213
.=
((x_r-seq m) ") . k
by VALUED_1:10
;
hence (2 / (k * PI)) + (((x_r-seq m) ") . k) =
((2 * (m + 1)) + 1) / (k * PI)
.=
((x_r-seq (m + 1)) . k) "
by A3, XCMPLX_1:213
.=
((x_r-seq (m + 1)) ") . k
by VALUED_1:10
;
verum