:: 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;