let s1, s2, s3, s4, s5 be Real_Sequence; ( s4 = s1 (#) s1 & s5 = s2 (#) s2 & ( for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 ) ) implies for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n)) )
assume that
A1:
s4 = s1 (#) s1
and
A2:
s5 = s2 (#) s2
and
A3:
for n being Nat holds
( s1 . n >= 0 & s2 . n >= 0 & s3 . n = ((s1 . n) + (s2 . n)) ^2 )
; for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))
A4:
s1 . 0 >= 0
by A3;
defpred S1[ Nat] means sqrt ((Partial_Sums s3) . $1) <= (sqrt ((Partial_Sums s4) . $1)) + (sqrt ((Partial_Sums s5) . $1));
A5:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A6:
sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))
;
S1[n + 1]
set j =
s2 . (n + 1);
set h =
s1 . (n + 1);
set w =
(Partial_Sums s5) . n;
set v =
(Partial_Sums s4) . n;
set u =
(Partial_Sums s3) . n;
A7:
(Partial_Sums s5) . n >= 0
by A2, Th36;
A8:
(s2 . (n + 1)) ^2 >= 0
by XREAL_1:63;
then A9:
sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) >= 0
by A7, SQUARE_1:def 2;
A10:
(Partial_Sums s4) . n >= 0
by A1, Th36;
then A11:
sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) >= 0
by A7, SQUARE_1:def 2;
A12:
(Partial_Sums s3) . n >= 0
by A3, Lm10;
then
sqrt ((Partial_Sums s3) . n) >= 0
by SQUARE_1:def 2;
then
(sqrt ((Partial_Sums s3) . n)) ^2 <= ((sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))) ^2
by A6, SQUARE_1:15;
then
(Partial_Sums s3) . n <= (((sqrt ((Partial_Sums s4) . n)) ^2) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((sqrt ((Partial_Sums s5) . n)) ^2)
by A12, SQUARE_1:def 2;
then
(Partial_Sums s3) . n <= (((Partial_Sums s4) . n) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((sqrt ((Partial_Sums s5) . n)) ^2)
by A10, SQUARE_1:def 2;
then
(Partial_Sums s3) . n <= (((Partial_Sums s4) . n) + ((2 * (sqrt ((Partial_Sums s4) . n))) * (sqrt ((Partial_Sums s5) . n)))) + ((Partial_Sums s5) . n)
by A7, SQUARE_1:def 2;
then
((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) <= ((((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * ((sqrt ((Partial_Sums s4) . n)) * (sqrt ((Partial_Sums s5) . n))))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))
by XREAL_1:6;
then A13:
((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) <= ((((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))
by A10, A7, SQUARE_1:29;
A14:
s1 . (n + 1) >= 0
by A3;
A15:
s2 . (n + 1) >= 0
by A3;
A16:
(s1 . (n + 1)) ^2 >= 0
by XREAL_1:63;
then A17:
sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) >= 0
by A10, SQUARE_1:def 2;
(((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= 2
* (sqrt ((((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) * (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n))))
by A10, A7, A16, A8, SIN_COS2:1;
then
(((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= 2
* (sqrt ((((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))))
;
then
(((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= 2
* ((sqrt (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n))))
by A10, A7, A16, A8, SQUARE_1:29;
then
(((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= (2 * (sqrt (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))
;
then
(((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= (2 * ((sqrt ((s1 . (n + 1)) ^2)) * (sqrt ((s2 . (n + 1)) ^2)))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))
by A16, A8, SQUARE_1:29;
then
(((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= ((2 * (sqrt ((s1 . (n + 1)) ^2))) * (sqrt ((s2 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))
;
then
(((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= ((2 * (s1 . (n + 1))) * (sqrt ((s2 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))
by A14, SQUARE_1:22;
then
(((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n)) >= ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))
by A15, SQUARE_1:22;
then
((((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n))) + ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))) >= (((2 * (s1 . (n + 1))) * (s2 . (n + 1))) * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) + ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)))
by XREAL_1:6;
then
(((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + (((s2 . (n + 1)) ^2) * ((Partial_Sums s4) . n))) + (((s1 . (n + 1)) ^2) * ((Partial_Sums s5) . n))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2)) >= ((((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)) + ((2 * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) * ((s1 . (n + 1)) * (s2 . (n + 1))))) + (((s1 . (n + 1)) ^2) * ((s2 . (n + 1)) ^2))
;
then
(
((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) ^2 >= 0 &
(((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)) >= (((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) ^2) + ((2 * (sqrt (((Partial_Sums s5) . n) * ((Partial_Sums s4) . n)))) * ((s1 . (n + 1)) * (s2 . (n + 1))))) + (((s1 . (n + 1)) * (s2 . (n + 1))) ^2) )
by A10, A7, SQUARE_1:def 2, XREAL_1:63;
then
sqrt (((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) ^2) <= sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))
by SQUARE_1:26;
then
(sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1))) <= sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))
by A14, A15, A11, SQUARE_1:22;
then
2
* ((sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n))) + ((s1 . (n + 1)) * (s2 . (n + 1)))) <= 2
* (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))))
by XREAL_1:64;
then
(((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + ((2 * (sqrt (((Partial_Sums s4) . n) * ((Partial_Sums s5) . n)))) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))) <= (((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))
by XREAL_1:6;
then
((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1))) <= (((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))
by A13, XXREAL_0:2;
then
(((Partial_Sums s3) . n) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))) + (((s1 . (n + 1)) ^2) + ((s2 . (n + 1)) ^2)) <= ((((Partial_Sums s4) . n) + ((Partial_Sums s5) . n)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + (((s1 . (n + 1)) ^2) + ((s2 . (n + 1)) ^2))
by XREAL_1:6;
then
((Partial_Sums s3) . n) + ((((s1 . (n + 1)) ^2) + ((2 * (s1 . (n + 1))) * (s2 . (n + 1)))) + ((s2 . (n + 1)) ^2)) <= ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))
;
then
((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2) <= (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) ^2) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))
by A10, A16, SQUARE_1:def 2;
then
((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2) <= (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) ^2) + (2 * (sqrt ((((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2)) * (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + ((sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) ^2)
by A7, A8, SQUARE_1:def 2;
then
(
((s1 . (n + 1)) + (s2 . (n + 1))) ^2 >= 0 &
((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2) <= (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) ^2) + (2 * ((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) * (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))))) + ((sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2))) ^2) )
by A10, A7, A16, A8, SQUARE_1:29, XREAL_1:63;
then A18:
sqrt (((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2)) <= sqrt (((sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) + (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))) ^2)
by A12, SQUARE_1:26;
A19:
sqrt ((Partial_Sums s3) . (n + 1)) =
sqrt (((Partial_Sums s3) . n) + (s3 . (n + 1)))
by SERIES_1:def 1
.=
sqrt (((Partial_Sums s3) . n) + (((s1 . (n + 1)) + (s2 . (n + 1))) ^2))
by A3
;
(sqrt ((Partial_Sums s4) . (n + 1))) + (sqrt ((Partial_Sums s5) . (n + 1))) =
(sqrt (((Partial_Sums s4) . n) + (s4 . (n + 1)))) + (sqrt ((Partial_Sums s5) . (n + 1)))
by SERIES_1:def 1
.=
(sqrt (((Partial_Sums s4) . n) + (s4 . (n + 1)))) + (sqrt (((Partial_Sums s5) . n) + (s5 . (n + 1))))
by SERIES_1:def 1
.=
(sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) * (s1 . (n + 1))))) + (sqrt (((Partial_Sums s5) . n) + (s5 . (n + 1))))
by A1, SEQ_1:8
.=
(sqrt (((Partial_Sums s4) . n) + ((s1 . (n + 1)) ^2))) + (sqrt (((Partial_Sums s5) . n) + ((s2 . (n + 1)) ^2)))
by A2, SEQ_1:8
;
hence
S1[
n + 1]
by A19, A17, A9, A18, SQUARE_1:22;
verum
end;
A20:
s2 . 0 >= 0
by A3;
(sqrt ((Partial_Sums s4) . 0)) + (sqrt ((Partial_Sums s5) . 0)) =
(sqrt (s4 . 0)) + (sqrt ((Partial_Sums s5) . 0))
by SERIES_1:def 1
.=
(sqrt (s4 . 0)) + (sqrt (s5 . 0))
by SERIES_1:def 1
.=
(sqrt ((s1 . 0) * (s1 . 0))) + (sqrt (s5 . 0))
by A1, SEQ_1:8
.=
(sqrt ((s1 . 0) ^2)) + (sqrt ((s2 . 0) * (s2 . 0)))
by A2, SEQ_1:8
.=
(s1 . 0) + (sqrt ((s2 . 0) ^2))
by A4, SQUARE_1:22
.=
(s1 . 0) + (s2 . 0)
by A20, SQUARE_1:22
.=
sqrt (((s1 . 0) + (s2 . 0)) ^2)
by A4, A20, SQUARE_1:22
.=
sqrt (s3 . 0)
by A3
.=
sqrt ((Partial_Sums s3) . 0)
by SERIES_1:def 1
;
then A21:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A21, A5);
hence
for n being Nat holds sqrt ((Partial_Sums s3) . n) <= (sqrt ((Partial_Sums s4) . n)) + (sqrt ((Partial_Sums s5) . n))
; verum