let a, b, c, d be Real; :: thesis: ( (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 ; :: thesis: (((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; :: thesis: verum