A1: MetrStruct(# the U1 of TarskiEuclid2Space, the distance of TarskiEuclid2Space #) = MetrStruct(# the U1 of (Euclid 2), the distance of (Euclid 2) #) by GTARSKI1:def 13;
let a, q, b, c be POINT of TarskiEuclid2Space; :: according to GTARSKI1:def 8 :: thesis: ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c )
per cases ( a = q or a <> q ) ;
suppose A1bis: a = q ; :: thesis: ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c )
now :: thesis: ex x being POINT of TarskiEuclid2Space st
( between q,a,x & a,x equiv b,c )
set alpha = |.((Tn2TR b) - (Tn2TR c)).|;
reconsider P = |[|.((Tn2TR b) - (Tn2TR c)).|,0]| as Element of (TOP-REAL 2) ;
reconsider x = |[(((Tn2TR a) `1) + |.((Tn2TR b) - (Tn2TR c)).|),((Tn2TR a) `2)]| as POINT of TarskiEuclid2Space by A1, EUCLID:67;
A2: ( (Tn2TR x) `1 = ((Tn2TR a) `1) + |.((Tn2TR b) - (Tn2TR c)).| & (Tn2TR x) `2 = (Tn2TR a) `2 ) by EUCLID:52;
A3: |.((Tn2TR a) - (Tn2TR x)).| = dist (a,x) by ThEquiv
.= sqrt (((((Tn2TR a) `1) - (((Tn2TR a) `1) + |.((Tn2TR b) - (Tn2TR c)).|)) ^2) + ((((Tn2TR a) `2) - ((Tn2TR a) `2)) ^2)) by A2, ThConv2
.= sqrt (((0 - |.((Tn2TR b) - (Tn2TR c)).|) ^2) + (0 * 0)) by SQUARE_1:def 1
.= sqrt (|.((Tn2TR b) - (Tn2TR c)).| ^2) by SQUARE_1:3
.= |.((Tn2TR b) - (Tn2TR c)).| by SQUARE_1:22 ;
take x = x; :: thesis: ( between q,a,x & a,x equiv b,c )
thus between q,a,x by A1bis, ThConv7; :: thesis: a,x equiv b,c
thus a,x equiv b,c by A3, ThConv4; :: thesis: verum
end;
hence ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c ) ; :: thesis: verum
end;
suppose A4: a <> q ; :: thesis: ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c )
A5: ( b = c implies ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c ) )
proof
assume A6: b = c ; :: thesis: ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c )
set x = a;
thus ex x being POINT of TarskiEuclid2Space st
( between q,a,x & a,x equiv b,c ) :: thesis: verum
proof
take a ; :: thesis: ( between q,a,a & a,a equiv b,c )
A7: Tn2R a = Tn2R a ;
Tn2R b = Tn2R c by A6;
then |.((Tn2TR b) - (Tn2TR c)).| = 0 ;
then |.((Tn2TR a) - (Tn2TR a)).| = |.((Tn2TR b) - (Tn2TR c)).| by A7;
hence ( between q,a,a & a,a equiv b,c ) by ThConv7, ThConv4; :: thesis: verum
end;
end;
( b <> c implies ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c ) )
proof
assume b <> c ; :: thesis: ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c )
then Tn2R b <> Tn2R c ;
then reconsider alpha = |.((Tn2TR b) - (Tn2TR c)).| as positive Real by EUCLID:17;
Tn2R a <> Tn2R q by A4;
then reconsider mu = |.((Tn2TR a) - (Tn2TR q)).| as positive Real by EUCLID:17;
reconsider nu = alpha / mu as positive Real ;
reconsider y = |[(((Tn2TR a) `1) + (nu * (((Tn2TR a) `1) - ((Tn2TR q) `1)))),(((Tn2TR a) `2) + (nu * (((Tn2TR a) `2) - ((Tn2TR q) `2))))]| as POINT of TarskiEuclid2Space by A1, EUCLID:67;
reconsider x = (Tn2TR a) + (nu * ((Tn2TR a) - (Tn2TR q))) as POINT of TarskiEuclid2Space by A1, EUCLID:67;
ex x being POINT of TarskiEuclid2Space st
( between q,a,x & a,x equiv b,c )
proof
take x ; :: thesis: ( between q,a,x & a,x equiv b,c )
reconsider t1 = - (nu * ((Tn2TR a) - (Tn2TR q))), t2 = Tn2TR a as Element of 2 -tuples_on REAL by EUCLID:22;
(Tn2TR a) - (Tn2TR x) = (Tn2TR a) + ((- (Tn2TR a)) + (- (nu * ((Tn2TR a) - (Tn2TR q))))) by RVSUM_1:26
.= (t1 + t2) - t2 by RVSUM_1:15
.= - (nu * ((Tn2TR a) - (Tn2TR q))) by RVSUM_1:42 ;
then A8: |.((Tn2TR a) - (Tn2TR x)).| = |.(nu * ((Tn2TR a) - (Tn2TR q))).| by EUCLID:10
.= |.nu.| * |.((Tn2TR a) - (Tn2TR q)).| by EUCLID:11
.= (alpha / mu) * mu by COMPLEX1:43
.= alpha by XCMPLX_1:87 ;
reconsider aq = (Tn2TR a) - (Tn2TR q), qa = (Tn2TR q) - (Tn2TR a) as Element of 2 -tuples_on REAL by EUCLID:22;
A9: (Tn2TR q) - (Tn2TR x) = (Tn2TR q) + ((- (Tn2TR a)) + (- (nu * ((Tn2TR a) - (Tn2TR q))))) by RVSUM_1:26
.= (- (nu * ((Tn2TR a) - (Tn2TR q)))) + ((- (- (Tn2TR q))) + (- (Tn2TR a))) by RVSUM_1:15
.= (- (nu * ((Tn2TR a) - (Tn2TR q)))) - ((- (Tn2TR q)) + (Tn2TR a)) by RVSUM_1:26
.= (((- 1) * nu) * aq) + ((- 1) * aq) by RVSUM_1:49
.= ((- 1) - nu) * ((Tn2TR a) - (Tn2TR q)) by RVSUM_1:50 ;
|.((Tn2TR q) - (Tn2TR x)).| = |.(- (1 + nu)).| * |.((Tn2TR a) - (Tn2TR q)).| by A9, EUCLID:11
.= |.(1 + nu).| * |.((Tn2TR a) - (Tn2TR q)).| by COMPLEX1:52
.= (1 + nu) * |.((Tn2TR a) - (Tn2TR q)).| by COMPLEX1:43
.= mu + ((alpha / mu) * mu)
.= mu + alpha by XCMPLX_1:87 ;
then |.((Tn2TR q) - (Tn2TR x)).| = |.((Tn2R q) - (Tn2R a)).| + |.((Tn2TR a) - (Tn2TR x)).| by A8, EUCLID:18
.= |.((Tn2TR q) - (Tn2TR a)).| + |.((Tn2TR a) - (Tn2TR x)).| ;
then Tn2TR a in LSeg ((Tn2TR q),(Tn2TR x)) by EUCLID12:11;
hence ( between q,a,x & a,x equiv b,c ) by ThConv6, A8, ThConv4; :: thesis: verum
end;
hence ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c ) ; :: thesis: verum
end;
hence ex b1 being Element of the U1 of TarskiEuclid2Space st
( between q,a,b1 & a,b1 equiv b,c ) by A5; :: thesis: verum
end;
end;