let p1, p2, p be Point of (TOP-REAL 2); :: thesis: for r1, s1, r2, s2, r being real number
for u being Point of (Euclid 2) st u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball u,r holds
p in Ball u,r
let r1, s1, r2, s2, r be real number ; :: thesis: for u being Point of (Euclid 2) st u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball u,r holds
p in Ball u,r
let u be Point of (Euclid 2); :: thesis: ( u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball u,r implies p in Ball u,r )
assume that
A1: u = p1 and
A2: p1 = |[r1,s1]| and
A3: p2 = |[r2,s2]| and
A4: p = |[r2,s1]| and
A5: p2 in Ball u,r ; :: thesis: p in Ball u,r
reconsider r1 = r1, s1 = s1, r2 = r2, s2 = s2 as Real by XREAL_0:def 1;
p2 in { u6 where u6 is Element of (Euclid 2) : dist u,u6 < r } by A5, METRIC_1:18;
then A6: ex u5 being Point of (Euclid 2) st
( u5 = p2 & dist u,u5 < r ) ;
reconsider p1' = p1, p2' = p2, p' = p as Element of REAL 2 by EUCLID:25;
A7: (Pitag_dist 2) . p1',p2' = |.(p1' - p2').| by EUCLID:def 6;
A8: (Pitag_dist 2) . p1',p' = |.(p1' - p').| by EUCLID:def 6;
reconsider up = p as Point of (Euclid 2) by EUCLID:25;
A9: dist u,up = |.(p1' - p').| by A1, A8, METRIC_1:def 1;
X: ( p1' - p2' = p1 - p2 & p1' - p' = p1 - p ) by EUCLID:73;
A10: |.(p1' - p2').| < r by A1, A6, A7, METRIC_1:def 1;
A11: ( p1' - p' = <*(r1 - r2),(s1 - s1)*> & p1' - p2' = <*(r1 - r2),(s1 - s2)*> ) by A2, A3, A4, Th10, X;
then A12: sqr (p1' - p') = <*(sqrreal . (r1 - r2)),(sqrreal . (s1 - s1))*> by FINSEQ_2:40;
A13: sqr (p1' - p2') = <*(sqrreal . (r1 - r2)),(sqrreal . (s1 - s2))*> by A11, FINSEQ_2:40;
A14: Sum (sqr (p1' - p')) = (sqrreal . (r1 - r2)) + (sqrreal . 0 ) by A12, RVSUM_1:107
.= (sqrreal . (r1 - r2)) + (0 ^2 ) by RVSUM_1:def 2
.= sqrreal . (r1 - r2) ;
(s1 - s2) ^2 >= 0 by XREAL_1:65;
then sqrreal . (s1 - s2) >= 0 by RVSUM_1:def 2;
then A15: (sqrreal . (r1 - r2)) + 0 <= (sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2)) by XREAL_1:9;
(r1 - r2) ^2 >= 0 by XREAL_1:65;
then sqrreal . (r1 - r2) >= 0 by RVSUM_1:def 2;
then A16: |.(p1' - p').| <= sqrt ((sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2))) by A14, A15, SQUARE_1:94;
|.(p1' - p2').| = sqrt ((sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2))) by A13, RVSUM_1:107;
then |.(p1' - p').| < r by A10, A16, XXREAL_0:2;
then p in { u6 where u6 is Element of (Euclid 2) : dist u,u6 < r } by A9;
hence p in Ball u,r by METRIC_1:18; :: thesis: verum