let n be Nat; for r, s, t being Real
for An, Bn, Cn being Point of (TOP-REAL n) st Bn <> Cn & Cn <> An & An <> Bn & not |((Cn - An),(Bn - Cn))| is zero & not |((Bn - Cn),(An - Bn))| is zero & not |((Cn - An),(An - Bn))| is zero & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & s = - ((((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|) / |((Cn - An),(Cn - An))|) & t = - ((((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|) / |((An - Bn),(An - Bn))|) holds
((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t) = 1
let r, s, t be Real; for An, Bn, Cn being Point of (TOP-REAL n) st Bn <> Cn & Cn <> An & An <> Bn & not |((Cn - An),(Bn - Cn))| is zero & not |((Bn - Cn),(An - Bn))| is zero & not |((Cn - An),(An - Bn))| is zero & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & s = - ((((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|) / |((Cn - An),(Cn - An))|) & t = - ((((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|) / |((An - Bn),(An - Bn))|) holds
((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t) = 1
let An, Bn, Cn be Point of (TOP-REAL n); ( Bn <> Cn & Cn <> An & An <> Bn & not |((Cn - An),(Bn - Cn))| is zero & not |((Bn - Cn),(An - Bn))| is zero & not |((Cn - An),(An - Bn))| is zero & r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) & s = - ((((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|) / |((Cn - An),(Cn - An))|) & t = - ((((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|) / |((An - Bn),(An - Bn))|) implies ((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t) = 1 )
assume that
A1:
Bn <> Cn
and
A2:
Cn <> An
and
A3:
An <> Bn
and
A4:
( not |((Cn - An),(Bn - Cn))| is zero & not |((Bn - Cn),(An - Bn))| is zero & not |((Cn - An),(An - Bn))| is zero )
and
A5:
r = - ((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|)
and
A6:
s = - ((((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|) / |((Cn - An),(Cn - An))|)
and
A7:
t = - ((((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|) / |((An - Bn),(An - Bn))|)
; ((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t) = 1
reconsider rA = An, rB = Bn, rC = Cn as Element of REAL n by EUCLID:22;
A8:
rB - rC <> 0* n
by A1, EUCLIDLP:9;
A9:
rC - rA <> 0* n
by A2, EUCLIDLP:9;
A10:
rA - rB <> 0* n
by A3, EUCLIDLP:9;
set rBC = |((Bn - Cn),(Bn - Cn))|;
set rCA = |((Cn - An),(Cn - An))|;
set rAB = |((An - Bn),(An - Bn))|;
set A = An;
set B = Bn;
set C = Cn;
A11: r * |((Bn - Cn),(Bn - Cn))| =
- (((((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|) / |((Bn - Cn),(Bn - Cn))|) * |((Bn - Cn),(Bn - Cn))|)
by A5
.=
- (((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|)
by A8, EUCLID_4:17, XCMPLX_1:87
;
r / (1 - r) =
((r / (1 - r)) * |((Bn - Cn),(Bn - Cn))|) / |((Bn - Cn),(Bn - Cn))|
by A8, EUCLID_4:17, XCMPLX_1:89
.=
((r * |((Bn - Cn),(Bn - Cn))|) / (1 - r)) / |((Bn - Cn),(Bn - Cn))|
.=
(r * |((Bn - Cn),(Bn - Cn))|) / ((1 - r) * |((Bn - Cn),(Bn - Cn))|)
by XCMPLX_1:78
.=
(- (((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|)) / ((((|((Bn - Cn),(Bn - Cn))| + |(Bn,Cn)|) - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|)
by A11
;
then A12: r / (1 - r) =
(- |((Cn - An),(Bn - Cn))|) / (|((Bn - Cn),(Bn - Cn))| + (((|(Bn,Cn)| - |(Cn,Cn)|) - |(An,Bn)|) + |(An,Cn)|))
by Th13
.=
(- |((Cn - An),(Bn - Cn))|) / (|((Bn - Cn),(Bn - Cn))| + |((Cn - An),(Bn - Cn))|)
by Th13
.=
(- |((Cn - An),(Bn - Cn))|) / |((Bn - Cn),(Bn - An))|
by Th13
;
A13: s * |((Cn - An),(Cn - An))| =
- (((((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|) / |((Cn - An),(Cn - An))|) * |((Cn - An),(Cn - An))|)
by A6
.=
- (((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|)
by A9, EUCLID_4:17, XCMPLX_1:87
;
s / (1 - s) =
((s / (1 - s)) * |((Cn - An),(Cn - An))|) / |((Cn - An),(Cn - An))|
by A9, EUCLID_4:17, XCMPLX_1:89
.=
((s * |((Cn - An),(Cn - An))|) / (1 - s)) / |((Cn - An),(Cn - An))|
.=
(s * |((Cn - An),(Cn - An))|) / ((1 - s) * |((Cn - An),(Cn - An))|)
by XCMPLX_1:78
.=
(- (((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|)) / (|((Cn - An),(Cn - An))| + (((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|))
by A13
;
then A14: s / (1 - s) =
(- |((Cn - An),(An - Bn))|) / (|((Cn - An),(Cn - An))| + (((|(Cn,An)| - |(An,An)|) - |(Bn,Cn)|) + |(Bn,An)|))
by Th13
.=
(- |((Cn - An),(An - Bn))|) / (|((Cn - An),(Cn - An))| + |((Cn - An),(An - Bn))|)
by Th13
.=
(- |((Cn - An),(An - Bn))|) / |((Cn - An),(Cn - Bn))|
by Th13
;
A15: t * |((An - Bn),(An - Bn))| =
- (((((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|) / |((An - Bn),(An - Bn))|) * |((An - Bn),(An - Bn))|)
by A7
.=
- (((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|)
by A10, EUCLID_4:17, XCMPLX_1:87
;
t / (1 - t) =
((t / (1 - t)) * |((An - Bn),(An - Bn))|) / |((An - Bn),(An - Bn))|
by A10, EUCLID_4:17, XCMPLX_1:89
.=
((t * |((An - Bn),(An - Bn))|) / (1 - t)) / |((An - Bn),(An - Bn))|
.=
(t * |((An - Bn),(An - Bn))|) / ((1 - t) * |((An - Bn),(An - Bn))|)
by XCMPLX_1:78
.=
(- (((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|)) / (|((An - Bn),(An - Bn))| + (((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|))
by A15
;
then A16: t / (1 - t) =
(- |((An - Bn),(Bn - Cn))|) / (|((An - Bn),(An - Bn))| + (((|(An,Bn)| - |(Bn,Bn)|) - |(Cn,An)|) + |(Cn,Bn)|))
by Th13
.=
(- |((An - Bn),(Bn - Cn))|) / (|((An - Bn),(An - Bn))| + |((An - Bn),(Bn - Cn))|)
by Th13
.=
(- |((An - Bn),(Bn - Cn))|) / |((An - Bn),(An - Cn))|
by Th13
;
((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t) =
(((- |((Cn - An),(Bn - Cn))|) / |((Bn - Cn),(Bn - An))|) * ((- |((Cn - An),(An - Bn))|) / |((Cn - An),(Cn - Bn))|)) * ((- |((An - Bn),(Bn - Cn))|) / |((An - Bn),(An - Cn))|)
by A12, A14, A16
.=
(((- |((Cn - An),(Bn - Cn))|) / (- |((Bn - Cn),(An - Bn))|)) * ((- |((Cn - An),(An - Bn))|) / |((Cn - An),(Cn - Bn))|)) * ((- |((An - Bn),(Bn - Cn))|) / |((An - Bn),(An - Cn))|)
by Th14
.=
(((- |((Cn - An),(Bn - Cn))|) / (- |((Bn - Cn),(An - Bn))|)) * ((- |((Cn - An),(An - Bn))|) / (- |((Cn - An),(Bn - Cn))|))) * ((- |((An - Bn),(Bn - Cn))|) / |((An - Bn),(An - Cn))|)
by Th14
.=
(((- |((Cn - An),(Bn - Cn))|) / (- |((Bn - Cn),(An - Bn))|)) * ((- |((Cn - An),(An - Bn))|) / (- |((Cn - An),(Bn - Cn))|))) * ((- |((Bn - Cn),(An - Bn))|) / (- |((Cn - An),(An - Bn))|))
by Th14
.=
1
by A4, Th3
;
hence
((((r / (1 - r)) * s) / (1 - s)) * t) / (1 - t) = 1
; verum