let n be Nat; for a, r being Real
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 a, r be Real; 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); 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; ( 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 )
; ( 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)
; 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 Th11;
A6:
Sphere (x,r) c= cl_Ball (x,r)
by Th15;
per cases
( z in Sphere (x,r) or not z in Sphere (x,r) )
;
suppose A7:
z in Sphere (
x,
r)
;
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
;
( 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, Th34;
verum end; suppose A8:
not
z in Sphere (
x,
r)
;
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 not ((1 / 2) * y) + ((1 / 2) * z) = zend;
(Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (
x,
r)
by Th16;
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 &
|.(1 / 2).| = 1
/ 2 )
by ABSVALUE:def 1;
Ball (
G,
r)
= Ball (
x,
r)
by Th11;
then
((1 / 2) * y) + ((1 / 2) * z) in Ball (
G,
r)
by A3, A6, A12, A11, Th22;
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, Th35;
take
e1
;
( 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 such that A16:
e1 = ((1 - l) * (((1 / 2) * y) + ((1 / 2) * z))) + (l * z)
and A17:
0 <= l
;
A18:
y in halfline (
y,
z)
by Th25;
hereby TARSKI:def 3,
XBOOLE_0:def 10 ( (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
object ;
( m in {y,e1} implies m in (halfline (y,z)) /\ (Sphere (x,r)) )assume
m in {y,e1}
;
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, RLVECT_1:def 5
.=
((((1 - l) * (1 / 2)) * y) + ((1 - l) * ((1 / 2) * z))) + (l * z)
by RLVECT_1:def 7
.=
((((1 - l) * (1 / 2)) * y) + (((1 - l) * (1 / 2)) * z)) + (l * z)
by RLVECT_1:def 7
.=
(((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) * z) + (l * z))
by RLVECT_1:def 3
.=
(((1 - l) * (1 / 2)) * y) + ((((1 - l) * (1 / 2)) + l) * z)
by RLVECT_1:def 6
.=
((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;
verum
end; hereby TARSKI:def 3 ( ( 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
object ;
( m in (halfline (y,z)) /\ (Sphere (x,r)) implies b1 in {y,e1} )assume A21:
m in (halfline (y,z)) /\ (Sphere (x,r))
;
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;
per cases
( m in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) or not m in halfline ((((1 / 2) * y) + ((1 / 2) * z)),z) )
;
suppose A24:
not
m in halfline (
(((1 / 2) * y) + ((1 / 2) * z)),
z)
;
b1 in {y,e1}consider M being
Real such that A25:
m = ((1 - M) * y) + (M * z)
and A26:
0 <= M
by A22;
(
|.(z - x).| <= r &
|.(z - x).| <> r )
by A4, A8, Th6;
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, Th31;
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;
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;
verum end; end;