let g, r, p be Real; :: thesis: ( r in ].p,g.[ iff |.((p + g) - (2 * r)).| < g - p )
thus ( r in ].p,g.[ implies |.((p + g) - (2 * r)).| < g - p ) :: thesis: ( |.((p + g) - (2 * r)).| < g - p implies r in ].p,g.[ )
proof
assume r in ].p,g.[ ; :: thesis: |.((p + g) - (2 * r)).| < g - p
then A1: ex s being Real st
( s = r & p < s & s < g ) ;
then 2 * r < 2 * g by XREAL_1:68;
then - (2 * r) > - (2 * g) by XREAL_1:24;
then (p + g) + (- (2 * r)) > (p + g) + (- (2 * g)) by XREAL_1:6;
then A2: (p + g) - (2 * r) > - (g - p) ;
2 * p < 2 * r by A1, XREAL_1:68;
then - (2 * p) > - (2 * r) by XREAL_1:24;
then (p + g) + (- (2 * p)) > (p + g) + (- (2 * r)) by XREAL_1:6;
hence |.((p + g) - (2 * r)).| < g - p by A2, SEQ_2:1; :: thesis: verum
end;
assume A3: |.((p + g) - (2 * r)).| < g - p ; :: thesis: r in ].p,g.[
then (p + g) - (2 * r) > - (g - p) by SEQ_2:1;
then p + g > (p - g) + (2 * r) by XREAL_1:20;
then (p + g) - (p - g) > 2 * r by XREAL_1:20;
then A4: (1 / 2) * (2 * g) > (1 / 2) * (2 * r) by XREAL_1:68;
g - p > (p + g) - (2 * r) by A3, SEQ_2:1;
then (2 * r) + (g - p) > p + g by XREAL_1:19;
then 2 * r > (p + g) - (g - p) by XREAL_1:19;
then (1 / 2) * (2 * r) > (1 / 2) * (2 * p) by XREAL_1:68;
hence r in ].p,g.[ by A4; :: thesis: verum