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 p1' = p1, p2' = p2, p' = p as Element of REAL 2 by EUCLID:25;
reconsider r1 = r1, s1 = s1, r2 = r2, s2 = s2 as Real by XREAL_0:def 1;
A6: (Pitag_dist 2) . p1',p2' = |.(p1' - p2').| by EUCLID:def 6;
p2 in { u6 where u6 is Element of (Euclid 2) : dist u,u6 < r } by A5, METRIC_1:18;
then ex u5 being Point of (Euclid 2) st
( u5 = p2 & dist u,u5 < r ) ;
then A7: |.(p1' - p2').| < r by A1, A6, METRIC_1:def 1;
reconsider up = p as Point of (Euclid 2) by EUCLID:25;
(Pitag_dist 2) . p1',p' = |.(p1' - p').| by EUCLID:def 6;
then A8: dist u,up = |.(p1' - p').| by A1, METRIC_1:def 1;
(s1 - s2) ^2 >= 0 by XREAL_1:65;
then sqrreal . (s1 - s2) >= 0 by RVSUM_1:def 2;
then A9: (sqrreal . (r1 - r2)) + 0 <= (sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2)) by XREAL_1:9;
p1' - p' = p1 - p by EUCLID:73;
then p1' - p' = <*(r1 - r2),(s1 - s1)*> by A2, A4, Th10;
then sqr (p1' - p') = <*(sqrreal . (r1 - r2)),(sqrreal . (s1 - s1))*> by FINSEQ_2:40;
then A10: Sum (sqr (p1' - p')) = (sqrreal . (r1 - r2)) + (sqrreal . 0 ) by RVSUM_1:107
.= (sqrreal . (r1 - r2)) + (0 ^2 ) by RVSUM_1:def 2
.= sqrreal . (r1 - r2) ;
p1' - p2' = p1 - p2 by EUCLID:73;
then p1' - p2' = <*(r1 - r2),(s1 - s2)*> by A2, A3, Th10;
then sqr (p1' - p2') = <*(sqrreal . (r1 - r2)),(sqrreal . (s1 - s2))*> by FINSEQ_2:40;
then A11: |.(p1' - p2').| = sqrt ((sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2))) by RVSUM_1:107;
(r1 - r2) ^2 >= 0 by XREAL_1:65;
then sqrreal . (r1 - r2) >= 0 by RVSUM_1:def 2;
then |.(p1' - p').| <= sqrt ((sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2))) by A10, A9, SQUARE_1:94;
then |.(p1' - p').| < r by A7, A11, XXREAL_0:2;
then p in { u6 where u6 is Element of (Euclid 2) : dist u,u6 < r } by A8;
hence p in Ball u,r by METRIC_1:18; :: thesis: verum