Copyright (c) 1992 Association of Mizar Users
environ
vocabulary PRE_TOPC, EUCLID, FINSEQ_1, ARYTM, ARYTM_1, ARYTM_3, METRIC_1,
RELAT_1, MCART_1, FUNCT_1, SQUARE_1, RVSUM_1, ABSVALUE, COMPLEX1,
RLVECT_1, TOPREAL1, BOOLE, TARSKI, FINSEQ_2, FINSEQ_4;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, RELAT_1, FUNCT_1, STRUCT_0, FINSEQ_1, FUNCT_2, BINOP_1,
PRE_TOPC, ABSVALUE, SQUARE_1, FINSEQ_2, FINSEQ_4, METRIC_1, FINSEQOP,
RVSUM_1, EUCLID, TOPREAL1;
constructors REAL_1, NAT_1, ABSVALUE, SQUARE_1, FINSEQOP, TOPREAL1, FINSEQ_4,
INT_1, SEQ_1, MEMBERED, PARTFUN1, XBOOLE_0;
clusters FUNCT_1, RELSET_1, STRUCT_0, EUCLID, XREAL_0, FINSEQ_1, INT_1,
MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, TOPREAL1, FUNCT_1, XBOOLE_0;
theorems TARSKI, AXIOMS, REAL_1, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE,
SEQ_2, SQUARE_1, FINSEQ_2, METRIC_1, RVSUM_1, REAL_2, EUCLID, TOPREAL1,
FINSEQ_3, FINSEQ_4, CQC_THE1, PROB_1, GROUP_5, PARTFUN2, TBSP_1, RELAT_1,
INT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
begin
reserve p,p1,p2,p3,p11,p22,q,q1,q2 for Point of TOP-REAL 2,
f,h for FinSequence of TOP-REAL 2,
r,r1,r2,s,s1,s2 for real number,
u,u1,u2,u5 for Point of Euclid 2,
n,m,i,j,k for Nat,
x,y,z for set;
:::::::::::::::::::::::::::::
:: Real numbers preliminaries
:::::::::::::::::::::::::::::
canceled 2;
theorem Th3:
r<s implies r < (r+s)/2 & (r+s)/2 < s
proof assume
r<s;
then A1: r/2 < s/2 by REAL_1:73;
then r/2 + r/2 < r/2 + s/2 by REAL_1:53;
then r < r/2 + s/2 by XCMPLX_1:66;
hence r < (r+s)/2 by XCMPLX_1:63;
r/2 + s/2 < s/2 + s/2 by A1,REAL_1:53;
then r/2 + s/2 < s by XCMPLX_1:66;
hence thesis by XCMPLX_1:63;
end;
Lm1: the carrier of Euclid n = REAL n
proof
Euclid n = MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7;
hence thesis;
end;
begin
:::::::::::::::::::::::::::::::::::
:: Properties of sets in TOP-REAL 2
:::::::::::::::::::::::::::::::::::
canceled 2;
theorem Th6:
1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*>
proof
len (<* x,y,z *>) = 3 by FINSEQ_1:62;
hence thesis by FINSEQ_3:27;
end;
theorem Th7:
(p1+p2)`1 = p1`1 + p2`1 & (p1+p2)`2 = p1`2 + p2`2
proof
p1 + p2 = |[ p1`1 + p2`1, p1`2 + p2`2]| by EUCLID:59;
hence thesis by EUCLID:56;
end;
theorem
(p1-p2)`1 = p1`1 - p2`1 & (p1-p2)`2 = p1`2 - p2`2
proof
p1 - p2 = |[ p1`1 - p2`1, p1`2 - p2`2]| by EUCLID:65;
hence thesis by EUCLID:56;
end;
theorem Th9:
(r*p)`1 = r*(p`1) & (r*p)`2 = r*(p`2)
proof
r*p = |[r*p`1,r*p`2]| by EUCLID:61;
hence thesis by EUCLID:56;
end;
theorem Th10:
p1=<*r1,s1*> & p2=<*r2,s2*> implies p1+p2=<*r1+r2,s1+s2*> &
p1-p2=<*r1-r2,s1-s2*>
proof
assume A1: p1=<*r1,s1*> & p2=<*r2,s2*>;
A2: p1+p2 = |[p1`1+p2`1,p1`2+p2`2]| & p1-p2 = |[p1`1-p2`1,p1`2-p2`2]|
by EUCLID:59,65;
|[r1,s1]|=<*r1,s1*> & |[r2,s2]|=<*r2,s2*> &
|[r1,s1]|`1=r1 & |[r1,s1]|`2=s1 & |[r2,s2]|`1=r2 & |[r2,s2]|`2=s2
by EUCLID:56,def 16;
hence thesis by A1,A2,EUCLID:def 16;
end;
theorem Th11:
p`1 = q`1 & p`2 = q`2 implies p=q
proof
assume p`1 = q`1 & p`2 = q`2;
hence p=|[q`1,q`2]| by EUCLID:57
.= q by EUCLID:57;
end;
theorem Th12:
u1 = p1 & u2 = p2 implies
(Pitag_dist 2).(u1,u2) = sqrt ((p1`1 - p2`1)^2 + (p1`2 - p2`2)^2)
proof assume
A1: u1 = p1 & u2 = p2;
p1 = |[p1`1,p1`2]| by EUCLID:57;
then A2: u1 = <* p1`1,p1`2 *> by A1,EUCLID:def 16;
p2 = |[p2`1,p2`2]| by EUCLID:57;
then A3: u2 = <* p2`1,p2`2 *> by A1,EUCLID:def 16;
Euclid 2 = MetrStruct(# REAL 2,Pitag_dist 2 #) by EUCLID:def 7;
then reconsider v1 = u1, v2 = u2 as Element of REAL 2;
A4: v1-v2= diffreal.:(v1,v2) by RVSUM_1:def 6
.= <* diffreal.(p1`1,p2`1), diffreal.(p1`2,p2`2) *> by A2,A3,FINSEQ_2:89
.= <* p1`1 - p2`1, diffreal.(p1`2,p2`2) *> by RVSUM_1:9
.= <* p1`1 - p2`1,p1`2 - p2`2*> by RVSUM_1:9;
A5: abs (v1-v2) = absreal * (v1-v2) by EUCLID:def 3
.= <* absreal.(p1`1-p2`1),absreal.(p1`2-p2`2) *> by A4,FINSEQ_2:40
.= <* abs( p1`1-p2`1 ),absreal.(p1`2-p2`2) *> by EUCLID:def 2
.= <* abs( p1`1-p2`1 ),abs( p1`2-p2`2) *> by EUCLID:def 2;
A6: sqr abs (v1-v2) = sqrreal *(abs (v1-v2)) by RVSUM_1:def 8
.= <* sqrreal.(abs( p1`1 - p2`1 )),sqrreal.(abs( p1`2-p2`2 )) *>
by A5,FINSEQ_2:40
.= <* (abs( p1`1 - p2`1 ))^2,sqrreal.(abs( p1`2-p2`2 )) *>
by RVSUM_1:def 2
.= <* (abs( p1`1 - p2`1 ))^2,(abs(p1`2-p2`2))^2 *> by RVSUM_1:def 2
.= <* (p1`1 - p2`1)^2,(abs(p1`2-p2`2))^2 *> by SQUARE_1:62
.= <* (p1`1-p2`1)^2,(p1`2 - p2`2)^2 *> by SQUARE_1:62;
(Pitag_dist 2).(u1,u2) = |.v1 - v2.| by EUCLID:def 6
.= sqrt Sum sqr (v1-v2) by EUCLID:def 5
.= sqrt Sum sqr abs (v1-v2) by EUCLID:29;
hence thesis by A6,RVSUM_1:107;
end;
theorem Th13:
the carrier of TOP-REAL n = the carrier of Euclid n
proof
thus the carrier of TOP-REAL n = REAL n by EUCLID:25
.= the carrier of Euclid n by Lm1;
end;
reserve r,r1,r2,lambda,s,s1,s2 for Real;
canceled;
theorem Th15:
r1 < s1 implies {p1: p1`1=r & r1<=p1`2 & p1`2<=s1} = LSeg(|[r,r1]|,|[r,s1]|)
proof assume
A1: r1 < s1;
set L = { p3 : p3`1 = r & r1 <= p3`2 & p3`2 <= s1},
p = |[ r,r1 ]|,
q = |[ r,s1 ]|;
A2: p`1 = r & p`2 = r1 by EUCLID:56;
A3: q`1 = r & q`2 = s1 by EUCLID:56;
A4: s1 - r1 > 0 by A1,SQUARE_1:11;
thus L c= LSeg(p,q)
proof let x; assume x in L; then consider p2 such that
A5: x = p2 & p2`1 = r & r1 <= p2`2 & p2`2 <= s1;
set t = p2`2,
l = (t - r1)/(s1-r1);
t - r1 <= s1 - r1 by A5,REAL_1:49;
then l <= (s1-r1)/(s1-r1) & (s1-r1) <> 0 by A4,REAL_1:73;
then A6: l <= 1 by XCMPLX_1:60;
r1 - r1 <= t - r1 & r1-r1=0 by A5,REAL_1:49,XCMPLX_1:14;
then A7: 0/(s1-r1) <= l & (s1-r1) <> 0 by A4,REAL_1:73;
A8: ((1-l)*p + l*q)`1 = ((1-l)*p)`1 + (l*q)`1 by Th7
.= (1-l)* (p`1) + (l*q)`1 by Th9
.= (1-l)*r + l*r by A2,A3,Th9
.= (1-l+l)*r by XCMPLX_1:8
.= 1*r by XCMPLX_1:27
.= p2`1 by A5;
A9: 1-l = (1*(s1-r1) -(t-r1))/(s1-r1) by A4,XCMPLX_1:128
.= (s1 - t)/(s1-r1) by XCMPLX_1:22;
((1-l)*p + l*q)`2 = ((1-l)*p)`2 + (l*q)`2 by Th7
.= (1-l)* (p`2) + (l*q)`2 by Th9
.= (1-l)*(p`2) + l*(q`2) by Th9
.= (s1-t)*(p`2)/(s1-r1) + l*(q`2) by A9,XCMPLX_1:75
.= (s1-t)*(p`2)/(s1-r1) + (t-r1)*(q`2)/(s1-r1) by XCMPLX_1:75
.= ((s1-t)*r1 + (t-r1)*s1)/(s1-r1) by A2,A3,XCMPLX_1:63
.= (s1 * r1 - t*r1 + (t-r1)*s1)/(s1-r1) by XCMPLX_1:40
.= (s1 * r1 - t*r1 + (t*s1 -r1 * s1))/(s1-r1) by XCMPLX_1:40
.= (s1 * r1 - t*r1 - (r1*s1 -t*s1))/(s1-r1) by XCMPLX_1:38
.= (s1 * r1 - t*r1 - r1*s1 +t*s1)/(s1-r1) by XCMPLX_1:37
.= (s1 * r1 +- t*r1 - s1*r1 +t*s1)/(s1-r1) by XCMPLX_0:def 8
.= (-t*r1 +t*s1)/(s1-r1) by XCMPLX_1:26
.= (t*s1 - t*r1)/(s1-r1) by XCMPLX_0:def 8
.= t*(s1 - r1)/(s1-r1) by XCMPLX_1:40
.= t*((s1 - r1)/(s1-r1)) by XCMPLX_1:75
.= t*1 by A4,XCMPLX_1:60
.= p2`2;
then p2 = (1-l)*p + l*q by A8,Th11;
then x in {(1-lambda)*p + lambda*q: 0 <= lambda & lambda <= 1 } by A5,A6,A7
;
hence x in LSeg(|[ r,r1 ]|,|[ r,s1 ]|) by TOPREAL1:def 4;
end;
let x; assume x in LSeg(p,q);
then x in {(1-lambda)*p + lambda*q: 0 <= lambda & lambda <= 1 } by TOPREAL1:
def 4;
then consider lambda such that
A10: (1-lambda)*p + lambda*q = x & 0 <= lambda & lambda <= 1;
set p2 = (1-lambda)*p + lambda*q;
A11: p2 `1 = ((1-lambda)*p)`1 + (lambda*q)`1 by Th7
.= (1-lambda)*(p`1) + (lambda*q)`1 by Th9
.= (1-lambda)*r + lambda*r by A2,A3,Th9
.= (1-lambda+lambda)*r by XCMPLX_1:8
.= 1*r by XCMPLX_1:27;
A12: p2 `2 = ((1-lambda)*p)`2 + (lambda*q)`2 by Th7
.= (1-lambda)*(p`2) + (lambda*q)`2 by Th9
.= (1-lambda)*r1 + lambda*s1 by A2,A3,Th9
.= 1*r1-lambda*r1 + lambda*s1 by XCMPLX_1:40
.= r1+lambda*s1 - lambda*r1 by XCMPLX_1:29
.= r1+(lambda*s1 - lambda*r1) by XCMPLX_1:29
.= r1+lambda*(s1 - r1) by XCMPLX_1:40;
0 * (s1-r1)<=lambda*(s1-r1) by A4,A10,AXIOMS:25;
then A13: r1+0<=r1+lambda*(s1-r1) by REAL_1:55;
lambda*(s1-r1)<= 1*(s1-r1) by A4,A10,AXIOMS:25;
then r1+lambda*(s1-r1)<=s1-r1+r1 by REAL_1:55;
then p2 `2 <= s1 by A12,XCMPLX_1:27;
hence x in L by A10,A11,A12,A13;
end;
theorem Th16:
r1 < s1 implies {p1: p1`2=r & r1<=p1 `1 & p1 `1<=s1} = LSeg(|[r1,r]|,|[s1,r]|)
proof assume
A1: r1 < s1;
set L = {p3 : p3`2 = r & r1 <= p3`1 & p3`1 <= s1},
p = |[ r1,r]|,
q = |[ s1,r]|;
A2: p`1 = r1 & p`2 = r by EUCLID:56;
A3: q`1 = s1 & q`2 = r by EUCLID:56;
A4: s1 - r1 > 0 by A1,SQUARE_1:11;
thus L c= LSeg(p,q)
proof let x; assume x in L; then consider p2 such that
A5: x = p2 & p2`2 = r & r1 <= p2`1 & p2`1 <= s1;
set t = p2`1,
l = (t - r1)/(s1-r1);
t - r1 <= s1 - r1 by A5,REAL_1:49;
then l <= (s1-r1)/(s1-r1) & (s1-r1) <> 0 by A4,REAL_1:73;
then A6: l <= 1 by XCMPLX_1:60;
r1 - r1 <= t - r1 & r1-r1=0 by A5,REAL_1:49,XCMPLX_1:14;
then A7: 0/(s1-r1) <= l & (s1-r1) <> 0 by A4,REAL_1:73;
A8: ((1-l)*p + l*q)`2 = ((1-l)*p)`2 + (l*q)`2 by Th7
.= (1-l)* (p`2) + (l*q)`2 by Th9
.= (1-l)*r + l*r by A2,A3,Th9
.= (1-l+l)*r by XCMPLX_1:8
.= 1*r by XCMPLX_1:27
.= p2`2 by A5;
A9: 1-l = (1*(s1-r1) -(t-r1))/(s1-r1) by A4,XCMPLX_1:128
.= (s1 - t)/(s1-r1) by XCMPLX_1:22;
((1-l)*p + l*q)`1 = ((1-l)*p)`1 + (l*q)`1 by Th7
.= (1-l)* (p`1) + (l*q)`1 by Th9
.= (1-l)*(p`1) + l*(q`1) by Th9
.= (s1-t)*(p`1)/(s1-r1) + l*(q`1) by A9,XCMPLX_1:75
.= (s1-t)*(p`1)/(s1-r1) + (t-r1)*(q`1)/(s1-r1) by XCMPLX_1:75
.= ((s1-t)*r1 + (t-r1)*s1)/(s1-r1) by A2,A3,XCMPLX_1:63
.= (s1 * r1 - t*r1 + (t-r1)*s1)/(s1-r1) by XCMPLX_1:40
.= (s1 * r1 - t*r1 + (t*s1 -r1 * s1))/(s1-r1) by XCMPLX_1:40
.= (s1 * r1 - t*r1 - (r1*s1 -t*s1))/(s1-r1) by XCMPLX_1:38
.= (s1 * r1 - t*r1 - r1*s1 +t*s1)/(s1-r1) by XCMPLX_1:37
.= (s1 * r1 +- t*r1 - s1*r1 +t*s1)/(s1-r1) by XCMPLX_0:def 8
.= (-t*r1 +t*s1)/(s1-r1) by XCMPLX_1:26
.= (t*s1 - t*r1)/(s1-r1) by XCMPLX_0:def 8
.= t*(s1 - r1)/(s1-r1) by XCMPLX_1:40
.= t*((s1 - r1)/(s1-r1)) by XCMPLX_1:75
.= t*1 by A4,XCMPLX_1:60
.= p2`1;
then p2 = (1-l)*p + l*q by A8,Th11;
then x in {(1-lambda)*p + lambda*q: 0 <= lambda & lambda <= 1 } by A5,A6,A7
;
hence x in LSeg(|[r1,r]|,|[s1,r]|) by TOPREAL1:def 4;
end;
let x; assume x in LSeg(p,q);
then x in {(1-lambda)*p + lambda*q: 0 <= lambda & lambda <= 1 } by TOPREAL1:
def 4;
then consider lambda such that
A10: (1-lambda)*p + lambda*q = x & 0 <= lambda & lambda <= 1;
set p2 = (1-lambda)*p + lambda*q;
A11: p2 `2 = ((1-lambda)*p)`2 + (lambda*q)`2 by Th7
.= (1-lambda)*(p`2) + (lambda*q)`2 by Th9
.= (1-lambda)*r + lambda*r by A2,A3,Th9
.= (1-lambda+lambda)*r by XCMPLX_1:8
.= 1*r by XCMPLX_1:27
.= r;
A12: p2 `1 = ((1-lambda)*p)`1 + (lambda*q)`1 by Th7
.= (1-lambda)*(p`1) + (lambda*q)`1 by Th9
.= (1-lambda)*r1 + lambda*s1 by A2,A3,Th9
.= 1*r1-lambda*r1 + lambda*s1 by XCMPLX_1:40
.= r1+lambda*s1 - lambda*r1 by XCMPLX_1:29
.= r1+(lambda*s1 - lambda*r1) by XCMPLX_1:29
.= r1+lambda*(s1 - r1) by XCMPLX_1:40;
0 * (s1-r1)<=lambda*(s1-r1) by A4,A10,AXIOMS:25;
then A13: r1+0<=r1+lambda*(s1-r1) by REAL_1:55;
lambda*(s1-r1)<= 1*(s1-r1) by A4,A10,AXIOMS:25;
then r1+lambda*(s1-r1)<=s1-r1+r1 by REAL_1:55;
then p2 `1 <= s1 by A12,XCMPLX_1:27;
hence x in L by A10,A11,A12,A13;
end;
theorem
p in LSeg(|[r,r1]|,|[r,s1]|) implies p`1 = r
proof assume
A1: p in LSeg(|[r,r1]|,|[r,s1]|);
per cases by AXIOMS:21;
suppose r1<s1;
then LSeg(|[r,r1]|,|[r,s1]|) = {q: q`1 = r & r1<=q`2 & q`2<=s1} by Th15;
then ex p1 st p1=p & p1`1 = r & r1<=p1`2 & p1`2<=s1 by A1;
hence p`1=r;
suppose r1=s1; then p in {|[r,r1]|} by A1,TOPREAL1:7;
then p = |[r,r1]| by TARSKI:def 1;
hence p`1 = r by EUCLID:56;
suppose r1>s1;
then LSeg(|[r,r1]|,|[r,s1]|) = {q: q`1 = r & s1<=q`2 & q`2<=r1} by Th15;
then ex p1 st p1=p & p1`1 = r & s1<=p1`2 & p1`2<=r1 by A1;
hence p`1=r;
end;
theorem
p in LSeg(|[r1,r]|,|[s1,r]|) implies p`2 = r
proof assume
A1: p in LSeg(|[r1,r]|,|[s1,r]|);
per cases by AXIOMS:21;
suppose r1<s1;
then LSeg(|[r1,r]|,|[s1,r]|) = {q: q`2 = r & r1<=q`1 & q`1<=s1} by Th16;
then ex p1 st p1=p & p1`2 = r & r1<=p1`1 & p1`1<=s1 by A1;
hence p`2=r;
suppose r1=s1; then p in {|[r1,r]|} by A1,TOPREAL1:7;
then p = |[r1,r]| by TARSKI:def 1;
hence p`2 = r by EUCLID:56;
suppose r1>s1;
then LSeg(|[r1,r]|,|[s1,r]|) = {q: q`2 = r & s1<=q`1 & q`1<=r1} by Th16
;
then ex p1 st p1=p & p1`2 = r & s1<=p1`1 & p1`1<=r1 by A1;
hence p`2=r;
end;
theorem
p`1 <> q`1 & p`2 = q`2 implies |[(p`1+q`1)/2,p`2]| in LSeg(p,q)
proof
set p1 = |[(p`1+q`1)/2,p`2]|; assume
A1: p`1 <> q`1 & p`2 = q`2;
then A2: p = |[p`1,p`2]| & q = |[q`1,p`2]| &
p1`1 = (p`1+q`1)/2 & p1`2 = p`2 by EUCLID:56,57;
per cases by A1,REAL_1:def 5;
suppose A3: p`1 < q`1;
then p`1 <= (p`1+q`1)/2 & (p`1+q`1)/2 <= q`1 by Th3;
then p1 in {p2: p2`2 = p`2 & p`1 <= p2`1 & p2`1 <= q`1} by A2;
hence thesis by A2,A3,Th16;
suppose A4: p`1 > q`1;
then q`1 <= (p`1+q`1)/2 & (p`1+q`1)/2 <= p`1 by Th3;
then p1 in {p2: p2`2 = p`2 & q`1 <= p2`1 & p2`1 <= p`1} by A2;
hence thesis by A2,A4,Th16;
end;
theorem
p`1 = q`1 & p`2 <> q`2 implies |[p`1,(p`2+q`2)/2]| in LSeg(p,q)
proof
set p1 = |[p`1,(p`2+q`2)/2]|; assume
A1: p`1 = q`1 & p`2 <> q`2;
then A2: p = |[p`1,p`2]| & q = |[p`1,q`2]| by EUCLID:57;
A3: p1`1 = p`1 & p1`2 = (p`2+q`2)/2 by EUCLID:56;
per cases by A1,REAL_1:def 5;
suppose A4: p`2 < q`2;
then p`2 <= (p`2+q`2)/2 & (p`2+q`2)/2 <= q`2 by Th3;
then p1 in {p2: p2`1 = p`1 & p`2 <= p2`2 & p2`2 <= q`2} by A3;
hence thesis by A2,A4,Th15;
suppose A5: p`2 > q`2;
then q`2 <= (p`2+q`2)/2 & (p`2+q`2)/2 <= p`2 by Th3;
then p1 in {p2: p2`1 = p`1 & q`2 <= p2`2 & p2`2 <= p`2} by A3;
hence thesis by A2,A5,Th15;
end;
theorem Th21:
f = <* p,p1,q *> & i<>0 & j>i+1 implies LSeg(f,j) = {}
proof assume
A1: f = <* p,p1,q *> & i<>0 & j>i+1;
then i>0 by NAT_1:19; then i>=0+1 by NAT_1:38;
then 1+i>=1+1 & j>1+i by A1,REAL_1:55;
then j>2 by AXIOMS:22; then j>=2+1 by NAT_1:38;
then j+1 > 3 & len f = 3 by A1,FINSEQ_1:62,NAT_1:38;
hence thesis by TOPREAL1:def 5;
end;
canceled;
theorem
f = <* p1,p2,p3 *> implies L~f = LSeg(p1,p2) \/ LSeg(p2,p3)
proof
set M = {LSeg(f,i) : 1 <= i & i+1 <= len f };
assume
A1: f = <* p1,p2,p3 *>;
then A2: len f = 2+1 & f/.1=p1 & f/.2=p2 & f/.3=p3
by FINSEQ_1:62,FINSEQ_4:27;
A3: 1+1 in dom f by A1,Th6;
A4: M = {LSeg(p1,p2),LSeg(p2,p3)}
proof
thus M c= {LSeg(p1,p2),LSeg(p2,p3)}
proof
let x; assume x in M; then consider j such that
A5: x = LSeg(f,j) & 1<=j & j+1<=len f;
A6: j <= 2 & j > 0 by A2,A5,AXIOMS:22,REAL_1:53;
per cases by A6,CQC_THE1:3;
suppose j=1;
then x = LSeg(p1,p2) by A2,A5,TOPREAL1:def 5;
hence x in {LSeg(p1,p2),LSeg(p2,p3)} by TARSKI:def 2;
suppose j=2;
then x = LSeg(p2,p3) by A2,A5,TOPREAL1:def 5;
hence x in {LSeg(p1,p2),LSeg(p2,p3)} by TARSKI:def 2;
end;
let x such that A7: x in {LSeg(p1,p2),LSeg(p2,p3)};
per cases by A7,TARSKI:def 2;
suppose x = LSeg(p1,p2);
then A8: x=LSeg(f,1) by A2,A3,TOPREAL1:def 5;
1+1 <= len f by A2;
hence thesis by A8;
suppose x = LSeg(p2,p3);
then x=LSeg(f,2) by A2,TOPREAL1:def 5;
hence thesis by A2;
end;
thus L~f = union M by TOPREAL1:def 6
.= LSeg(p1,p2) \/ LSeg(p2,p3) by A4,ZFMISC_1:93;
end;
theorem Th24:
i in dom f & j in dom(f|i) & j+1 in dom(f|i) implies LSeg(f,j) = LSeg(f|i,j)
proof assume
A1: i in dom f & j in dom(f|i) & j+1 in dom(f|i);
set p1 = (f|i)/.j, p2 = (f|i)/.(j+1);
A2: f|i = f|(Seg i) by TOPREAL1:def 1;
A3: p1 = f/.j by A1,TOPREAL1:1;
A4: p2 = f/.(j+1) by A1,TOPREAL1:1;
j in dom f /\ (Seg i) & j+1 in dom f /\ (Seg i) by A1,A2,FUNCT_1:68;
then j in dom f & j+1 in dom f by XBOOLE_0:def 3;
then 1 <= j & j+1 <= len f by FINSEQ_3:27;
then A5: LSeg(f,j) = LSeg(p1,p2) by A3,A4,TOPREAL1:def 5;
1 <= j & j+1 <= len(f|i) by A1,FINSEQ_3:27;
hence thesis by A5,TOPREAL1:def 5;
end;
theorem
j in dom f & j+1 in dom f implies LSeg(f^h,j) = LSeg(f,j)
proof assume
A1: j in dom f & j+1 in dom f;
set p1 = f/.j, p2 = f/.(j+1);
A2: p1 = (f^h)/.j by A1,GROUP_5:95;
A3: p2 = (f^h)/.(j+1) by A1,GROUP_5:95;
dom f c= dom(f^h) by FINSEQ_1:39;
then 1 <= j & j+1 <= len(f^h) by A1,FINSEQ_3:27;
then A4: LSeg(f^h,j) = LSeg(p1,p2) by A2,A3,TOPREAL1:def 5;
1 <= j & j+1 <= len f by A1,FINSEQ_3:27;
hence thesis by A4,TOPREAL1:def 5;
end;
theorem Th26:
for f being FinSequence of TOP-REAL n,i being Nat holds LSeg(f,i) c= L~f
proof let f be FinSequence of TOP-REAL n,i be Nat;
let x such that
A1: x in LSeg(f,i);
now per cases;
case i < 1;
hence contradiction by A1,TOPREAL1:def 5;
case A2: i >= 1;
now per cases;
case i+1 > len f;
hence contradiction by A1,TOPREAL1:def 5;
case A3: i+1 <= len f;
set M = {LSeg(f,j) : 1<=j & j+1<=len f};
LSeg(f,i) in M & L~f = union M by A2,A3,TOPREAL1:def 6;
hence thesis by A1,TARSKI:def 4;
end;
hence thesis;
end;
hence thesis;
end;
theorem
L~(f|i) c= L~f
proof
set h = f|i,
Mh = {LSeg(h,n) : 1<=n & n+1<=len h},
Mf = {LSeg(f,m) : 1<=m & m+1<=len f};
let x; assume
A1: x in L~h; then x in union Mh by TOPREAL1:def 6;
then consider X be set such that
A2: x in X & X in Mh by TARSKI:def 4;
consider k such that
A3: X = LSeg(h,k) & 1<=k & k+1<=len h by A2;
A4: h = f|Seg i & dom f = Seg len f by FINSEQ_1:def 3,TOPREAL1:def 1;
per cases;
suppose A5: i in dom f;
then A6: i<=len f by FINSEQ_3:27;
then Seg i c= dom f & dom h=dom f /\ Seg i by A4,FINSEQ_1:7,RELAT_1:90;
then dom h = Seg i by XBOOLE_1:28;
then len h <= len f by A6,FINSEQ_1:def 3;
then A7: k+1<=len f by A3,AXIOMS:22;
k <= k+1 by NAT_1:37;
then k <= len h by A3,AXIOMS:22;
then A8: k in dom h by A3,FINSEQ_3:27;
1<=k+1 by NAT_1:37;
then k+1 in dom h by A3,FINSEQ_3:27;
then X = LSeg(f,k) by A3,A5,A8,Th24;
then X in Mf by A3,A7;
then x in union Mf by A2,TARSKI:def 4;
hence thesis by TOPREAL1:def 6;
suppose A9: not i in dom f;
now per cases by A9,FINSEQ_3:27;
case i<1; then i<0+1; then i<=0 & 0<=i by NAT_1:18,38;
then Seg i = {} by AXIOMS:21,FINSEQ_1:4;
then dom h = dom f /\ {} by A4,FUNCT_1:68;
then len h = 0 by FINSEQ_1:4,def 3;
hence contradiction by A1,TOPREAL1:28;
case len f<i;
then Seg len f c= Seg i by FINSEQ_1:7;
then dom f c= Seg i by FINSEQ_1:def 3;
then dom f = dom f /\ (Seg i) by XBOOLE_1:28;
then dom f=dom h & for x st x in dom h holds h.x = f.x by A4,FUNCT_1:68;
then h = f by FUNCT_1:9;
then x in union Mf by A2,TARSKI:def 4;
hence x in L~f by TOPREAL1:def 6;
end;
hence thesis;
end;
theorem Th28:
for r being Real, p1,p2 being Point of TOP-REAL n, u being Point of Euclid n
st p1 in Ball(u,r) & p2 in Ball(u,r) holds
LSeg(p1,p2) c= Ball(u,r)
proof let r be Real, p1,p2 be Point of TOP-REAL n, u be Point of Euclid n
; assume
A1: p1 in Ball(u,r) & p2 in Ball(u,r);
then reconsider p'=p1 as Point of Euclid n;
A2:dist(p',u)<r by A1,METRIC_1:12;
thus LSeg(p1,p2) c= Ball(u,r)
proof let a be set;
assume a in LSeg(p1,p2);
then a in { (1-lambda)*p1 + lambda*p2 : 0 <= lambda & lambda <= 1 }
by TOPREAL1:def 4;
then consider lambda such that
A3: (1-lambda)*p1 + lambda*p2=a and
A4: 0 <= lambda & lambda <= 1;
set p = (1-lambda)*p1 + lambda*p2;
u in the carrier of Euclid n;
then u in the carrier of TOP-REAL n by Th13;
then reconsider q2'=u as Element of REAL n by EUCLID:25;
reconsider q2=q2' as Point of TOP-REAL n by EUCLID:25;
A5: q2 - p = 1*q2-((1-lambda)*p1 + lambda*p2) by EUCLID:33
.= (1-lambda+lambda)*q2-((1-lambda)*p1 + lambda*p2) by XCMPLX_1:27
.= (1-lambda)*q2+lambda*q2-((1-lambda)*p1 + lambda*p2) by EUCLID:37
.= (1-lambda)*q2+lambda*q2+-((1-lambda)*p1 + lambda*p2) by EUCLID:45
.= (1-lambda)*q2+lambda*q2+(-(1-lambda)*p1 + -lambda*p2) by EUCLID:42
.= (1-lambda)*q2+lambda*q2+-(1-lambda)*p1 + -lambda*p2 by EUCLID:30
.= (1-lambda)*q2+-(1-lambda)*p1+lambda*q2 + -lambda*p2 by EUCLID:30
.= (1-lambda)*q2+(1-lambda)*(-p1)+lambda*q2 + -lambda*p2 by EUCLID:44
.= (1-lambda)*(q2+-p1)+lambda*q2 + -lambda*p2 by EUCLID:36
.= (1-lambda)*(q2+-p1)+(lambda*q2 + -lambda*p2) by EUCLID:30
.= (1-lambda)*(q2+-p1)+(lambda*q2 + lambda*(-p2)) by EUCLID:44
.= (1-lambda)*(q2+-p1)+(lambda*(q2 + -p2)) by EUCLID:36;
reconsider p'=(1-lambda)*p1 + lambda*p2,p1'=p1,p2'=p2 as Element of REAL n
by EUCLID:25;
-p1 = -p1' by EUCLID:def 12; then q2+-p1 = q2'+-p1' by EUCLID:def 10;
then A6: (1-lambda)*(q2+-p1)=(1-lambda)*(q2'+-p1') by EUCLID:def 11;
-p2 = -p2' by EUCLID:def 12;
then q2+-p2 = q2'+-p2' by EUCLID:def 10;
then A7: lambda*(q2+-p2)=lambda*(q2'+(-p2')) by EUCLID:def 11;
q2-p = q2' - p' by EUCLID:def 13;
then q2' - p' = (1-lambda)*(q2'+-p1')+lambda*(q2' + -p2')
by A5,A6,A7,EUCLID:def 10;
then A8: |. q2'-p' .| <= |.(1-lambda)*(q2'+-p1').|
+ |.lambda*(q2' + -p2').| by EUCLID:15;
A9: |.(1-lambda)*(q2'+-p1').| + |.lambda*(q2' + -p2').| =
abs(1-lambda)*|.q2'+-p1'.| + |.lambda*(q2' + -p2').| by EUCLID:14
.= abs(1-lambda)*|.q2'+-p1'.| + abs(lambda)*|.q2' + -p2'.| by EUCLID:14;
consider u3 being Point of Euclid n such that
A10: u3=p1 & dist(u,u3)<r by A2;
A11: (Pitag_dist n).(q2',p1')=|.q2'-p1'.| by EUCLID:def 6;
A12: Euclid n = MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7;
then A13: dist(u,u3) = |.q2'-p1'.| by A10,A11,METRIC_1:def 1;
A14: n-tuples_on REAL = REAL n by EUCLID:def 1;
then A15: |.q2'+-p1'.| <= r by A10,A13,RVSUM_1:52;
p2 in {u4 where u4 is Point of Euclid n :
dist(u,u4)<r} by A1,METRIC_1:18;
then consider u4 be Point of Euclid n such that
A16: u4=p2 & dist(u,u4)<r;
(Pitag_dist n).(q2',p2')=|.q2'-p2'.| by EUCLID:def 6;
then dist(u,u4)= |.q2'-p2'.| by A12,A16,METRIC_1:def 1;
then A17: |.q2'+-p2'.| < r by A14,A16,RVSUM_1:52;
A18: 0 <= 1-lambda by A4,SQUARE_1:12;
then A19: 1-lambda= abs(1-lambda) & lambda=abs(lambda) by A4,ABSVALUE:def
1;
abs(1-lambda)*|.q2'+-p1'.| < (1-lambda)*r &
abs(lambda)*|.q2' + -p2'.| <= lambda*r or
abs(1-lambda)*|.q2'+-p1'.| <= (1-lambda)*r &
abs(lambda)*|.q2' + -p2'.| < lambda*r
proof
per cases by A4;
suppose lambda=0;
hence thesis by A10,A13,A14,A19,RVSUM_1:52;
suppose lambda>0;
hence thesis by A15,A17,A18,A19,AXIOMS:25,REAL_1:70;
end;
then A20: abs(1-lambda)*|.q2'+-p1'.| + abs(lambda)*|.q2' + -p2'.|
< (1-lambda)*r + lambda*r by REAL_1:67;
(1-lambda)*r + lambda*r = ((1-lambda)+lambda)*r by XCMPLX_1:8
.= 1*r by XCMPLX_1:27
.= r;
then A21: |.q2'-p'.| < r by A8,A9,A20,AXIOMS:22;
reconsider u5=(1-lambda)*p1 + lambda*p2 as Point of Euclid n
by Th13;
A22: (Pitag_dist n).(q2',p')=|.q2'-p'.| by EUCLID:def 6;
(Pitag_dist n).(u,u5)=dist(u,u5) by A12,METRIC_1:def 1;
then a in {u6 where u6 is Element of Euclid n:dist(u,u6)<
r}
by A3,A21,A22;
hence thesis by METRIC_1:18;
end;
thus thesis;
end;
theorem
u=p1 & p1=|[r1,s1]| & p2=|[r2,s2]| & p=|[r2,s1]| & p2 in Ball(u,r) implies
p in Ball(u,r)
proof
assume that
A1: u=p1 and
A2: p1=|[r1,s1]| and
A3: p2=|[r2,s2]| and
A4: p=|[r2,s1]| and
A5: p2 in Ball(u,r);
p2 in {u6 where u6 is Element of Euclid 2:dist(u,u6)<r}
by A5,METRIC_1:18;
then A6: ex u5 st u5 = p2 & dist(u,u5)<r;
reconsider p1'= p1, p2'= p2,p'=p as Element of REAL 2 by EUCLID:25;
A7: (Pitag_dist 2).(p1',p2')=|.p1'-p2'.| by EUCLID:def 6;
A8: (Pitag_dist 2).(p1',p')=|.p1'-p'.| by EUCLID:def 6;
reconsider up=p as Point of Euclid 2 by Th13;
A9: Euclid 2 = MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then A10: dist(u,up)=|.p1'-p'.| by A1,A8,METRIC_1:def 1;
A11: |.p1'-p2'.| < r by A1,A6,A7,A9,METRIC_1:def 1;
A12: |.p1'-p'.| = sqrt Sum sqr (p1'-p') by EUCLID:def 5;
A13: p1'= <*r1,s1*> & p'= <*r2,s1*> & p2'=<*r2,s2*> by A2,A3,A4,EUCLID:def 16
;
p1'-p'=p1-p & p1'-p2'=p1-p2 by EUCLID:def 13;
then A14: (p1'-p')=<*r1-r2,s1-s1*> & (p1'-p2')=<*r1-r2,s1-s2*>
by A13,Th10;
A15: sqr (p1'-p') = sqrreal*(p1'-p') by RVSUM_1:def 8
.= <* sqrreal.(r1-r2),sqrreal.(s1-s1)*> by A14,FINSEQ_2:40;
A16: sqr (p1'-p2') = sqrreal*(p1'-p2') by RVSUM_1:def 8
.= <* sqrreal.(r1-r2),sqrreal.(s1-s2)*> by A14,FINSEQ_2:40;
A17: Sum sqr (p1'-p') =
sqrreal.(r1-r2) + sqrreal.(s1-s1) by A15,RVSUM_1:107
.= sqrreal.(r1-r2) + sqrreal.0 by XCMPLX_1:14
.= sqrreal.(r1-r2) + 0 by RVSUM_1:def 2,SQUARE_1:60
.= sqrreal.(r1-r2);
(s1-s2)^2 >= 0 by SQUARE_1:72;
then sqrreal.(s1-s2) >= 0 by RVSUM_1:def 2;
then A18: sqrreal.(r1-r2)+0 <= sqrreal.(r1-r2)
+ sqrreal.(s1-s2) by REAL_1:55;
(r1-r2)^2 >= 0 by SQUARE_1:72;
then sqrreal.(r1-r2) >= 0 by RVSUM_1:def 2;
then A19: |.p1'-p'.| <= sqrt(sqrreal.(r1-r2)
+ sqrreal.(s1-s2)) by A12,A17,A18,SQUARE_1:94;
|.p1'-p2'.| =
sqrt Sum <*sqrreal.(r1-r2),sqrreal.(s1-s2)*>
by A16,EUCLID:def 5
.= sqrt (sqrreal.(r1-r2) + sqrreal.(s1-s2)) by RVSUM_1:107;
then |.p1'-p'.| < r by A11,A19,AXIOMS:22;
then p in {u6 where u6 is Element of Euclid 2:dist(u,u6)<r}
by A10;
hence thesis by METRIC_1:18;
end;
theorem
|[s,r1]| in Ball(u,r) & |[s,s1]| in Ball(u,r) implies
|[s,(r1+s1)/2]| in Ball(u,r)
proof
set p = |[s,r1]|,
q = |[s,s1]|,
p3 = |[s,(r1+s1)/2]|; assume
|[s,r1]| in Ball(u,r) & |[s,s1]| in Ball(u,r);
then A1: LSeg(|[s,r1]|,|[s,s1]|) c= Ball(u,r) &
p`1 = s & p`2 = r1 & q`1 = s & q`2 = s1 & 2<>0 by Th28,EUCLID:56;
A2: p3`1 = s by EUCLID:56
.= (p`1)/2 + (q`1)*1/2 by A1,XCMPLX_1:66
.= (p`1)*1/2 + (1/2)*(q`1) by XCMPLX_1:75
.= (1 - 1/2)*(p`1) + (1/2)*(q`1) by XCMPLX_1:75
.= ((1 - 1/2)*p)`1 + (1/2)*(q`1) by Th9
.= ((1 - 1/2)*p)`1 + ((1/2)*q)`1 by Th9
.= ((1 - 1/2)*p + (1/2)*q)`1 by Th7;
p3`2 = (r1+s1)/2 by EUCLID:56
.= (p`2)/2 + (q`2)*1/2 by A1,XCMPLX_1:63
.= (p`2)*1/2 + (1/2)*(q`2) by XCMPLX_1:75
.= (1 - 1/2)*(p`2) + (1/2)*(q`2) by XCMPLX_1:75
.= ((1 - 1/2)*p)`2 + (1/2)*(q`2) by Th9
.= ((1 - 1/2)*p)`2 + ((1/2)*q)`2 by Th9
.= ((1 - 1/2)*p + (1/2)*q)`2 by Th7;
then p3 = (1 - 1/2)*p + (1/2)*q by A2,Th11;
then p3 in {(1-lambda)*p + lambda*q: 0<=lambda & lambda<=1 };
then p3 in LSeg(|[s,r1]|,|[s,s1]|) by TOPREAL1:def 4;
hence thesis by A1;
end;
theorem
|[r1,s]| in Ball(u,r) & |[s1,s]| in Ball(u,r) implies
|[(r1+s1)/2,s]| in Ball(u,r)
proof
set p = |[r1,s]|,
q = |[s1,s]|,
p3 = |[(r1+s1)/2,s]|; assume
|[r1,s]| in Ball(u,r) & |[s1,s]| in Ball(u,r);
then A1: LSeg(|[r1,s]|,|[s1,s]|) c= Ball(u,r) &
p`2 = s & p`1 = r1 & q`2 = s & q`1 = s1 & 2<>0 by Th28,EUCLID:56;
A2: p3`2 = s by EUCLID:56
.= (p`2)/2 + (q`2)*1/2 by A1,XCMPLX_1:66
.= (p`2)*1/2 + (1/2)*(q`2) by XCMPLX_1:75
.= (1 - 1/2)*(p`2) + (1/2)*(q`2) by XCMPLX_1:75
.= ((1 - 1/2)*p)`2 + (1/2)*(q`2) by Th9
.= ((1 - 1/2)*p)`2 + ((1/2)*q)`2 by Th9
.= ((1 - 1/2)*p + (1/2)*q)`2 by Th7;
p3`1 = (r1+s1)/2 by EUCLID:56
.= (p`1)/2 + (q`1)*1/2 by A1,XCMPLX_1:63
.= (p`1)*1/2 + (1/2)*(q`1) by XCMPLX_1:75
.= (1 - 1/2)*(p`1) + (1/2)*(q`1) by XCMPLX_1:75
.= ((1 - 1/2)*p)`1 + (1/2)*(q`1) by Th9
.= ((1 - 1/2)*p)`1 + ((1/2)*q)`1 by Th9
.= ((1 - 1/2)*p + (1/2)*q)`1 by Th7;
then p3 = (1 - 1/2)*p + (1/2)*q by A2,Th11;
then p3 in {(1-lambda)*p + lambda*q: 0<=lambda & lambda<=1 };
then p3 in LSeg(|[r1,s]|,|[s1,s]|) by TOPREAL1:def 4;
hence thesis by A1;
end;
theorem
r1 <> s1 & s2 <> r2 & |[r1,r2]| in Ball(u,r) & |[s1,s2]| in Ball(u,r)
implies |[r1,s2]| in Ball(u,r) or |[s1,r2]| in Ball(u,r)
proof assume
A1: r1<>s1 & s2<>r2 & |[r1,r2]| in Ball(u,r) & |[s1,s2]| in Ball(u,r);
then A2: r > 0 by TBSP_1:17;
per cases;
suppose |[r1,s2]| in Ball(u,r); hence thesis;
suppose A3: not |[r1,s2]| in Ball(u,r);
set p1 = |[r1,s2]|,
p2 = |[s1,r2]|,
p3 = |[s1,s2]|,
p4 = |[r1,r2]|;
A4: p1`1 = r1 & p1`2 = s2 &
p2`1 = s1 & p2`2 = r2 &
p3`1 = s1 & p3`2 = s2 &
p4`1 = r1 & p4`2 = r2 by EUCLID:56;
reconsider u1 = p1, u2 = p2, u3 = p3, u4 = p4 as Point of Euclid 2 by Th13;
reconsider p = u as Point of TOP-REAL 2 by Th13;
set a = (p`1 - p1`1)^2 + (p`2 - p1`2)^2,
b = (p`1 - p4`1)^2 + (p`2 - p4`2)^2,
c = (p`1 - p3`1)^2 + (p`2 - p3`2)^2,
d = (p`1 - p2`1)^2 + (p`2 - p2`2)^2;
(p`1 - p1`1)^2 >= 0 & (p`2 - p1`2)^2 >= 0 by SQUARE_1:72;
then A5: 0+0<=(p`1 - p1`1)^2 + (p`2 - p1`2)^2 by REAL_1:55;
(p`1 - p4`1)^2 >= 0 & (p`2 - p4`2)^2 >= 0 by SQUARE_1:72;
then A6: 0+0<=(p`1 - p4`1)^2 + (p`2 - p4`2)^2 by REAL_1:55;
then A7: 0<=sqrt b & (p`1 - p3`1)^2 >= 0 & (p`2 - p3`2)^2 >=
0 by SQUARE_1:72,def 4;
then A8: 0+0<=(p`1 - p3`1)^2 + (p`2 - p3`2)^2 by REAL_1:55;
then A9: 0<=sqrt c & (p`1 - p2`1)^2 >= 0 & (p`2 - p2`2)^2 >=
0 by SQUARE_1:72,def 4;
then A10: 0+0 <= (p`1 - p2`1)^2 + (p`2 - p2`2)^2 by REAL_1:55;
A11: Euclid 2=MetrStruct (# REAL 2, Pitag_dist 2 #) by EUCLID:def 7;
then A12: (Pitag_dist 2).(u,u1) = dist(u,u1) by METRIC_1:def 1;
r <= dist(u,u1) by A3,METRIC_1:12;
then r <= sqrt a by A12,Th12;
then r * r <= (sqrt a)*sqrt a by A2,REAL_2:197;
then r * r <= (sqrt a)^2 by SQUARE_1:def 3;
then r^2 <= (sqrt a)^2 by SQUARE_1:def 3;
then A13: r^2 <= a by A5,SQUARE_1:def 4;
A14: c + b = (p`1 - p2`1)^2 + (p`2 - p1`2)^2 + (p`1 - p1`1)^2 + (p`2 - p2`2)^2
by A4,XCMPLX_1:1
.= (p`1 - p1`1)^2 + (p`2 - p1`2)^2 + (p`1 - p2`1)^2 + (p`2 - p2`2)^2
by XCMPLX_1:1
.= a + d by XCMPLX_1:1;
A15: (Pitag_dist 2).(u,u4) = dist(u,u4) by A11,METRIC_1:def 1;
dist(u,u4) < r by A1,METRIC_1:12;
then sqrt b < r by A15,Th12;
then (sqrt b)*sqrt b < r*r by A7,SEQ_2:7;
then (sqrt b)^2 < r*r by SQUARE_1:def 3;
then b < r*r by A6,SQUARE_1:def 4;
then A16: b < r^2 by SQUARE_1:def 3;
A17: (Pitag_dist 2).(u,u3) = dist(u,u3) by A11,METRIC_1:def 1;
dist(u,u3) < r by A1,METRIC_1:12;
then sqrt c < r by A17,Th12;
then (sqrt c)*sqrt c < r*r by A9,SEQ_2:7;
then (sqrt c)^2 < r*r by SQUARE_1:def 3;
then c < r*r by A8,SQUARE_1:def 4;
then c < r^2 by SQUARE_1:def 3;
then A18: c+b <r^2 + r^2 by A16,REAL_1:67;
r^2+d <= c + b by A13,A14,AXIOMS:24;
then r^2+d < r^2+r^2 by A18,AXIOMS:22;
then d < r^2+r^2 - r^2 by REAL_1:86;
then d < r^2 by XCMPLX_1:26;
then sqrt d < sqrt(r^2) by A10,SQUARE_1:95;
then A19: sqrt d < r by A2,SQUARE_1:89;
dist(u,u2) = (Pitag_dist 2).(u,u2) by A11,METRIC_1:def 1
.= sqrt d by Th12;
hence thesis by A19,METRIC_1:12;
end;
theorem
not f/.1 in Ball(u,r) & 1<=m & m<=len f - 1 & LSeg(f,m) meets Ball(u,r) &
(for i st 1<=i & i<=len f - 1 & LSeg(f,i) /\
Ball(u,r) <> {} holds m<=i) implies
not f/.m in Ball(u,r)
proof assume
A1: not f/.1 in Ball(u,r) &
1<=m & m<=len f - 1 & LSeg(f,m) /\ Ball(u,r) <> {} &
for i st 1<=i & i<=len f - 1 & LSeg(f,i) /\ Ball(u,r) <> {} holds m<=i;
assume A2: f/.m in Ball(u,r);
per cases by A1,REAL_1:def 5;
suppose 1=m; hence contradiction by A1,A2;
suppose A3: 1<m; then 1+1<=m by NAT_1:38;
then A4: 1<=m-1 by REAL_1:84; reconsider k=m-1 as Nat by A3,INT_1:18
; m-1<=m by PROB_1:2;
then A5: k<=len f - 1
by A1,AXIOMS:22;
then k+1<=len f by REAL_1:84;
then f/.(k+1) in LSeg(f,k) by A4,TOPREAL1:27;
then f/.m in LSeg(f,k) by XCMPLX_1:27;
then LSeg(f,k) /\ Ball(u,r) <> {} by A2,XBOOLE_0:def 3;
then m<=k by A1,A4,A5;
then m+1<=m by REAL_1:84;
hence contradiction by NAT_1:38;
end;
theorem
for q,p2,p st q`2 = p2`2 & p`2 <> p2`2 holds
(LSeg(p2,|[p2`1,p`2]|) \/ LSeg(|[p2`1,p`2]|,p)) /\ LSeg(q,p2) = {p2}
proof let q,p2,p such that
A1: q`2 = p2`2 & p`2 <> p2`2;
set p3 = |[(p2)`1,p`2]|;
set l23 = LSeg(p2,p3),
l3 = LSeg(p3,p),
l = LSeg(q,p2);
A2: l23 /\ l = {p2}
proof
thus l23 /\ l c= {p2}
proof let x be set; assume
x in l23 /\ l;
then A3: x in l23 & x in l by XBOOLE_0:def 3;
then x in {(1-lambda)*p2+lambda*p3: 0 <=lambda & lambda <= 1 }
by TOPREAL1:def 4;
then consider s1 such that
A4: (1-s1)*p2 + s1*p3=x & 0<=s1 & s1<=1;
set t = (1-s1)*p2 + s1*p3;
A5: t`1 = ((1-s1)*p2) `1 + (s1*p3) `1 by Th7
.= (1-s1)*(p2 `1) + (s1*p3) `1 by Th9
.= (1-s1)*(p2 `1) + s1*(p3 `1) by Th9
.= (1-s1)*(p2 `1) + s1*(p2 `1) by EUCLID:56
.= (1-s1 + s1)*(p2 `1) by XCMPLX_1:8
.= 1*(p2 `1) by XCMPLX_1:27
.= p2 `1;
x in {(1-lambda)*q+lambda*p2: 0 <=lambda & lambda <= 1 }
by A3,TOPREAL1:def 4;
then consider s2 such that
A6: (1-s2)*q + s2*p2=x & 0 <= s2 & s2 <= 1;
A7: ((1-s2)*q + s2*p2) `2 = ((1-s2)*q) `2 + (s2*p2) `2 by Th7
.= (1-s2)*(q`2) + (s2*p2) `2 by Th9
.= (1-s2)*(q `2) + s2*(p2 `2) by Th9
.= (1-s2 + s2)*(p2 `2) by A1,XCMPLX_1:8
.= 1*(p2 `2) by XCMPLX_1:27
.= p2 `2;
t = |[t`1, t`2]| by EUCLID:57
.= p2 by A4,A5,A6,A7,EUCLID:57;
hence x in {p2} by A4,TARSKI:def 1;
end;
let x be set; assume x in {p2};
then A8: x=p2 by TARSKI:def 1;
p2 in l23 & p2 in l by TOPREAL1:6;
hence x in l23 /\ l by A8,XBOOLE_0:def 3;
end;
A9: l3 /\ l = {}
proof assume A10: l3 /\ l <> {};
consider x being Element of l3 /\ l;
A11: x in l3 & x in l by A10,XBOOLE_0:def 3;
then x in {(1-lambda)*p3+lambda*p: 0 <=lambda & lambda <= 1 }
by TOPREAL1:def 4;
then consider s1 such that
A12: x = (1-s1)*p3 + s1*p & 0 <= s1 & s1 <= 1;
A13: ((1-s1)*p3 + s1*p)`2 = ((1-s1)*p3) `2 + (s1*p) `2 by Th7
.= (1-s1)*(p3 `2) + (s1*p) `2 by Th9
.= (1-s1)*(p3 `2) + s1*(p `2) by Th9
.= (1-s1)*(p `2) + s1*(p `2) by EUCLID:56
.= (1-s1 + s1)*(p `2) by XCMPLX_1:8
.= 1*(p `2) by XCMPLX_1:27
.= p `2;
x in {(1-lambda)*q+lambda*p2: 0 <=lambda & lambda <= 1 }
by A11,TOPREAL1:def 4;
then consider s2 such that
A14: x = (1-s2)*q + s2*p2 & 0 <= s2 & s2 <= 1;
((1-s2)*q + s2*p2) `2 = ((1-s2)*q) `2 + (s2*p2) `2 by Th7
.= (1-s2)*(q`2) + (s2*p2) `2 by Th9
.= (1-s2)*(q `2) + s2*(p2 `2) by Th9
.= (1-s2 + s2)*(p2 `2) by A1,XCMPLX_1:8
.= 1*(p2 `2) by XCMPLX_1:27
.= p2 `2;
hence contradiction by A1,A12,A13,A14;
end;
thus (l23 \/ l3) /\ l = l23 /\ l \/ l3 /\ l by XBOOLE_1:23
.= {p2} by A2,A9;
end;
theorem
for q,p2,p st q`1 = p2`1 & p`1 <> p2`1 holds
(LSeg(p2,|[p`1,p2`2]|) \/ LSeg(|[p`1,p2`2]|,p)) /\ LSeg(q,p2) = {p2}
proof let q,p2,p such that
A1: q`1 = (p2)`1 & p`1 <> (p2)`1;
set p3 = |[p`1,(p2)`2]|;
set l23 = LSeg(p2,p3),
l3 = LSeg(p3,p),
l = LSeg(q,p2);
A2: l23 /\ l = {p2}
proof
thus l23 /\ l c= {p2}
proof let x be set; assume
x in l23 /\ l;
then A3: x in l23 & x in l by XBOOLE_0:def 3;
then x in {(1-lambda)*p2+lambda*p3: 0 <=lambda & lambda <= 1 }
by TOPREAL1:def 4;
then consider s1 such that
A4: x = (1-s1)*p2 + s1*p3 & 0 <= s1 & s1 <= 1;
set t = (1-s1)*p2 + s1*p3;
A5: t`2 = ((1-s1)*p2) `2 + (s1*p3) `2 by Th7
.= (1-s1)*(p2 `2) + (s1*p3) `2 by Th9
.= (1-s1)*(p2 `2) + s1*(p3 `2) by Th9
.= (1-s1)*(p2 `2) + s1*(p2 `2) by EUCLID:56
.= (1-s1 + s1)*(p2 `2) by XCMPLX_1:8
.= 1*(p2 `2) by XCMPLX_1:27
.= p2 `2;
x in {(1-lambda)*q+lambda*p2: 0 <=lambda & lambda <= 1 }
by A3,TOPREAL1:def 4;
then consider s2 such that
A6: x = (1-s2)*q + s2*p2 & 0 <= s2 & s2 <= 1;
A7: ((1-s2)*q + s2*p2) `1 = ((1-s2)*q) `1 + (s2*p2) `1 by Th7
.= (1-s2)*(q`1) + (s2*p2) `1 by Th9
.= (1-s2)*(q `1) + s2*(p2 `1) by Th9
.= (1-s2 + s2)*(p2 `1) by A1,XCMPLX_1:8
.= 1*(p2 `1) by XCMPLX_1:27
.= p2 `1;
t = |[t`1, t`2]| by EUCLID:57
.= p2 by A4,A5,A6,A7,EUCLID:57;
hence x in {p2} by A4,TARSKI:def 1;
end;
let x be set; assume x in {p2};
then A8: x=p2 by TARSKI:def 1;
p2 in l23 & p2 in l by TOPREAL1:6;
hence x in l23 /\ l by A8,XBOOLE_0:def 3;
end;
A9: l3 /\ l = {}
proof assume A10: l3 /\ l <> {};
consider x being Element of l3 /\ l;
A11: x in l3 & x in l by A10,XBOOLE_0:def 3;
then x in {(1-lambda)*p3+lambda*p: 0 <=lambda & lambda <= 1 }
by TOPREAL1:def 4;
then consider d1 be Real such that
A12: x = (1-d1)*p3 + d1*p & 0 <= d1 & d1 <= 1;
A13: ((1-d1)*p3 + d1*p)`1 = ((1-d1)*p3) `1 + (d1*p) `1 by Th7
.= (1-d1)*(p3 `1) + (d1*p) `1 by Th9
.= (1-d1)*(p3 `1) + d1*(p `1) by Th9
.= (1-d1)*(p `1) + d1*(p `1) by EUCLID:56
.= (1-d1 + d1)*(p `1) by XCMPLX_1:8
.= 1*(p `1) by XCMPLX_1:27
.= p `1;
x in {(1-lambda)*q+lambda*p2: 0 <=lambda & lambda <= 1 }
by A11,TOPREAL1:def 4;
then consider d2 be Real such that
A14: x = (1-d2)*q + d2*p2 & 0 <= d2 & d2 <= 1;
((1-d2)*q + d2*p2) `1 = ((1-d2)*q) `1 + (d2*p2) `1 by Th7
.= (1-d2)*(q`1) + (d2*p2) `1 by Th9
.= (1-d2)*(q `1) + d2*(p2 `1) by Th9
.= (1-d2 + d2)*(p2 `1) by A1,XCMPLX_1:8
.= 1*(p2 `1) by XCMPLX_1:27
.= p2 `1;
hence contradiction by A1,A12,A13,A14;
end;
thus (l23 \/ l3) /\ l = l23 /\ l \/ l3 /\ l by XBOOLE_1:23
.= {p2} by A2,A9;
end;
theorem Th36:
LSeg(p,|[p`1,q`2]|) /\ LSeg(|[p`1,q`2]|,q) ={|[p`1,q`2]|}
proof
set p3 = |[p`1,q`2]|;
set l23 = LSeg(p,p3),
l = LSeg(p3,q);
thus l23 /\ l c= {p3}
proof let x be set; assume
x in l23 /\ l;
then A1: x in l23 & x in l by XBOOLE_0:def 3;
then x in {(1-lambda)*p+lambda*p3: 0 <=lambda & lambda <= 1 }
by TOPREAL1:def 4;
then consider d1 be Real such that
A2: x = (1-d1)*p + d1*p3 & 0 <= d1 & d1 <= 1;
set t = (1-d1)*p + d1*p3;
A3: t`1 = ((1-d1)*p) `1 + (d1*p3) `1 by Th7
.= (1-d1)*(p `1) + (d1*p3) `1 by Th9
.= (1-d1)*(p `1) + d1*(p3 `1) by Th9
.= (1-d1)*(p `1) + d1*(p `1) by EUCLID:56
.= (1-d1 + d1)*(p `1) by XCMPLX_1:8
.= 1*(p `1) by XCMPLX_1:27
.= p3 `1 by EUCLID:56;
x in {(1-lambda)*p3+lambda*q: 0 <=lambda & lambda <= 1}
by A1,TOPREAL1:def 4;
then consider d2 be Real such that
A4: x = (1-d2)*p3 + d2*q & 0 <= d2 & d2 <= 1;
t`2 = ((1-d2)*p3) `2 + (d2*q) `2 by A2,A4,Th7
.= (1-d2)*(p3 `2) + (d2*q) `2 by Th9
.= (1-d2)*(p3 `2) + d2*(q`2) by Th9
.= (1-d2)*(q`2) + d2*(q`2) by EUCLID:56
.= (1-d2 + d2)*(q`2) by XCMPLX_1:8
.= 1*(q`2) by XCMPLX_1:27
.= p3 `2 by EUCLID:56;
then t = p3 by A3,Th11;
hence x in {p3} by A2,TARSKI:def 1;
end;
let x be set; assume x in {p3};
then x=p3 & p3 in l23 & p3 in l by TARSKI:def 1,TOPREAL1:6;
hence x in l23 /\ l by XBOOLE_0:def 3;
end;
theorem Th37:
LSeg(p,|[q`1,p`2]|) /\ LSeg(|[q`1,p`2]|,q) ={|[q`1,p`2]|}
proof
set p3 = |[q`1,p`2]|;
set l23 = LSeg(p,p3),
l = LSeg(p3,q);
thus l23 /\ l c= {p3}
proof let x be set; assume
x in l23 /\ l;
then A1: x in l23 & x in l by XBOOLE_0:def 3;
then x in {(1-lambda)*p+lambda*p3: 0 <=lambda & lambda <= 1}
by TOPREAL1:def 4;
then consider d1 be Real such that
A2: x = (1-d1)*p + d1*p3 & 0 <= d1 & d1 <= 1;
set t = (1-d1)*p + d1*p3;
A3: t`2 = ((1-d1)*p) `2 + (d1*p3) `2 by Th7
.= (1-d1)*(p `2) + (d1*p3) `2 by Th9
.= (1-d1)*(p `2) + d1*(p3 `2) by Th9
.= (1-d1)*(p3 `2) + d1*(p3 `2) by EUCLID:56
.= (1-d1 + d1)*(p3 `2) by XCMPLX_1:8
.= 1*(p3 `2) by XCMPLX_1:27
.= p3 `2;
x in {(1-lambda)*p3+lambda*q: 0 <=lambda & lambda <= 1}
by A1,TOPREAL1:def 4;
then consider d2 be Real such that
A4: x = (1-d2)*p3 + d2*q & 0 <= d2 & d2 <= 1;
t`1 = ((1-d2)*p3) `1 + (d2*q) `1 by A2,A4,Th7
.= (1-d2)*(p3 `1) + (d2*q) `1 by Th9
.= (1-d2)*(p3 `1) + d2*(q`1) by Th9
.= (1-d2)*(p3`1) + d2*(p3`1) by EUCLID:56
.= (1-d2 + d2)*(p3`1) by XCMPLX_1:8
.= 1*(p3`1) by XCMPLX_1:27
.= p3`1;
then t = p3 by A3,Th11;
hence x in {p3} by A2,TARSKI:def 1;
end;
let x be set; assume x in {p3};
then x=p3 & p3 in l23 & p3 in l by TARSKI:def 1,TOPREAL1:6;
hence x in l23 /\ l by XBOOLE_0:def 3;
end;
theorem Th38:
p`1 = q`1 & p`2 <> q`2 implies
LSeg(p,|[p`1,(p`2+q`2)/2]|) /\
LSeg(|[p`1,(p`2+q`2)/2]|,q)={|[p`1,(p`2+q`2)/2]|}
proof assume
A1: p`1 = q`1 & p`2 <> q`2;
set p3 = |[p`1,(p`2+q`2)/2]|;
set l23 = LSeg(p,p3),
l = LSeg(p3,q);
thus l23 /\ l c= {p3}
proof let x be set; assume
x in l23 /\ l;
then A2: x in l23 & x in l by XBOOLE_0:def 3;
A3: l23 = LSeg(|[p`1,p`2]|,|[p`1,(p`2+q`2)/2]|) by EUCLID:57;
A4: l = LSeg(|[q`1,(p`2+q`2)/2]|,|[q`1,q`2]|) by A1,EUCLID:57;
now per cases by A1,REAL_1:def 5;
suppose A5: p`2 < q`2; then p`2 < (p`2+q`2)/2 by Th3;
then x in {p1: p1 `1 = p`1 & p`2 <= p1 `2 & p1 `2 <=
(p`2+q`2)/2} by A2,A3,Th15;
then consider t1 be Point of TOP-REAL 2 such that
A6: t1 = x & t1 `1 = p`1 & p`2 <= t1 `2 & t1 `2 <= (p`2+q`2)/2;
A7: t1`2 <= p3 `2 by A6,EUCLID:56;
(p`2+q`2)/2 < q`2 by A5,Th3;
then x in {p2: p2 `1 = q`1 & (p`2+q`2)/2 <= p2 `2 & p2 `2 <=
q`2} by A2,A4,Th15;
then ex t2 be Point of TOP-REAL 2 st
t2 = x & t2 `1 = q`1 & (p`2+q`2)/2 <= t2 `2 & t2 `2 <= q`2;
then t1`2 >= p3 `2 by A6,EUCLID:56;
then t1`2 = p3 `2 & t1 `1 = p3 `1 by A6,A7,AXIOMS:21,EUCLID:56;
hence x=p3 by A6,Th11;
suppose A8: p`2 > q`2; then p`2 > (p`2+q`2)/2 by Th3;
then x in {p11: p11 `1 = p`1 & (p`2+q`2)/2<=p11 `2 & p11 `2<=
p`2} by A2,A3,Th15;
then consider t1 be Point of TOP-REAL 2 such that
A9: t1 = x & t1 `1 = p`1 & (p`2+q`2)/2 <= t1 `2 & t1 `2 <= p`2;
A10: p3 `2 <= t1 `2 by A9,EUCLID:56;
q`2 < (p`2+q`2)/2 by A8,Th3;
then x in {p22: p22 `1=q`1 & q`2<=p22 `2 & p22 `2<=(p`2+q`2)/2} by A2,A4,
Th15;
then ex t2 be Point of TOP-REAL 2 st
t2 = x & t2 `1 = q`1 & q`2 <= t2 `2 & t2 `2 <= (p`2+q`2)/2;
then t1`2 <= p3 `2 by A9,EUCLID:56;
then t1`2 = p3 `2 & t1 `1 = p3 `1 by A9,A10,AXIOMS:21,EUCLID:56;
hence x=p3 by A9,Th11;
end;
hence x in {p3} by TARSKI:def 1;
end;
let x be set; assume x in {p3};
then x=p3 & p3 in l23 & p3 in l by TARSKI:def 1,TOPREAL1:6;
hence x in l23 /\ l by XBOOLE_0:def 3;
end;
theorem Th39:
p`1 <> q`1 & p`2 = q`2 implies
LSeg(p,|[(p`1+q`1)/2,p`2]|) /\
LSeg(|[(p`1+q`1)/2,p`2]|,q)={|[(p`1+q`1)/2,p`2]|}
proof assume
A1: p`1 <> q`1 & p`2 = q`2;
set p3 = |[(p`1+q`1)/2,p`2]|;
set l23 = LSeg(p,p3),
l = LSeg(p3,q);
thus l23 /\ l c= {p3}
proof let x be set; assume
x in l23 /\ l;
then A2: x in l23 & x in l by XBOOLE_0:def 3;
A3: l23 = LSeg(|[p`1,p`2]|,|[(p`1+q`1)/2,p`2]|) by EUCLID:57;
A4: l = LSeg(|[(p`1+q`1)/2,q`2]|,|[q`1,q`2]|) by A1,EUCLID:57;
now per cases by A1,REAL_1:def 5;
suppose A5: p`1 < q`1; then p`1 < (p`1+q`1)/2 by Th3;
then x in {p1: p1 `2 = p`2 & p`1 <= p1 `1 & p1 `1 <=
(p`1+q`1)/2} by A2,A3,Th16;
then consider t1 be Point of TOP-REAL 2 such that
A6: t1 = x & t1 `2 = p`2 & p`1 <= t1 `1 & t1 `1 <= (p`1+q`1)/2;
A7: t1`1 <= p3 `1 by A6,EUCLID:56;
(p`1+q`1)/2 < q`1 by A5,Th3;
then x in {p2: p2 `2 = q`2 & (p`1+q`1)/2 <= p2 `1 & p2 `1 <=
q`1} by A2,A4,Th16;
then ex t2 be Point of TOP-REAL 2 st
t2 = x & t2 `2 = q`2 & (p`1+q`1)/2 <= t2 `1 & t2 `1 <= q`1;
then t1`1 >= p3 `1 by A6,EUCLID:56;
then t1`2 = p3 `2 & t1 `1 = p3 `1 by A6,A7,AXIOMS:21,EUCLID:56;
hence x=p3 by A6,Th11;
suppose A8: p`1 > q`1; then p`1 > (p`1+q`1)/2 by Th3;
then x in {p11: p11 `2 = p`2 & (p`1+q`1)/2 <= p11 `1 & p11 `1 <= p`1}
by A2,A3,Th16;
then consider t1 be Point of TOP-REAL 2 such that
A9: t1 = x & t1 `2 = p`2 & (p`1+q`1)/2 <= t1 `1 & t1 `1 <= p`1;
A10: p3 `1 <= t1 `1 by A9,EUCLID:56;
q`1 < (p`1+q`1)/2 by A8,Th3;
then x in {p22: p22 `2 = q`2 & q`1<=p22 `1 & p22 `1<=
(p`1+q`1)/2} by A2,A4,Th16;
then ex t2 be Point of TOP-REAL 2 st
t2 = x & t2 `2 = q`2 & q`1 <= t2 `1 & t2 `1 <= (p`1+q`1)/2;
then t1`1 <= p3 `1 by A9,EUCLID:56;
then t1`2 = p3 `2 & t1 `1 = p3 `1 by A9,A10,AXIOMS:21,EUCLID:56;
hence x=p3 by A9,Th11;
end;
hence x in {p3} by TARSKI:def 1;
end;
let x be set; assume x in {p3};
then x=p3 & p3 in l23 & p3 in l by TARSKI:def 1,TOPREAL1:6;
hence x in l23 /\ l by XBOOLE_0:def 3;
end;
theorem
i>2 & i in dom f & f is_S-Seq implies f|i is_S-Seq
proof assume
A1: i>2 & i in dom f & f is_S-Seq;
then A2: f is s.n.c. by TOPREAL1:def 10;
A3: f is unfolded by A1,TOPREAL1:def 10;
A4: f is special by A1,TOPREAL1:def 10;
A5: f|i = f|Seg i & Seg len f = dom f by FINSEQ_1:def 3,TOPREAL1:def 1;
A6: i<=len f by A1,FINSEQ_3:27;
then A7: Seg i c= dom f & dom(f|i)=dom f /\ Seg i by A5,FINSEQ_1:7,RELAT_1:90
;
then A8: dom (f|i) = Seg i by XBOOLE_1:28;
thus f|i is one-to-one
proof let x,y; assume
A9: x in dom (f|i) & y in dom (f|i) & (f|i).x = (f|i).y;
then A10: f.x = (f|i).x by A5,FUNCT_1:70
.= f.y by A5,A9,FUNCT_1:70;
f is one-to-one & x in dom f & y in dom f
by A1,A7,A9,TOPREAL1:def 10,XBOOLE_0:def 3;
hence x=y by A10,FUNCT_1:def 8;
end;
thus len (f|i) >= 2 by A1,A8,FINSEQ_1:def 3;
thus f|i is unfolded
proof let j such that
A11: 1 <= j & j + 2 <= len (f|i);
len(f|i) <= len f by A6,A8,FINSEQ_1:def 3;
then A12: j + 2 <= len f by A11,AXIOMS:22;
j <= j+2 by NAT_1:29;
then j <= len(f|i) by A11,AXIOMS:22;
then A13: j in dom(f|i) by A11,FINSEQ_3:27;
j + 1 <= j + 2 by AXIOMS:24;
then A14: j+1 <= len(f|i) by A11,AXIOMS:22;
1<=j+1 by NAT_1:37;
then A15: j+1 in dom(f|i) by A14,FINSEQ_3:27;
then A16: LSeg(f,j) = LSeg(f|i,j) & j+(1+1) = j + 1+ 1
by A1,A13,Th24,XCMPLX_1:1;
1<=j+1+1 by NAT_1:37;
then j+1+1 in dom(f|i) by A11,A16,FINSEQ_3:27;
then LSeg(f,j+1) = LSeg(f|i,j+1) by A1,A15,Th24;
then LSeg(f|i,j) /\ LSeg(f|i,j+1) = {f/.(j+1)}
by A3,A11,A12,A16,TOPREAL1:def 8;
hence LSeg(f|i,j)/\ LSeg(f|i,j+1)={(f|i)/.(j+1)}
by A15,TOPREAL1:1;
end;
thus f|i is s.n.c.
proof let n,k; assume n+1 < k;
then LSeg(f,n) misses LSeg(f,k) by A2,TOPREAL1:def 9;
then A17: LSeg(f,n) /\ LSeg(f,k) = {} by XBOOLE_0:def 7;
A18: k+1 >= 1 by NAT_1:29;
A19: n+1 >= 1 by NAT_1:29;
A20: k+1 >= k by NAT_1:29;
A21: n+1 >= n by NAT_1:29;
per cases;
suppose A22: n in dom(f|i);
now per cases;
suppose n+1 in dom(f|i);
then A23: LSeg(f,n)=LSeg(f|i,n) by A1,A22,Th24;
now per cases;
suppose A24: k in dom (f|i);
now per cases;
suppose k+1 in dom(f|i);
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {} by A1,A17,A23,A24,Th24;
suppose not k+1 in dom(f|i);
then k+1 > len(f|i) by A18,FINSEQ_3:27;
then LSeg(f|i,k) = {} by TOPREAL1:def 5;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
suppose not k in dom (f|i);
then k < 1 or k > len(f|i) by FINSEQ_3:27;
then k < 1 or k+1 > len(f|i) by A20,AXIOMS:22;
then LSeg(f|i,k) = {} by TOPREAL1:def 5;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
suppose not n+1 in dom(f|i);
then n+1 > len(f|i) by A19,FINSEQ_3:27;
then LSeg(f|i,n) = {} by TOPREAL1:def 5;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
suppose not n in dom(f|i);
then n < 1 or n > len(f|i) by FINSEQ_3:27;
then n < 1 or n+1 > len(f|i) by A21,AXIOMS:22;
then LSeg(f|i,n) = {} by TOPREAL1:def 5;
hence LSeg(f|i,n) /\ LSeg(f|i,k) = {};
end;
let j such that
A25: 1 <= j & j + 1 <= len (f|i);
len(f|i) <= len f by A6,A8,FINSEQ_1:def 3;
then A26: j + 1 <= len f by A25,AXIOMS:22;
j <= j + 1 by NAT_1:29;
then j <= len(f|i) by A25,AXIOMS:22;
then j in dom (f|i) by A25,FINSEQ_3:27;
then A27: (f|i)/.j=f/.j by TOPREAL1:1;
1<=j+1 by NAT_1:37;
then j+1 in dom(f|i) by A25,FINSEQ_3:27;
then (f|i)/.(j+1)=f/.(j+1) by TOPREAL1:1;
hence ((f|i)/.j)`1 = ((f|i)/.(j+1))`1 or ((f|i)/.j)`2 = ((f|i)/.(j+1))`2
by A4,A25,A26,A27,TOPREAL1:def 7;
end;
theorem
p`1 <> q`1 & p`2 <> q`2 & f = <* p,|[p`1,q`2]|,q *> implies
f/.1 = p & f/.len f = q & f is_S-Seq
proof
set p1 = |[p`1,q`2]|; assume
A1: p`1 <> q`1 & p`2 <> q`2 & f = <* p,p1,q *>;
then A2: len f = 1 + 2 & f/.1 = p & f/.2 = p1 & f/.3 = q
by FINSEQ_1:62,FINSEQ_4:27;
hence f/.1 = p & f/.len f = q;
p<>p1 & q<>p1 by A1,EUCLID:56;
hence f is one-to-one & len f>=2 by A1,A2,FINSEQ_3:104;
thus f is unfolded
proof let i;
assume
A3: 1 <= i & i + 2 <= len f;
then i <= 1 by A2,REAL_1:53;
then A4: i = 1 by A3,AXIOMS:21;
hence LSeg(f,i) /\ LSeg(f,i+1) = LSeg(p,p1) /\ LSeg(f,2)
by A2,TOPREAL1:def 5
.= LSeg(p,p1) /\ LSeg(p1,q) by A2,TOPREAL1:def 5
.= {f/.(i+1)} by A2,A4,Th36;
end;
thus f is s.n.c.
proof let i,j such that
A5: i+1 < j;
now per cases;
suppose i=0; then LSeg(f,i)={} by TOPREAL1:def 5;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
suppose i<>0; then LSeg(f,j)={} by A1,A5,Th21;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
hence thesis;
end;
let i such that
A6: 1 <= i & i + 1 <= len f;
set p2 = f/.i, p3 = f/.(i+1);
A7: i <= 2 & i > 0 by A2,A6,AXIOMS:22,REAL_1:53;
per cases by A7,CQC_THE1:3;
suppose i=1;
hence p2`1 = p3`1 or p2`2 = p3`2 by A2,EUCLID:56;
suppose i=2;
hence p2 `1 = p3`1 or p2`2 = p3`2 by A2,EUCLID:56;
end;
theorem
p`1 <> q`1 & p`2 <> q`2 & f = <* p,|[q`1,p`2]|,q *> implies
f/.1 = p & f/.len f = q & f is_S-Seq
proof
set p1 = |[q`1,p`2]|; assume
A1: p`1 <> q`1 & p`2 <> q`2 & f = <* p,p1,q *>;
then A2: len f = 1 + 2 & f/.1 = p & f/.2 = p1 & f/.3 = q
by FINSEQ_1:62,FINSEQ_4:27;
hence f/.1 = p & f/.len f = q;
p<>p1 & q<>p1 by A1,EUCLID:56;
hence f is one-to-one & len f >= 2 by A1,A2,FINSEQ_3:104;
thus f is unfolded
proof let i; assume
A3: 1 <= i & i + 2 <= len f;
then i <= 1 by A2,REAL_1:53;
then A4: i = 1 by A3,AXIOMS:21;
hence LSeg(f,i) /\ LSeg(f,i+1) = LSeg(p,p1) /\ LSeg(f,2)
by A2,TOPREAL1:def 5
.= LSeg(p,p1) /\ LSeg(p1,q) by A2,TOPREAL1:def 5
.= {f/.(i+1)} by A2,A4,Th37;
end;
thus f is s.n.c.
proof let i,j such that
A5: i+1 < j;
now per cases;
suppose i=0; then LSeg(f,i)={} by TOPREAL1:def 5;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
suppose i<>0; then LSeg(f,j)={} by A1,A5,Th21;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
hence thesis;
end;
let i such that
A6: 1 <= i & i + 1 <= len f;
set p2 = f/.i, p3 = f/.(i+1);
A7: i <= 2 & i > 0 by A2,A6,AXIOMS:22,REAL_1:53;
per cases by A7,CQC_THE1:3;
suppose i=1;
hence p2`1 = p3`1 or p2`2 = p3`2 by A2,EUCLID:56;
suppose i=2;
hence p2 `1 = p3`1 or p2`2 = p3`2 by A2,EUCLID:56;
end;
theorem
p`1 = q`1 & p`2 <> q`2 & f = <* p,|[p`1,(p`2 + q`2)/2]|,q *> implies
f/.1 = p & f/.len f = q & f is_S-Seq
proof
set p1 = |[p`1,(p`2 + q`2)/2]|; assume
A1: p`1 = q`1 & p`2 <> q`2 & f = <* p,p1,q *>;
then A2: len f = 1 + 2 & f/.1 = p & f/.2 = p1 & f/.3 = q
by FINSEQ_1:62,FINSEQ_4:27;
hence f/.1 = p & f/.len f = q;
p`2 <> (p`2+q`2)/2 &
q`2 <> (p`2+q`2)/2 & p1`2 = (p`2+q`2)/2 by A1,EUCLID:56,XCMPLX_1:67;
hence f is one-to-one & len f >= 2 by A1,A2,FINSEQ_3:104;
thus f is unfolded
proof let i; assume
A3: 1 <= i & i + 2 <= len f;
then i <= 1 by A2,REAL_1:53;
then A4: i = 1 by A3,AXIOMS:21;
hence LSeg(f,i) /\ LSeg(f,i+1) = LSeg(p,p1) /\ LSeg(f,2)
by A2,TOPREAL1:def 5
.= LSeg(p,p1) /\ LSeg(p1,q) by A2,TOPREAL1:def 5
.= {f/.(i+1)} by A1,A2,A4,Th38;
end;
thus f is s.n.c.
proof let i,j such that
A5: i+1 < j;
now per cases;
suppose i=0; then LSeg(f,i)={} by TOPREAL1:def 5;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
suppose i<>0; then LSeg(f,j)={} by A1,A5,Th21;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
hence thesis;
end;
let i such that
A6: 1 <= i & i + 1 <= len f;
set p2 = f/.i, p3 = f/.(i+1);
A7: i <= 2 & i > 0 by A2,A6,AXIOMS:22,REAL_1:53;
per cases by A7,CQC_THE1:3;
suppose i=1;
hence p2`1 = p3`1 or p2`2 = p3`2 by A2,EUCLID:56;
suppose i=2;
hence p2 `1 = p3`1 or p2`2 = p3`2 by A1,A2,EUCLID:56;
end;
theorem
p`1 <> q`1 & p`2 = q`2 & f = <* p,|[(p`1 + q`1)/2,p`2]|,q *> implies
f/.1 = p & f/.len f = q & f is_S-Seq
proof
set p1 = |[(p`1 + q`1)/2,p`2]|; assume
A1: p`1 <> q`1 & p`2 = q`2 & f = <* p,p1,q *>;
then A2: len f = 1 + 2 & f/.1 = p & f/.2 = p1 & f/.3 = q
by FINSEQ_1:62,FINSEQ_4:27;
hence f/.1 = p & f/.len f = q;
p`1 <> (p`1 + q`1)/2 &
q`1 <> (p`1 + q`1)/2 & p1`1 = (p`1 + q`1)/2 by A1,EUCLID:56,XCMPLX_1:67;
hence f is one-to-one & len f >= 2 by A1,A2,FINSEQ_3:104;
thus f is unfolded
proof let i; assume
A3: 1 <= i & i + 2 <= len f;
then i <= 1 by A2,REAL_1:53;
then A4: i = 1 by A3,AXIOMS:21;
hence LSeg(f,i) /\ LSeg(f,i+1) = LSeg(p,p1) /\ LSeg(f,2)
by A2,TOPREAL1:def 5
.= LSeg(p,p1) /\ LSeg(p1,q) by A2,TOPREAL1:def 5
.= {f/.(i+1)} by A1,A2,A4,Th39;
end;
thus f is s.n.c.
proof let i,j such that
A5: i+1 < j;
now per cases;
suppose i=0; then LSeg(f,i)={} by TOPREAL1:def 5;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
suppose i<>0; then LSeg(f,j)={} by A1,A5,Th21;
then LSeg(f,i) /\ LSeg(f,j) = {};
hence thesis by XBOOLE_0:def 7;
end;
hence thesis;
end;
let i such that
A6: 1 <= i & i + 1 <= len f;
set p2 = f/.i, p3 = f/.(i+1);
A7: i <= 2 & i > 0 by A2,A6,AXIOMS:22,REAL_1:53;
per cases by A7,CQC_THE1:3;
suppose i=1;
hence p2`1 = p3`1 or p2`2 = p3`2 by A2,EUCLID:56;
suppose i=2;
hence p2 `1 = p3`1 or p2`2 = p3`2 by A1,A2,EUCLID:56;
end;
theorem
i in dom f & i+1 in dom f implies
L~(f|(i+1)) = L~(f|i) \/ LSeg(f/.i,f/.(i+1))
proof
set M1={LSeg(f|(i+1),k): 1<=k & k+1<=len(f|(i+1))},
Mi={LSeg(f|i,n): 1<=n & n+1<=len(f|i)}; assume
A1: i in dom f & i+1 in dom f;
set p = f/.i, q= f/.(i+1);
A2: Seg len(f|(i+1)) = dom(f|(i+1)) &
Seg len f = dom f & f|(i+1) = f|Seg(i+1) & f|i = f|Seg i
by FINSEQ_1:def 3,TOPREAL1:def 1;
A3: 1<=i+1 & i+1<=len f & 1<=i & i<=len f by A1,FINSEQ_3:27;
then Seg(i+1) c= Seg len f & Seg i c= Seg len f by FINSEQ_1:7;
then Seg(i+1) c= dom f & Seg i c= dom f by FINSEQ_1:def 3;
then Seg(i+1) = dom f /\ Seg(i+1) & dom f /\ Seg i = Seg i by XBOOLE_1:28;
then A4: Seg(i+1)=dom(f|Seg(i+1)) & dom(f|(Seg i))=Seg i by FUNCT_1:68;
then A5: i+1=len(f|(i+1)) & i=len(f|i) & i<=i+1 by A2,FINSEQ_1:def 3,NAT_1:29
;
then LSeg(f,i) = LSeg(p,q) & i+1 in dom(f|(i+1)) & i in dom(f|(i+1))
by A3,FINSEQ_3:27,TOPREAL1:def 5;
then A6: LSeg(f|(i+1),i) = LSeg(p,q) by A1,Th24;
then A7: LSeg(p,q) c= L~(f|(i+1)) by Th26;
thus L~(f|(i+1)) c= L~(f|i) \/ LSeg(p,q)
proof
let x; assume x in L~(f|(i+1)); then x in union M1 by TOPREAL1:def 6;
then consider X be set such that
A8: x in X & X in M1 by TARSKI:def 4;
consider m such that
A9: X=LSeg(f|(i+1),m) & 1<=m & m+1<=len(f|(i+1)) by A8;
A10: m <= i by A5,A9,REAL_1:53;
per cases by A10,REAL_1:def 5;
suppose m = i;
then X c= L~(f|i) \/ LSeg(p,q) by A6,A9,XBOOLE_1:7;
hence thesis by A8;
suppose A11: m < i;
then A12: m<=i & m+1<=i & m<=m+1 & i<=i+1 by NAT_1:38;
A13: m+1<=len(f|i) & 1<=m+1 by A5,A9,A11,NAT_1:38;
then A14: m in dom(f|i) & m+1 in dom(f|i) & m<=i+1
by A2,A4,A9,A12,AXIOMS:22,FINSEQ_1:3;
then m in dom(f|(i+1)) & m+1 in dom(f|(i+1)) by A2,A4,A9,A13,FINSEQ_1:3;
then X = LSeg(f,m) by A1,A9,Th24
.= LSeg(f|i,m) by A1,A14,Th24;
then X in Mi by A5,A9,A12;
then x in union Mi by A8,TARSKI:def 4;
then x in L~(f|i) by TOPREAL1:def 6;
hence thesis by XBOOLE_0:def 2;
end;
let x such that A15: x in L~(f|i) \/ LSeg(p,q);
per cases by A15,XBOOLE_0:def 2;
suppose x in L~(f|i); then x in union Mi by TOPREAL1:def 6;
then consider X be set such that
A16: x in X & X in Mi by TARSKI:def 4;
consider m such that
A17: X=LSeg(f|i,m) & 1<=m & m+1<=len(f|i) by A16;
m<=m+1 by NAT_1:29;
then A18: 1<=m & m<=len(f|i) & 1<=m+1 & m+1<=len(f|i) by A17,AXIOMS:22;
then A19: m in dom(f|i) & m+1 in dom(f|i) & m<=len(f|(i+1)) & m+1<=len(f|(i
+1))
by A5,AXIOMS:22,FINSEQ_3:27;
then A20: m in dom(f|(i+1)) & m+1 in dom(f|(i+1)) & len(f|i) <= len(f|(i+1)
)
by A5,A18,FINSEQ_3:27;
X = LSeg(f,m) by A1,A17,A19,Th24
.= LSeg(f|(i+1),m) by A1,A20,Th24;
then X in M1 by A17,A19;
then x in union M1 by A16,TARSKI:def 4;
hence thesis by TOPREAL1:def 6;
suppose x in LSeg(p,q); hence thesis by A7;
end;
theorem
len f>=2 & not p in L~f implies for n st 1<=n & n<=len f holds f/.n<>p
proof assume
A1: len f>=2 & not p in L~f;
given n such that
A2: 1<=n & n<=len f & f/.n=p;
set Mf={LSeg(f,k): 1<=k & k+1<=len f};
per cases by A2,REAL_1:def 5;
suppose A3: n=len f;
len f>=1 by A1,AXIOMS:22;
then reconsider j = len f - 1 as Nat by INT_1:18;
1+1<=len f
by A1;
then 1<=j & j+1<=len f by REAL_1:84;
then f/.(j+1) in LSeg(f,j) & LSeg(f,j) in Mf by TOPREAL1:27;
then f/.(j+1) in union Mf by TARSKI:def 4;
then f/.n in union Mf by A3,XCMPLX_1:27;
hence contradiction by A1,A2,TOPREAL1:def 6;
suppose A4: n<len f;
then n+1<=len f by NAT_1:38;
then A5: LSeg(f,n) in Mf by A2;
n+1<=len f & 1<=n by A2,A4,NAT_1:38;
then f/.n in LSeg(f,n) by TOPREAL1:27;
then f/.n in union Mf by A5,TARSKI:def 4;
hence contradiction by A1,A2,TOPREAL1:def 6;
end;
theorem
q<>p & LSeg(q,p) /\ L~f = {q} implies not p in L~f
proof assume
A1: q<>p & LSeg(q,p) /\ L~f = {q} & p in L~f;
p in LSeg(q,p) by TOPREAL1:6;
then p in {q} by A1,XBOOLE_0:def 3;
hence contradiction by A1,TARSKI:def 1;
end;
theorem
f is_S-Seq & not f/.1 in Ball(u,r) & q in Ball(u,r) &
f/.len f in LSeg(f,m) & 1<=m & m + 1 <=len f & LSeg(f,m) meets Ball(u,r)
implies m + 1 = len f
proof assume
A1: f is_S-Seq & not f/.1 in Ball(u,r) & q in Ball(u,r) &
f/.len f in LSeg(f,m) & 1<=m & m + 1 <= len f &
LSeg(f,m) /\ Ball(u,r) <> {};
then A2: len f >=2 by TOPREAL1:def 10;
then A3: 1<=len f by AXIOMS:22;
then reconsider k = len f - 1 as Nat by INT_1:18;
A4: k+1 = len f by XCMPLX_1:27;
set q= f/.len f;
A5: f is s.n.c. by A1,TOPREAL1:def 10;
A6: f is unfolded by A1,TOPREAL1:def 10;
assume m + 1 <> len f;
then A7: m+1<=k by A1,A4,NAT_1:26;
A8: m+1+1=m+(1+1) by XCMPLX_1:1;
A9: f is one-to-one by A1,TOPREAL1:def 10;
A10: len f in dom f by A3,FINSEQ_3:27;
per cases by A7,REAL_1:def 5;
suppose A11: m+1=k;
then A12: LSeg(f,m) /\ LSeg(f,m+1) = {f/.(m+1)} by A1,A4,A6,A8,TOPREAL1:
def 8;
A13: m+1+1<=len f & 1<=m+1 & m+1<=len f by A4,A11,NAT_1:29;
then f/.(m+2) in LSeg(f,m+1) by A8,TOPREAL1:27;
then q in LSeg(f,m+1) by A8,A11,XCMPLX_1:27;
then q in {f/.(m+1)} by A1,A12,XBOOLE_0:def 3;
then A14: f/.len f=f/.(m+1) by TARSKI:def 1;
m+1 in dom f by A13,FINSEQ_3:27;
then len f= len f -1 by A9,A10,A11,A14,PARTFUN2:17; hence contradiction
by XCMPLX_1:16;
suppose m+1<k;
then LSeg(f,m) misses LSeg(f,k) by A5,TOPREAL1:def 9;
then A15: LSeg(f,m) /\ LSeg(f,k) = {} by XBOOLE_0:def 7;
A16: k+1 = len f by XCMPLX_1:27;
(1+1)-1 = 1;
then 1<=k by A2,REAL_1:92;
then q in LSeg(f,k) by A16,TOPREAL1:27;
hence contradiction by A1,A15,XBOOLE_0:def 3;
end;
theorem
not p1 in Ball(u,r) & q in Ball(u,r) & p in Ball(u,r) & not p in LSeg(p1,q) &
((q`1=p`1 & q`2<>p`2) or (q`1<>p`1 & q`2=p`2)) & (p1`1=q`1 or p1`2=q`2) implies
LSeg(p1,q) /\ LSeg(q,p) = {q}
proof
assume A1: not p1 in Ball(u,r) & q in Ball(u,r) & p in Ball(u,r) &
not p in LSeg(p1,q);
assume A2: (q`1=p`1 & q`2<>p`2) or (q`1<>p`1 & q`2=p`2);
assume A3: p1`1=q`1 or p1`2=q`2;
A4: now per cases by A3;
suppose p1`1=q`1;
hence (p1`1=q`1 & p1`2<>q`2) or (p1`1<>q`1 & p1`2=q`2) by A1,Th11;
suppose p1`2=q`2;
hence (p1`1=q`1 & p1`2<>q`2) or (p1`1<>q`1 & p1`2=q`2) by A1,Th11;
end;
A5: p=|[p`1,p`2]| & p1=|[p1`1,p1`2]| & q=|[q`1,q`2]| by EUCLID:57;
A6: LSeg(p,q) c= Ball(u,r) by A1,Th28;
now per cases by A2;
suppose A7: q`1=p`1 & q`2<>p`2;
set r = p`1,
pq = {p2: p2`1=r & p`2<=p2`2 & p2`2<=q`2},
qp = {p3: p3`1=r & q`2<=p3`2 & p3`2<=p`2},
pp1 = {p11: p11`1=r & p`2<=p11`2 & p11`2<=p1`2},
p1p = {p22: p22`1=r & p1`2<=p22`2 & p22`2<=p`2},
qp1 = {q1: q1`1=r & q`2<=q1`2 & q1`2<=p1`2},
p1q = {q2: q2`1=r & p1`2<=q2`2 & q2`2<=q`2};
now per cases by A7,REAL_1:def 5;
suppose A8: q`2>p`2;
now per cases by A4;
suppose A9: p1`1=q`1 & p1`2<>q`2;
now per cases by A9,REAL_1:def 5;
case p1`2>q`2;
then q in pp1 & p1`2>p`2 by A7,A8,AXIOMS:22;
then q in LSeg(p,p1) by A5,A7,A9,Th15;
hence thesis by TOPREAL1:14;
case A10: p1`2<q`2;
now per cases by AXIOMS:21;
suppose p1`2>p`2;
then p1 in pq & p`2<q`2 by A7,A9,A10,AXIOMS:22;
then p1 in LSeg(p,q) by A5,A7,Th15;
hence contradiction by A1,A6;
suppose p1`2=p`2;hence contradiction by A1,A7,A9,Th11;
suppose p1`2<p`2;
then p in p1q by A8;
hence contradiction by A1,A5,A7,A9,A10,Th15;
end;
hence contradiction;
end;
hence thesis;
suppose p1`1<>q`1 & p1`2=q`2;
hence thesis by A5,A7,Th37;
end;
hence thesis;
suppose A11: q`2<p`2;
now per cases by A4;
suppose A12: p1`1=q`1 & p1`2<>q`2;
now per cases by A12,REAL_1:def 5;
case A13: p1`2>q`2;
now per cases by AXIOMS:21;
suppose p1`2>p`2;
then p in qp1 by A11;
hence contradiction by A1,A5,A7,A12,A13,Th15;
suppose p1`2=p`2;hence contradiction by A1,A7,A12,Th11;
suppose p1`2<p`2;
then p1 in qp by A7,A12,A13;
then p1 in LSeg(p,q) by A5,A7,A11,Th15;
hence contradiction by A1,A6;
end;
hence contradiction;
case p1`2<q`2;
then q in p1p & p1`2<p`2 by A7,A11,AXIOMS:22;
then q in LSeg(p1,p) by A5,A7,A12,Th15;
hence LSeg(p1,q) /\ LSeg(q,p) = {q} by TOPREAL1:14;
end;
hence thesis;
suppose p1`1<>q`1 & p1`2=q`2;
hence thesis by A5,A7,Th37;
end;
hence thesis;
end;
hence thesis;
suppose A14: q`1<>p`1 & q`2=p`2;
set r = p`2,
pq = {p2: p2`2=r & p`1<=p2`1 & p2`1<=q`1},
qp = {p3: p3`2=r & q`1<=p3`1 & p3`1<=p`1},
pp1 = {p11: p11`2=r & p`1<=p11`1 & p11`1<=p1`1},
p1p = {p22: p22`2=r & p1`1<=p22`1 & p22`1<=p`1},
qp1 = {q1: q1`2=r & q`1<=q1`1 & q1`1<=p1`1},
p1q = {q2: q2`2=r & p1`1<=q2`1 & q2`1<=q`1};
now per cases by A14,REAL_1:def 5;
suppose A15: q`1>p`1;
now per cases by A4;
suppose p1`1=q`1 & p1`2<>q`2;
hence thesis by A5,A14,Th36;
suppose A16: p1`1<>q`1 & p1`2=q`2;
now per cases by A16,REAL_1:def 5;
case p1`1>q`1;
then q in pp1 & p1`1>p`1 by A14,A15,AXIOMS:22;
then q in LSeg(p,p1) by A5,A14,A16,Th16;
hence thesis by TOPREAL1:14;
case A17: p1`1<q`1;
now per cases by AXIOMS:21;
suppose p1`1>p`1;
then p1 in pq & p`1<q`1 by A14,A16,A17,AXIOMS:22;
then p1 in LSeg(p,q) by A5,A14,Th16;
hence contradiction by A1,A6;
suppose p1`1=p`1;
hence contradiction by A1,A14,A16,Th11;
suppose p1`1<p`1; then p in p1q by A15;
hence contradiction by A1,A5,A14,A16,A17,Th16;
end;
hence contradiction;
end;
hence thesis;
end;
hence thesis;
suppose A18: q`1<p`1;
now per cases by A4;
suppose p1`1=q`1 & p1`2<>q`2;
hence thesis by A5,A14,Th36;
suppose A19: p1`1<>q`1 & p1`2=q`2;
now per cases by A19,REAL_1:def 5;
case A20: p1`1>q`1;
now per cases by AXIOMS:21;
suppose p1`1>p`1;
then p in qp1 by A18;
hence contradiction by A1,A5,A14,A19,A20,Th16;
suppose p1`1=p`1;
hence contradiction by A1,A14,A19,Th11;
suppose p1`1<p`1;
then p1 in qp by A14,A19,A20;
then p1 in LSeg(p,q) by A5,A14,A18,Th16;
hence contradiction by A1,A6;
end;
hence contradiction;
case p1`1<q`1;
then q in p1p & p1`1<p`1 by A14,A18,AXIOMS:22;
then q in LSeg(p1,p) by A5,A14,A19,Th16;
hence thesis by TOPREAL1:14;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
theorem
not p1 in Ball(u,r) & p in Ball(u,r) &
|[p`1,q`2]| in Ball(u,r) & q in Ball(u,r) &
not |[p`1,q`2]| in LSeg(p1,p) & p1`1 = p`1 & p`1<>q`1 & p`2<>q`2 implies
(LSeg(p,|[p`1,q`2]|) \/ LSeg(|[p`1,q`2]|,q)) /\ LSeg(p1,p) = {p}
proof
set v = |[p`1,q`2]|; assume
A1: not p1 in Ball(u,r) & p in Ball(u,r) & v in Ball(u,r) & q in Ball(u,r) &
not v in LSeg(p1,p) & p1`1=p`1 & p`1<>q`1 & p`2<>q`2;
A2: p in LSeg(p,v) & p in LSeg(p1,p) by TOPREAL1:6;
then A3: p in LSeg(p,v) \/ LSeg(v,q) by XBOOLE_0:def 2;
A4: (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) =
LSeg(p,v) /\ LSeg(p1,p) \/ LSeg(v,q) /\ LSeg(p1,p) by XBOOLE_1:23;
p in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by A2,A3,XBOOLE_0:def 3;
then A5: {p} c= (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by ZFMISC_1:37;
A6: p1=|[p`1,p1`2]| & p=|[p`1,p`2]| & q=|[q`1,q`2]| &
v`1=p`1 & v`2=q`2 by A1,EUCLID:56,57;
A7: LSeg(p,v) c= Ball(u,r) by A1,Th28;
per cases;
suppose p1`2=p`2;
hence thesis by A1,Th11;
suppose A8: p1`2<>p`2;
now per cases by A8,REAL_1:def 5;
suppose A9: p1`2>p`2;
now per cases by A1,REAL_1:def 5;
suppose A10: p`1>q`1;
now per cases by A1,REAL_1:def 5;
case A11: p`2>q`2;
then A12: p`2>=v`2 by EUCLID:56;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof let x such that A13:
x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now per cases by A4,A13,XBOOLE_0:def 2;
case A14: x in LSeg(p,v) /\ LSeg(p1,p);
A15: v`2<p1`2 by A6,A9,A11,AXIOMS:22;
p in {q1: q1`1=p`1 & v`2<=q1`2 & q1`2<=p1`2} by A9,A12;
then p in LSeg(p1,v) by A6,A15,Th15;
hence x in {p} by A14,TOPREAL1:14;
case x in LSeg(v,q) /\ LSeg(p1,p);
then A16: x in LSeg(v,q) & x in LSeg(p1,p) by XBOOLE_0:def 3;
then x in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2} by A6,A9,Th15;
then consider q2 such that
A17: q2=x & q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2;
x in {p2: p2`2=q`2 & q`1<=p2`1 & p2`1<=p`1} by A6,A10,A16,Th16;
then ex p2 st p2=x & p2`2=q`2 & q`1<=p2`1 & p2`1<=p`1;
hence contradiction by A11,A17;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_0:def 10;
case A18: p`2<q`2;
now per cases by AXIOMS:21;
suppose A19: q`2>p1`2;
then A20: p1 in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=v`2} by A1,A6,A9;
p`2<v`2 by A6,A9,A19,AXIOMS:22;
then p1 in LSeg(p,v) by A6,A20,Th15;
hence contradiction by A1,A7;
suppose q`2=p1`2;
hence contradiction by A1,EUCLID:57;
suppose A21: q`2<p1`2;
then A22: v in {p2: p2`1=p`1 & p`2<=p2`2 & p2`2<=p1`2} by A6,A18;
p`2<p1`2 by A18,A21,AXIOMS:22;
hence contradiction by A1,A6,A22,Th15;
end;
hence contradiction;
end;
hence thesis;
suppose A23: p`1<q`1;
now per cases by A1,REAL_1:def 5;
case A24: p`2>q`2;
then A25: p`2>=v`2 by EUCLID:56;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof let x such that A26:
x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now per cases by A4,A26,XBOOLE_0:def 2;
case A27: x in LSeg(p,v) /\ LSeg(p1,p);
A28: v`2<p1`2 by A6,A9,A24,AXIOMS:22;
p in {q1: q1`1=p`1 & v`2<=q1`2 & q1`2<=p1`2} by A9,A25;
then p in LSeg(p1,v) by A6,A28,Th15;
hence x in {p} by A27,TOPREAL1:14;
case x in LSeg(v,q) /\ LSeg(p1,p);
then A29: x in LSeg(v,q) & x in LSeg(p1,p) by XBOOLE_0:def 3;
then x in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2} by A6,A9,Th15;
then A30: ex q2 st q2=x & q2`1=p`1 & p`2<=q2`2 & q2`2<=p1`2;
x in {p2: p2`2=q`2 & p`1<=p2`1 & p2`1<=q`1}
by A6,A23,A29,Th16;
then ex p2 st p2=x & p2`2=q`2 & p`1<=p2`1 & p2`1<=q`1;
hence contradiction by A24,A30;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_0:def 10;
case A31: p`2<q`2;
now per cases by AXIOMS:21;
suppose A32: q`2>p1`2;
then A33: p1 in {q2: q2`1=p`1 & p`2<=q2`2 & q2`2<=v`2} by A1,A6,A9;
p`2<v`2 by A6,A9,A32,AXIOMS:22;
then p1 in LSeg(p,v) by A6,A33,Th15;
hence contradiction by A1,A7;
suppose q`2=p1`2;
hence contradiction by A1,EUCLID:57;
suppose A34: q`2<p1`2;
then A35: v in {p2: p2`1=p`1 & p`2<=p2`2 & p2`2<=p1`2} by A6,A31;
p`2<p1`2 by A31,A34,AXIOMS:22;
hence contradiction by A1,A6,A35,Th15;
end;
hence contradiction;
end;
hence thesis;
end;
hence thesis;
suppose A36: p1`2<p`2;
now per cases by A1,REAL_1:def 5;
suppose A37: p`1>q`1;
now per cases by A1,REAL_1:def 5;
case A38: p`2>q`2;
now per cases by AXIOMS:21;
suppose A39: q`2>p1`2;
then A40: v in {p2: p2`1=p`1 & p1`2<=p2`2 & p2`2<=p`2} by A6,A38;
p1`2<p`2 by A38,A39,AXIOMS:22;
hence contradiction by A1,A6,A40,Th15;
suppose q`2=p1`2;
hence contradiction by A1,EUCLID:57;
suppose A41: q`2<p1`2;
then A42: p1 in {q2: q2`1=p`1 & v`2<=q2`2 & q2`2<=p`2} by A1,A6,A36
;
v`2<p`2 by A6,A36,A41,AXIOMS:22;
then p1 in LSeg(p,v) by A6,A42,Th15;
hence contradiction by A1,A7;
end;
hence contradiction;
case A43: p`2<q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof let x such that A44:
x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now per cases by A4,A44,XBOOLE_0:def 2;
case A45: x in LSeg(p,v) /\ LSeg(p1,p);
A46: p1`2<v`2 by A6,A36,A43,AXIOMS:22;
p in {q1: q1`1=p`1 & p1`2<=q1`2 & q1`2<=v`2} by A6,A36,A43;
then p in LSeg(p1,v) by A6,A46,Th15;
hence x in {p} by A45,TOPREAL1:14;
case x in LSeg(v,q) /\ LSeg(p1,p);
then A47: x in LSeg(v,q) & x in LSeg(p1,p) by XBOOLE_0:def 3;
then x in {q2: q2`1=p`1 & p1`2<=q2`2 & q2`2<=p`2} by A6,A36,Th15
;
then A48: ex q2 st q2=x & q2`1=p`1 & p1`2<=q2`2 & q2`2<=p`2;
x in {p2: p2`2=q`2 & q`1<=p2`1 & p2`1<=p`1}
by A6,A37,A47,Th16;
then ex p2 st p2=x & p2`2=q`2 & q`1<=p2`1 & p2`1<=p`1;
hence contradiction by A43,A48;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
hence thesis;
suppose A49: p`1<q`1;
now per cases by A1,REAL_1:def 5;
case A50: p`2>q`2;
now per cases by AXIOMS:21;
suppose A51: q`2>p1`2;
then A52: v in {p2: p2`1=p`1 & p1`2<=p2`2 & p2`2<=p`2} by A6,A50;
p1`2<p`2 by A50,A51,AXIOMS:22;
hence contradiction by A1,A6,A52,Th15;
suppose q`2=p1`2;
hence contradiction by A1,EUCLID:57;
suppose A53: q`2<p1`2;
then A54: p1 in {q2: q2`1=p`1 & v`2<=q2`2 & q2`2<=p`2} by A1,A6,A36
;
v`2<p`2 by A6,A36,A53,AXIOMS:22;
then p1 in LSeg(p,v) by A6,A54,Th15;
hence contradiction by A1,A7;
end;
hence contradiction;
case A55: p`2<q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof let x such that
A56: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now per cases by A4,A56,XBOOLE_0:def 2;
case A57: x in LSeg(p,v) /\ LSeg(p1,p);
A58: p1`2<v`2 by A6,A36,A55,AXIOMS:22;
p in {q1: q1`1=p`1 & p1`2<=q1`2 & q1`2<=v`2} by A6,A36,A55;
then p in LSeg(p1,v) by A6,A58,Th15;
hence x in {p} by A57,TOPREAL1:14;
case x in LSeg(v,q) /\ LSeg(p1,p);
then A59: x in LSeg(v,q) & x in LSeg(p1,p) by XBOOLE_0:def 3;
then x in {q2: q2`1=p`1 & p1`2<=q2`2 & q2`2<=p`2} by A6,A36,Th15
;
then A60: ex q2 st q2=x & q2`1=p`1 & p1`2<=q2`2 & q2`2<=p`2;
x in {p2: p2`2=q`2 & p`1<=p2`1 & p2`1<=q`1}
by A6,A49,A59,Th16;
then ex p2 st p2=x & p2`2=q`2 & p`1<=p2`1 & p2`1<=q`1;
hence contradiction by A55,A60;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
theorem
not p1 in Ball(u,r) & p in Ball(u,r) &
|[q`1,p`2]| in Ball(u,r) & q in Ball(u,r) &
not |[q`1,p`2]| in LSeg(p1,p) & p1`2 = p`2 & p`1<>q`1 & p`2<>q`2 implies
(LSeg(p,|[q`1,p`2]|) \/ LSeg(|[q`1,p`2]|,q)) /\ LSeg(p1,p) = {p}
proof
set v = |[q`1,p`2]|; assume
A1: not p1 in Ball(u,r) & p in Ball(u,r) & v in Ball(u,r) & q in Ball(u,r) &
not v in LSeg(p1,p) & p1`2=p`2 & p`1<>q`1 & p`2<>q`2;
A2: p in LSeg(p,v) & p in LSeg(p1,p) by TOPREAL1:6;
then A3: p in LSeg(p,v) \/ LSeg(v,q) by XBOOLE_0:def 2;
A4: (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) =
LSeg(p,v) /\ LSeg(p1,p) \/ LSeg(v,q) /\ LSeg(p1,p) by XBOOLE_1:23;
p in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by A2,A3,XBOOLE_0:def 3;
then A5: {p} c= (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) by ZFMISC_1:37;
A6: p1=|[p1`1,p`2]| & p=|[p`1,p`2]| & q=|[q`1,q`2]| &
v`1=q`1 & v`2=p`2 by A1,EUCLID:56,57;
A7: LSeg(p,v) c= Ball(u,r) by A1,Th28;
per cases;
suppose p1`1=p`1;
hence thesis by A1,Th11;
suppose A8: p1`1<>p`1;
now per cases by A8,REAL_1:def 5;
suppose A9: p1`1>p`1;
now per cases by A1,REAL_1:def 5;
case A10: p`1>q`1;
then A11: p`1>=v`1 by EUCLID:56;
now per cases by A1,REAL_1:def 5;
suppose A12: p`2>q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof let x such that A13:
x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now per cases by A4,A13,XBOOLE_0:def 2;
case A14: x in LSeg(p,v) /\ LSeg(p1,p);
A15: v`1<p1`1 by A6,A9,A10,AXIOMS:22;
p in {q1: q1`2=p`2 & v`1<=q1`1 & q1`1<=p1`1} by A9,A11;
then p in LSeg(p1,v) by A6,A15,Th16;
hence x in {p} by A14,TOPREAL1:14;
case x in LSeg(v,q) /\ LSeg(p1,p);
then A16: x in LSeg(q,v) & x in LSeg(p,p1) by XBOOLE_0:def 3;
then x in {q2: q2`2=p`2 & p`1<=q2`1 & q2`1<=p1`1} by A6,A9,Th16;
then A17: ex q2 st q2=x & q2`2=p`2 & p`1<=q2`1 & q2`1<=p1`1;
x in {p2: p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2} by A6,A12,A16,Th15;
then ex p2 st p2=x & p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2;
hence contradiction by A10,A17;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_0:def 10;
suppose A18: p`2<q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof let x such that
A19: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now per cases by A4,A19,XBOOLE_0:def 2;
case A20: x in LSeg(p,v) /\ LSeg(p1,p);
A21: v`1<p1`1 by A6,A9,A10,AXIOMS:22;
p in {q1: q1`2=p`2 & v`1<=q1`1 & q1`1<=p1`1} by A9,A11;
then p in LSeg(p1,v) by A6,A21,Th16;
hence x in {p} by A20,TOPREAL1:14;
case x in LSeg(v,q) /\ LSeg(p1,p);
then A22: x in LSeg(v,q) & x in LSeg(p1,p) by XBOOLE_0:def 3;
then x in {q2: q2`2=p`2 & p`1<=q2`1 & q2`1<=p1`1} by A6,A9,Th16;
then A23: ex q2 st q2=x & q2`2=p`2 & p`1<=q2`1 & q2`1<=p1`1;
x in {p2: p2`1=q`1 & v`2<=p2`2 & p2`2<=q`2} by A6,A18,A22,Th15;
then ex p2 st p2=x & p2`1=q`1 & v`2<=p2`2 & p2`2<=q`2;
hence contradiction by A10,A23;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
hence thesis;
case A24: p`1<q`1;
now per cases by AXIOMS:21;
suppose A25: q`1>p1`1;
then A26: p1 in {q2: q2`2=p`2 & p`1<=q2`1 & q2`1<=v`1} by A1,A6,A9;
p`1<v`1 by A6,A9,A25,AXIOMS:22;
then p1 in LSeg(p,v) by A6,A26,Th16;
hence contradiction by A1,A7;
suppose q`1=p1`1;
hence contradiction by A1,EUCLID:57;
suppose q`1<p1`1;
then v in {p2: p2`2=p`2 & p`1<=p2`1 & p2`1<=p1`1} by A6,A24;
hence contradiction by A1,A6,A9,Th16;
end;
hence contradiction;
end;
hence thesis;
suppose A27: p1`1<p`1;
now per cases by A1,REAL_1:def 5;
case A28: p`1>q`1;
now per cases by AXIOMS:21;
suppose q`1>p1`1;
then v in {q2: q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1} by A6,A28;
hence contradiction by A1,A6,A27,Th16;
suppose q`1=p1`1;
hence contradiction by A1,EUCLID:57;
suppose A29: q`1<p1`1;
then A30: p1 in {p2: p2`2=p`2 & v`1<=p2`1 & p2`1<=p`1} by A1,A6,A27;
v`1<p`1 by A6,A27,A29,AXIOMS:22;
then p1 in LSeg(p,v) by A6,A30,Th16;
hence contradiction by A1,A7;
end;
hence contradiction;
case A31: p`1<q`1;
then A32: p`1<=v`1 by EUCLID:56;
now per cases by A1,REAL_1:def 5;
suppose A33: p`2>q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof let x such that
A34: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now per cases by A4,A34,XBOOLE_0:def 2;
case A35: x in LSeg(p,v) /\ LSeg(p1,p);
A36: p1`1<v`1 by A6,A27,A31,AXIOMS:22;
p in {q1: q1`2=p`2 & p1`1<=q1`1 & q1`1<=v`1} by A27,A32;
then p in LSeg(p1,v) by A6,A36,Th16;
hence x in {p} by A35,TOPREAL1:14;
case x in LSeg(v,q) /\ LSeg(p1,p);
then A37: x in LSeg(v,q) & x in LSeg(p1,p) by XBOOLE_0:def 3;
then x in {q2: q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1} by A6,A27,Th16
;
then A38: ex q2 st q2=x & q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1;
x in {p2: p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2} by A6,A33,A37,Th15;
then ex p2 st p2=x & p2`1=q`1 & q`2<=p2`2 & p2`2<=p`2;
hence contradiction by A31,A38;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_0:def 10;
suppose A39: p`2<q`2;
(LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p) c= {p}
proof let x such that
A40: x in (LSeg(p,v) \/ LSeg(v,q)) /\ LSeg(p1,p);
now per cases by A4,A40,XBOOLE_0:def 2;
case A41: x in LSeg(p,v) /\ LSeg(p1,p);
A42: p1`1<v`1 by A6,A27,A31,AXIOMS:22;
p in {q1: q1`2=p`2 & p1`1<=q1`1 & q1`1<=v`1} by A27,A32;
then p in LSeg(p1,v) by A6,A42,Th16;
hence x in {p} by A41,TOPREAL1:14;
case x in LSeg(v,q) /\ LSeg(p1,p);
then A43: x in LSeg(v,q) & x in LSeg(p1,p) by XBOOLE_0:def 3;
then x in {q2: q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1} by A6,A27,Th16
;
then A44: ex q2 st q2=x & q2`2=p`2 & p1`1<=q2`1 & q2`1<=p`1;
x in {p2: p2`1=q`1 & v`2<=p2`2 & p2`2<=q`2} by A6,A39,A43,Th15;
then ex p2 st p2=x & p2`1=q`1 & v`2<=p2`2 & p2`2<=q`2;
hence contradiction by A31,A44;
end;
hence thesis;
end;
hence thesis by A5,XBOOLE_0:def 10;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;