let a, b, c, d be Real; ( (a ^2) + (b ^2) < 1 & (c ^2) + (d ^2) = 1 implies (((a + c) / 2) ^2) + (((b + d) / 2) ^2) < 1 )
assume that
A1:
(a ^2) + (b ^2) < 1
and
A2:
(c ^2) + (d ^2) = 1
; (((a + c) / 2) ^2) + (((b + d) / 2) ^2) < 1
reconsider u = |[a,b]|, v = |[c,d]| as Element of (TOP-REAL 2) ;
A4:
|.|(u,v)|.| <= |.u.| * |.v.|
by EUCLID_2:51;
A5:
( |.u.| ^2 < 1 & |.v.| ^2 = 1 )
by A1, A2, TOPGEN_5:9;
A6: |(u,v)| =
((u `1) * (v `1)) + ((u `2) * (v `2))
by EUCLID_3:41
.=
(a * (v `1)) + ((u `2) * (v `2))
by EUCLID:52
.=
(a * (v `1)) + (b * (v `2))
by EUCLID:52
.=
(a * c) + (b * (v `2))
by EUCLID:52
.=
(a * c) + (b * d)
by EUCLID:52
;
(|.u.| ^2) * (|.v.| ^2) < 1 * 1
by A5;
then
(|.u.| * |.v.|) ^2 < 1
;
then
|.u.| * |.v.| < 1
by SQUARE_1:52;
then A7:
|.|(u,v)|.| < 1
by XXREAL_0:2, A4;
|(u,v)| <= |.|(u,v)|.|
by COMPLEX1:76;
then
(a * c) + (b * d) < 1
by A6, A7, XXREAL_0:2;
then
2 * ((a * c) + (b * d)) < 2 * 1
by XREAL_1:68;
then
(((2 * a) * c) + ((2 * b) * d)) + ((a ^2) + (b ^2)) < 2 + 1
by A1, XREAL_1:8;
then
((((2 * a) * c) + ((2 * b) * d)) + ((a ^2) + (b ^2))) + 1 < (2 + 1) + 1
by XREAL_1:8;
then
(((((2 * a) * c) + ((2 * b) * d)) + ((a ^2) + (b ^2))) + 1) / 4 < 4 / 4
by XREAL_1:74;
hence
(((a + c) / 2) ^2) + (((b + d) / 2) ^2) < 1
by A2; verum