:: BROUWER semantic presentation
set c1 = TOP-REAL 2;
E1:
[#] (TOP-REAL 2) = the carrier of (TOP-REAL 2)
by PRE_TOPC:12;
:: deftheorem defines DiffElems BROUWER:def 1 :
theorem :: BROUWER:1
theorem E2: :: BROUWER:2
:: deftheorem defines Tdisk BROUWER:def 2 :
theorem E3: :: BROUWER:3
theorem E4: :: BROUWER:4
proof
let c
2 be
Nat;
let c
3 be
real non
negative number ;
let c
4, c
5, c
6 be
Point of
(TOP-REAL c2);
assume that E5:
c
4 <> c
5
and E6:
c
4 is
Point of
(Tdisk c6,c3)
and E7:
not c
4 is
Point of
(Tcircle c6,c3)
;
E8:
the
carrier of
(Tcircle c6,c3) = Sphere c
6,c
3
by TOPREALB:9;
E9:
the
carrier of
(Tdisk c6,c3) = cl_Ball c
6,c
3
by E3;
E10:
|.(c4 - c6).| <> c
3
by E7, E8, TOPREAL9:9;
reconsider c
7 = c
4, c
8 = c
5, c
9 = c
6 as
Element of
REAL c
2 by EUCLID:25;
set c
10 =
((- (2 * |((c5 - c4),(c4 - c6))|)) + (sqrt (delta (Sum (sqr (c8 - c7))),(2 * |((c5 - c4),(c4 - c6))|),((Sum (sqr (c7 - c9))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c8 - c7))));
|.(c4 - c6).| <= c
3
by E6, E9, TOPREAL9:8;
then
|.(c4 - c6).| < c
3
by E10, REAL_1:def 5;
then
c
4 in Ball c
6,c
3
by TOPREAL9:7;
then consider c
11 being
Point of
(TOP-REAL c2) such that E11:
{c11} = (halfline c4,c5) /\ (Sphere c6,c3)
and
c
11 = ((1 - (((- (2 * |((c5 - c4),(c4 - c6))|)) + (sqrt (delta (Sum (sqr (c8 - c7))),(2 * |((c5 - c4),(c4 - c6))|),((Sum (sqr (c7 - c9))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c8 - c7)))))) * c4) + ((((- (2 * |((c5 - c4),(c4 - c6))|)) + (sqrt (delta (Sum (sqr (c8 - c7))),(2 * |((c5 - c4),(c4 - c6))|),((Sum (sqr (c7 - c9))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c8 - c7))))) * c5)
by E5, TOPREAL9:37;
c
11 in {c11}
by TARSKI:def 1;
then
c
11 in Sphere c
6,c
3
by E11, XBOOLE_0:def 3;
hence
ex b
1 being
Point of
(Tcircle c6,c3) st
{b1} = (halfline c4,c5) /\ (Sphere c6,c3)
by E8, E11;
end;
theorem E5: :: BROUWER:5
proof
let c
2 be
Nat;
let c
3 be
real non
negative number ;
let c
4, c
5, c
6 be
Point of
(TOP-REAL c2);
assume that E6:
c
4 <> c
5
and E7:
c
4 in the
carrier of
(Tcircle c6,c3)
and E8:
c
5 is
Point of
(Tdisk c6,c3)
;
E9:
the
carrier of
(Tcircle c6,c3) = Sphere c
6,c
3
by TOPREALB:9;
reconsider c
7 =
((1 / 2) * c4) + ((1 / 2) * c5), c
8 = c
5, c
9 = c
6 as
Element of
REAL c
2 by EUCLID:25;
set c
10 =
((- (2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|)) + (sqrt (delta (Sum (sqr (c8 - c7))),(2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|),((Sum (sqr (c7 - c9))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c8 - c7))));
the
carrier of
(Tdisk c6,c3) = cl_Ball c
6,c
3
by E3;
then consider c
11 being
Point of
(TOP-REAL c2) such that E10:
c
11 <> c
4
and E11:
{c4,c11} = (halfline c4,c5) /\ (Sphere c6,c3)
and
( ( c
5 in Sphere c
6,c
3 implies c
11 = c
5 ) & ( (
((- (2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|)) + (sqrt (delta (Sum (sqr (c8 - c7))),(2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|),((Sum (sqr (c7 - c9))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c8 - c7)))) = ((- (2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|)) + (sqrt (delta (Sum (sqr (c8 - c7))),(2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|),((Sum (sqr (c7 - c9))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c8 - c7)))) ) implies ( c
5 in Sphere c
6,c
3 or c
11 = ((1 - (((- (2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|)) + (sqrt (delta (Sum (sqr (c8 - c7))),(2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|),((Sum (sqr (c7 - c9))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c8 - c7)))))) * (((1 / 2) * c4) + ((1 / 2) * c5))) + ((((- (2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|)) + (sqrt (delta (Sum (sqr (c8 - c7))),(2 * |((c5 - (((1 / 2) * c4) + ((1 / 2) * c5))),((((1 / 2) * c4) + ((1 / 2) * c5)) - c6))|),((Sum (sqr (c7 - c9))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c8 - c7))))) * c5) ) ) )
by E8, E6, E9, E7, TOPREAL9:38;
( c
11 in {c4,c11} & c
4 in {c4,c11} )
by TARSKI:def 2;
then
( c
11 in Sphere c
6,c
3 & c
4 in Sphere c
6,c
3 )
by E11, XBOOLE_0:def 3;
hence
ex b
1 being
Point of
(Tcircle c6,c3) st
( b
1 <> c
4 &
{c4,b1} = (halfline c4,c5) /\ (Sphere c6,c3) )
by E9, E10, E11;
end;
definition
let c
2 be non
empty Nat;
let c
3 be
Point of
(TOP-REAL c2);
let c
4, c
5 be
Point of
(TOP-REAL c2);
let c
6 be
real non
negative number ;
assume that E6:
c
4 is
Point of
(Tdisk c3,c6)
and E7:
c
5 is
Point of
(Tdisk c3,c6)
and E8:
c
4 <> c
5
;
func HC c
3,c
4,c
2,c
5 -> Point of
(TOP-REAL a1) means :
E6:
:: BROUWER:def 3
( a
6 in (halfline a3,a4) /\ (Sphere a2,a5) & a
6 <> a
3 );
existence
ex b1 being Point of (TOP-REAL c2) st
( b1 in (halfline c4,c5) /\ (Sphere c3,c6) & b1 <> c4 )
proof
per cases
not ( not c
4 is
Point of
(Tcircle c3,c6) & c
4 is
Point of
(Tcircle c3,c6) )
;
suppose E9:
c
4 is
Point of
(Tcircle c3,c6)
;
consider c
7 being
Point of
(Tcircle c3,c6) such that E10:
( c
7 <> c
4 &
{c4,c7} = (halfline c4,c5) /\ (Sphere c3,c6) )
by E7, E8, E9, E5;
reconsider c
8 = c
7 as
Point of
(TOP-REAL c2) by TOPMETR:2;
take
c
8
;
thus
( c
8 in (halfline c4,c5) /\ (Sphere c3,c6) & c
8 <> c
4 )
by E10, TARSKI:def 2;
end;
suppose E9:
not c
4 is
Point of
(Tcircle c3,c6)
;
consider c
7 being
Point of
(Tcircle c3,c6) such that E10:
{c7} = (halfline c4,c5) /\ (Sphere c3,c6)
by E9, E8, E6, E4;
reconsider c
8 = c
7 as
Point of
(TOP-REAL c2) by TOPMETR:2;
take
c
8
;
thus
( c
8 in (halfline c4,c5) /\ (Sphere c3,c6) & c
8 <> c
4 )
by E10, E9, TARSKI:def 1;
end;
end;
end;
uniqueness
for b1, b2 being Point of (TOP-REAL c2) holds
( ( b1 in (halfline c4,c5) /\ (Sphere c3,c6) & b2 in (halfline c4,c5) /\ (Sphere c3,c6) ) implies ( not b1 <> c4 or not b2 <> c4 or b1 = b2 ) )
proof
let c
7, c
8 be
Point of
(TOP-REAL c2);
assume that E9:
( c
7 in (halfline c4,c5) /\ (Sphere c3,c6) & c
7 <> c
4 )
and E10:
( c
8 in (halfline c4,c5) /\ (Sphere c3,c6) & c
8 <> c
4 )
;
per cases
not ( not c
4 is
Point of
(Tcircle c3,c6) & c
4 is
Point of
(Tcircle c3,c6) )
;
suppose E11:
c
4 is
Point of
(Tcircle c3,c6)
;
consider c
9 being
Point of
(Tcircle c3,c6) such that
c
9 <> c
4
and E12:
{c4,c9} = (halfline c4,c5) /\ (Sphere c3,c6)
by E7, E8, E11, E5;
per cases
not ( not ( c
7 = c
9 & c
8 = c
9 ) & not ( c
7 = c
9 & c
8 = c
4 ) & not ( c
7 = c
4 & c
8 = c
9 ) & not ( c
7 = c
4 & c
8 = c
4 ) )
by E9, E10, E12, TARSKI:def 2;
suppose
( c
7 = c
9 & c
8 = c
9 )
;
end;
suppose
( c
7 = c
9 & c
8 = c
4 )
;
end;
suppose
( c
7 = c
4 & c
8 = c
9 )
;
end;
suppose
( c
7 = c
4 & c
8 = c
4 )
;
end;
end;
end;
suppose E11:
not c
4 is
Point of
(Tcircle c3,c6)
;
consider c
9 being
Point of
(Tcircle c3,c6) such that E12:
{c9} = (halfline c4,c5) /\ (Sphere c3,c6)
by E11, E6, E8, E4;
c
7 = c
9
by E9, E12, TARSKI:def 1;
hence
c
7 = c
8
by E10, E12, TARSKI:def 1;
end;
end;
end;
end;
:: deftheorem E6 defines HC BROUWER:def 3 :
theorem E7: :: BROUWER:6
proof
let c
2 be
real non
negative number ;
let c
3 be non
empty Nat;
let c
4, c
5, c
6 be
Point of
(TOP-REAL c3);
assume E8:
( c
4 is
Point of
(Tdisk c5,c2) & c
6 is
Point of
(Tdisk c5,c2) & c
4 <> c
6 )
;
E9:
the
carrier of
(Tcircle c5,c2) = Sphere c
5,c
2
by TOPREALB:9;
HC c
4,c
6,c
5,c
2 in (halfline c4,c6) /\ (Sphere c5,c2)
by E8, E6;
hence
HC c
4,c
6,c
5,c
2 is
Point of
(Tcircle c5,c2)
by E9, XBOOLE_0:def 3;
end;
theorem :: BROUWER:7
for b
1 being
real number for b
2 being
real non
negative number for b
3 being non
empty Natfor b
4, b
5, b
6 being
Point of
(TOP-REAL b3)for b
7, b
8, b
9 being
Element of
REAL b
3 holds
( ( b
7 = b
4 & b
8 = b
5 & b
9 = b
6 & b
4 is
Point of
(Tdisk b6,b2) & b
5 is
Point of
(Tdisk b6,b2) & b
1 = ((- |((b5 - b4),(b4 - b6))|) + (sqrt ((|((b5 - b4),(b4 - b6))| ^2 ) - ((Sum (sqr (b8 - b7))) * ((Sum (sqr (b7 - b9))) - (b2 ^2 )))))) / (Sum (sqr (b8 - b7))) ) implies ( not b
4 <> b
5 or
HC b
4,b
5,b
6,b
2 = ((1 - b1) * b4) + (b1 * b5) ) )
proof
let c
2 be
real number ;
let c
3 be
real non
negative number ;
let c
4 be non
empty Nat;
let c
5, c
6, c
7 be
Point of
(TOP-REAL c4);
let c
8, c
9, c
10 be
Element of
REAL c
4;
assume that E8:
( c
8 = c
5 & c
9 = c
6 & c
10 = c
7 )
and E9:
c
5 is
Point of
(Tdisk c7,c3)
and E10:
c
6 is
Point of
(Tdisk c7,c3)
and E11:
c
5 <> c
6
;
set c
11 =
HC c
5,c
6,c
7,c
3;
set c
12 =
|((c6 - c5),(c5 - c7))|;
set c
13 =
Sum (sqr (c9 - c8));
set c
14 = 2
* |((c6 - c5),(c5 - c7))|;
set c
15 =
(Sum (sqr (c8 - c10))) - (c3 ^2 );
set c
16 =
((- (2 * |((c6 - c5),(c5 - c7))|)) - (sqrt (delta (Sum (sqr (c9 - c8))),(2 * |((c6 - c5),(c5 - c7))|),((Sum (sqr (c8 - c10))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c9 - c8))));
set c
17 =
((- (2 * |((c6 - c5),(c5 - c7))|)) + (sqrt (delta (Sum (sqr (c9 - c8))),(2 * |((c6 - c5),(c5 - c7))|),((Sum (sqr (c8 - c10))) - (c3 ^2 ))))) / (2 * (Sum (sqr (c9 - c8))));
assume E12:
c
2 = ((- |((c6 - c5),(c5 - c7))|) + (sqrt ((|((c6 - c5),(c5 - c7))| ^2 ) - ((Sum (sqr (c9 - c8))) * ((Sum (sqr (c8 - c10))) - (c3 ^2 )))))) / (Sum (sqr (c9 - c8)))
;
E13:
HC c
5,c
6,c
7,c
3 in (halfline c5,c6) /\ (Sphere c7,c3)
by E9, E10, E11, E6;
then
HC c
5,c
6,c
7,c
3 in halfline c
5,c
6
by XBOOLE_0:def 3;
then consider c
18 being
real number such that E14:
HC c
5,c
6,c
7,c
3 = ((1 - c18) * c5) + (c18 * c6)
and E15:
0
<= c
18
by TOPREAL9:26;
E16:
HC c
5,c
6,c
7,c
3 =
((1 * c5) - (c18 * c5)) + (c18 * c6)
by E14, EUCLID:54
.=
(c5 - (c18 * c5)) + (c18 * c6)
by EUCLID:33
.=
(c5 + (c18 * c6)) - (c18 * c5)
by JORDAN2C:9
.=
c
5 + ((c18 * c6) - (c18 * c5))
by EUCLID:49
.=
c
5 + (c18 * (c6 - c5))
by EUCLID:53
;
E17:
|.(c9 - c8).| <> 0
by E8, E11, EUCLID:19;
E19:
delta (Sum (sqr (c9 - c8))),
(2 * |((c6 - c5),(c5 - c7))|),
((Sum (sqr (c8 - c10))) - (c3 ^2 )) =
((2 * |((c6 - c5),(c5 - c7))|) ^2 ) - ((4 * (Sum (sqr (c9 - c8)))) * ((Sum (sqr (c8 - c10))) - (c3 ^2 )))
by QUIN_1:def 1
.=
((2 ^2 ) * (|((c6 - c5),(c5 - c7))| ^2 )) - ((4 * (Sum (sqr (c9 - c8)))) * ((Sum (sqr (c8 - c10))) - (c3 ^2 )))
.=
((2 * 2) * (|((c6 - c5),(c5 - c7))| ^2 )) - ((4 * (Sum (sqr (c9 - c8)))) * ((Sum (sqr (c8 - c10))) - (c3 ^2 )))
.=
4
* ((|((c6 - c5),(c5 - c7))| ^2 ) - ((Sum (sqr (c9 - c8))) * ((Sum (sqr (c8 - c10))) - (c3 ^2 ))))
;
the
carrier of
(Tdisk c7,c3) = cl_Ball c
7,c
3
by E3;
then E20:
|.(c5 - c7).| <= c
3
by E9, TOPREAL9:8;
E21:
|.(c8 - c10).| = sqrt (Sum (sqr (c8 - c10)))
by EUCLID:def 5;
E22:
|.(c8 - c10).| >= 0
by EUCLID:12;
c
6 - c
5 = c
9 - c
8
by E8, EUCLID:def 13;
then E23:
|.(c6 - c5).| = |.(c9 - c8).|
by TOPRNS_1:def 6;
E24:
|.(c9 - c8).| = sqrt (Sum (sqr (c9 - c8)))
by EUCLID:def 5;
Sum (sqr (c9 - c8)) >= 0
by RVSUM_1:116;
then E25:
|.(c9 - c8).| ^2 = Sum (sqr (c9 - c8))
by E24, SQUARE_1:def 4;
Sum (sqr (c8 - c10)) >= 0
by RVSUM_1:116;
then E26:
|.(c8 - c10).| ^2 = Sum (sqr (c8 - c10))
by E21, SQUARE_1:def 4;
c
5 - c
7 = c
8 - c
10
by E8, EUCLID:def 13;
then E27:
|.(c5 - c7).| = |.(c8 - c10).|
by TOPRNS_1:def 6;
then E28:
(sqrt (Sum (sqr (c8 - c10)))) ^2 <= c
3 ^2
by E20, E21, E22, SQUARE_1:77;
then E29:
(Sum (sqr (c8 - c10))) - (c3 ^2 ) <= 0
by E21, E26, REAL_2:106;
E30:
delta (Sum (sqr (c9 - c8))),
(2 * |((c6 - c5),(c5 - c7))|),
((Sum (sqr (c8 - c10))) - (c3 ^2 )) = ((2 * |((c6 - c5),(c5 - c7))|) ^2 ) - ((4 * (Sum (sqr (c9 - c8)))) * ((Sum (sqr (c8 - c10))) - (c3 ^2 )))
by QUIN_1:def 1;
4
* (Sum (sqr (c9 - c8))) > 0
by E18, XREAL_1:131;
then E31:
(4 * (Sum (sqr (c9 - c8)))) * ((Sum (sqr (c8 - c10))) - (c3 ^2 )) <= 0
by E29, XREAL_1:133;
E32:
((2 * |((c6 - c5),(c5 - c7))|) ^2 ) - ((4 * (Sum (sqr (