:: TOPREAL9 semantic presentation begin theorem :: TOPREAL9:1 canceled; theorem Th2: :: TOPREAL9:2 for n being Element of NAT for x, y, z being Point of (TOP-REAL n) st x + y = x + z holds y = z proof let n be Element of NAT ; ::_thesis: for x, y, z being Point of (TOP-REAL n) st x + y = x + z holds y = z let x, y, z be Point of (TOP-REAL n); ::_thesis: ( x + y = x + z implies y = z ) assume x + y = x + z ; ::_thesis: y = z then (x - x) + y = (x + z) - x by EUCLID:26; then ( x - x = 0. (TOP-REAL n) & (x - x) + y = (x - x) + z ) by EUCLID:42, EUCLID:26; hence y = (0. (TOP-REAL n)) + z by EUCLID:27 .= z by EUCLID:27 ; ::_thesis: verum end; theorem Th3: :: TOPREAL9:3 for n being Element of NAT for x being Point of (TOP-REAL n) st not n is empty holds x <> x + (1.REAL n) proof let n be Element of NAT ; ::_thesis: for x being Point of (TOP-REAL n) st not n is empty holds x <> x + (1.REAL n) let x be Point of (TOP-REAL n); ::_thesis: ( not n is empty implies x <> x + (1.REAL n) ) A1: ( 0.REAL n = 0. (TOP-REAL n) & x = x + (0. (TOP-REAL n)) ) by EUCLID:27, EUCLID:66; assume ( not n is empty & x = x + (1.REAL n) ) ; ::_thesis: contradiction hence contradiction by A1, Th2, REVROT_1:19; ::_thesis: verum end; theorem Th4: :: TOPREAL9:4 for n being Element of NAT for r being real number for y, z being Point of (TOP-REAL n) for x being set st x = ((1 - r) * y) + (r * z) holds ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) ) proof let n be Element of NAT ; ::_thesis: for r being real number for y, z being Point of (TOP-REAL n) for x being set st x = ((1 - r) * y) + (r * z) holds ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) ) let r be real number ; ::_thesis: for y, z being Point of (TOP-REAL n) for x being set st x = ((1 - r) * y) + (r * z) holds ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) ) let y, z be Point of (TOP-REAL n); ::_thesis: for x being set st x = ((1 - r) * y) + (r * z) holds ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) ) let x be set ; ::_thesis: ( x = ((1 - r) * y) + (r * z) implies ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) ) ) assume A1: x = ((1 - r) * y) + (r * z) ; ::_thesis: ( ( not x = y or r = 0 or y = z ) & ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) ) hereby ::_thesis: ( ( ( r = 0 or y = z ) implies x = y ) & ( not x = z or r = 1 or y = z ) & ( ( r = 1 or y = z ) implies x = z ) ) assume x = y ; ::_thesis: ( r = 0 or y = z ) then 0. (TOP-REAL n) = (((1 - r) * y) + (r * z)) - y by A1, EUCLID:42 .= (((1 - r) * y) - y) + (r * z) by EUCLID:26 .= (((1 - r) * y) - (1 * y)) + (r * z) by EUCLID:29 .= (((1 - r) - 1) * y) + (r * z) by EUCLID:50 .= (r * z) - (r * y) by EUCLID:40 .= r * (z - y) by EUCLID:49 ; then ( r = 0 or z - y = 0. (TOP-REAL n) ) by EUCLID:31; hence ( r = 0 or y = z ) by EUCLID:43; ::_thesis: verum end; hereby ::_thesis: ( x = z iff ( r = 1 or y = z ) ) assume A2: ( r = 0 or y = z ) ; ::_thesis: x = y percases ( r = 0 or z = y ) by A2; suppose r = 0 ; ::_thesis: x = y hence x = y + (0 * z) by A1, EUCLID:29 .= y + (0. (TOP-REAL n)) by EUCLID:29 .= y by EUCLID:27 ; ::_thesis: verum end; suppose z = y ; ::_thesis: x = y hence x = ((1 - r) + r) * y by A1, EUCLID:33 .= y by EUCLID:29 ; ::_thesis: verum end; end; end; hereby ::_thesis: ( ( r = 1 or y = z ) implies x = z ) assume x = z ; ::_thesis: ( r = 1 or y = z ) then 0. (TOP-REAL n) = (((1 - r) * y) + (r * z)) - z by A1, EUCLID:42 .= ((1 - r) * y) + ((r * z) - z) by EUCLID:45 .= ((1 - r) * y) + ((r * z) + ((- 1) * z)) .= ((1 - r) * y) + (((- 1) + r) * z) by EUCLID:33 .= ((1 - r) * y) + ((- (1 - r)) * z) .= ((1 - r) * y) - ((1 - r) * z) by EUCLID:40 .= (1 - r) * (y - z) by EUCLID:49 ; then ( (1 - r) + r = 0 + r or y - z = 0. (TOP-REAL n) ) by EUCLID:31; hence ( r = 1 or y = z ) by EUCLID:43; ::_thesis: verum end; assume A3: ( r = 1 or y = z ) ; ::_thesis: x = z percases ( r = 1 or y = z ) by A3; suppose r = 1 ; ::_thesis: x = z hence x = (0. (TOP-REAL n)) + (1 * z) by A1, EUCLID:29 .= 1 * z by EUCLID:27 .= z by EUCLID:29 ; ::_thesis: verum end; suppose y = z ; ::_thesis: x = z hence x = ((1 - r) + r) * z by A1, EUCLID:33 .= z by EUCLID:29 ; ::_thesis: verum end; end; end; theorem Th5: :: TOPREAL9:5 for f being real-valued FinSequence holds |.f.| ^2 = Sum (sqr f) proof let f be real-valued FinSequence; ::_thesis: |.f.| ^2 = Sum (sqr f) Sum (sqr f) >= 0 by RVSUM_1:86; hence |.f.| ^2 = Sum (sqr f) by SQUARE_1:def_2; ::_thesis: verum end; theorem Th6: :: TOPREAL9:6 for r being real number for M being non empty MetrSpace for z1, z2, z3 being Point of M st z1 <> z2 & z1 in cl_Ball (z3,r) & z2 in cl_Ball (z3,r) holds r > 0 proof let r be real number ; ::_thesis: for M being non empty MetrSpace for z1, z2, z3 being Point of M st z1 <> z2 & z1 in cl_Ball (z3,r) & z2 in cl_Ball (z3,r) holds r > 0 let M be non empty MetrSpace; ::_thesis: for z1, z2, z3 being Point of M st z1 <> z2 & z1 in cl_Ball (z3,r) & z2 in cl_Ball (z3,r) holds r > 0 let z1, z2, z3 be Point of M; ::_thesis: ( z1 <> z2 & z1 in cl_Ball (z3,r) & z2 in cl_Ball (z3,r) implies r > 0 ) assume that A1: z1 <> z2 and A2: z1 in cl_Ball (z3,r) and A3: z2 in cl_Ball (z3,r) ; ::_thesis: r > 0 now__::_thesis:_not_r_=_0 assume r = 0 ; ::_thesis: contradiction then A4: cl_Ball (z3,r) = {z3} by TOPREAL6:56; then z1 = z3 by A2, TARSKI:def_1; hence contradiction by A1, A3, A4, TARSKI:def_1; ::_thesis: verum end; hence r > 0 by A2, TOPREAL6:55; ::_thesis: verum end; begin definition let n be Nat; let x be Point of (TOP-REAL n); let r be real number ; func Ball (x,r) -> Subset of (TOP-REAL n) equals :: TOPREAL9:def 1 { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } ; coherence { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } is Subset of (TOP-REAL n) proof { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } c= the carrier of (TOP-REAL n) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } or q in the carrier of (TOP-REAL n) ) assume q in { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } ; ::_thesis: q in the carrier of (TOP-REAL n) then ex p being Point of (TOP-REAL n) st ( q = p & |.(p - x).| < r ) ; hence q in the carrier of (TOP-REAL n) ; ::_thesis: verum end; hence { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } is Subset of (TOP-REAL n) ; ::_thesis: verum end; func cl_Ball (x,r) -> Subset of (TOP-REAL n) equals :: TOPREAL9:def 2 { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } ; coherence { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } is Subset of (TOP-REAL n) proof { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } c= the carrier of (TOP-REAL n) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } or q in the carrier of (TOP-REAL n) ) assume q in { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } ; ::_thesis: q in the carrier of (TOP-REAL n) then ex p being Point of (TOP-REAL n) st ( q = p & |.(p - x).| <= r ) ; hence q in the carrier of (TOP-REAL n) ; ::_thesis: verum end; hence { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } is Subset of (TOP-REAL n) ; ::_thesis: verum end; func Sphere (x,r) -> Subset of (TOP-REAL n) equals :: TOPREAL9:def 3 { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } ; coherence { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } is Subset of (TOP-REAL n) proof { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } c= the carrier of (TOP-REAL n) proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } or q in the carrier of (TOP-REAL n) ) assume q in { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } ; ::_thesis: q in the carrier of (TOP-REAL n) then ex p being Point of (TOP-REAL n) st ( q = p & |.(p - x).| = r ) ; hence q in the carrier of (TOP-REAL n) ; ::_thesis: verum end; hence { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } is Subset of (TOP-REAL n) ; ::_thesis: verum end; end; :: deftheorem defines Ball TOPREAL9:def_1_:_ for n being Nat for x being Point of (TOP-REAL n) for r being real number holds Ball (x,r) = { p where p is Point of (TOP-REAL n) : |.(p - x).| < r } ; :: deftheorem defines cl_Ball TOPREAL9:def_2_:_ for n being Nat for x being Point of (TOP-REAL n) for r being real number holds cl_Ball (x,r) = { p where p is Point of (TOP-REAL n) : |.(p - x).| <= r } ; :: deftheorem defines Sphere TOPREAL9:def_3_:_ for n being Nat for x being Point of (TOP-REAL n) for r being real number holds Sphere (x,r) = { p where p is Point of (TOP-REAL n) : |.(p - x).| = r } ; theorem Th7: :: TOPREAL9:7 for n being Element of NAT for r being real number for y, x being Point of (TOP-REAL n) holds ( y in Ball (x,r) iff |.(y - x).| < r ) proof let n be Element of NAT ; ::_thesis: for r being real number for y, x being Point of (TOP-REAL n) holds ( y in Ball (x,r) iff |.(y - x).| < r ) let r be real number ; ::_thesis: for y, x being Point of (TOP-REAL n) holds ( y in Ball (x,r) iff |.(y - x).| < r ) let y, x be Point of (TOP-REAL n); ::_thesis: ( y in Ball (x,r) iff |.(y - x).| < r ) hereby ::_thesis: ( |.(y - x).| < r implies y in Ball (x,r) ) assume y in Ball (x,r) ; ::_thesis: |.(y - x).| < r then ex p being Point of (TOP-REAL n) st ( y = p & |.(p - x).| < r ) ; hence |.(y - x).| < r ; ::_thesis: verum end; thus ( |.(y - x).| < r implies y in Ball (x,r) ) ; ::_thesis: verum end; theorem Th8: :: TOPREAL9:8 for n being Element of NAT for r being real number for y, x being Point of (TOP-REAL n) holds ( y in cl_Ball (x,r) iff |.(y - x).| <= r ) proof let n be Element of NAT ; ::_thesis: for r being real number for y, x being Point of (TOP-REAL n) holds ( y in cl_Ball (x,r) iff |.(y - x).| <= r ) let r be real number ; ::_thesis: for y, x being Point of (TOP-REAL n) holds ( y in cl_Ball (x,r) iff |.(y - x).| <= r ) let y, x be Point of (TOP-REAL n); ::_thesis: ( y in cl_Ball (x,r) iff |.(y - x).| <= r ) hereby ::_thesis: ( |.(y - x).| <= r implies y in cl_Ball (x,r) ) assume y in cl_Ball (x,r) ; ::_thesis: |.(y - x).| <= r then ex p being Point of (TOP-REAL n) st ( y = p & |.(p - x).| <= r ) ; hence |.(y - x).| <= r ; ::_thesis: verum end; thus ( |.(y - x).| <= r implies y in cl_Ball (x,r) ) ; ::_thesis: verum end; theorem Th9: :: TOPREAL9:9 for n being Element of NAT for r being real number for y, x being Point of (TOP-REAL n) holds ( y in Sphere (x,r) iff |.(y - x).| = r ) proof let n be Element of NAT ; ::_thesis: for r being real number for y, x being Point of (TOP-REAL n) holds ( y in Sphere (x,r) iff |.(y - x).| = r ) let r be real number ; ::_thesis: for y, x being Point of (TOP-REAL n) holds ( y in Sphere (x,r) iff |.(y - x).| = r ) let y, x be Point of (TOP-REAL n); ::_thesis: ( y in Sphere (x,r) iff |.(y - x).| = r ) hereby ::_thesis: ( |.(y - x).| = r implies y in Sphere (x,r) ) assume y in Sphere (x,r) ; ::_thesis: |.(y - x).| = r then ex p being Point of (TOP-REAL n) st ( y = p & |.(p - x).| = r ) ; hence |.(y - x).| = r ; ::_thesis: verum end; thus ( |.(y - x).| = r implies y in Sphere (x,r) ) ; ::_thesis: verum end; theorem :: TOPREAL9:10 for n being Element of NAT for r being real number for y being Point of (TOP-REAL n) st y in Ball ((0. (TOP-REAL n)),r) holds |.y.| < r proof let n be Element of NAT ; ::_thesis: for r being real number for y being Point of (TOP-REAL n) st y in Ball ((0. (TOP-REAL n)),r) holds |.y.| < r let r be real number ; ::_thesis: for y being Point of (TOP-REAL n) st y in Ball ((0. (TOP-REAL n)),r) holds |.y.| < r let y be Point of (TOP-REAL n); ::_thesis: ( y in Ball ((0. (TOP-REAL n)),r) implies |.y.| < r ) assume y in Ball ((0. (TOP-REAL n)),r) ; ::_thesis: |.y.| < r then |.(y - (0. (TOP-REAL n))).| < r by Th7; hence |.y.| < r by RLVECT_1:13; ::_thesis: verum end; theorem :: TOPREAL9:11 for n being Element of NAT for r being real number for y being Point of (TOP-REAL n) st y in cl_Ball ((0. (TOP-REAL n)),r) holds |.y.| <= r proof let n be Element of NAT ; ::_thesis: for r being real number for y being Point of (TOP-REAL n) st y in cl_Ball ((0. (TOP-REAL n)),r) holds |.y.| <= r let r be real number ; ::_thesis: for y being Point of (TOP-REAL n) st y in cl_Ball ((0. (TOP-REAL n)),r) holds |.y.| <= r let y be Point of (TOP-REAL n); ::_thesis: ( y in cl_Ball ((0. (TOP-REAL n)),r) implies |.y.| <= r ) assume y in cl_Ball ((0. (TOP-REAL n)),r) ; ::_thesis: |.y.| <= r then |.(y - (0. (TOP-REAL n))).| <= r by Th8; hence |.y.| <= r by RLVECT_1:13; ::_thesis: verum end; theorem :: TOPREAL9:12 for n being Element of NAT for r being real number for y being Point of (TOP-REAL n) st y in Sphere ((0. (TOP-REAL n)),r) holds |.y.| = r proof let n be Element of NAT ; ::_thesis: for r being real number for y being Point of (TOP-REAL n) st y in Sphere ((0. (TOP-REAL n)),r) holds |.y.| = r let r be real number ; ::_thesis: for y being Point of (TOP-REAL n) st y in Sphere ((0. (TOP-REAL n)),r) holds |.y.| = r let y be Point of (TOP-REAL n); ::_thesis: ( y in Sphere ((0. (TOP-REAL n)),r) implies |.y.| = r ) assume y in Sphere ((0. (TOP-REAL n)),r) ; ::_thesis: |.y.| = r then |.(y - (0. (TOP-REAL n))).| = r by Th9; hence |.y.| = r by RLVECT_1:13; ::_thesis: verum end; theorem Th13: :: TOPREAL9:13 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) for e being Point of (Euclid n) st x = e holds Ball (e,r) = Ball (x,r) proof let n be Element of NAT ; ::_thesis: for r being real number for x being Point of (TOP-REAL n) for e being Point of (Euclid n) st x = e holds Ball (e,r) = Ball (x,r) let r be real number ; ::_thesis: for x being Point of (TOP-REAL n) for e being Point of (Euclid n) st x = e holds Ball (e,r) = Ball (x,r) let x be Point of (TOP-REAL n); ::_thesis: for e being Point of (Euclid n) st x = e holds Ball (e,r) = Ball (x,r) let e be Point of (Euclid n); ::_thesis: ( x = e implies Ball (e,r) = Ball (x,r) ) assume A1: x = e ; ::_thesis: Ball (e,r) = Ball (x,r) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Ball (x,r) c= Ball (e,r) let q be set ; ::_thesis: ( q in Ball (e,r) implies q in Ball (x,r) ) assume A2: q in Ball (e,r) ; ::_thesis: q in Ball (x,r) then reconsider f = q as Point of (Euclid n) ; reconsider p = f as Point of (TOP-REAL n) by TOPREAL3:8; dist (f,e) < r by A2, METRIC_1:11; then |.(p - x).| < r by A1, JGRAPH_1:28; hence q in Ball (x,r) ; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Ball (x,r) or q in Ball (e,r) ) assume A3: q in Ball (x,r) ; ::_thesis: q in Ball (e,r) then reconsider q = q as Point of (TOP-REAL n) ; reconsider f = q as Point of (Euclid n) by TOPREAL3:8; |.(q - x).| < r by A3, Th7; then dist (f,e) < r by A1, JGRAPH_1:28; hence q in Ball (e,r) by METRIC_1:11; ::_thesis: verum end; theorem Th14: :: TOPREAL9:14 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) for e being Point of (Euclid n) st x = e holds cl_Ball (e,r) = cl_Ball (x,r) proof let n be Element of NAT ; ::_thesis: for r being real number for x being Point of (TOP-REAL n) for e being Point of (Euclid n) st x = e holds cl_Ball (e,r) = cl_Ball (x,r) let r be real number ; ::_thesis: for x being Point of (TOP-REAL n) for e being Point of (Euclid n) st x = e holds cl_Ball (e,r) = cl_Ball (x,r) let x be Point of (TOP-REAL n); ::_thesis: for e being Point of (Euclid n) st x = e holds cl_Ball (e,r) = cl_Ball (x,r) let e be Point of (Euclid n); ::_thesis: ( x = e implies cl_Ball (e,r) = cl_Ball (x,r) ) assume A1: x = e ; ::_thesis: cl_Ball (e,r) = cl_Ball (x,r) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: cl_Ball (x,r) c= cl_Ball (e,r) let q be set ; ::_thesis: ( q in cl_Ball (e,r) implies q in cl_Ball (x,r) ) assume A2: q in cl_Ball (e,r) ; ::_thesis: q in cl_Ball (x,r) then reconsider f = q as Point of (Euclid n) ; reconsider p = f as Point of (TOP-REAL n) by TOPREAL3:8; dist (f,e) <= r by A2, METRIC_1:12; then |.(p - x).| <= r by A1, JGRAPH_1:28; hence q in cl_Ball (x,r) ; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in cl_Ball (x,r) or q in cl_Ball (e,r) ) assume A3: q in cl_Ball (x,r) ; ::_thesis: q in cl_Ball (e,r) then reconsider q = q as Point of (TOP-REAL n) ; reconsider f = q as Point of (Euclid n) by TOPREAL3:8; |.(q - x).| <= r by A3, Th8; then dist (f,e) <= r by A1, JGRAPH_1:28; hence q in cl_Ball (e,r) by METRIC_1:12; ::_thesis: verum end; theorem Th15: :: TOPREAL9:15 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) for e being Point of (Euclid n) st x = e holds Sphere (e,r) = Sphere (x,r) proof let n be Element of NAT ; ::_thesis: for r being real number for x being Point of (TOP-REAL n) for e being Point of (Euclid n) st x = e holds Sphere (e,r) = Sphere (x,r) let r be real number ; ::_thesis: for x being Point of (TOP-REAL n) for e being Point of (Euclid n) st x = e holds Sphere (e,r) = Sphere (x,r) let x be Point of (TOP-REAL n); ::_thesis: for e being Point of (Euclid n) st x = e holds Sphere (e,r) = Sphere (x,r) let e be Point of (Euclid n); ::_thesis: ( x = e implies Sphere (e,r) = Sphere (x,r) ) assume A1: x = e ; ::_thesis: Sphere (e,r) = Sphere (x,r) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Sphere (x,r) c= Sphere (e,r) let q be set ; ::_thesis: ( q in Sphere (e,r) implies q in Sphere (x,r) ) assume A2: q in Sphere (e,r) ; ::_thesis: q in Sphere (x,r) then reconsider f = q as Point of (Euclid n) ; reconsider p = f as Point of (TOP-REAL n) by TOPREAL3:8; dist (f,e) = r by A2, METRIC_1:13; then |.(p - x).| = r by A1, JGRAPH_1:28; hence q in Sphere (x,r) ; ::_thesis: verum end; let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Sphere (x,r) or q in Sphere (e,r) ) assume A3: q in Sphere (x,r) ; ::_thesis: q in Sphere (e,r) then reconsider q = q as Point of (TOP-REAL n) ; reconsider f = q as Point of (Euclid n) by TOPREAL3:8; |.(q - x).| = r by A3, Th9; then dist (f,e) = r by A1, JGRAPH_1:28; hence q in Sphere (e,r) by METRIC_1:13; ::_thesis: verum end; theorem :: TOPREAL9:16 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) holds Ball (x,r) c= cl_Ball (x,r) proof let n be Element of NAT ; ::_thesis: for r being real number for x being Point of (TOP-REAL n) holds Ball (x,r) c= cl_Ball (x,r) let r be real number ; ::_thesis: for x being Point of (TOP-REAL n) holds Ball (x,r) c= cl_Ball (x,r) let x be Point of (TOP-REAL n); ::_thesis: Ball (x,r) c= cl_Ball (x,r) reconsider e = x as Point of (Euclid n) by TOPREAL3:8; ( Ball (x,r) = Ball (e,r) & cl_Ball (x,r) = cl_Ball (e,r) ) by Th13, Th14; hence Ball (x,r) c= cl_Ball (x,r) by METRIC_1:14; ::_thesis: verum end; theorem Th17: :: TOPREAL9:17 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) holds Sphere (x,r) c= cl_Ball (x,r) proof let n be Element of NAT ; ::_thesis: for r being real number for x being Point of (TOP-REAL n) holds Sphere (x,r) c= cl_Ball (x,r) let r be real number ; ::_thesis: for x being Point of (TOP-REAL n) holds Sphere (x,r) c= cl_Ball (x,r) let x be Point of (TOP-REAL n); ::_thesis: Sphere (x,r) c= cl_Ball (x,r) reconsider e = x as Point of (Euclid n) by TOPREAL3:8; ( Sphere (x,r) = Sphere (e,r) & cl_Ball (x,r) = cl_Ball (e,r) ) by Th14, Th15; hence Sphere (x,r) c= cl_Ball (x,r) by METRIC_1:15; ::_thesis: verum end; theorem Th18: :: TOPREAL9:18 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) proof let n be Element of NAT ; ::_thesis: for r being real number for x being Point of (TOP-REAL n) holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) let r be real number ; ::_thesis: for x being Point of (TOP-REAL n) holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) let x be Point of (TOP-REAL n); ::_thesis: (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) reconsider e = x as Point of (Euclid n) by TOPREAL3:8; A1: cl_Ball (x,r) = cl_Ball (e,r) by Th14; ( Sphere (x,r) = Sphere (e,r) & Ball (x,r) = Ball (e,r) ) by Th13, Th15; hence (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) by A1, METRIC_1:16; ::_thesis: verum end; theorem Th19: :: TOPREAL9:19 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r) proof let n be Element of NAT ; ::_thesis: for r being real number for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r) let r be real number ; ::_thesis: for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r) let x be Point of (TOP-REAL n); ::_thesis: Ball (x,r) misses Sphere (x,r) assume not Ball (x,r) misses Sphere (x,r) ; ::_thesis: contradiction then consider q being set such that A1: q in Ball (x,r) and A2: q in Sphere (x,r) by XBOOLE_0:3; reconsider q = q as Point of (TOP-REAL n) by A1; |.(q - x).| = r by A2, Th9; hence contradiction by A1, Th7; ::_thesis: verum end; registration let n be Nat; let x be Point of (TOP-REAL n); let r be real non positive number ; cluster Ball (x,r) -> empty ; coherence Ball (x,r) is empty proof assume not Ball (x,r) is empty ; ::_thesis: contradiction then consider y being Point of (TOP-REAL n) such that A1: y in Ball (x,r) by SUBSET_1:4; n in NAT by ORDINAL1:def_12; then |.(y - x).| < r by A1, Th7; hence contradiction ; ::_thesis: verum end; end; registration let n be Nat; let x be Point of (TOP-REAL n); let r be real positive number ; cluster Ball (x,r) -> non empty ; coherence not Ball (x,r) is empty proof reconsider e = x as Point of (Euclid n) by TOPREAL3:8; n in NAT by ORDINAL1:def_12; then Ball (x,r) = Ball (e,r) by Th13; hence not Ball (x,r) is empty by GOBOARD6:1; ::_thesis: verum end; end; theorem :: TOPREAL9:20 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) st not Ball (x,r) is empty holds r > 0 ; theorem :: TOPREAL9:21 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) st Ball (x,r) is empty holds r <= 0 ; registration let n be Nat; let x be Point of (TOP-REAL n); let r be real negative number ; cluster cl_Ball (x,r) -> empty ; coherence cl_Ball (x,r) is empty proof assume not cl_Ball (x,r) is empty ; ::_thesis: contradiction then consider y being Point of (TOP-REAL n) such that A1: y in cl_Ball (x,r) by SUBSET_1:4; n in NAT by ORDINAL1:def_12; then |.(y - x).| <= r by A1, Th8; hence contradiction ; ::_thesis: verum end; end; registration let n be Nat; let x be Point of (TOP-REAL n); let r be real non negative number ; cluster cl_Ball (x,r) -> non empty ; coherence not cl_Ball (x,r) is empty proof A1: n in NAT by ORDINAL1:def_12; then |.(x - x).| = 0 by TOPRNS_1:28; hence not cl_Ball (x,r) is empty by A1, Th8; ::_thesis: verum end; end; theorem :: TOPREAL9:22 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) st not cl_Ball (x,r) is empty holds r >= 0 ; theorem :: TOPREAL9:23 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) st cl_Ball (x,r) is empty holds r < 0 ; theorem Th24: :: TOPREAL9:24 for n being Element of NAT for a, b, r being real number for x, z, y being Point of (TOP-REAL n) st a + b = 1 & (abs a) + (abs b) = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds (a * x) + (b * y) in Ball (z,r) proof let n be Element of NAT ; ::_thesis: for a, b, r being real number for x, z, y being Point of (TOP-REAL n) st a + b = 1 & (abs a) + (abs b) = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds (a * x) + (b * y) in Ball (z,r) let a, b, r be real number ; ::_thesis: for x, z, y being Point of (TOP-REAL n) st a + b = 1 & (abs a) + (abs b) = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) holds (a * x) + (b * y) in Ball (z,r) let x, z, y be Point of (TOP-REAL n); ::_thesis: ( a + b = 1 & (abs a) + (abs b) = 1 & b <> 0 & x in cl_Ball (z,r) & y in Ball (z,r) implies (a * x) + (b * y) in Ball (z,r) ) assume that A1: a + b = 1 and A2: (abs a) + (abs b) = 1 and A3: b <> 0 and A4: x in cl_Ball (z,r) and A5: y in Ball (z,r) ; ::_thesis: (a * x) + (b * y) in Ball (z,r) |.(y - z).| < r by A5, Th7; then A6: |.(z - y).| < r by TOPRNS_1:27; |.(x - z).| <= r by A4, Th8; then ( 0 <= abs a & |.(z - x).| <= r ) by COMPLEX1:46, TOPRNS_1:27; then A7: (abs a) * |.(z - x).| <= (abs a) * r by XREAL_1:64; 0 < abs b by A3, COMPLEX1:47; then (abs b) * |.(z - y).| < (abs b) * r by A6, XREAL_1:68; then ((abs a) * |.(z - x).|) + ((abs b) * |.(z - y).|) < ((abs a) * r) + ((abs b) * r) by A7, XREAL_1:8; then ( a is Real & ((abs a) * |.(z - x).|) + ((abs b) * |.(z - y).|) < ((abs a) + (abs b)) * r ) by XREAL_0:def_1; then ( b is Real & |.(a * (z - x)).| + ((abs b) * |.(z - y).|) < 1 * r ) by A2, TOPRNS_1:7, XREAL_0:def_1; then A8: |.(a * (z - x)).| + |.(b * (z - y)).| < r by TOPRNS_1:7; |.(((a * z) + (b * z)) - ((a * x) + (b * y))).| = |.(((a * z) - ((a * x) + (b * y))) + (b * z)).| by EUCLID:26 .= |.((((a * z) - (a * x)) - (b * y)) + (b * z)).| by EUCLID:46 .= |.((((a * z) - (a * x)) + (b * z)) - (b * y)).| by EUCLID:26 .= |.(((a * z) - (a * x)) + ((b * z) - (b * y))).| by EUCLID:45 .= |.((a * (z - x)) + ((b * z) - (b * y))).| by EUCLID:49 .= |.((a * (z - x)) + (b * (z - y))).| by EUCLID:49 ; then |.(((a * z) + (b * z)) - ((a * x) + (b * y))).| <= |.(a * (z - x)).| + |.(b * (z - y)).| by TOPRNS_1:29; then |.(((a * z) + (b * z)) - ((a * x) + (b * y))).| < r by A8, XXREAL_0:2; then A9: |.(((a * x) + (b * y)) - ((a * z) + (b * z))).| < r by TOPRNS_1:27; (a * z) + (b * z) = (a + b) * z by EUCLID:33 .= z by A1, EUCLID:29 ; hence (a * x) + (b * y) in Ball (z,r) by A9; ::_thesis: verum end; registration let n be Nat; let x be Point of (TOP-REAL n); let r be real number ; cluster Ball (x,r) -> open ; coherence Ball (x,r) is open proof reconsider e = x as Point of (Euclid n) by TOPREAL3:8; A1: ( r is Real & Ball (e,r) is bounded ) by XREAL_0:def_1; n in NAT by ORDINAL1:def_12; then Ball (e,r) = Ball (x,r) by Th13; hence Ball (x,r) is open by A1, GOBOARD6:3; ::_thesis: verum end; cluster cl_Ball (x,r) -> closed ; coherence cl_Ball (x,r) is closed proof reconsider e = x as Point of (Euclid n) by TOPREAL3:8; A2: n in NAT by ORDINAL1:def_12; then ( cl_Ball (e,r) is bounded & cl_Ball (e,r) = cl_Ball (x,r) ) by Th14, TOPREAL6:59; hence cl_Ball (x,r) is closed by A2, TOPREAL6:58; ::_thesis: verum end; cluster Sphere (x,r) -> closed ; coherence Sphere (x,r) is closed proof reconsider e = x as Point of (Euclid n) by TOPREAL3:8; A3: n in NAT by ORDINAL1:def_12; then ( Sphere (e,r) is bounded & Sphere (e,r) = Sphere (x,r) ) by Th15, TOPREAL6:62; hence Sphere (x,r) is closed by A3, TOPREAL6:61; ::_thesis: verum end; end; registration let n be Element of NAT ; let x be Point of (TOP-REAL n); let r be real number ; cluster Ball (x,r) -> bounded ; coherence Ball (x,r) is bounded proof reconsider e = x as Point of (Euclid n) by TOPREAL3:8; Ball (e,r) = Ball (x,r) by Th13; hence Ball (x,r) is bounded by JORDAN2C:11; ::_thesis: verum end; cluster cl_Ball (x,r) -> bounded ; coherence cl_Ball (x,r) is bounded proof reconsider e = x as Point of (Euclid n) by TOPREAL3:8; ( cl_Ball (e,r) is bounded & cl_Ball (e,r) = cl_Ball (x,r) ) by Th14, TOPREAL6:59; hence cl_Ball (x,r) is bounded by JORDAN2C:11; ::_thesis: verum end; cluster Sphere (x,r) -> bounded ; coherence Sphere (x,r) is bounded proof reconsider e = x as Point of (Euclid n) by TOPREAL3:8; ( Sphere (e,r) is bounded & Sphere (e,r) = Sphere (x,r) ) by Th15, TOPREAL6:62; hence Sphere (x,r) is bounded by JORDAN2C:11; ::_thesis: verum end; end; Lm1: for n being Element of NAT for a being real number for P being Subset of (TOP-REAL n) for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } holds P is convex proof let n be Element of NAT ; ::_thesis: for a being real number for P being Subset of (TOP-REAL n) for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } holds P is convex let a be real number ; ::_thesis: for P being Subset of (TOP-REAL n) for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } holds P is convex let P be Subset of (TOP-REAL n); ::_thesis: for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } holds P is convex let Q be Point of (TOP-REAL n); ::_thesis: ( P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } implies P is convex ) assume A1: P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a } ; ::_thesis: P is convex let p1, p2 be Point of (TOP-REAL n); :: according to JORDAN1:def_1 ::_thesis: ( not p1 in P or not p2 in P or LSeg (p1,p2) c= P ) assume p1 in P ; ::_thesis: ( not p2 in P or LSeg (p1,p2) c= P ) then A2: ex q1 being Point of (TOP-REAL n) st ( q1 = p1 & |.(q1 - Q).| <= a ) by A1; assume A3: p2 in P ; ::_thesis: LSeg (p1,p2) c= P then A4: ex q2 being Point of (TOP-REAL n) st ( q2 = p2 & |.(q2 - Q).| <= a ) by A1; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (p1,p2) or x in P ) assume A5: x in LSeg (p1,p2) ; ::_thesis: x in P then consider r being Real such that A6: x = ((1 - r) * p1) + (r * p2) and A7: 0 <= r and A8: r <= 1 ; A9: r = abs r by A7, ABSVALUE:def_1; reconsider q = x as Point of (TOP-REAL n) by A5; A10: |.((1 - r) * (p1 - Q)).| = (abs (1 - r)) * |.(p1 - Q).| by TOPRNS_1:7; A11: 1 - r >= 0 by A8, XREAL_1:48; then A12: abs (1 - r) = 1 - r by ABSVALUE:def_1; percases ( 1 - r > 0 or 1 - r <= 0 ) ; supposeA13: 1 - r > 0 ; ::_thesis: x in P 0 <= abs r by COMPLEX1:46; then A14: ( |.(r * (p2 - Q)).| = (abs r) * |.(p2 - Q).| & (abs r) * |.(p2 - Q).| <= (abs r) * a ) by A4, TOPRNS_1:7, XREAL_1:64; ((1 - r) * Q) + (r * Q) = ((1 * Q) - (r * Q)) + (r * Q) by EUCLID:50 .= 1 * Q by EUCLID:48 .= Q by EUCLID:29 ; then q - Q = ((((1 - r) * p1) + (r * p2)) - ((1 - r) * Q)) - (r * Q) by A6, EUCLID:46 .= ((((1 - r) * p1) - ((1 - r) * Q)) + (r * p2)) - (r * Q) by EUCLID:26 .= (((1 - r) * (p1 - Q)) + (r * p2)) - (r * Q) by EUCLID:49 .= ((1 - r) * (p1 - Q)) + ((r * p2) - (r * Q)) by EUCLID:45 .= ((1 - r) * (p1 - Q)) + (r * (p2 - Q)) by EUCLID:49 ; then A15: |.(q - Q).| <= |.((1 - r) * (p1 - Q)).| + |.(r * (p2 - Q)).| by TOPRNS_1:29; (abs (1 - r)) * |.(p1 - Q).| <= (abs (1 - r)) * a by A2, A12, A13, XREAL_1:64; then |.((1 - r) * (p1 - Q)).| + |.(r * (p2 - Q)).| <= ((1 - r) * a) + (r * a) by A9, A10, A12, A14, XREAL_1:7; then |.(q - Q).| <= a by A15, XXREAL_0:2; hence x in P by A1; ::_thesis: verum end; suppose 1 - r <= 0 ; ::_thesis: x in P then (1 - r) + r = 0 + r by A11; hence x in P by A3, A6, Th4; ::_thesis: verum end; end; end; Lm2: for n being Element of NAT for a being real number for P being Subset of (TOP-REAL n) for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } holds P is convex proof let n be Element of NAT ; ::_thesis: for a being real number for P being Subset of (TOP-REAL n) for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } holds P is convex let a be real number ; ::_thesis: for P being Subset of (TOP-REAL n) for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } holds P is convex let P be Subset of (TOP-REAL n); ::_thesis: for Q being Point of (TOP-REAL n) st P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } holds P is convex let Q be Point of (TOP-REAL n); ::_thesis: ( P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } implies P is convex ) assume A1: P = { q where q is Point of (TOP-REAL n) : |.(q - Q).| < a } ; ::_thesis: P is convex reconsider e = Q as Point of (Euclid n) by TOPREAL3:8; let p1, p2 be Point of (TOP-REAL n); :: according to JORDAN1:def_1 ::_thesis: ( not p1 in P or not p2 in P or LSeg (p1,p2) c= P ) assume A2: ( p1 in P & p2 in P ) ; ::_thesis: LSeg (p1,p2) c= P Ball (e,a) = Ball (Q,a) by Th13 .= P by A1 ; hence LSeg (p1,p2) c= P by A2, TOPREAL3:21; ::_thesis: verum end; registration let n be Nat; let x be Point of (TOP-REAL n); let r be real number ; cluster Ball (x,r) -> convex ; coherence Ball (x,r) is convex proof n in NAT by ORDINAL1:def_12; hence Ball (x,r) is convex by Lm2; ::_thesis: verum end; cluster cl_Ball (x,r) -> convex ; coherence cl_Ball (x,r) is convex proof n in NAT by ORDINAL1:def_12; hence cl_Ball (x,r) is convex by Lm1; ::_thesis: verum end; end; definition let n be Nat; let f be Function of (TOP-REAL n),(TOP-REAL n); attrf is homogeneous means :Def4: :: TOPREAL9:def 4 for r being real number for x being Point of (TOP-REAL n) holds f . (r * x) = r * (f . x); end; :: deftheorem Def4 defines homogeneous TOPREAL9:def_4_:_ for n being Nat for f being Function of (TOP-REAL n),(TOP-REAL n) holds ( f is homogeneous iff for r being real number for x being Point of (TOP-REAL n) holds f . (r * x) = r * (f . x) ); registration let n be Element of NAT ; cluster(TOP-REAL n) --> (0. (TOP-REAL n)) -> additive homogeneous ; coherence ( (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous & (TOP-REAL n) --> (0. (TOP-REAL n)) is additive ) proof set f = (TOP-REAL n) --> (0. (TOP-REAL n)); thus (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous ::_thesis: (TOP-REAL n) --> (0. (TOP-REAL n)) is additive proof let r be real number ; :: according to TOPREAL9:def_4 ::_thesis: for x being Point of (TOP-REAL n) holds ((TOP-REAL n) --> (0. (TOP-REAL n))) . (r * x) = r * (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) let x be Point of (TOP-REAL n); ::_thesis: ((TOP-REAL n) --> (0. (TOP-REAL n))) . (r * x) = r * (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) thus ((TOP-REAL n) --> (0. (TOP-REAL n))) . (r * x) = 0. (TOP-REAL n) by FUNCOP_1:7 .= r * (0. (TOP-REAL n)) by EUCLID:28 .= r * (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) by FUNCOP_1:7 ; ::_thesis: verum end; let x, y be Point of (TOP-REAL n); :: according to VECTSP_1:def_20 ::_thesis: ((TOP-REAL n) --> (0. (TOP-REAL n))) . K382((TOP-REAL n),x,y) = K382((TOP-REAL n),(((TOP-REAL n) --> (0. (TOP-REAL n))) . x),(((TOP-REAL n) --> (0. (TOP-REAL n))) . y)) thus ((TOP-REAL n) --> (0. (TOP-REAL n))) . (x + y) = 0. (TOP-REAL n) by FUNCOP_1:7 .= (0. (TOP-REAL n)) + (0. (TOP-REAL n)) by EUCLID:27 .= (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) + (0. (TOP-REAL n)) by FUNCOP_1:7 .= (((TOP-REAL n) --> (0. (TOP-REAL n))) . x) + (((TOP-REAL n) --> (0. (TOP-REAL n))) . y) by FUNCOP_1:7 ; ::_thesis: verum end; end; registration let n be Element of NAT ; clusterV16() V21() V30( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) continuous additive homogeneous for Element of K6(K7( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n))); existence ex b1 being Function of (TOP-REAL n),(TOP-REAL n) st ( b1 is homogeneous & b1 is additive & b1 is continuous ) proof take (TOP-REAL n) --> (0. (TOP-REAL n)) ; ::_thesis: ( (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous & (TOP-REAL n) --> (0. (TOP-REAL n)) is additive & (TOP-REAL n) --> (0. (TOP-REAL n)) is continuous ) thus ( (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous & (TOP-REAL n) --> (0. (TOP-REAL n)) is additive & (TOP-REAL n) --> (0. (TOP-REAL n)) is continuous ) ; ::_thesis: verum end; end; registration let a, c be real number ; cluster AffineMap (a,0,c,0) -> additive homogeneous ; coherence ( AffineMap (a,0,c,0) is homogeneous & AffineMap (a,0,c,0) is additive ) proof set f = AffineMap (a,0,c,0); hereby :: according to TOPREAL9:def_4 ::_thesis: AffineMap (a,0,c,0) is additive let r be real number ; ::_thesis: for x being Point of (TOP-REAL 2) holds (AffineMap (a,0,c,0)) . (r * x) = r * ((AffineMap (a,0,c,0)) . x) let x be Point of (TOP-REAL 2); ::_thesis: (AffineMap (a,0,c,0)) . (r * x) = r * ((AffineMap (a,0,c,0)) . x) A1: ( (r * x) `1 = r * (x `1) & (r * x) `2 = r * (x `2) ) by TOPREAL3:4; thus (AffineMap (a,0,c,0)) . (r * x) = |[((a * ((r * x) `1)) + 0),((c * ((r * x) `2)) + 0)]| by JGRAPH_2:def_2 .= |[(r * (a * (x `1))),(r * (c * (x `2)))]| by A1 .= r * |[((a * (x `1)) + 0),((c * (x `2)) + 0)]| by EUCLID:58 .= r * ((AffineMap (a,0,c,0)) . x) by JGRAPH_2:def_2 ; ::_thesis: verum end; let x, y be Point of (TOP-REAL 2); :: according to VECTSP_1:def_20 ::_thesis: (AffineMap (a,0,c,0)) . K382((TOP-REAL 2),x,y) = K382((TOP-REAL 2),((AffineMap (a,0,c,0)) . x),((AffineMap (a,0,c,0)) . y)) A2: ( (x + y) `1 = (x `1) + (y `1) & (x + y) `2 = (x `2) + (y `2) ) by TOPREAL3:2; thus (AffineMap (a,0,c,0)) . (x + y) = |[((a * ((x + y) `1)) + 0),((c * ((x + y) `2)) + 0)]| by JGRAPH_2:def_2 .= |[((a * (x `1)) + (a * (y `1))),((c * (x `2)) + (c * (y `2)))]| by A2 .= |[((a * (x `1)) + 0),((c * (x `2)) + 0)]| + |[(a * (y `1)),(c * (y `2))]| by EUCLID:56 .= ((AffineMap (a,0,c,0)) . x) + |[((a * (y `1)) + 0),((c * (y `2)) + 0)]| by JGRAPH_2:def_2 .= ((AffineMap (a,0,c,0)) . x) + ((AffineMap (a,0,c,0)) . y) by JGRAPH_2:def_2 ; ::_thesis: verum end; end; theorem :: TOPREAL9:25 for n being Element of NAT for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) for X being convex Subset of (TOP-REAL n) holds f .: X is convex proof let n be Element of NAT ; ::_thesis: for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) for X being convex Subset of (TOP-REAL n) holds f .: X is convex let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); ::_thesis: for X being convex Subset of (TOP-REAL n) holds f .: X is convex let X be convex Subset of (TOP-REAL n); ::_thesis: f .: X is convex let p, q be Point of (TOP-REAL n); :: according to JORDAN1:def_1 ::_thesis: ( not p in f .: X or not q in f .: X or LSeg (p,q) c= f .: X ) assume p in f .: X ; ::_thesis: ( not q in f .: X or LSeg (p,q) c= f .: X ) then consider p0 being Point of (TOP-REAL n) such that A1: p0 in X and A2: p = f . p0 by FUNCT_2:65; assume q in f .: X ; ::_thesis: LSeg (p,q) c= f .: X then consider q0 being Point of (TOP-REAL n) such that A3: q0 in X and A4: q = f . q0 by FUNCT_2:65; A5: LSeg (p0,q0) c= X by A1, A3, JORDAN1:def_1; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (p,q) or x in f .: X ) assume x in LSeg (p,q) ; ::_thesis: x in f .: X then consider l being Real such that A6: x = ((1 - l) * p) + (l * q) and A7: ( 0 <= l & l <= 1 ) ; set a = ((1 - l) * p0) + (l * q0); A8: ((1 - l) * p0) + (l * q0) in LSeg (p0,q0) by A7; f . (((1 - l) * p0) + (l * q0)) = (f . ((1 - l) * p0)) + (f . (l * q0)) by VECTSP_1:def_20 .= (f . ((1 - l) * p0)) + (l * (f . q0)) by Def4 .= x by A2, A4, A6, Def4 ; hence x in f .: X by A8, A5, FUNCT_2:35; ::_thesis: verum end; definition let n be Nat; let p, q be Point of (TOP-REAL n); func halfline (p,q) -> Subset of (TOP-REAL n) equals :: TOPREAL9:def 5 { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ; coherence { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } is Subset of (TOP-REAL n) proof set X = { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ; { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } c= the carrier of (TOP-REAL n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } or x in the carrier of (TOP-REAL n) ) assume x in { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ; ::_thesis: x in the carrier of (TOP-REAL n) then ex l being Real st ( x = ((1 - l) * p) + (l * q) & 0 <= l ) ; hence x in the carrier of (TOP-REAL n) ; ::_thesis: verum end; hence { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } is Subset of (TOP-REAL n) ; ::_thesis: verum end; end; :: deftheorem defines halfline TOPREAL9:def_5_:_ for n being Nat for p, q being Point of (TOP-REAL n) holds halfline (p,q) = { (((1 - l) * p) + (l * q)) where l is Real : 0 <= l } ; theorem Th26: :: TOPREAL9:26 for n being Element of NAT for p, q being Point of (TOP-REAL n) for x being set holds ( x in halfline (p,q) iff ex l being real number st ( x = ((1 - l) * p) + (l * q) & 0 <= l ) ) proof let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) for x being set holds ( x in halfline (p,q) iff ex l being real number st ( x = ((1 - l) * p) + (l * q) & 0 <= l ) ) let p, q be Point of (TOP-REAL n); ::_thesis: for x being set holds ( x in halfline (p,q) iff ex l being real number st ( x = ((1 - l) * p) + (l * q) & 0 <= l ) ) let x be set ; ::_thesis: ( x in halfline (p,q) iff ex l being real number st ( x = ((1 - l) * p) + (l * q) & 0 <= l ) ) hereby ::_thesis: ( ex l being real number st ( x = ((1 - l) * p) + (l * q) & 0 <= l ) implies x in halfline (p,q) ) assume x in halfline (p,q) ; ::_thesis: ex l being real number st ( x = ((1 - l) * p) + (l * q) & 0 <= l ) then ex l being Real st ( x = ((1 - l) * p) + (l * q) & 0 <= l ) ; hence ex l being real number st ( x = ((1 - l) * p) + (l * q) & 0 <= l ) ; ::_thesis: verum end; given l being real number such that A1: ( x = ((1 - l) * p) + (l * q) & 0 <= l ) ; ::_thesis: x in halfline (p,q) l is Real by XREAL_0:def_1; hence x in halfline (p,q) by A1; ::_thesis: verum end; registration let n be Element of NAT ; let p, q be Point of (TOP-REAL n); cluster halfline (p,q) -> non empty ; coherence not halfline (p,q) is empty proof ((1 - 0) * p) + (0 * q) in halfline (p,q) ; hence not halfline (p,q) is empty ; ::_thesis: verum end; end; theorem Th27: :: TOPREAL9:27 for n being Element of NAT for p, q being Point of (TOP-REAL n) holds p in halfline (p,q) proof let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) holds p in halfline (p,q) let p, q be Point of (TOP-REAL n); ::_thesis: p in halfline (p,q) ((1 - 0) * p) + (0 * q) = p + (0 * q) by EUCLID:29 .= p + (0. (TOP-REAL n)) by EUCLID:29 .= p by EUCLID:27 ; hence p in halfline (p,q) ; ::_thesis: verum end; theorem Th28: :: TOPREAL9:28 for n being Element of NAT for q, p being Point of (TOP-REAL n) holds q in halfline (p,q) proof let n be Element of NAT ; ::_thesis: for q, p being Point of (TOP-REAL n) holds q in halfline (p,q) let q, p be Point of (TOP-REAL n); ::_thesis: q in halfline (p,q) ((1 - 1) * p) + (1 * q) = (0 * p) + q by EUCLID:29 .= (0. (TOP-REAL n)) + q by EUCLID:29 .= q by EUCLID:27 ; hence q in halfline (p,q) ; ::_thesis: verum end; theorem Th29: :: TOPREAL9:29 for n being Element of NAT for p being Point of (TOP-REAL n) holds halfline (p,p) = {p} proof let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL n) holds halfline (p,p) = {p} let p be Point of (TOP-REAL n); ::_thesis: halfline (p,p) = {p} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {p} c= halfline (p,p) let d be set ; ::_thesis: ( d in halfline (p,p) implies d in {p} ) assume d in halfline (p,p) ; ::_thesis: d in {p} then ex r being real number st ( d = ((1 - r) * p) + (r * p) & 0 <= r ) by Th26; then d = p by Th4; hence d in {p} by TARSKI:def_1; ::_thesis: verum end; let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in {p} or d in halfline (p,p) ) assume d in {p} ; ::_thesis: d in halfline (p,p) then d = p by TARSKI:def_1; hence d in halfline (p,p) by Th27; ::_thesis: verum end; theorem Th30: :: TOPREAL9:30 for n being Element of NAT for x, p, q being Point of (TOP-REAL n) st x in halfline (p,q) holds halfline (p,x) c= halfline (p,q) proof let n be Element of NAT ; ::_thesis: for x, p, q being Point of (TOP-REAL n) st x in halfline (p,q) holds halfline (p,x) c= halfline (p,q) let x, p, q be Point of (TOP-REAL n); ::_thesis: ( x in halfline (p,q) implies halfline (p,x) c= halfline (p,q) ) assume x in halfline (p,q) ; ::_thesis: halfline (p,x) c= halfline (p,q) then consider R being real number such that A1: x = ((1 - R) * p) + (R * q) and A2: 0 <= R by Th26; let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in halfline (p,x) or d in halfline (p,q) ) assume A3: d in halfline (p,x) ; ::_thesis: d in halfline (p,q) then reconsider d = d as Point of (TOP-REAL n) ; consider r being real number such that A4: d = ((1 - r) * p) + (r * x) and A5: 0 <= r by A3, Th26; set o = r * R; d = ((1 - r) * p) + ((r * ((1 - R) * p)) + (r * (R * q))) by A1, A4, EUCLID:32 .= (((1 - r) * p) + (r * ((1 - R) * p))) + (r * (R * q)) by EUCLID:26 .= (((1 - r) * p) + ((r * (1 - R)) * p)) + (r * (R * q)) by EUCLID:30 .= (((1 - r) + (r * (1 - R))) * p) + (r * (R * q)) by EUCLID:33 .= ((1 - (r * R)) * p) + ((r * R) * q) by EUCLID:30 ; hence d in halfline (p,q) by A2, A5, Th26; ::_thesis: verum end; theorem :: TOPREAL9:31 for n being Element of NAT for x, p, q being Point of (TOP-REAL n) st x in halfline (p,q) & x <> p holds halfline (p,q) = halfline (p,x) proof let n be Element of NAT ; ::_thesis: for x, p, q being Point of (TOP-REAL n) st x in halfline (p,q) & x <> p holds halfline (p,q) = halfline (p,x) let x, p, q be Point of (TOP-REAL n); ::_thesis: ( x in halfline (p,q) & x <> p implies halfline (p,q) = halfline (p,x) ) assume A1: x in halfline (p,q) ; ::_thesis: ( not x <> p or halfline (p,q) = halfline (p,x) ) then consider R being real number such that A2: x = ((1 - R) * p) + (R * q) and A3: 0 <= R by Th26; assume A4: x <> p ; ::_thesis: halfline (p,q) = halfline (p,x) thus halfline (p,q) c= halfline (p,x) :: according to XBOOLE_0:def_10 ::_thesis: halfline (p,x) c= halfline (p,q) proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in halfline (p,q) or d in halfline (p,x) ) assume A5: d in halfline (p,q) ; ::_thesis: d in halfline (p,x) then reconsider d = d as Point of (TOP-REAL n) ; consider r being real number such that A6: d = ((1 - r) * p) + (r * q) and A7: 0 <= r by A5, Th26; set o = r / R; R <> 0 by A2, A4, Th4; then (r / R) * R = r by XCMPLX_1:87; then d = (((1 - (r / R)) + ((r / R) * (1 - R))) * p) + ((r / R) * (R * q)) by A6, EUCLID:30 .= (((1 - (r / R)) * p) + (((r / R) * (1 - R)) * p)) + ((r / R) * (R * q)) by EUCLID:33 .= (((1 - (r / R)) * p) + ((r / R) * ((1 - R) * p))) + ((r / R) * (R * q)) by EUCLID:30 .= ((1 - (r / R)) * p) + (((r / R) * ((1 - R) * p)) + ((r / R) * (R * q))) by EUCLID:26 .= ((1 - (r / R)) * p) + ((r / R) * (((1 - R) * p) + (R * q))) by EUCLID:32 ; hence d in halfline (p,x) by A2, A3, A7, Th26; ::_thesis: verum end; thus halfline (p,x) c= halfline (p,q) by A1, Th30; ::_thesis: verum end; theorem :: TOPREAL9:32 for n being Element of NAT for p, q being Point of (TOP-REAL n) holds LSeg (p,q) c= halfline (p,q) proof let n be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL n) holds LSeg (p,q) c= halfline (p,q) let p, q be Point of (TOP-REAL n); ::_thesis: LSeg (p,q) c= halfline (p,q) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (p,q) or a in halfline (p,q) ) assume a in LSeg (p,q) ; ::_thesis: a in halfline (p,q) then ex r being Real st ( 0 <= r & r <= 1 & a = ((1 - r) * p) + (r * q) ) by JGRAPH_1:35; hence a in halfline (p,q) ; ::_thesis: verum end; registration let n be Element of NAT ; let p, q be Point of (TOP-REAL n); cluster halfline (p,q) -> convex ; coherence halfline (p,q) is convex proof let u, v be Point of (TOP-REAL n); :: according to JORDAN1:def_1 ::_thesis: ( not u in halfline (p,q) or not v in halfline (p,q) or LSeg (u,v) c= halfline (p,q) ) set P = halfline (p,q); assume u in halfline (p,q) ; ::_thesis: ( not v in halfline (p,q) or LSeg (u,v) c= halfline (p,q) ) then consider a being real number such that A1: u = ((1 - a) * p) + (a * q) and A2: 0 <= a by Th26; assume v in halfline (p,q) ; ::_thesis: LSeg (u,v) c= halfline (p,q) then consider b being real number such that A3: v = ((1 - b) * p) + (b * q) and A4: 0 <= b by Th26; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (u,v) or x in halfline (p,q) ) assume x in LSeg (u,v) ; ::_thesis: x in halfline (p,q) then consider r being Real such that A5: 0 <= r and A6: r <= 1 and A7: x = ((1 - r) * u) + (r * v) by JGRAPH_1:35; set o = ((1 - r) * a) + (r * b); A8: 1 - r >= r - r by A6, XREAL_1:13; x = (((1 - r) * ((1 - a) * p)) + ((1 - r) * (a * q))) + (r * (((1 - b) * p) + (b * q))) by A1, A3, A7, EUCLID:32 .= (((1 - r) * ((1 - a) * p)) + ((1 - r) * (a * q))) + ((r * ((1 - b) * p)) + (r * (b * q))) by EUCLID:32 .= (((1 - r) * ((1 - a) * p)) + ((r * ((1 - b) * p)) + (r * (b * q)))) + ((1 - r) * (a * q)) by EUCLID:26 .= ((((1 - r) * ((1 - a) * p)) + (r * ((1 - b) * p))) + (r * (b * q))) + ((1 - r) * (a * q)) by EUCLID:26 .= (((((1 - r) * (1 - a)) * p) + (r * ((1 - b) * p))) + (r * (b * q))) + ((1 - r) * (a * q)) by EUCLID:30 .= (((((1 - r) * (1 - a)) * p) + ((r * (1 - b)) * p)) + (r * (b * q))) + ((1 - r) * (a * q)) by EUCLID:30 .= (((((1 - r) * (1 - a)) * p) + ((r * (1 - b)) * p)) + ((r * b) * q)) + ((1 - r) * (a * q)) by EUCLID:30 .= (((((1 - r) * (1 - a)) * p) + ((r * (1 - b)) * p)) + ((r * b) * q)) + (((1 - r) * a) * q) by EUCLID:30 .= (((((1 - r) * (1 - a)) + (r * (1 - b))) * p) + ((r * b) * q)) + (((1 - r) * a) * q) by EUCLID:33 .= ((((1 - r) * (1 - a)) + (r * (1 - b))) * p) + (((r * b) * q) + (((1 - r) * a) * q)) by EUCLID:26 .= ((1 - (((1 - r) * a) + (r * b))) * p) + ((((1 - r) * a) + (r * b)) * q) by EUCLID:33 ; hence x in halfline (p,q) by A2, A4, A5, A8; ::_thesis: verum end; end; theorem Th33: :: TOPREAL9:33 for n being Element of NAT for r being real number for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Ball (x,r) holds (LSeg (y,z)) /\ (Sphere (x,r)) = {y} proof let n be Element of NAT ; ::_thesis: for r being real number for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Ball (x,r) holds (LSeg (y,z)) /\ (Sphere (x,r)) = {y} let r be real number ; ::_thesis: for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Ball (x,r) holds (LSeg (y,z)) /\ (Sphere (x,r)) = {y} let y, x, z be Point of (TOP-REAL n); ::_thesis: ( y in Sphere (x,r) & z in Ball (x,r) implies (LSeg (y,z)) /\ (Sphere (x,r)) = {y} ) set s = y; set t = z; assume that A1: y in Sphere (x,r) and A2: z in Ball (x,r) ; ::_thesis: (LSeg (y,z)) /\ (Sphere (x,r)) = {y} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {y} c= (LSeg (y,z)) /\ (Sphere (x,r)) let m be set ; ::_thesis: ( m in (LSeg (y,z)) /\ (Sphere (x,r)) implies b1 in {y} ) assume A3: m in (LSeg (y,z)) /\ (Sphere (x,r)) ; ::_thesis: b1 in {y} then reconsider w = m as Point of (TOP-REAL n) ; w in LSeg (y,z) by A3, XBOOLE_0:def_4; then consider d being Real such that A4: 0 <= d and A5: d <= 1 and A6: w = ((1 - d) * y) + (d * z) by JGRAPH_1:35; A7: |.(d * (z - x)).| = (abs d) * |.(z - x).| by TOPRNS_1:7 .= d * |.(z - x).| by A4, ABSVALUE:def_1 ; d - 1 <= 1 - 1 by A5, XREAL_1:9; then A8: - 0 <= - (d - 1) ; A9: |.((1 - d) * (y - x)).| = (abs (1 - d)) * |.(y - x).| by TOPRNS_1:7 .= (1 - d) * |.(y - x).| by A8, ABSVALUE:def_1 .= (1 - d) * r by A1, Th9 ; m in Sphere (x,r) by A3, XBOOLE_0:def_4; then A10: r = |.(w - x).| by Th9 .= |.((((1 - d) * y) + (d * z)) - (((1 - d) + d) * x)).| by A6, EUCLID:29 .= |.((((1 - d) * y) + (d * z)) - (((1 - d) * x) + (d * x))).| by EUCLID:33 .= |.(((((1 - d) * y) + (d * z)) - ((1 - d) * x)) - (d * x)).| by EUCLID:46 .= |.(((((1 - d) * y) - ((1 - d) * x)) + (d * z)) - (d * x)).| by EUCLID:26 .= |.((((1 - d) * (y - x)) + (d * z)) - (d * x)).| by EUCLID:49 .= |.(((1 - d) * (y - x)) + ((d * z) - (d * x))).| by EUCLID:45 .= |.(((1 - d) * (y - x)) + (d * (z - x))).| by EUCLID:49 ; percases ( d > 0 or d = 0 ) by A4; supposeA11: d > 0 ; ::_thesis: b1 in {y} |.(z - x).| < r by A2, Th7; then d * |.(z - x).| < d * r by A11, XREAL_1:68; then ((1 - d) * r) + (d * |.(z - x).|) < ((1 - d) * r) + (d * r) by XREAL_1:8; hence m in {y} by A10, A9, A7, TOPRNS_1:29; ::_thesis: verum end; suppose d = 0 ; ::_thesis: b1 in {y} then m = (1 * y) + (0. (TOP-REAL n)) by A6, EUCLID:29 .= 1 * y by EUCLID:27 .= y by EUCLID:29 ; hence m in {y} by TARSKI:def_1; ::_thesis: verum end; end; end; let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in {y} or m in (LSeg (y,z)) /\ (Sphere (x,r)) ) A12: y in LSeg (y,z) by RLTOPSP1:68; assume m in {y} ; ::_thesis: m in (LSeg (y,z)) /\ (Sphere (x,r)) then m = y by TARSKI:def_1; hence m in (LSeg (y,z)) /\ (Sphere (x,r)) by A1, A12, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th34: :: TOPREAL9:34 for n being Element of NAT for r being real number for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds (LSeg (y,z)) \ {y,z} c= Ball (x,r) proof let n be Element of NAT ; ::_thesis: for r being real number for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds (LSeg (y,z)) \ {y,z} c= Ball (x,r) let r be real number ; ::_thesis: for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds (LSeg (y,z)) \ {y,z} c= Ball (x,r) let y, x, z be Point of (TOP-REAL n); ::_thesis: ( y in Sphere (x,r) & z in Sphere (x,r) implies (LSeg (y,z)) \ {y,z} c= Ball (x,r) ) assume that A1: y in Sphere (x,r) and A2: z in Sphere (x,r) ; ::_thesis: (LSeg (y,z)) \ {y,z} c= Ball (x,r) percases ( y = z or y <> z ) ; suppose y = z ; ::_thesis: (LSeg (y,z)) \ {y,z} c= Ball (x,r) then ( LSeg (y,z) = {y} & {y,z} = {y} ) by ENUMSET1:29, RLTOPSP1:70; then (LSeg (y,z)) \ {y,z} = {} by XBOOLE_1:37; hence (LSeg (y,z)) \ {y,z} c= Ball (x,r) by XBOOLE_1:2; ::_thesis: verum end; supposeA3: y <> z ; ::_thesis: (LSeg (y,z)) \ {y,z} c= Ball (x,r) the carrier of (TOP-REAL n) = REAL n by EUCLID:22 .= n -tuples_on REAL ; then reconsider xf = x, yf = y, zf = z as Element of n -tuples_on REAL ; reconsider yyf = yf, zzf = zf, xxf = xf as Element of REAL n ; reconsider y1 = y - x, z1 = z - x as FinSequence of REAL ; set X = |((y - x),(z - x))|; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (LSeg (y,z)) \ {y,z} or a in Ball (x,r) ) A4: Sum (sqr (zf - xf)) = |.z1.| ^2 by Th5; A5: |.(z - x).| ^2 = r ^2 by A2, Th9; assume A6: a in (LSeg (y,z)) \ {y,z} ; ::_thesis: a in Ball (x,r) then reconsider R = a as Point of (TOP-REAL n) ; A7: R in LSeg (y,z) by A6, XBOOLE_0:def_5; then consider l being Real such that A8: 0 <= l and A9: l <= 1 and A10: R = ((1 - l) * y) + (l * z) by JGRAPH_1:35; set l1 = 1 - l; reconsider W1 = (1 - l) * (y - x), W2 = l * (z - x) as Element of REAL n by EUCLID:22; A11: Sum (sqr (yf - zf)) >= 0 by RVSUM_1:86; reconsider Rf = R - x as FinSequence of REAL ; A12: W1 + W2 = (((1 - l) * y) - ((1 - l) * x)) + (l * (z - x)) by EUCLID:49 .= (((1 - l) * y) - ((1 - l) * x)) + ((l * z) - (l * x)) by EUCLID:49 .= ((((1 - l) * y) - ((1 - l) * x)) + (l * z)) - (l * x) by EUCLID:45 .= ((((1 - l) * y) + (l * z)) - ((1 - l) * x)) - (l * x) by EUCLID:26 .= (((1 - l) * y) + (l * z)) - (((1 - l) * x) + (l * x)) by EUCLID:46 .= (((1 - l) * y) + (l * z)) - (((1 * x) - (l * x)) + (l * x)) by EUCLID:50 .= (((1 - l) * y) + (l * z)) - (1 * x) by EUCLID:48 .= Rf by A10, EUCLID:29 ; reconsider W1 = W1, W2 = W2 as Element of n -tuples_on REAL ; A13: mlt (W1,W2) = (1 - l) * (mlt ((yf - xf),(l * (zf - xf)))) by RVSUM_1:65; A14: sqr W1 = ((1 - l) ^2) * (sqr (yf - xf)) by RVSUM_1:58; Sum (sqr Rf) >= 0 by RVSUM_1:86; then |.(R - x).| ^2 = Sum (sqr Rf) by SQUARE_1:def_2 .= Sum (((sqr W1) + (2 * (mlt (W1,W2)))) + (sqr W2)) by A12, RVSUM_1:68 .= (Sum ((sqr W1) + (2 * (mlt (W1,W2))))) + (Sum (sqr W2)) by RVSUM_1:89 .= ((Sum (sqr W1)) + (Sum (2 * (mlt (W1,W2))))) + (Sum (sqr W2)) by RVSUM_1:89 .= ((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + (Sum (sqr (l * (zf - xf)))) by RVSUM_1:87, A14 .= ((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + (Sum ((l ^2) * (sqr (zf - xf)))) by RVSUM_1:58 .= ((((1 - l) ^2) * (Sum (sqr (yf - xf)))) + (Sum (2 * (mlt (W1,W2))))) + ((l ^2) * (Sum (sqr (zf - xf)))) by RVSUM_1:87 .= ((((1 - l) ^2) * (|.y1.| ^2)) + (Sum (2 * (mlt (W1,W2))))) + ((l ^2) * (Sum (sqr (zf - xf)))) by Th5 .= ((((1 - l) ^2) * (r ^2)) + (Sum (2 * (mlt (W1,W2))))) + ((l ^2) * (|.z1.| ^2)) by A1, A4, Th9 .= ((((1 - l) ^2) * (r ^2)) + (2 * (Sum (mlt (W1,W2))))) + ((l ^2) * (r ^2)) by A5, RVSUM_1:87 .= ((((1 - l) ^2) * (r ^2)) + (2 * (Sum ((1 - l) * (l * (mlt ((yf - xf),(zf - xf)))))))) + ((l ^2) * (r ^2)) by RVSUM_1:65, A13 .= ((((1 - l) ^2) * (r ^2)) + (2 * (Sum (((1 - l) * l) * (mlt ((yf - xf),(zf - xf))))))) + ((l ^2) * (r ^2)) by RVSUM_1:49 .= ((((1 - l) ^2) * (r ^2)) + (2 * (((1 - l) * l) * (Sum (mlt ((yf - xf),(zf - xf))))))) + ((l ^2) * (r ^2)) by RVSUM_1:87 .= ((((1 - l) ^2) * (r ^2)) + (((2 * (1 - l)) * l) * (Sum (mlt ((yf - xf),(zf - xf)))))) + ((l ^2) * (r ^2)) .= ((((1 - l) ^2) * (r ^2)) + (((2 * (1 - l)) * l) * |((y - x),(z - x))|)) + ((l ^2) * (r ^2)) by RVSUM_1:def_16 .= ((((1 - (2 * l)) + (l ^2)) + (l ^2)) * (r ^2)) + (((2 * l) * (1 - l)) * |((y - x),(z - x))|) ; then A15: (|.(R - x).| ^2) - (r ^2) = ((2 * l) * (1 - l)) * ((- (r ^2)) + |((y - x),(z - x))|) ; now__::_thesis:_not_l_=_0 assume l = 0 ; ::_thesis: contradiction then R = y by A10, Th4; then R in {y,z} by TARSKI:def_2; hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum end; then A16: 2 * l > 0 by A8, XREAL_1:129; A17: now__::_thesis:_not_1_-_l_=_0 assume 1 - l = 0 ; ::_thesis: contradiction then R = z by A10, Th4; then R in {y,z} by TARSKI:def_2; hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum end; 1 - 1 <= 1 - l by A9, XREAL_1:13; then A18: (2 * l) * (1 - l) > 0 by A16, A17, XREAL_1:129; A19: |.(y - x).| ^2 = r ^2 by A1, Th9; A20: now__::_thesis:_not_|.(R_-_x).|_=_r assume |.(R - x).| = r ; ::_thesis: contradiction then |((y - x),(z - x))| - (r ^2) = 0 by A15, A18, XCMPLX_1:6; then 0 = ((|.(y - x).| ^2) - (2 * |((y - x),(z - x))|)) + (|.(z - x).| ^2) by A2, A19, Th9 .= |.((y - x) - (z - x)).| ^2 by EUCLID_2:46 .= |.(((y - x) - z) + x).| ^2 by EUCLID:47 .= |.(((y - x) + x) - z).| ^2 by EUCLID:26 .= |.(yf - zf).| ^2 by EUCLID:48 .= Sum (sqr (yf - zf)) by A11, SQUARE_1:def_2 ; then yf - zf = n |-> 0 by RVSUM_1:91; hence contradiction by A3, RVSUM_1:38; ::_thesis: verum end; Sphere (x,r) c= cl_Ball (x,r) by Th17; then LSeg (y,z) c= cl_Ball (x,r) by A1, A2, JORDAN1:def_1; then |.(R - x).| <= r by A7, Th8; then |.(R - x).| < r by A20, XXREAL_0:1; hence a in Ball (x,r) ; ::_thesis: verum end; end; end; theorem Th35: :: TOPREAL9:35 for n being Element of NAT for r being real number for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds (LSeg (y,z)) /\ (Sphere (x,r)) = {y,z} proof let n be Element of NAT ; ::_thesis: for r being real number for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds (LSeg (y,z)) /\ (Sphere (x,r)) = {y,z} let r be real number ; ::_thesis: for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds (LSeg (y,z)) /\ (Sphere (x,r)) = {y,z} let y, x, z be Point of (TOP-REAL n); ::_thesis: ( y in Sphere (x,r) & z in Sphere (x,r) implies (LSeg (y,z)) /\ (Sphere (x,r)) = {y,z} ) A1: ( y in LSeg (y,z) & z in LSeg (y,z) ) by RLTOPSP1:68; assume A2: ( y in Sphere (x,r) & z in Sphere (x,r) ) ; ::_thesis: (LSeg (y,z)) /\ (Sphere (x,r)) = {y,z} then A3: (LSeg (y,z)) \ {y,z} c= Ball (x,r) by Th34; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {y,z} c= (LSeg (y,z)) /\ (Sphere (x,r)) let a be set ; ::_thesis: ( a in (LSeg (y,z)) /\ (Sphere (x,r)) implies a in {y,z} ) assume A4: a in (LSeg (y,z)) /\ (Sphere (x,r)) ; ::_thesis: a in {y,z} assume A5: not a in {y,z} ; ::_thesis: contradiction a in LSeg (y,z) by A4, XBOOLE_0:def_4; then A6: a in (LSeg (y,z)) \ {y,z} by A5, XBOOLE_0:def_5; A7: Ball (x,r) misses Sphere (x,r) by Th19; a in Sphere (x,r) by A4, XBOOLE_0:def_4; hence contradiction by A3, A6, A7, XBOOLE_0:3; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {y,z} or a in (LSeg (y,z)) /\ (Sphere (x,r)) ) assume a in {y,z} ; ::_thesis: a in (LSeg (y,z)) /\ (Sphere (x,r)) then ( a = y or a = z ) by TARSKI:def_2; hence a in (LSeg (y,z)) /\ (Sphere (x,r)) by A2, A1, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th36: :: TOPREAL9:36 for n being Element of NAT for r being real number for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds (halfline (y,z)) /\ (Sphere (x,r)) = {y,z} proof let n be Element of NAT ; ::_thesis: for r being real number for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds (halfline (y,z)) /\ (Sphere (x,r)) = {y,z} let r be real number ; ::_thesis: for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) & z in Sphere (x,r) holds (halfline (y,z)) /\ (Sphere (x,r)) = {y,z} let y, x, z be Point of (TOP-REAL n); ::_thesis: ( y in Sphere (x,r) & z in Sphere (x,r) implies (halfline (y,z)) /\ (Sphere (x,r)) = {y,z} ) assume that A1: y in Sphere (x,r) and A2: z in Sphere (x,r) ; ::_thesis: (halfline (y,z)) /\ (Sphere (x,r)) = {y,z} percases ( y = z or y <> z ) ; supposeA3: y = z ; ::_thesis: (halfline (y,z)) /\ (Sphere (x,r)) = {y,z} then A4: {y,z} = {y} by ENUMSET1:29; A5: halfline (y,z) = {y} by A3, Th29; hence for m being set st m in (halfline (y,z)) /\ (Sphere (x,r)) holds m in {y,z} by A4, XBOOLE_0:def_4; :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {y,z} c= (halfline (y,z)) /\ (Sphere (x,r)) let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in {y,z} or m in (halfline (y,z)) /\ (Sphere (x,r)) ) assume A6: m in {y,z} ; ::_thesis: m in (halfline (y,z)) /\ (Sphere (x,r)) then m = y by A4, TARSKI:def_1; hence m in (halfline (y,z)) /\ (Sphere (x,r)) by A1, A5, A4, A6, XBOOLE_0:def_4; ::_thesis: verum end; supposeA7: y <> z ; ::_thesis: (halfline (y,z)) /\ (Sphere (x,r)) = {y,z} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {y,z} c= (halfline (y,z)) /\ (Sphere (x,r)) let m be set ; ::_thesis: ( m in (halfline (y,z)) /\ (Sphere (x,r)) implies b1 in {y,z} ) assume A8: m in (halfline (y,z)) /\ (Sphere (x,r)) ; ::_thesis: b1 in {y,z} then A9: m in Sphere (x,r) by XBOOLE_0:def_4; reconsider w = m as Point of (TOP-REAL n) by A8; m in halfline (y,z) by A8, XBOOLE_0:def_4; then consider R being real number such that A10: m = ((1 - R) * y) + (R * z) and A11: 0 <= R by Th26; reconsider R = R as Real by XREAL_0:def_1; percases ( R = 0 or R = 1 or ( R > 0 & R < 1 ) or R > 1 ) by A11, XXREAL_0:1; suppose R = 0 ; ::_thesis: b1 in {y,z} then m = y by A10, Th4; hence m in {y,z} by TARSKI:def_2; ::_thesis: verum end; suppose R = 1 ; ::_thesis: b1 in {y,z} then m = z by A10, Th4; hence m in {y,z} by TARSKI:def_2; ::_thesis: verum end; supposeA12: ( R > 0 & R < 1 ) ; ::_thesis: b1 in {y,z} A13: now__::_thesis:_not_m_in_{y,z} assume m in {y,z} ; ::_thesis: contradiction then ( m = y or m = z ) by TARSKI:def_2; hence contradiction by A7, A10, A12, Th4; ::_thesis: verum end; w in LSeg (y,z) by A10, A12; then A14: m in (LSeg (y,z)) \ {y,z} by A13, XBOOLE_0:def_5; (LSeg (y,z)) \ {y,z} c= Ball (x,r) by A1, A2, Th34; then |.(w - x).| < r by A14, Th7; hence m in {y,z} by A9, Th9; ::_thesis: verum end; supposeA15: R > 1 ; ::_thesis: b1 in {y,z} then A16: 1 / R < 1 by XREAL_1:212; A17: ((1 - (1 / R)) * y) + ((1 / R) * w) = ((1 - (1 / R)) * y) + (((1 / R) * ((1 - R) * y)) + ((1 / R) * (R * z))) by A10, EUCLID:32 .= ((1 - (1 / R)) * y) + (((1 / R) * ((1 - R) * y)) + (((1 / R) * R) * z)) by EUCLID:30 .= ((1 - (1 / R)) * y) + (((1 / R) * ((1 - R) * y)) + (1 * z)) by A15, XCMPLX_1:87 .= ((1 - (1 / R)) * y) + (((1 / R) * ((1 - R) * y)) + z) by EUCLID:29 .= (((1 - (1 / R)) * y) + ((1 / R) * ((1 - R) * y))) + z by EUCLID:26 .= (((1 - (1 / R)) * y) + (((1 / R) * (1 - R)) * y)) + z by EUCLID:30 .= (((1 - (1 / R)) + ((1 / R) * (1 - R))) * y) + z by EUCLID:33 .= ((((1 - (1 / R)) + ((1 / R) * 1)) - ((1 / R) * R)) * y) + z .= ((((1 - (1 / R)) + ((1 / R) * 1)) - 1) * y) + z by A15, XCMPLX_1:87 .= (0. (TOP-REAL n)) + z by EUCLID:29 .= z by EUCLID:27 ; A18: now__::_thesis:_not_z_in_{y,w} assume z in {y,w} ; ::_thesis: contradiction then ( z = y or z = w ) by TARSKI:def_2; hence contradiction by A7, A16, A17, Th4; ::_thesis: verum end; z in LSeg (y,w) by A15, A16, A17; then A19: z in (LSeg (y,w)) \ {y,w} by A18, XBOOLE_0:def_5; (LSeg (y,w)) \ {y,w} c= Ball (x,r) by A1, A9, Th34; then |.(z - x).| < r by A19, Th7; hence m in {y,z} by A2, Th9; ::_thesis: verum end; end; end; let m be set ; :: according to TARSKI:def_3 ::_thesis: ( not m in {y,z} or m in (halfline (y,z)) /\ (Sphere (x,r)) ) assume m in {y,z} ; ::_thesis: m in (halfline (y,z)) /\ (Sphere (x,r)) then A20: ( m = y or m = z ) by TARSKI:def_2; ( y in halfline (y,z) & z in halfline (y,z) ) by Th27, Th28; hence m in (halfline (y,z)) /\ (Sphere (x,r)) by A1, A2, A20, XBOOLE_0:def_4; ::_thesis: verum end; end; end; theorem Th37: :: TOPREAL9:37 for n being Element of NAT for r, a being real number for y, z, x being Point of (TOP-REAL n) for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds ex e being Point of (TOP-REAL n) st ( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) proof let n be Element of NAT ; ::_thesis: for r, a being real number for y, z, x being Point of (TOP-REAL n) for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds ex e being Point of (TOP-REAL n) st ( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) let r, a be real number ; ::_thesis: for y, z, x being Point of (TOP-REAL n) for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds ex e being Point of (TOP-REAL n) st ( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) let y, z, x be Point of (TOP-REAL n); ::_thesis: for S, T, X being Element of REAL n st S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds ex e being Point of (TOP-REAL n) st ( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) let S, T, X be Element of REAL n; ::_thesis: ( S = y & T = z & X = x & y <> z & y in Ball (x,r) & a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies ex e being Point of (TOP-REAL n) st ( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) ) assume that A1: S = y and A2: T = z and A3: X = x ; ::_thesis: ( not y <> z or not y in Ball (x,r) or not a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or ex e being Point of (TOP-REAL n) st ( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) ) set s = y; set t = z; A4: Sum (sqr (T - S)) >= 0 by RVSUM_1:86; then A5: |.(T - S).| ^2 = Sum (sqr (T - S)) by SQUARE_1:def_2; set A = Sum (sqr (T - S)); assume that A6: y <> z and A7: y in Ball (x,r) and A8: a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; ::_thesis: ex e being Point of (TOP-REAL n) st ( {e} = (halfline (y,z)) /\ (Sphere (x,r)) & e = ((1 - a) * y) + (a * z) ) A9: |.(T - S).| <> 0 by A1, A2, A6, EUCLID:16; A10: now__::_thesis:_not_Sum_(sqr_(T_-_S))_<=_0 assume Sum (sqr (T - S)) <= 0 ; ::_thesis: contradiction then Sum (sqr (T - S)) = 0 by RVSUM_1:86; hence contradiction by A9, SQUARE_1:17; ::_thesis: verum end; set C = (Sum (sqr (S - X))) - (r ^2); set B = 2 * |((z - y),(y - x))|; A11: ( r = 0 or r <> 0 ) ; Sum (sqr (S - X)) >= 0 by RVSUM_1:86; then A12: |.(S - X).| ^2 = Sum (sqr (S - X)) by SQUARE_1:def_2; |.(y - x).| < r by A7, Th7; then (sqrt (Sum (sqr (S - X)))) ^2 < r ^2 by A1, A3, SQUARE_1:16; then A13: (Sum (sqr (S - X))) - (r ^2) < 0 by A12, XREAL_1:49; then A14: ((Sum (sqr (S - X))) - (r ^2)) / (Sum (sqr (T - S))) < 0 by A10, XREAL_1:141; set l2 = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))); set l1 = ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))); take e1 = ((1 - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * y) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z); ::_thesis: ( {e1} = (halfline (y,z)) /\ (Sphere (x,r)) & e1 = ((1 - a) * y) + (a * z) ) A15: 0 <= - (- r) by A7; A16: ( delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2))) = ((2 * |((z - y),(y - x))|) ^2) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - X))) - (r ^2))) & (2 * |((z - y),(y - x))|) ^2 >= 0 ) by QUIN_1:def_1, XREAL_1:63; A17: for x being real number holds Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x) proof let x be real number ; ::_thesis: Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x) thus Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),x) = (((Sum (sqr (T - S))) * (x ^2)) + ((2 * |((z - y),(y - x))|) * x)) + ((Sum (sqr (S - X))) - (r ^2)) by POLYEQ_1:def_2 .= ((Sum (sqr (T - S))) * (x - (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) * (x - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) by A10, A13, A16, QUIN_1:16 .= (Sum (sqr (T - S))) * ((x - (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (x - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) .= Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x) by POLYEQ_1:def_3 ; ::_thesis: verum end; then ((Sum (sqr (S - X))) - (r ^2)) / (Sum (sqr (T - S))) = (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) by A10, POLYEQ_1:11; then A18: ( ( ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) < 0 & ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > 0 ) or ( ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > 0 & ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) < 0 ) ) by A14, XREAL_1:133; A19: (((Sum (sqr (T - S))) * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2)) + ((2 * |((z - y),(y - x))|) * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) - (- ((Sum (sqr (S - X))) - (r ^2))) = Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) by POLYEQ_1:def_2 .= Quard ((Sum (sqr (T - S))),(((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) by A17 .= (Sum (sqr (T - S))) * (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) - (((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) - (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) by POLYEQ_1:def_3 .= 0 ; |.(e1 - x).| ^2 = |.((((1 * y) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y)) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z)) - x).| ^2 by EUCLID:50 .= |.(((y - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y)) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z)) - x).| ^2 by EUCLID:29 .= |.(((y + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z)) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y)) - x).| ^2 by EUCLID:26 .= |.((y + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y))) - x).| ^2 by EUCLID:45 .= |.((y - x) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z) - ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * y))).| ^2 by EUCLID:26 .= |.((y - x) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y))).| ^2 by EUCLID:49 .= ((|.(y - x).| ^2) + (2 * |(((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y)),(y - x))|)) + (|.((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y)).| ^2) by EUCLID_2:45 .= ((Sum (sqr (S - X))) + (2 * ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * |((z - y),(y - x))|))) + (|.((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (z - y)).| ^2) by A12, A1, A3, EUCLID_2:19 .= ((Sum (sqr (S - X))) + ((2 * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * |((z - y),(y - x))|)) + (((abs (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * |.(z - y).|) ^2) by TOPRNS_1:7 .= ((Sum (sqr (S - X))) + ((2 * (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * |((z - y),(y - x))|)) + (((abs (((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) ^2) * (|.(z - y).| ^2)) .= ((Sum (sqr (S - X))) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (|.(T - S).| ^2)) by A1, A2, COMPLEX1:75 .= ((Sum (sqr (S - X))) + ((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (2 * |((z - y),(y - x))|))) + (((((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) ^2) * (Sum (sqr (T - S)))) by A4, SQUARE_1:def_2 .= r ^2 by A19 ; then ( |.(e1 - x).| = r or |.(e1 - x).| = - r ) by SQUARE_1:40; then A20: e1 in Sphere (x,r) by A15, A11; A21: (4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - X))) - (r ^2)) < 0 by A10, A13, XREAL_1:129, XREAL_1:132; then A22: e1 in halfline (y,z) by A10, A16, A18, QUIN_1:25; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ( (halfline (y,z)) /\ (Sphere (x,r)) c= {e1} & e1 = ((1 - a) * y) + (a * z) ) let d be set ; ::_thesis: ( d in {e1} implies d in (halfline (y,z)) /\ (Sphere (x,r)) ) assume d in {e1} ; ::_thesis: d in (halfline (y,z)) /\ (Sphere (x,r)) then d = e1 by TARSKI:def_1; hence d in (halfline (y,z)) /\ (Sphere (x,r)) by A22, A20, XBOOLE_0:def_4; ::_thesis: verum end; hereby :: according to TARSKI:def_3 ::_thesis: e1 = ((1 - a) * y) + (a * z) let d be set ; ::_thesis: ( d in (halfline (y,z)) /\ (Sphere (x,r)) implies d in {e1} ) assume A23: d in (halfline (y,z)) /\ (Sphere (x,r)) ; ::_thesis: d in {e1} then d in halfline (y,z) by XBOOLE_0:def_4; then consider l being real number such that A24: d = ((1 - l) * y) + (l * z) and A25: 0 <= l by Th26; l is Real by XREAL_0:def_1; then A26: |.(l * (z - y)).| ^2 = ((abs l) * |.(z - y).|) ^2 by TOPRNS_1:7 .= ((abs l) ^2) * (|.(z - y).| ^2) .= (l ^2) * (|.(z - y).| ^2) by COMPLEX1:75 ; d in Sphere (x,r) by A23, XBOOLE_0:def_4; then r = |.((((1 - l) * y) + (l * z)) - x).| by A24, Th9 .= |.((((1 * y) - (l * y)) + (l * z)) - x).| by EUCLID:50 .= |.(((y - (l * y)) + (l * z)) - x).| by EUCLID:29 .= |.((y - ((l * y) - (l * z))) - x).| by EUCLID:47 .= |.((y + (- ((l * y) - (l * z)))) + (- x)).| .= |.((y + (- x)) + (- ((l * y) - (l * z)))).| by EUCLID:26 .= |.((y - x) - ((l * y) - (l * z))).| .= |.((y + (- x)) + (- ((l * y) - (l * z)))).| .= |.((y - x) + (- (l * (y - z)))).| by EUCLID:49 .= |.((y - x) + (l * (- (y - z)))).| by EUCLID:40 .= |.((y - x) + (l * (z - y))).| by EUCLID:44 ; then r ^2 = ((|.(y - x).| ^2) + (2 * |((l * (z - y)),(y - x))|)) + (|.(l * (z - y)).| ^2) by EUCLID_2:45 .= ((|.(y - x).| ^2) + (2 * (l * |((z - y),(y - x))|))) + (|.(l * (z - y)).| ^2) by EUCLID_2:19 ; then (((Sum (sqr (T - S))) * (l ^2)) + ((2 * |((z - y),(y - x))|) * l)) + ((Sum (sqr (S - X))) - (r ^2)) = 0 by A5, A12, A1, A3, A2, A26; then Polynom ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)),l) = 0 by POLYEQ_1:def_2; then ( l = ((- (2 * |((z - y),(y - x))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or l = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ) by A10, A13, A16, POLYEQ_1:5; hence d in {e1} by A10, A21, A16, A18, A24, A25, QUIN_1:25, TARSKI:def_1; ::_thesis: verum end; thus e1 = ((1 - a) * y) + (a * z) by A8; ::_thesis: verum end; theorem Th38: :: TOPREAL9:38 for n being Element of NAT for r, a being real number for y, z, x being Point of (TOP-REAL n) for S, T, Y being Element of REAL n st S = ((1 / 2) * y) + ((1 / 2) * z) & T = z & Y = x & y <> z & y in Sphere (x,r) & z in cl_Ball (x,r) holds ex e being Point of (TOP-REAL n) st ( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) proof let n be Element of NAT ; ::_thesis: for r, a being real number for y, z, x being Point of (TOP-REAL n) for S, T, Y being Element of REAL n st S = ((1 / 2) * y) + ((1 / 2) * z) & T = z & Y = x & y <> z & y in Sphere (x,r) & z in cl_Ball (x,r) holds ex e being Point of (TOP-REAL n) st ( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) let r, a be real number ; ::_thesis: for y, z, x being Point of (TOP-REAL n) for S, T, Y being Element of REAL n st S = ((1 / 2) * y) + ((1 / 2) * z) & T = z & Y = x & y <> z & y in Sphere (x,r) & z in cl_Ball (x,r) holds ex e being Point of (TOP-REAL n) st ( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) let y, z, x be Point of (TOP-REAL n); ::_thesis: for S, T, Y being Element of REAL n st S = ((1 / 2) * y) + ((1 / 2) * z) & T = z & Y = x & y <> z & y in Sphere (x,r) & z in cl_Ball (x,r) holds ex e being Point of (TOP-REAL n) st ( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) let S, T, Y be Element of REAL n; ::_thesis: ( S = ((1 / 2) * y) + ((1 / 2) * z) & T = z & Y = x & y <> z & y in Sphere (x,r) & z in cl_Ball (x,r) implies ex e being Point of (TOP-REAL n) st ( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) ) assume A1: ( S = ((1 / 2) * y) + ((1 / 2) * z) & T = z & Y = x ) ; ::_thesis: ( not y <> z or not y in Sphere (x,r) or not z in cl_Ball (x,r) or ex e being Point of (TOP-REAL n) st ( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) ) reconsider G = x as Point of (Euclid n) by TOPREAL3:8; set s = y; set t = z; set X = ((1 / 2) * y) + ((1 / 2) * z); assume that A2: y <> z and A3: y in Sphere (x,r) and A4: z in cl_Ball (x,r) ; ::_thesis: ex e being Point of (TOP-REAL n) st ( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) A5: Ball (G,r) = Ball (x,r) by Th13; A6: Sphere (x,r) c= cl_Ball (x,r) by Th17; percases ( z in Sphere (x,r) or not z in Sphere (x,r) ) ; supposeA7: z in Sphere (x,r) ; ::_thesis: ex e being Point of (TOP-REAL n) st ( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) take z ; ::_thesis: ( z <> y & {y,z} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies z = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies z = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) thus ( z <> y & {y,z} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies z = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies z = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) by A2, A3, A7, Th36; ::_thesis: verum end; supposeA8: not z in Sphere (x,r) ; ::_thesis: ex e being Point of (TOP-REAL n) st ( e <> y & {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) A9: now__::_thesis:_not_((1_/_2)_*_y)_+_((1_/_2)_*_z)_=_z assume A10: ((1 / 2) * y) + ((1 / 2) * z) = z ; ::_thesis: contradiction (z + (- ((1 / 2) * y))) + (- ((1 / 2) * z)) = (z - ((1 / 2) * y)) - ((1 / 2) * z) .= z - z by EUCLID:46, A10 .= 0. (TOP-REAL n) by EUCLID:42 ; then 0. (TOP-REAL n) = (z + (- ((1 / 2) * z))) + (- ((1 / 2) * y)) by EUCLID:26 .= ((1 * z) - ((1 / 2) * z)) - ((1 / 2) * y) by EUCLID:29 .= ((1 - (1 / 2)) * z) - ((1 / 2) * y) by EUCLID:50 .= (1 / 2) * (z - y) by EUCLID:49 ; then z - y = 0. (TOP-REAL n) by EUCLID:31; hence contradiction by A2, EUCLID:43; ::_thesis: verum end; (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r) by Th18; then A11: z in Ball (G,r) by A4, A5, A8, XBOOLE_0:def_3; set a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))); A12: ( (1 / 2) + (1 / 2) = 1 & abs (1 / 2) = 1 / 2 ) by ABSVALUE:def_1; Ball (G,r) = Ball (x,r) by Th13; then ((1 / 2) * y) + ((1 / 2) * z) in Ball (G,r) by A3, A6, A12, A11, Th24; then consider e1 being Point of (TOP-REAL n) such that A13: {e1} = (halfline ((((1 / 2) * y) + ((1 / 2) * z)),z)) /\ (Sphere (x,r)) and A14: e1 = ((1 - (((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (((1 / 2) * y) + ((1 / 2) * z))) + ((((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * z) by A1, A5, A9, Th37; take e1 ; ::_thesis: ( e1 <> y & {y,e1} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e1 = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e1 = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) A15: e1 in {e1} by TARSKI:def_1; then e1 in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) by A13, XBOOLE_0:def_4; then consider l being real number such that A16: e1 = ((1 - l) * (((1 / 2) * y) + ((1 / 2) * z))) + (l * z) and A17: 0 <= l by Th26; hereby ::_thesis: ( {y,e1} = (halfline (y,z)) /\ (Sphere (x,r)) & ( z in Sphere (x,r) implies e1 = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e1 = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) assume e1 = y ; ::_thesis: contradiction then 0. (TOP-REAL n) = (((1 - l) * (((1 / 2) * y) + ((1 / 2) * z))) + (l * z)) - y by A16, EUCLID:42 .= ((((1 - l) * ((1 / 2) * y)) + ((1 - l) * ((1 / 2) * z))) + (l * z)) - y by EUCLID:32 .= (((1 - l) * ((1 / 2) * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z))) - y by EUCLID:26 .= (((1 - l) * ((1 / 2) * y)) - y) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:26 .= (((1 - l) * ((1 / 2) * y)) - (1 * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:29 .= ((((1 - l) * (1 / 2)) * y) - (1 * y)) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:30 .= ((((1 - l) * (1 / 2)) - 1) * y) + (((1 - l) * ((1 / 2) * z)) + (l * z)) by EUCLID:50 .= (((- (1 / 2)) - (l * (1 / 2))) * y) + ((((1 - l) * (1 / 2)) * z) + (l * z)) by EUCLID:30 .= (((- (1 / 2)) - (l * (1 / 2))) * y) + ((((1 - l) * (1 / 2)) + l) * z) by EUCLID:33 .= ((- ((1 / 2) + (l * (1 / 2)))) * y) + (((1 / 2) + (l * (1 / 2))) * z) .= (((1 / 2) + (l * (1 / 2))) * z) - (((1 / 2) + (l * (1 / 2))) * y) by EUCLID:40 .= ((1 / 2) + (l * (1 / 2))) * (z - y) by EUCLID:49 ; then ( (1 / 2) + (l * (1 / 2)) = 0 or z - y = 0. (TOP-REAL n) ) by EUCLID:31; hence contradiction by A2, A17, EUCLID:43; ::_thesis: verum end; A18: y in halfline (y,z) by Th27; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ( (halfline (y,z)) /\ (Sphere (x,r)) c= {y,e1} & ( z in Sphere (x,r) implies e1 = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e1 = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) set o = (1 + l) / 2; let m be set ; ::_thesis: ( m in {y,e1} implies m in (halfline (y,z)) /\ (Sphere (x,r)) ) assume m in {y,e1} ; ::_thesis: m in (halfline (y,z)) /\ (Sphere (x,r)) then A19: ( m = y or m = e1 ) by TARSKI:def_2; e1 = (((1 - l) * ((1 / 2) * y)) + ((1 - l) * ((1 / 2) * z))) + (l * z) by A16, EUCLID:32 .= ((((1 - l) * (1 / 2)) * y) + ((1 - l) * ((1 / 2) * z))) + (l * z) by EUCLID:30 .= ((((1 - l) * (1 / 2)) * y) + (((1 - l) * (1 / 2)) * z)) + (l * z) by EUCLID:30 .= (((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) * z) + (l * z)) by EUCLID:26 .= (((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) + l) * z) by EUCLID:33 .= ((1 - ((1 + l) / 2)) * y) + (((1 + l) / 2) * z) ; then A20: e1 in halfline (y,z) by A17; e1 in Sphere (x,r) by A13, A15, XBOOLE_0:def_4; hence m in (halfline (y,z)) /\ (Sphere (x,r)) by A3, A18, A19, A20, XBOOLE_0:def_4; ::_thesis: verum end; hereby :: according to TARSKI:def_3 ::_thesis: ( ( z in Sphere (x,r) implies e1 = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e1 = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) let m be set ; ::_thesis: ( m in (halfline (y,z)) /\ (Sphere (x,r)) implies b1 in {y,e1} ) assume A21: m in (halfline (y,z)) /\ (Sphere (x,r)) ; ::_thesis: b1 in {y,e1} then A22: m in halfline (y,z) by XBOOLE_0:def_4; A23: m in Sphere (x,r) by A21, XBOOLE_0:def_4; percases ( m in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) or not m in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) ) ; suppose m in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) ; ::_thesis: b1 in {y,e1} then m in (halfline ((((1 / 2) * y) + ((1 / 2) * z)),z)) /\ (Sphere (x,r)) by A23, XBOOLE_0:def_4; then m = e1 by A13, TARSKI:def_1; hence m in {y,e1} by TARSKI:def_2; ::_thesis: verum end; supposeA24: not m in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) ; ::_thesis: b1 in {y,e1} consider M being real number such that A25: m = ((1 - M) * y) + (M * z) and A26: 0 <= M by A22, Th26; A27: now__::_thesis:_not_M_>_1 set o = (2 * M) - 1; assume M > 1 ; ::_thesis: contradiction then 2 * M > 2 * 1 by XREAL_1:68; then A28: (2 * M) - 1 > (2 * 1) - 1 by XREAL_1:14; ((1 - ((2 * M) - 1)) * (((1 / 2) * y) + ((1 / 2) * z))) + (((2 * M) - 1) * z) = (((1 - ((2 * M) - 1)) * ((1 / 2) * y)) + ((1 - ((2 * M) - 1)) * ((1 / 2) * z))) + (((2 * M) - 1) * z) by EUCLID:32 .= ((((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((1 - ((2 * M) - 1)) * ((1 / 2) * z))) + (((2 * M) - 1) * z) by EUCLID:30 .= ((((1 - ((2 * M) - 1)) * (1 / 2)) * y) + (((1 - ((2 * M) - 1)) * (1 / 2)) * z)) + (((2 * M) - 1) * z) by EUCLID:30 .= (((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((((1 - ((2 * M) - 1)) * (1 / 2)) * z) + (((2 * M) - 1) * z)) by EUCLID:26 .= (((1 - ((2 * M) - 1)) * (1 / 2)) * y) + ((((1 - ((2 * M) - 1)) * (1 / 2)) + ((2 * M) - 1)) * z) by EUCLID:33 .= m by A25 ; hence contradiction by A24, A28; ::_thesis: verum end; ( |.(z - x).| <= r & |.(z - x).| <> r ) by A4, A8, Th8; then |.(z - x).| < r by XXREAL_0:1; then z in Ball (x,r) ; then A29: (LSeg (y,z)) /\ (Sphere (x,r)) = {y} by A3, Th33; M is Real by XREAL_0:def_1; then m in LSeg (y,z) by A25, A26, A27; then m in {y} by A23, A29, XBOOLE_0:def_4; then m = y by TARSKI:def_1; hence m in {y,e1} by TARSKI:def_2; ::_thesis: verum end; end; end; thus ( ( z in Sphere (x,r) implies e1 = z ) & ( not z in Sphere (x,r) & a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e1 = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) ) by A8, A14; ::_thesis: verum end; end; end; registration let n be Nat; let x be Point of (TOP-REAL n); let r be real negative number ; cluster Sphere (x,r) -> empty ; coherence Sphere (x,r) is empty proof assume not Sphere (x,r) is empty ; ::_thesis: contradiction then consider y being Point of (TOP-REAL n) such that A1: y in Sphere (x,r) by SUBSET_1:4; n in NAT by ORDINAL1:def_12; then |.(y - x).| = r by A1, Th9; hence contradiction ; ::_thesis: verum end; end; registration let n be non empty Nat; let x be Point of (TOP-REAL n); let r be real non negative number ; cluster Sphere (x,r) -> non empty ; coherence not Sphere (x,r) is empty proof A1: n in NAT by ORDINAL1:def_12; reconsider e = x as Point of (Euclid n) by TOPREAL3:8; percases ( r = 0 or r > 0 ) ; suppose r = 0 ; ::_thesis: not Sphere (x,r) is empty then Sphere (e,r) = {e} by TOPREAL6:54; hence not Sphere (x,r) is empty by A1, Th15; ::_thesis: verum end; suppose r > 0 ; ::_thesis: not Sphere (x,r) is empty then reconsider r = r as real positive number ; consider s being Point of (TOP-REAL n) such that A2: s in Ball (x,r) by SUBSET_1:4; reconsider S = s, T = s + (1.REAL n), XX = x as Element of REAL n by EUCLID:22; set a = ((- (2 * |(((s + (1.REAL n)) - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |(((s + (1.REAL n)) - s),(s - x))|),((Sum (sqr (S - XX))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))); s <> s + (1.REAL n) by A1, Th3; then ex e being Point of (TOP-REAL n) st ( {e} = (halfline (s,(s + (1.REAL n)))) /\ (Sphere (x,r)) & e = ((1 - (((- (2 * |(((s + (1.REAL n)) - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |(((s + (1.REAL n)) - s),(s - x))|),((Sum (sqr (S - XX))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * s) + ((((- (2 * |(((s + (1.REAL n)) - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |(((s + (1.REAL n)) - s),(s - x))|),((Sum (sqr (S - XX))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (s + (1.REAL n))) ) by A1, A2, Th37; hence not Sphere (x,r) is empty ; ::_thesis: verum end; end; end; end; theorem :: TOPREAL9:39 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) st not Sphere (x,r) is empty holds r >= 0 ; theorem :: TOPREAL9:40 for n being Element of NAT for r being real number for x being Point of (TOP-REAL n) st not n is empty & Sphere (x,r) is empty holds r < 0 ; begin theorem :: TOPREAL9:41 for a, b being real number for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `1 = (a * (s `1)) + (b * (t `1)) proof let a, b be real number ; ::_thesis: for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `1 = (a * (s `1)) + (b * (t `1)) let s, t be Point of (TOP-REAL 2); ::_thesis: ((a * s) + (b * t)) `1 = (a * (s `1)) + (b * (t `1)) thus ((a * s) + (b * t)) `1 = ((a * s) `1) + ((b * t) `1) by TOPREAL3:2 .= (a * (s `1)) + ((b * t) `1) by TOPREAL3:4 .= (a * (s `1)) + (b * (t `1)) by TOPREAL3:4 ; ::_thesis: verum end; theorem :: TOPREAL9:42 for a, b being real number for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `2 = (a * (s `2)) + (b * (t `2)) proof let a, b be real number ; ::_thesis: for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `2 = (a * (s `2)) + (b * (t `2)) let s, t be Point of (TOP-REAL 2); ::_thesis: ((a * s) + (b * t)) `2 = (a * (s `2)) + (b * (t `2)) thus ((a * s) + (b * t)) `2 = ((a * s) `2) + ((b * t) `2) by TOPREAL3:2 .= (a * (s `2)) + ((b * t) `2) by TOPREAL3:4 .= (a * (s `2)) + (b * (t `2)) by TOPREAL3:4 ; ::_thesis: verum end; theorem Th43: :: TOPREAL9:43 for a, b, r being real number for t being Point of (TOP-REAL 2) holds ( t in circle (a,b,r) iff |.(t - |[a,b]|).| = r ) proof let a, b, r be real number ; ::_thesis: for t being Point of (TOP-REAL 2) holds ( t in circle (a,b,r) iff |.(t - |[a,b]|).| = r ) let t be Point of (TOP-REAL 2); ::_thesis: ( t in circle (a,b,r) iff |.(t - |[a,b]|).| = r ) A1: circle (a,b,r) = { x where x is Point of (TOP-REAL 2) : |.(x - |[a,b]|).| = r } by JGRAPH_6:def_5; hereby ::_thesis: ( |.(t - |[a,b]|).| = r implies t in circle (a,b,r) ) assume t in circle (a,b,r) ; ::_thesis: |.(t - |[a,b]|).| = r then ex x being Point of (TOP-REAL 2) st ( t = x & |.(x - |[a,b]|).| = r ) by A1; hence |.(t - |[a,b]|).| = r ; ::_thesis: verum end; thus ( |.(t - |[a,b]|).| = r implies t in circle (a,b,r) ) by A1; ::_thesis: verum end; theorem Th44: :: TOPREAL9:44 for a, b, r being real number for t being Point of (TOP-REAL 2) holds ( t in closed_inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| <= r ) proof let a, b, r be real number ; ::_thesis: for t being Point of (TOP-REAL 2) holds ( t in closed_inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| <= r ) let t be Point of (TOP-REAL 2); ::_thesis: ( t in closed_inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| <= r ) A1: closed_inside_of_circle (a,b,r) = { x where x is Point of (TOP-REAL 2) : |.(x - |[a,b]|).| <= r } by JGRAPH_6:def_7; hereby ::_thesis: ( |.(t - |[a,b]|).| <= r implies t in closed_inside_of_circle (a,b,r) ) assume t in closed_inside_of_circle (a,b,r) ; ::_thesis: |.(t - |[a,b]|).| <= r then ex x being Point of (TOP-REAL 2) st ( t = x & |.(x - |[a,b]|).| <= r ) by A1; hence |.(t - |[a,b]|).| <= r ; ::_thesis: verum end; thus ( |.(t - |[a,b]|).| <= r implies t in closed_inside_of_circle (a,b,r) ) by A1; ::_thesis: verum end; theorem Th45: :: TOPREAL9:45 for a, b, r being real number for t being Point of (TOP-REAL 2) holds ( t in inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| < r ) proof let a, b, r be real number ; ::_thesis: for t being Point of (TOP-REAL 2) holds ( t in inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| < r ) let t be Point of (TOP-REAL 2); ::_thesis: ( t in inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| < r ) A1: inside_of_circle (a,b,r) = { x where x is Point of (TOP-REAL 2) : |.(x - |[a,b]|).| < r } by JGRAPH_6:def_6; hereby ::_thesis: ( |.(t - |[a,b]|).| < r implies t in inside_of_circle (a,b,r) ) assume t in inside_of_circle (a,b,r) ; ::_thesis: |.(t - |[a,b]|).| < r then ex x being Point of (TOP-REAL 2) st ( t = x & |.(x - |[a,b]|).| < r ) by A1; hence |.(t - |[a,b]|).| < r ; ::_thesis: verum end; thus ( |.(t - |[a,b]|).| < r implies t in inside_of_circle (a,b,r) ) by A1; ::_thesis: verum end; registration let a, b be real number ; let r be real positive number ; cluster inside_of_circle (a,b,r) -> non empty ; coherence not inside_of_circle (a,b,r) is empty proof |.(|[a,b]| - |[a,b]|).| = 0 by TOPRNS_1:28; hence not inside_of_circle (a,b,r) is empty by Th45; ::_thesis: verum end; end; registration let a, b be real number ; let r be real non negative number ; cluster closed_inside_of_circle (a,b,r) -> non empty ; coherence not closed_inside_of_circle (a,b,r) is empty proof |.(|[a,b]| - |[a,b]|).| = 0 by TOPRNS_1:28; hence not closed_inside_of_circle (a,b,r) is empty by Th44; ::_thesis: verum end; end; theorem :: TOPREAL9:46 for a, b, r being real number holds circle (a,b,r) c= closed_inside_of_circle (a,b,r) proof let a, b, r be real number ; ::_thesis: circle (a,b,r) c= closed_inside_of_circle (a,b,r) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in circle (a,b,r) or x in closed_inside_of_circle (a,b,r) ) assume A1: x in circle (a,b,r) ; ::_thesis: x in closed_inside_of_circle (a,b,r) then reconsider x = x as Point of (TOP-REAL 2) ; |.(x - |[a,b]|).| = r by A1, Th43; hence x in closed_inside_of_circle (a,b,r) by Th44; ::_thesis: verum end; theorem Th47: :: TOPREAL9:47 for a, b, r being real number for x being Point of (Euclid 2) st x = |[a,b]| holds cl_Ball (x,r) = closed_inside_of_circle (a,b,r) proof let a, b, r be real number ; ::_thesis: for x being Point of (Euclid 2) st x = |[a,b]| holds cl_Ball (x,r) = closed_inside_of_circle (a,b,r) let x be Point of (Euclid 2); ::_thesis: ( x = |[a,b]| implies cl_Ball (x,r) = closed_inside_of_circle (a,b,r) ) assume A1: x = |[a,b]| ; ::_thesis: cl_Ball (x,r) = closed_inside_of_circle (a,b,r) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: closed_inside_of_circle (a,b,r) c= cl_Ball (x,r) let w be set ; ::_thesis: ( w in cl_Ball (x,r) implies w in closed_inside_of_circle (a,b,r) ) assume A2: w in cl_Ball (x,r) ; ::_thesis: w in closed_inside_of_circle (a,b,r) then reconsider u = w as Point of (TOP-REAL 2) by TOPREAL3:8; reconsider e = u as Point of (Euclid 2) by TOPREAL3:8; dist (e,x) = |.(u - |[a,b]|).| by A1, JGRAPH_1:28; then |.(u - |[a,b]|).| <= r by A2, METRIC_1:12; hence w in closed_inside_of_circle (a,b,r) by Th44; ::_thesis: verum end; let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in closed_inside_of_circle (a,b,r) or w in cl_Ball (x,r) ) assume A3: w in closed_inside_of_circle (a,b,r) ; ::_thesis: w in cl_Ball (x,r) then reconsider u = w as Point of (TOP-REAL 2) ; reconsider e = u as Point of (Euclid 2) by TOPREAL3:8; dist (e,x) = |.(u - |[a,b]|).| by A1, JGRAPH_1:28; then dist (e,x) <= r by A3, Th44; hence w in cl_Ball (x,r) by METRIC_1:12; ::_thesis: verum end; theorem Th48: :: TOPREAL9:48 for a, b, r being real number for x being Point of (Euclid 2) st x = |[a,b]| holds Ball (x,r) = inside_of_circle (a,b,r) proof let a, b, r be real number ; ::_thesis: for x being Point of (Euclid 2) st x = |[a,b]| holds Ball (x,r) = inside_of_circle (a,b,r) let x be Point of (Euclid 2); ::_thesis: ( x = |[a,b]| implies Ball (x,r) = inside_of_circle (a,b,r) ) assume A1: x = |[a,b]| ; ::_thesis: Ball (x,r) = inside_of_circle (a,b,r) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: inside_of_circle (a,b,r) c= Ball (x,r) let w be set ; ::_thesis: ( w in Ball (x,r) implies w in inside_of_circle (a,b,r) ) assume A2: w in Ball (x,r) ; ::_thesis: w in inside_of_circle (a,b,r) then reconsider u = w as Point of (TOP-REAL 2) by TOPREAL3:8; reconsider e = u as Point of (Euclid 2) by TOPREAL3:8; dist (e,x) = |.(u - |[a,b]|).| by A1, JGRAPH_1:28; then |.(u - |[a,b]|).| < r by A2, METRIC_1:11; hence w in inside_of_circle (a,b,r) by Th45; ::_thesis: verum end; let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in inside_of_circle (a,b,r) or w in Ball (x,r) ) assume A3: w in inside_of_circle (a,b,r) ; ::_thesis: w in Ball (x,r) then reconsider u = w as Point of (TOP-REAL 2) ; reconsider e = u as Point of (Euclid 2) by TOPREAL3:8; dist (e,x) = |.(u - |[a,b]|).| by A1, JGRAPH_1:28; then dist (e,x) < r by A3, Th45; hence w in Ball (x,r) by METRIC_1:11; ::_thesis: verum end; theorem Th49: :: TOPREAL9:49 for a, b, r being real number for x being Point of (Euclid 2) st x = |[a,b]| holds Sphere (x,r) = circle (a,b,r) proof let a, b, r be real number ; ::_thesis: for x being Point of (Euclid 2) st x = |[a,b]| holds Sphere (x,r) = circle (a,b,r) let x be Point of (Euclid 2); ::_thesis: ( x = |[a,b]| implies Sphere (x,r) = circle (a,b,r) ) assume A1: x = |[a,b]| ; ::_thesis: Sphere (x,r) = circle (a,b,r) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: circle (a,b,r) c= Sphere (x,r) let w be set ; ::_thesis: ( w in Sphere (x,r) implies w in circle (a,b,r) ) assume A2: w in Sphere (x,r) ; ::_thesis: w in circle (a,b,r) then reconsider u = w as Point of (TOP-REAL 2) by TOPREAL3:8; reconsider e = u as Point of (Euclid 2) by TOPREAL3:8; dist (e,x) = |.(u - |[a,b]|).| by A1, JGRAPH_1:28; then |.(u - |[a,b]|).| = r by A2, METRIC_1:13; hence w in circle (a,b,r) by Th43; ::_thesis: verum end; let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in circle (a,b,r) or w in Sphere (x,r) ) assume A3: w in circle (a,b,r) ; ::_thesis: w in Sphere (x,r) then reconsider u = w as Point of (TOP-REAL 2) ; reconsider e = u as Point of (Euclid 2) by TOPREAL3:8; dist (e,x) = |.(u - |[a,b]|).| by A1, JGRAPH_1:28; then dist (e,x) = r by A3, Th43; hence w in Sphere (x,r) by METRIC_1:13; ::_thesis: verum end; theorem Th50: :: TOPREAL9:50 for a, b, r being real number holds Ball (|[a,b]|,r) = inside_of_circle (a,b,r) proof let a, b, r be real number ; ::_thesis: Ball (|[a,b]|,r) = inside_of_circle (a,b,r) reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; thus Ball (|[a,b]|,r) = Ball (e,r) by Th13 .= inside_of_circle (a,b,r) by Th48 ; ::_thesis: verum end; theorem :: TOPREAL9:51 for a, b, r being real number holds cl_Ball (|[a,b]|,r) = closed_inside_of_circle (a,b,r) proof let a, b, r be real number ; ::_thesis: cl_Ball (|[a,b]|,r) = closed_inside_of_circle (a,b,r) reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; thus cl_Ball (|[a,b]|,r) = cl_Ball (e,r) by Th14 .= closed_inside_of_circle (a,b,r) by Th47 ; ::_thesis: verum end; theorem Th52: :: TOPREAL9:52 for a, b, r being real number holds Sphere (|[a,b]|,r) = circle (a,b,r) proof let a, b, r be real number ; ::_thesis: Sphere (|[a,b]|,r) = circle (a,b,r) reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; thus Sphere (|[a,b]|,r) = Sphere (e,r) by Th15 .= circle (a,b,r) by Th49 ; ::_thesis: verum end; theorem :: TOPREAL9:53 for a, b, r being real number holds inside_of_circle (a,b,r) c= closed_inside_of_circle (a,b,r) proof let a, b, r be real number ; ::_thesis: inside_of_circle (a,b,r) c= closed_inside_of_circle (a,b,r) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in inside_of_circle (a,b,r) or x in closed_inside_of_circle (a,b,r) ) assume A1: x in inside_of_circle (a,b,r) ; ::_thesis: x in closed_inside_of_circle (a,b,r) then reconsider x = x as Point of (TOP-REAL 2) ; |.(x - |[a,b]|).| < r by A1, Th45; hence x in closed_inside_of_circle (a,b,r) by Th44; ::_thesis: verum end; theorem :: TOPREAL9:54 for a, b, r being real number holds inside_of_circle (a,b,r) misses circle (a,b,r) proof let a, b, r be real number ; ::_thesis: inside_of_circle (a,b,r) misses circle (a,b,r) assume not inside_of_circle (a,b,r) misses circle (a,b,r) ; ::_thesis: contradiction then consider x being set such that A1: x in inside_of_circle (a,b,r) and A2: x in circle (a,b,r) by XBOOLE_0:3; reconsider x = x as Point of (TOP-REAL 2) by A1; |.(x - |[a,b]|).| = r by A2, Th43; hence contradiction by A1, Th45; ::_thesis: verum end; theorem :: TOPREAL9:55 for a, b, r being real number holds (inside_of_circle (a,b,r)) \/ (circle (a,b,r)) = closed_inside_of_circle (a,b,r) proof let a, b, r be real number ; ::_thesis: (inside_of_circle (a,b,r)) \/ (circle (a,b,r)) = closed_inside_of_circle (a,b,r) reconsider p = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; A1: cl_Ball (p,r) = closed_inside_of_circle (a,b,r) by Th47; ( Sphere (p,r) = circle (a,b,r) & Ball (p,r) = inside_of_circle (a,b,r) ) by Th48, Th49; hence (inside_of_circle (a,b,r)) \/ (circle (a,b,r)) = closed_inside_of_circle (a,b,r) by A1, METRIC_1:16; ::_thesis: verum end; theorem :: TOPREAL9:56 for r being real number for s being Point of (TOP-REAL 2) st s in Sphere ((0. (TOP-REAL 2)),r) holds ((s `1) ^2) + ((s `2) ^2) = r ^2 proof let r be real number ; ::_thesis: for s being Point of (TOP-REAL 2) st s in Sphere ((0. (TOP-REAL 2)),r) holds ((s `1) ^2) + ((s `2) ^2) = r ^2 let s be Point of (TOP-REAL 2); ::_thesis: ( s in Sphere ((0. (TOP-REAL 2)),r) implies ((s `1) ^2) + ((s `2) ^2) = r ^2 ) assume s in Sphere ((0. (TOP-REAL 2)),r) ; ::_thesis: ((s `1) ^2) + ((s `2) ^2) = r ^2 then |.(s - (0. (TOP-REAL 2))).| = r by Th9; then |.s.| = r by RLVECT_1:13; hence ((s `1) ^2) + ((s `2) ^2) = r ^2 by JGRAPH_1:29; ::_thesis: verum end; theorem :: TOPREAL9:57 for a, b, r being real number for s, t being Point of (TOP-REAL 2) st s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) holds r > 0 proof let a, b, r be real number ; ::_thesis: for s, t being Point of (TOP-REAL 2) st s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) holds r > 0 let s, t be Point of (TOP-REAL 2); ::_thesis: ( s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) implies r > 0 ) reconsider x = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; cl_Ball (x,r) = closed_inside_of_circle (a,b,r) by Th47; hence ( s <> t & s in closed_inside_of_circle (a,b,r) & t in closed_inside_of_circle (a,b,r) implies r > 0 ) by Th6; ::_thesis: verum end; theorem :: TOPREAL9:58 for a, b, w, r being real number for s, t being Point of (TOP-REAL 2) for S, T, X being Element of REAL 2 st S = s & T = t & X = |[a,b]| & w = ((- (2 * |((t - s),(s - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) & s <> t & s in inside_of_circle (a,b,r) holds ex e being Point of (TOP-REAL 2) st ( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) ) proof let a, b, w, r be real number ; ::_thesis: for s, t being Point of (TOP-REAL 2) for S, T, X being Element of REAL 2 st S = s & T = t & X = |[a,b]| & w = ((- (2 * |((t - s),(s - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) & s <> t & s in inside_of_circle (a,b,r) holds ex e being Point of (TOP-REAL 2) st ( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) ) let s, t be Point of (TOP-REAL 2); ::_thesis: for S, T, X being Element of REAL 2 st S = s & T = t & X = |[a,b]| & w = ((- (2 * |((t - s),(s - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) & s <> t & s in inside_of_circle (a,b,r) holds ex e being Point of (TOP-REAL 2) st ( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) ) A1: ( Ball (|[a,b]|,r) = inside_of_circle (a,b,r) & Sphere (|[a,b]|,r) = circle (a,b,r) ) by Th50, Th52; let S, T, X be Element of REAL 2; ::_thesis: ( S = s & T = t & X = |[a,b]| & w = ((- (2 * |((t - s),(s - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) & s <> t & s in inside_of_circle (a,b,r) implies ex e being Point of (TOP-REAL 2) st ( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) ) ) assume ( S = s & T = t & X = |[a,b]| & w = ((- (2 * |((t - s),(s - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) & s <> t & s in inside_of_circle (a,b,r) ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) ) hence ex e being Point of (TOP-REAL 2) st ( {e} = (halfline (s,t)) /\ (circle (a,b,r)) & e = ((1 - w) * s) + (w * t) ) by A1, Th37; ::_thesis: verum end; theorem :: TOPREAL9:59 for a, b, r being real number for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in inside_of_circle (a,b,r) holds (LSeg (s,t)) /\ (circle (a,b,r)) = {s} proof let a, b, r be real number ; ::_thesis: for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in inside_of_circle (a,b,r) holds (LSeg (s,t)) /\ (circle (a,b,r)) = {s} let s, t be Point of (TOP-REAL 2); ::_thesis: ( s in circle (a,b,r) & t in inside_of_circle (a,b,r) implies (LSeg (s,t)) /\ (circle (a,b,r)) = {s} ) assume A1: ( s in circle (a,b,r) & t in inside_of_circle (a,b,r) ) ; ::_thesis: (LSeg (s,t)) /\ (circle (a,b,r)) = {s} reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; A2: inside_of_circle (a,b,r) = Ball (e,r) by Th48 .= Ball (|[a,b]|,r) by Th13 ; circle (a,b,r) = Sphere (e,r) by Th49 .= Sphere (|[a,b]|,r) by Th15 ; hence (LSeg (s,t)) /\ (circle (a,b,r)) = {s} by A1, A2, Th33; ::_thesis: verum end; theorem :: TOPREAL9:60 for a, b, r being real number for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in circle (a,b,r) holds (LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r) proof let a, b, r be real number ; ::_thesis: for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in circle (a,b,r) holds (LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r) let s, t be Point of (TOP-REAL 2); ::_thesis: ( s in circle (a,b,r) & t in circle (a,b,r) implies (LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r) ) assume A1: ( s in circle (a,b,r) & t in circle (a,b,r) ) ; ::_thesis: (LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r) reconsider G = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; Sphere (G,r) = circle (a,b,r) by Th49; then A2: Sphere (|[a,b]|,r) = circle (a,b,r) by Th15; Ball (|[a,b]|,r) = inside_of_circle (a,b,r) by Th50; hence (LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r) by A1, A2, Th34; ::_thesis: verum end; theorem :: TOPREAL9:61 for a, b, r being real number for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in circle (a,b,r) holds (LSeg (s,t)) /\ (circle (a,b,r)) = {s,t} proof let a, b, r be real number ; ::_thesis: for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in circle (a,b,r) holds (LSeg (s,t)) /\ (circle (a,b,r)) = {s,t} let s, t be Point of (TOP-REAL 2); ::_thesis: ( s in circle (a,b,r) & t in circle (a,b,r) implies (LSeg (s,t)) /\ (circle (a,b,r)) = {s,t} ) reconsider G = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; Sphere (G,r) = circle (a,b,r) by Th49; then A1: Sphere (|[a,b]|,r) = circle (a,b,r) by Th15; assume ( s in circle (a,b,r) & t in circle (a,b,r) ) ; ::_thesis: (LSeg (s,t)) /\ (circle (a,b,r)) = {s,t} hence (LSeg (s,t)) /\ (circle (a,b,r)) = {s,t} by A1, Th35; ::_thesis: verum end; theorem :: TOPREAL9:62 for a, b, r being real number for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in circle (a,b,r) holds (halfline (s,t)) /\ (circle (a,b,r)) = {s,t} proof let a, b, r be real number ; ::_thesis: for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) & t in circle (a,b,r) holds (halfline (s,t)) /\ (circle (a,b,r)) = {s,t} let s, t be Point of (TOP-REAL 2); ::_thesis: ( s in circle (a,b,r) & t in circle (a,b,r) implies (halfline (s,t)) /\ (circle (a,b,r)) = {s,t} ) assume A1: ( s in circle (a,b,r) & t in circle (a,b,r) ) ; ::_thesis: (halfline (s,t)) /\ (circle (a,b,r)) = {s,t} reconsider e = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; circle (a,b,r) = Sphere (e,r) by Th49 .= Sphere (|[a,b]|,r) by Th15 ; hence (halfline (s,t)) /\ (circle (a,b,r)) = {s,t} by A1, Th36; ::_thesis: verum end; theorem :: TOPREAL9:63 for a, b, r, w being real number for s, t being Point of (TOP-REAL 2) for S, T, Y being Element of REAL 2 st S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| & s <> t & s in circle (a,b,r) & t in closed_inside_of_circle (a,b,r) holds ex e being Point of (TOP-REAL 2) st ( e <> s & {s,e} = (halfline (s,t)) /\ (circle (a,b,r)) & ( t in Sphere (|[a,b]|,r) implies e = t ) & ( not t in Sphere (|[a,b]|,r) & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) ) proof let a, b, r, w be real number ; ::_thesis: for s, t being Point of (TOP-REAL 2) for S, T, Y being Element of REAL 2 st S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| & s <> t & s in circle (a,b,r) & t in closed_inside_of_circle (a,b,r) holds ex e being Point of (TOP-REAL 2) st ( e <> s & {s,e} = (halfline (s,t)) /\ (circle (a,b,r)) & ( t in Sphere (|[a,b]|,r) implies e = t ) & ( not t in Sphere (|[a,b]|,r) & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) ) let s, t be Point of (TOP-REAL 2); ::_thesis: for S, T, Y being Element of REAL 2 st S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| & s <> t & s in circle (a,b,r) & t in closed_inside_of_circle (a,b,r) holds ex e being Point of (TOP-REAL 2) st ( e <> s & {s,e} = (halfline (s,t)) /\ (circle (a,b,r)) & ( t in Sphere (|[a,b]|,r) implies e = t ) & ( not t in Sphere (|[a,b]|,r) & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) ) reconsider G = |[a,b]| as Point of (Euclid 2) by TOPREAL3:8; A1: ( cl_Ball (G,r) = closed_inside_of_circle (a,b,r) & cl_Ball (G,r) = cl_Ball (|[a,b]|,r) ) by Th14, Th47; Sphere (G,r) = circle (a,b,r) by Th49; then A2: Sphere (|[a,b]|,r) = circle (a,b,r) by Th15; let S, T, Y be Element of REAL 2; ::_thesis: ( S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| & s <> t & s in circle (a,b,r) & t in closed_inside_of_circle (a,b,r) implies ex e being Point of (TOP-REAL 2) st ( e <> s & {s,e} = (halfline (s,t)) /\ (circle (a,b,r)) & ( t in Sphere (|[a,b]|,r) implies e = t ) & ( not t in Sphere (|[a,b]|,r) & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) ) ) assume ( S = ((1 / 2) * s) + ((1 / 2) * t) & T = t & Y = |[a,b]| & s <> t & s in circle (a,b,r) & t in closed_inside_of_circle (a,b,r) ) ; ::_thesis: ex e being Point of (TOP-REAL 2) st ( e <> s & {s,e} = (halfline (s,t)) /\ (circle (a,b,r)) & ( t in Sphere (|[a,b]|,r) implies e = t ) & ( not t in Sphere (|[a,b]|,r) & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) ) hence ex e being Point of (TOP-REAL 2) st ( e <> s & {s,e} = (halfline (s,t)) /\ (circle (a,b,r)) & ( t in Sphere (|[a,b]|,r) implies e = t ) & ( not t in Sphere (|[a,b]|,r) & w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) ) by A1, A2, Th38; ::_thesis: verum end; registration let a, b, r be real number ; cluster inside_of_circle (a,b,r) -> convex ; coherence inside_of_circle (a,b,r) is convex proof inside_of_circle (a,b,r) = { q where q is Point of (TOP-REAL 2) : |.(q - |[a,b]|).| < r } by JGRAPH_6:def_6; hence inside_of_circle (a,b,r) is convex by Lm2; ::_thesis: verum end; cluster closed_inside_of_circle (a,b,r) -> convex ; coherence closed_inside_of_circle (a,b,r) is convex proof closed_inside_of_circle (a,b,r) = { q where q is Point of (TOP-REAL 2) : |.(q - |[a,b]|).| <= r } by JGRAPH_6:def_7; hence closed_inside_of_circle (a,b,r) is convex by Lm1; ::_thesis: verum end; end;