:: TOPREAL9 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: TOPREAL9:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y, z being Point of (TOP-REAL n) holds (x - y) - z = (x - z) - y
proof end;

theorem Th2: :: TOPREAL9:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x, y, z being Point of (TOP-REAL n) st x + y = x + z holds
y = z
proof end;

theorem Th3: :: TOPREAL9:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x being Point of (TOP-REAL n) st not n is empty holds
x <> x + (1.REAL n)
proof end;

theorem Th4: :: TOPREAL9:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th5: :: TOPREAL9:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL holds |.f.| ^2 = Sum (sqr f)
proof end;

theorem Th6: :: TOPREAL9:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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 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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th8: :: TOPREAL9:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th9: :: TOPREAL9:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem :: TOPREAL9:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for y being Point of (TOP-REAL n) st y in Ball (0.REAL n),r holds
|.y.| < r
proof end;

theorem :: TOPREAL9:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for y being Point of (TOP-REAL n) st y in cl_Ball (0.REAL n),r holds
|.y.| <= r
proof end;

theorem :: TOPREAL9:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for y being Point of (TOP-REAL n) st y in Sphere (0.REAL n),r holds
|.y.| = r
proof end;

theorem Th13: :: TOPREAL9:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th14: :: TOPREAL9:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th15: :: TOPREAL9:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th16: :: TOPREAL9:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for x being Point of (TOP-REAL n) holds Ball x,r c= cl_Ball x,r
proof end;

theorem Th17: :: TOPREAL9:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for x being Point of (TOP-REAL n) holds Sphere x,r c= cl_Ball x,r
proof end;

theorem Th18: :: TOPREAL9:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th19: :: TOPREAL9:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for x being Point of (TOP-REAL n) holds Ball x,r misses Sphere x,r
proof 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 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 end;
end;

theorem :: TOPREAL9:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for x being Point of (TOP-REAL n) st not Ball x,r is empty holds
r > 0
proof end;

theorem :: TOPREAL9:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for x being Point of (TOP-REAL n) st Ball x,r is empty holds
r <= 0
proof end;

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

theorem :: TOPREAL9:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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
proof end;

theorem :: TOPREAL9:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for x being Point of (TOP-REAL n) st cl_Ball x,r is empty holds
r < 0
proof end;

theorem Th24: :: TOPREAL9:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real number ;
cluster Ball x,r -> open Bounded ;
coherence
( Ball x,r is open & Ball x,r is Bounded )
proof end;
cluster cl_Ball x,r -> closed Bounded ;
coherence
( cl_Ball x,r is closed & cl_Ball x,r is Bounded )
proof end;
cluster Sphere x,r -> closed Bounded ;
coherence
( Sphere x,r is closed & Sphere x,r is Bounded )
proof end;
end;

Lm1: for n being 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 end;

Lm2: for n being 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 end;

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real number ;
cluster Ball x,r -> open Bounded convex ;
coherence
Ball x,r is convex by Lm2;
cluster cl_Ball x,r -> closed Bounded convex ;
coherence
cl_Ball x,r is convex by Lm1;
end;

definition
let n be Nat;
let f be Function of (TOP-REAL n),(TOP-REAL n);
attr f 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);
attr f is additive means :Def5: :: TOPREAL9:def 5
for x, y being Point of (TOP-REAL n) holds f . (x + y) = (f . x) + (f . y);
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) );

:: deftheorem Def5 defines additive TOPREAL9:def 5 :
for n being Nat
for f being Function of (TOP-REAL n),(TOP-REAL n) holds
( f is additive iff for x, y being Point of (TOP-REAL n) holds f . (x + y) = (f . x) + (f . y) );

registration
let n be Nat;
cluster (TOP-REAL n) --> (0.REAL n) -> homogeneous additive ;
coherence
( (TOP-REAL n) --> (0.REAL n) is homogeneous & (TOP-REAL n) --> (0.REAL n) is additive )
proof end;
end;

registration
let n be Nat;
cluster continuous homogeneous additive M5(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 end;
end;

registration
let a, c be real number ;
cluster AffineMap a,0,c,0 -> homogeneous additive ;
coherence
( AffineMap a,0,c,0 is homogeneous & AffineMap a,0,c,0 is additive )
proof end;
end;

theorem :: TOPREAL9:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being homogeneous additive Function of (TOP-REAL n),(TOP-REAL n)
for X being convex Subset of (TOP-REAL n) holds f .: X is convex
proof 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 6
{ (((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 end;
end;

:: deftheorem defines halfline TOPREAL9:def 6 :
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

registration
let n be Nat;
let p, q be Point of (TOP-REAL n);
cluster halfline p,q -> non empty ;
coherence
not halfline p,q is empty
proof end;
end;

theorem Th27: :: TOPREAL9:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being Point of (TOP-REAL n) holds p in halfline p,q
proof end;

theorem Th28: :: TOPREAL9:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for q, p being Point of (TOP-REAL n) holds q in halfline p,q
proof end;

theorem Th29: :: TOPREAL9:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p being Point of (TOP-REAL n) holds halfline p,p = {p}
proof end;

theorem Th30: :: TOPREAL9:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem :: TOPREAL9:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem :: TOPREAL9:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for p, q being Point of (TOP-REAL n) holds LSeg p,q c= halfline p,q
proof end;

registration
let n be Nat;
let p, q be Point of (TOP-REAL n);
cluster halfline p,q -> non empty convex ;
coherence
halfline p,q is convex
proof end;
end;

theorem Th33: :: TOPREAL9:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th34: :: TOPREAL9:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th35: :: TOPREAL9:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th36: :: TOPREAL9:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th37: :: TOPREAL9:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 end;

theorem Th38: :: TOPREAL9:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 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 closed Bounded ;
coherence
Sphere x,r is empty
proof 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 closed Bounded ;
coherence
not Sphere x,r is empty
proof end;
end;

theorem :: TOPREAL9:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for x being Point of (TOP-REAL n) st not Sphere x,r is empty holds
r >= 0
proof end;

theorem :: TOPREAL9:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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
proof end;

theorem :: TOPREAL9:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TOPREAL9:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th43: :: TOPREAL9:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th44: :: TOPREAL9:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th45: :: TOPREAL9:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 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 end;
end;

theorem :: TOPREAL9:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r being real number holds circle a,b,r c= closed_inside_of_circle a,b,r
proof end;

theorem Th47: :: TOPREAL9:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th48: :: TOPREAL9:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th49: :: TOPREAL9:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th50: :: TOPREAL9:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r being real number holds Ball |[a,b]|,r = inside_of_circle a,b,r
proof end;

theorem :: TOPREAL9:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r being real number holds cl_Ball |[a,b]|,r = closed_inside_of_circle a,b,r
proof end;

theorem Th52: :: TOPREAL9:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r being real number holds Sphere |[a,b]|,r = circle a,b,r
proof end;

theorem :: TOPREAL9:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r being real number holds inside_of_circle a,b,r c= closed_inside_of_circle a,b,r
proof end;

theorem :: TOPREAL9:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, r being real number holds inside_of_circle a,b,r misses circle a,b,r
proof end;

theorem :: TOPREAL9:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TOPREAL9:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number
for s being Point of (TOP-REAL 2) st s in Sphere (0.REAL 2),r holds
((s `1 ) ^2 ) + ((s `2 ) ^2 ) = r ^2
proof end;

theorem :: TOPREAL9:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TOPREAL9:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TOPREAL9:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TOPREAL9:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TOPREAL9:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TOPREAL9:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: TOPREAL9:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 end;
cluster closed_inside_of_circle a,b,r -> convex ;
coherence
closed_inside_of_circle a,b,r is convex
proof end;
end;