Copyright (c) 1995 Association of Mizar Users
environ
vocabulary PRE_TOPC, EUCLID, GOBOARD1, MCART_1, ARYTM_1, METRIC_1, PCOMPS_1,
TOPS_1, SQUARE_1, FUNCT_1, FINSEQ_1, TREES_1, GOBOARD5, ARYTM_3,
ABSVALUE, BOOLE, TOPREAL1, ARYTM;
notation TARSKI, XBOOLE_0, ORDINAL1, XREAL_0, REAL_1, NAT_1, ABSVALUE,
SQUARE_1, BINARITH, BINOP_1, FINSEQ_1, MATRIX_1, STRUCT_0, METRIC_1,
PRE_TOPC, TOPS_1, PCOMPS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD5;
constructors REAL_1, ABSVALUE, SQUARE_1, BINARITH, TOPS_1, PCOMPS_1, GOBOARD1,
GOBOARD5, MEMBERED, XBOOLE_0;
clusters STRUCT_0, RELSET_1, EUCLID, XREAL_0, PCOMPS_1, METRIC_1, ARYTM_3,
MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems GOBOARD5, TOPS_1, SPPOL_2, TOPMETR, METRIC_1, PCOMPS_1, PRE_TOPC,
EUCLID, GOBOARD1, RLVECT_1, REAL_1, AXIOMS, SEQ_2, TOPREAL3, REAL_2,
SQUARE_1, ABSVALUE, TARSKI, SPPOL_1, TOPREAL1, NAT_1, AMI_5, XBOOLE_0,
XBOOLE_1, XREAL_0, XCMPLX_0, XCMPLX_1;
begin
reserve i,j,n for Nat,
r,s,r1,s1,r2,s2,r',s' for Real,
p,q for Point of TOP-REAL 2,
G for Go-board,
x,y for set,
v for Point of Euclid 2;
Lm1:
(p+q)`1 = p`1+q`1 & (p+q)`2 = p`2+q`2
proof
p + q = |[ p`1 + q`1, p`2 + q`2]| by EUCLID:59;
hence thesis by EUCLID:56;
end;
Lm2:
(p-q)`1 = p`1-q`1 & (p-q)`2 = p`2-q`2
proof
p - q = |[ p`1 - q`1, p`2 - q`2]| by EUCLID:65;
hence thesis by EUCLID:56;
end;
Lm3:
(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;
canceled 3;
theorem Th4:
for M being non empty Reflexive MetrStruct, u being Point of M,
r being real number holds
r > 0 implies u in Ball(u,r)
proof let M be non empty Reflexive MetrStruct, u be Point of M,
r be real number;
A1: Ball(u,r) = {q where q is Point of M:dist(u,q)<r} by METRIC_1:18;
assume
A2: r > 0;
dist(u,u) = 0 by METRIC_1:1;
hence u in Ball(u,r) by A1,A2;
end;
Lm4:
for M being MetrSpace, B being Subset of TopSpaceMetr(M),r being real number,
u being Point of M st B = Ball(u,r)
holds B is open
proof let M be MetrSpace, B be Subset of TopSpaceMetr(M), r be real number,
u be Point of M;
A1: TopSpaceMetr M = TopStruct (#the carrier of M,Family_open_set M#)
by PCOMPS_1:def 6;
assume
A2: B = Ball(u,r);
Ball(u,r) in Family_open_set M by PCOMPS_1:33;
hence B is open by A1,A2,PRE_TOPC:def 5;
end;
canceled;
theorem Th6:
for B being Subset of TOP-REAL n, u being Point of Euclid n
st B = Ball(u,r) holds B is open
proof TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
hence thesis by Lm4;
end;
theorem Th7:
for M being non empty MetrSpace, u being Point of M,
P being Subset of TopSpaceMetr(M)
holds u in Int P iff ex r being real number st r > 0 & Ball(u,r) c= P
proof let M be non empty MetrSpace, u be Point of M,
P be Subset of TopSpaceMetr(M);
A1:Int P is open by TOPS_1:51;
hereby assume u in Int P;
then consider r be real number such that
A2: r > 0 and
A3: Ball(u,r) c= Int P by A1,TOPMETR:22;
take r;
thus r > 0 by A2;
Int P c= P by TOPS_1:44;
hence Ball(u,r) c= P by A3,XBOOLE_1:1;
end;
given r being real number such that
A4: r > 0 and
A5: Ball(u,r) c= P;
A6: u in Ball(u,r) by A4,Th4;
TopSpaceMetr M = TopStruct (#the carrier of M,Family_open_set M#)
by PCOMPS_1:def 6;
then reconsider B = Ball(u,r) as Subset of TopSpaceMetr(M);
B is open by Lm4;
hence u in Int P by A5,A6,TOPS_1:54;
end;
theorem Th8:
for u being Point of Euclid n, P being Subset of TOP-REAL n
holds u in Int P iff ex r being real number st r > 0 & Ball(u,r) c= P
proof TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
hence thesis by Th7;
end;
theorem Th9: :: TOPREAL3:12
for u,v being Point of Euclid 2 st u = |[r1,s1]| & v = |[r2,s2]| holds
dist(u,v) =sqrt ((r1 - r2)^2 + (s1 - s2)^2)
proof let u,v be Point of Euclid 2 such that
A1: u = |[r1,s1]| and
A2: v = |[r2,s2]|;
A3: |[r1,s1]|`1 = r1 & |[r1,s1]|`2 = s1 & |[r2,s2]|`1 = r2 & |[r2,s2]|`2 = s2
by EUCLID:56;
Euclid 2 = MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
hence dist(u,v) = (Pitag_dist 2).(u,v) by METRIC_1:def 1
.= sqrt ((r1 - r2)^2 + (s1 - s2)^2) by A1,A2,A3,TOPREAL3:12;
end;
theorem Th10:
for u being Point of Euclid 2 st u = |[r,s]| holds
0 <= r2 & r2 < r1 implies |[r+r2,s]| in Ball(u,r1)
proof let u be Point of Euclid 2 such that
A1: u = |[r,s]| and
A2: 0 <= r2 and
A3: r2 < r1;
reconsider v = |[r+r2,s]| as Point of Euclid 2 by TOPREAL3:13;
dist(u,v) = sqrt ((r - (r+r2))^2 + (s - s)^2) by A1,Th9
.= sqrt ((r - (r+r2))^2 + 0^2) by XCMPLX_1:14
.= sqrt ((-(r - (r+r2)))^2) by SQUARE_1:60,61
.= sqrt ((r+r2-r)^2) by XCMPLX_1:143
.= sqrt (r2^2) by XCMPLX_1:26
.= r2 by A2,SQUARE_1:89;
hence |[r+r2,s]| in Ball(u,r1) by A3,METRIC_1:12;
end;
theorem Th11:
for u being Point of Euclid 2 st u = |[r,s]| holds
0 <= s2 & s2 < s1 implies |[r,s+s2]| in Ball(u,s1)
proof let u be Point of Euclid 2 such that
A1: u = |[r,s]| and
A2: 0 <= s2 and
A3: s2 < s1;
reconsider v = |[r,s+s2]| as Point of Euclid 2 by TOPREAL3:13;
dist(u,v) = sqrt ((r - r)^2 + (s - (s+s2))^2) by A1,Th9
.= sqrt ((s - (s+s2))^2 + 0^2) by XCMPLX_1:14
.= sqrt ((-(s - (s+s2)))^2) by SQUARE_1:60,61
.= sqrt ((s+s2-s)^2) by XCMPLX_1:143
.= sqrt (s2^2) by XCMPLX_1:26
.= s2 by A2,SQUARE_1:89;
hence |[r,s+s2]| in Ball(u,s1) by A3,METRIC_1:12;
end;
theorem Th12:
for u being Point of Euclid 2 st u = |[r,s]| holds
0 <= r2 & r2 < r1 implies |[r-r2,s]| in Ball(u,r1)
proof let u be Point of Euclid 2 such that
A1: u = |[r,s]| and
A2: 0 <= r2 and
A3: r2 < r1;
reconsider v = |[r-r2,s]| as Point of Euclid 2 by TOPREAL3:13;
dist(u,v) = sqrt ((r - (r-r2))^2 + (s - s)^2) by A1,Th9
.= sqrt ((r - (r-r2))^2 + 0^2) by XCMPLX_1:14
.= sqrt (r2^2) by SQUARE_1:60,XCMPLX_1:18
.= r2 by A2,SQUARE_1:89;
hence |[r-r2,s]| in Ball(u,r1) by A3,METRIC_1:12;
end;
theorem Th13:
for u being Point of Euclid 2 st u = |[r,s]| holds
0 <= s2 & s2 < s1 implies |[r,s-s2]| in Ball(u,s1)
proof let u be Point of Euclid 2 such that
A1: u = |[r,s]| and
A2: 0 <= s2 and
A3: s2 < s1;
reconsider v = |[r,s-s2]| as Point of Euclid 2 by TOPREAL3:13;
dist(u,v) = sqrt ((s - (s-s2))^2 + (r - r)^2) by A1,Th9
.= sqrt ((s - (s-s2))^2 + 0^2) by XCMPLX_1:14
.= sqrt (s2^2) by SQUARE_1:60,XCMPLX_1:18
.= s2 by A2,SQUARE_1:89;
hence |[r,s-s2]| in Ball(u,s1) by A3,METRIC_1:12;
end;
theorem Th14:
1 <= i & i < len G & 1 <= j & j < width G
implies G*(i,j)+G*(i+1,j+1) = G*(i,j+1)+G*(i+1,j)
proof assume that
A1: 1 <= i & i < len G and
A2: 1 <= j & j < width G;
A3: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
A4: 1 <= j+1 & j+1 <= width G by A2,NAT_1:38;
A5: G*(i,j)`1 = G*(i,1)`1 by A1,A2,GOBOARD5:3
.= G*(i,j+1)`1 by A1,A4,GOBOARD5:3;
A6: G*(i+1,j+1)`1 = G*(i+1,1)`1 by A3,A4,GOBOARD5:3
.= G*(i+1,j)`1 by A2,A3,GOBOARD5:3;
A7: (G*(i,j)+G*(i+1,j+1))`1 = G*(i,j)`1+G*(i+1,j+1)`1 by Lm1
.= (G*(i,j+1)+G*(i+1,j))`1 by A5,A6,Lm1;
A8: G*(i,j)`2 = G*(1,j)`2 by A1,A2,GOBOARD5:2
.= G*(i+1,j)`2 by A2,A3,GOBOARD5:2;
A9: G*(i+1,j+1)`2 = G*(1,j+1)`2 by A3,A4,GOBOARD5:2
.= G*(i,j+1)`2 by A1,A4,GOBOARD5:2;
(G*(i,j)+G*(i+1,j+1))`2 = G*(i,j)`2+G*(i+1,j+1)`2 by Lm1
.= (G*(i,j+1)+G*(i+1,j))`2 by A8,A9,Lm1;
hence G*(i,j)+G*(i+1,j+1)
= |[(G*(i,j+1)+G*(i+1,j))`1,(G*(i,j+1)+G*(i+1,j))`2]| by A7,EUCLID:57
.= G*(i,j+1)+G*(i+1,j) by EUCLID:57;
end;
Lm5: TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8
.= TopStruct (#the carrier of Euclid 2,Family_open_set Euclid 2#)
by PCOMPS_1:def 6;
theorem Th15:
Int v_strip(G,0) = { |[r,s]| : r < G*(1,1)`1 }
proof
0 <> width G by GOBOARD1:def 5;
then 1 <= width G by RLVECT_1:99;
then A1: v_strip(G,0) = { |[r,s]| : r <= G*(1,1)`1 } by GOBOARD5:11;
thus Int v_strip(G,0) c= { |[r,s]| : r < G*(1,1)`1 }
proof let x;
assume
A2: x in Int v_strip(G,0);
then reconsider u = x as Point of Euclid 2 by Lm5;
consider r1 being real number such that
A3: r1 > 0 and
A4: Ball(u,r1) c= v_strip(G,0) by A2,Th8;
reconsider r1 as Real by XREAL_0:def 1;
reconsider p = u as Point of TOP-REAL 2 by Lm5;
set q = |[p`1+r1/2,p`2+0]|;
A5: p = |[p`1,p`2]| by EUCLID:57;
A6: r1/2 > 0 & r1/2 < r1 by A3,SEQ_2:3,4;
then q in Ball(u,r1) by A5,Th10;
then q in v_strip(G,0) by A4;
then ex r2,s2 st q = |[r2,s2]| & r2 <= G*(1,1)`1 by A1;
then A7: p`1+r1/2 <= G*(1,1)`1 by SPPOL_2:1;
p`1 < p`1 + r1/2 by A6,REAL_1:69;
then p`1 < G*(1,1)`1 by A7,AXIOMS:22;
hence x in {|[r,s]| : r < G*(1,1)`1} by A5;
end;
let x;
assume x in { |[r,s]| : r < G*(1,1)`1 };
then consider r,s such that
A8: x = |[r,s]| and
A9: r < G*(1,1)`1;
reconsider u = |[r,s]| as Point of Euclid 2 by TOPREAL3:13;
G*(1,1)`1-r > 0 by A9,SQUARE_1:11;
then A10: u in Ball(u,G*(1,1)`1-r) by Th4;
A11: Ball(u,G*(1,1)`1-r) c= v_strip(G,0)
proof let y;
A12: Ball(u,G*(1,1)`1-r) = { v : dist(u,v)<G*(1,1)`1-r} by METRIC_1:18;
assume y in Ball(u,G*(1,1)`1-r);
then consider v such that
A13: v = y and
A14: dist(u,v)<G*(1,1)`1-r by A12;
reconsider q = v as Point of TOP-REAL 2 by TOPREAL3:13;
A15: q = |[q`1,q`2]| by EUCLID:57;
then A16: sqrt ((r - q`1)^2 + (s - q`2)^2) < G*(1,1)`1-r by A14,Th9;
A17: (r - q`1)^2 >= 0 by SQUARE_1:72;
0 <= (s - q`2)^2 by SQUARE_1:72;
then (r - q`1)^2 + 0 <= (r - q`1)^2 + (s - q`2)^2 by AXIOMS:24;
then sqrt (r - q`1)^2 <= sqrt ((r - q`1)^2 + (s - q`2)^2)
by A17,SQUARE_1:94;
then sqrt (r - q`1)^2 <= G*(1,1)`1-r by A16,AXIOMS:22;
then A18: abs(r-q`1) <= G*(1,1)`1-r by SQUARE_1:91;
per cases;
suppose r <= q`1;
then A19: q`1-r >= 0 by SQUARE_1:12;
abs(r-q`1) = abs(-(r-q`1)) by ABSVALUE:17
.= abs(q`1 - r) by XCMPLX_1:143
.= q`1 - r by A19,ABSVALUE:def 1;
then q`1 <= G*(1,1)`1 by A18,REAL_1:54;
hence y in v_strip(G,0) by A1,A13,A15;
suppose r >= q`1;
then q`1 <= G*(1,1)`1 by A9,AXIOMS:22;
hence y in v_strip(G,0) by A1,A13,A15;
end;
Ball(u,G*(1,1)`1-r) is Subset of TOP-REAL2
by TOPREAL3:13;
then reconsider B = Ball(u,G*(1,1)`1-r) as Subset of TOP-REAL2;
B is open by Th6;
hence x in Int v_strip(G,0) by A8,A10,A11,TOPS_1:54;
end;
theorem Th16:
Int v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 < r }
proof
0 <> width G by GOBOARD1:def 5;
then 1 <= width G by RLVECT_1:99;
then A1: v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 <= r } by GOBOARD5:10;
thus Int v_strip(G,len G) c= { |[r,s]| : G*(len G,1)`1 < r }
proof let x;
assume
A2: x in Int v_strip(G,len G);
then reconsider u = x as Point of Euclid 2 by Lm5;
consider r1 being real number such that
A3: r1 > 0 and
A4: Ball(u,r1) c= v_strip(G,len G) by A2,Th8;
reconsider r1 as Real by XREAL_0:def 1;
reconsider p = u as Point of TOP-REAL 2 by Lm5;
set q = |[p`1-r1/2,p`2+0]|;
A5: p = |[p`1,p`2]| by EUCLID:57;
A6: r1/2 > 0 & r1/2 < r1 by A3,SEQ_2:3,4;
then q in Ball(u,r1) by A5,Th12;
then q in v_strip(G,len G) by A4;
then ex r2,s2 st q = |[r2,s2]| & G*(len G,1)`1 <= r2 by A1;
then G*(len G,1)`1 <= p`1-r1/2 by SPPOL_2:1;
then A7: G*(len G,1)`1+r1/2 <= p`1 by REAL_1:84;
G*(len G,1)`1 < G*(len G,1)`1 + r1/2 by A6,REAL_1:69;
then G*(len G,1)`1 < p`1 by A7,AXIOMS:22;
hence x in {|[r,s]| : G*(len G,1)`1 < r } by A5;
end;
let x;
assume x in { |[r,s]| : G*(len G,1)`1 < r };
then consider r,s such that
A8: x = |[r,s]| and
A9: G*(len G,1)`1 < r;
reconsider u = |[r,s]| as Point of Euclid 2 by TOPREAL3:13;
r - G*(len G,1)`1 > 0 by A9,SQUARE_1:11;
then A10: u in Ball(u,r-G*(len G,1)`1) by Th4;
A11: Ball(u,r-G*(len G,1)`1) c= v_strip(G,len G)
proof let y;
A12: Ball(u,r-G*(len G,1)`1) = { v : dist(u,v)<r-G*(len G,1)`1}
by METRIC_1:18;
assume y in Ball(u,r-G*(len G,1)`1);
then consider v such that
A13: v = y and
A14: dist(u,v)<r-G*(len G,1)`1 by A12;
reconsider q = v as Point of TOP-REAL 2 by TOPREAL3:13;
A15: q = |[q`1,q`2]| by EUCLID:57;
then A16: sqrt ((r - q`1)^2 + (s - q`2)^2) < r-G*(len G,1)`1 by A14,
Th9;
A17: (r - q`1)^2 >= 0 by SQUARE_1:72;
0 <= (s - q`2)^2 by SQUARE_1:72;
then (r - q`1)^2 + 0 <= (r - q`1)^2 + (s - q`2)^2 by AXIOMS:24;
then sqrt (r - q`1)^2 <= sqrt ((r - q`1)^2 + (s - q`2)^2)
by A17,SQUARE_1:94;
then sqrt (r - q`1)^2 <= r-G*(len G,1)`1 by A16,AXIOMS:22;
then A18: abs(r-q`1) <= r-G*(len G,1)`1 by SQUARE_1:91;
per cases;
suppose r >= q`1;
then r-q`1 >= 0 by SQUARE_1:12;
then abs(r-q`1) = r - q`1 by ABSVALUE:def 1;
then G*(len G,1)`1 <= q`1 by A18,REAL_2:105;
hence y in v_strip(G,len G) by A1,A13,A15;
suppose r <= q`1;
then G*(len G,1)`1 <= q`1 by A9,AXIOMS:22;
hence y in v_strip(G,len G) by A1,A13,A15;
end;
Ball(u,r-G*(len G,1)`1) is Subset of TOP-REAL2
by TOPREAL3:13;
then reconsider B = Ball(u,r-G*(len G,1)`1) as Subset of TOP-REAL2
;
B is open by Th6;
hence x in Int v_strip(G,len G) by A8,A10,A11,TOPS_1:54;
end;
theorem Th17:
1 <= i & i < len G
implies Int v_strip(G,i) = { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 }
proof assume
A1: 1 <= i & i < len G;
0 <> width G by GOBOARD1:def 5;
then 1 <= width G by RLVECT_1:99;
then A2: v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 }
by A1,GOBOARD5:9;
thus Int v_strip(G,i) c= { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 }
proof let x;
assume
A3: x in Int v_strip(G,i);
then reconsider u = x as Point of Euclid 2 by Lm5;
consider r1 being real number such that
A4: r1 > 0 and
A5: Ball(u,r1) c= v_strip(G,i) by A3,Th8;
reconsider r1 as Real by XREAL_0:def 1;
reconsider p = u as Point of TOP-REAL 2 by Lm5;
set q1 = |[p`1+r1/2,p`2+0]|;
A6: p = |[p`1,p`2]| by EUCLID:57;
A7: r1/2 > 0 & r1/2 < r1 by A4,SEQ_2:3,4;
then q1 in Ball(u,r1) by A6,Th10;
then q1 in v_strip(G,i) by A5;
then ex r2,s2 st q1 = |[r2,s2]| & G*(i,1)`1 <= r2 & r2 <=
G*(i+1,1)`1 by A2;
then A8: p`1+r1/2 <= G*(i+1,1)`1 by SPPOL_2:1;
p`1 < p`1 + r1/2 by A7,REAL_1:69;
then A9: p`1 < G*(i+1,1)`1 by A8,AXIOMS:22;
set q2 = |[p`1-r1/2,p`2+0]|;
q2 in Ball(u,r1) by A6,A7,Th12;
then q2 in v_strip(G,i) by A5;
then ex r2,s2 st q2 = |[r2,s2]| & G*(i,1)`1 <= r2 & r2 <=
G*(i+1,1)`1 by A2;
then G*(i,1)`1 <= p`1-r1/2 by SPPOL_2:1;
then A10: G*(i,1)`1+r1/2 <= p`1 by REAL_1:84;
G*(i,1)`1 < G*(i,1)`1 + r1/2 by A7,REAL_1:69;
then G*(i,1)`1 < p`1 by A10,AXIOMS:22;
hence x in {|[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1} by A6,A9;
end;
let x;
assume x in { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 };
then consider r,s such that
A11: x = |[r,s]| and
A12: G*(i,1)`1 < r and
A13: r < G*(i+1,1)`1;
reconsider u = |[r,s]| as Point of Euclid 2 by TOPREAL3:13;
A14:G*(i+1,1)`1-r > 0 by A13,SQUARE_1:11;
r - G*(i,1)`1 > 0 by A12,SQUARE_1:11;
then min(r-G*(i,1)`1,G*(i+1,1)`1-r) > 0 by A14,SQUARE_1:38;
then A15: u in Ball(u,min(r-G*(i,1)`1,G*(i+1,1)`1-r)) by Th4;
A16: Ball(u,min(r-G*(i,1)`1,G*(i+1,1)`1-r)) c= v_strip(G,i)
proof let y;
A17: Ball(u,min(r-G*(i,1)`1,G*(i+1,1)`1-r))
= { v : dist(u,v)<min(r-G*(i,1)`1,G*(i+1,1)`1-r)} by METRIC_1:18;
assume y in Ball(u,min(r-G*(i,1)`1,G*(i+1,1)`1-r));
then consider v such that
A18: v = y and
A19: dist(u,v)<min(r-G*(i,1)`1,G*(i+1,1)`1-r) by A17;
reconsider q = v as Point of TOP-REAL 2 by TOPREAL3:13;
A20: q = |[q`1,q`2]| by EUCLID:57;
then A21: sqrt ((r - q`1)^2 + (s - q`2)^2) < min(r-G*(i,1)`1,G*(i+1,1
)`1-r)
by A19,Th9;
A22: (r - q`1)^2 >= 0 by SQUARE_1:72;
0 <= (s - q`2)^2 by SQUARE_1:72;
then (r - q`1)^2 + 0 <= (r - q`1)^2 + (s - q`2)^2 by AXIOMS:24;
then sqrt (r - q`1)^2 <= sqrt ((r - q`1)^2 + (s - q`2)^2)
by A22,SQUARE_1:94;
then sqrt (r - q`1)^2 <= min(r-G*(i,1)`1,G*
(i+1,1)`1-r) by A21,AXIOMS:22;
then abs(r-q`1) <= min(r-G*(i,1)`1,G*(i+1,1)`1-r) by SQUARE_1:91;
then A23: abs(r-q`1) <= r-G*(i,1)`1 & abs(r-q`1) <= G*
(i+1,1)`1-r by SQUARE_1:39;
per cases;
suppose
A24: r <= q`1;
then A25: q`1-r >= 0 by SQUARE_1:12;
abs(r-q`1) = abs(-(r-q`1)) by ABSVALUE:17
.= abs(q`1 - r) by XCMPLX_1:143
.= q`1 - r by A25,ABSVALUE:def 1;
then A26: q`1 <= G*(i+1,1)`1 by A23,REAL_1:54;
G*(i,1)`1 <= q`1 by A12,A24,AXIOMS:22;
hence y in v_strip(G,i) by A2,A18,A20,A26;
suppose
A27: r >= q`1;
then r-q`1 >= 0 by SQUARE_1:12;
then abs(r-q`1) = r - q`1 by ABSVALUE:def 1;
then A28: G*(i,1)`1 <= q`1 by A23,REAL_2:105;
q`1 <= G*(i+1,1)`1 by A13,A27,AXIOMS:22;
hence y in v_strip(G,i) by A2,A18,A20,A28;
end;
Ball(u,min(r-G*(i,1)`1,G*(i+1,1)`1-r))
is Subset of TOP-REAL2 by TOPREAL3:13;
then reconsider B = Ball(u,min(r-G*(i,1)`1,G*(i+1,1)`1-r))
as Subset of TOP-REAL2;
B is open by Th6;
hence x in Int v_strip(G,i) by A11,A15,A16,TOPS_1:54;
end;
theorem Th18:
Int h_strip(G,0) = { |[r,s]| : s < G*(1,1)`2 }
proof
0 <> len G by GOBOARD1:def 5;
then 1 <= len G by RLVECT_1:99;
then A1: h_strip(G,0) = { |[r,s]| : s <= G*(1,1)`2 } by GOBOARD5:8;
thus Int h_strip(G,0) c= { |[r,s]| : s < G*(1,1)`2 }
proof let x;
assume
A2: x in Int h_strip(G,0);
then reconsider u = x as Point of Euclid 2 by Lm5;
consider s1 being real number such that
A3: s1 > 0 and
A4: Ball(u,s1) c= h_strip(G,0) by A2,Th8;
reconsider s1 as Real by XREAL_0:def 1;
reconsider p = u as Point of TOP-REAL 2 by Lm5;
set q = |[p`1+0,p`2+s1/2]|;
A5: p = |[p`1,p`2]| by EUCLID:57;
A6: s1/2 > 0 & s1/2 < s1 by A3,SEQ_2:3,4;
then q in Ball(u,s1) by A5,Th11;
then q in h_strip(G,0) by A4;
then ex r2,s2 st q = |[r2,s2]| & s2 <= G*(1,1)`2 by A1;
then A7: p`2+s1/2 <= G*(1,1)`2 by SPPOL_2:1;
p`2 < p`2 + s1/2 by A6,REAL_1:69;
then p`2 < G*(1,1)`2 by A7,AXIOMS:22;
hence x in {|[r,s]| : s < G*(1,1)`2} by A5;
end;
let x;
assume x in { |[r,s]| : s < G*(1,1)`2 };
then consider r,s such that
A8: x = |[r,s]| and
A9: s < G*(1,1)`2;
reconsider u = |[r,s]| as Point of Euclid 2 by TOPREAL3:13;
G*(1,1)`2-s > 0 by A9,SQUARE_1:11;
then A10: u in Ball(u,G*(1,1)`2-s) by Th4;
A11: Ball(u,G*(1,1)`2-s) c= h_strip(G,0)
proof let y;
A12: Ball(u,G*(1,1)`2-s) = { v : dist(u,v)<G*(1,1)`2-s} by METRIC_1:18;
assume y in Ball(u,G*(1,1)`2-s);
then consider v such that
A13: v = y and
A14: dist(u,v)<G*(1,1)`2-s by A12;
reconsider q = v as Point of TOP-REAL 2 by TOPREAL3:13;
A15: q = |[q`1,q`2]| by EUCLID:57;
then A16: sqrt ((r - q`1)^2 + (s - q`2)^2) < G*(1,1)`2-s by A14,Th9;
A17: (s - q`2)^2 >= 0 by SQUARE_1:72;
0 <= (r - q`1)^2 by SQUARE_1:72;
then (s - q`2)^2 + 0 <= (r - q`1)^2 + (s - q`2)^2 by AXIOMS:24;
then sqrt (s - q`2)^2 <= sqrt ((r - q`1)^2 + (s - q`2)^2)
by A17,SQUARE_1:94;
then sqrt (s - q`2)^2 <= G*(1,1)`2-s by A16,AXIOMS:22;
then A18: abs(s-q`2) <= G*(1,1)`2-s by SQUARE_1:91;
per cases;
suppose s <= q`2;
then A19: q`2-s >= 0 by SQUARE_1:12;
abs(s-q`2) = abs(-(s-q`2)) by ABSVALUE:17
.= abs(q`2 - s) by XCMPLX_1:143
.= q`2 - s by A19,ABSVALUE:def 1;
then q`2 <= G*(1,1)`2 by A18,REAL_1:54;
hence y in h_strip(G,0) by A1,A13,A15;
suppose s >= q`2;
then q`2 <= G*(1,1)`2 by A9,AXIOMS:22;
hence y in h_strip(G,0) by A1,A13,A15;
end;
Ball(u,G*(1,1)`2-s) is Subset of TOP-REAL2
by TOPREAL3:13;
then reconsider B = Ball(u,G*(1,1)`2-s) as Subset of TOP-REAL2
;
B is open by Th6;
hence x in Int h_strip(G,0) by A8,A10,A11,TOPS_1:54;
end;
theorem Th19:
Int h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 < s }
proof
0 <> len G by GOBOARD1:def 5;
then 1 <= len G by RLVECT_1:99;
then A1: h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 <= s } by GOBOARD5:7;
thus Int h_strip(G,width G) c= { |[r,s]| : G*(1,width G)`2 < s }
proof let x;
assume
A2: x in Int h_strip(G,width G);
then reconsider u = x as Point of Euclid 2 by Lm5;
consider s1 being real number such that
A3: s1 > 0 and
A4: Ball(u,s1) c= h_strip(G,width G) by A2,Th8;
reconsider s1 as Real by XREAL_0:def 1;
reconsider p = u as Point of TOP-REAL 2 by Lm5;
set q = |[p`1+0,p`2-s1/2]|;
A5: p = |[p`1,p`2]| by EUCLID:57;
A6: s1/2 > 0 & s1/2 < s1 by A3,SEQ_2:3,4;
then q in Ball(u,s1) by A5,Th13;
then q in h_strip(G,width G) by A4;
then ex r2,s2 st q = |[r2,s2]| & G*(1,width G)`2 <= s2 by A1;
then G*(1,width G)`2 <= p`2-s1/2 by SPPOL_2:1;
then A7: G*(1,width G)`2+s1/2 <= p`2 by REAL_1:84;
G*(1,width G)`2 < G*(1,width G)`2 + s1/2 by A6,REAL_1:69;
then G*(1,width G)`2 < p`2 by A7,AXIOMS:22;
hence x in {|[r,s]| : G*(1,width G)`2 < s } by A5;
end;
let x;
assume x in { |[r,s]| : G*(1,width G)`2 < s };
then consider r,s such that
A8: x = |[r,s]| and
A9: G*(1,width G)`2 < s;
reconsider u = |[r,s]| as Point of Euclid 2 by TOPREAL3:13;
s - G*(1,width G)`2 > 0 by A9,SQUARE_1:11;
then A10: u in Ball(u,s-G*(1,width G)`2) by Th4;
A11: Ball(u,s-G*(1,width G)`2) c= h_strip(G,width G)
proof let y;
A12: Ball(u,s-G*(1,width G)`2) = { v : dist(u,v)<s-G*(1,width G)`2}
by METRIC_1:18;
assume y in Ball(u,s-G*(1,width G)`2);
then consider v such that
A13: v = y and
A14: dist(u,v)<s-G*(1,width G)`2 by A12;
reconsider q = v as Point of TOP-REAL 2 by TOPREAL3:13;
A15: q = |[q`1,q`2]| by EUCLID:57;
then A16: sqrt ((r - q`1)^2 + (s - q`2)^2) < s-G*(1,width G)`2 by A14
,Th9;
A17: (s - q`2)^2 >= 0 by SQUARE_1:72;
0 <= (r - q`1)^2 by SQUARE_1:72;
then (s - q`2)^2 + 0 <= (r - q`1)^2 + (s - q`2)^2 by AXIOMS:24;
then sqrt (s - q`2)^2 <= sqrt ((r - q`1)^2 + (s - q`2)^2)
by A17,SQUARE_1:94;
then sqrt (s - q`2)^2 <= s-G*(1,width G)`2 by A16,AXIOMS:22;
then A18: abs(s-q`2) <= s-G*(1,width G)`2 by SQUARE_1:91;
per cases;
suppose s >= q`2;
then s-q`2 >= 0 by SQUARE_1:12;
then abs(s-q`2) = s - q`2 by ABSVALUE:def 1;
then G*(1,width G)`2 <= q`2 by A18,REAL_2:105;
hence y in h_strip(G,width G) by A1,A13,A15;
suppose s <= q`2;
then G*(1,width G)`2 <= q`2 by A9,AXIOMS:22;
hence y in h_strip(G,width G) by A1,A13,A15;
end;
Ball(u,s-G*(1,width G)`2)
is Subset of TOP-REAL2 by TOPREAL3:13;
then reconsider B = Ball(u,s-G*(1,width G)`2)
as Subset of TOP-REAL2;
B is open by Th6;
hence x in Int h_strip(G,width G) by A8,A10,A11,TOPS_1:54;
end;
theorem Th20:
1 <= j & j < width G
implies Int h_strip(G,j) = { |[r,s]| : G*(1,j)`2 < s & s < G*(1,j+1)`2 }
proof assume
A1: 1 <= j & j < width G;
0 <> len G by GOBOARD1:def 5;
then 1 <= len G by RLVECT_1:99;
then A2: h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
by A1,GOBOARD5:6;
thus Int h_strip(G,j) c= { |[r,s]| : G*(1,j)`2 < s & s < G*(1,j+1)`2 }
proof let x;
assume
A3: x in Int h_strip(G,j);
then reconsider u = x as Point of Euclid 2 by Lm5;
consider s1 being real number such that
A4: s1 > 0 and
A5: Ball(u,s1) c= h_strip(G,j) by A3,Th8;
reconsider s1 as Real by XREAL_0:def 1;
reconsider p = u as Point of TOP-REAL 2 by Lm5;
set q1 = |[p`1+0,p`2+s1/2]|;
A6: p = |[p`1,p`2]| by EUCLID:57;
A7: s1/2 > 0 & s1/2 < s1 by A4,SEQ_2:3,4;
then q1 in Ball(u,s1) by A6,Th11;
then q1 in h_strip(G,j) by A5;
then ex r2,s2 st q1 = |[r2,s2]| & G*(1,j)`2 <= s2 & s2 <=
G*(1,j+1)`2 by A2;
then A8: p`2+s1/2 <= G*(1,j+1)`2 by SPPOL_2:1;
p`2 < p`2 + s1/2 by A7,REAL_1:69;
then A9: p`2 < G*(1,j+1)`2 by A8,AXIOMS:22;
set q2 = |[p`1+0,p`2-s1/2]|;
q2 in Ball(u,s1) by A6,A7,Th13;
then q2 in h_strip(G,j) by A5;
then ex r2,s2 st q2 = |[r2,s2]| & G*(1,j)`2 <= s2 & s2 <=
G*(1,j+1)`2 by A2;
then G*(1,j)`2 <= p`2-s1/2 by SPPOL_2:1;
then A10: G*(1,j)`2+s1/2 <= p`2 by REAL_1:84;
G*(1,j)`2 < G*(1,j)`2 + s1/2 by A7,REAL_1:69;
then G*(1,j)`2 < p`2 by A10,AXIOMS:22;
hence x in {|[r,s]| : G*(1,j)`2 < s & s < G*(1,j+1)`2} by A6,A9;
end;
let x;
assume x in { |[r,s]| : G*(1,j)`2 < s & s < G*(1,j+1)`2 };
then consider r,s such that
A11: x = |[r,s]| and
A12: G*(1,j)`2 < s and
A13: s < G*(1,j+1)`2;
reconsider u = |[r,s]| as Point of Euclid 2 by TOPREAL3:13;
A14:G*(1,j+1)`2-s > 0 by A13,SQUARE_1:11;
s - G*(1,j)`2 > 0 by A12,SQUARE_1:11;
then min(s-G*(1,j)`2,G*(1,j+1)`2-s) > 0 by A14,SQUARE_1:38;
then A15: u in Ball(u,min(s-G*(1,j)`2,G*(1,j+1)`2-s)) by Th4;
A16: Ball(u,min(s-G*(1,j)`2,G*(1,j+1)`2-s)) c= h_strip(G,j)
proof let y;
A17: Ball(u,min(s-G*(1,j)`2,G*(1,j+1)`2-s))
= { v : dist(u,v)<min(s-G*(1,j)`2,G*(1,j+1)`2-s)} by METRIC_1:18;
assume y in Ball(u,min(s-G*(1,j)`2,G*(1,j+1)`2-s));
then consider v such that
A18: v = y and
A19: dist(u,v)<min(s-G*(1,j)`2,G*(1,j+1)`2-s) by A17;
reconsider q = v as Point of TOP-REAL 2 by TOPREAL3:13;
A20: q = |[q`1,q`2]| by EUCLID:57;
then A21: sqrt ((r - q`1)^2 + (s - q`2)^2) < min(s-G*(1,j)`2,G*(1,j+1
)`2-s)
by A19,Th9;
A22: (s - q`2)^2 >= 0 by SQUARE_1:72;
0 <= (r - q`1)^2 by SQUARE_1:72;
then (s - q`2)^2 + 0 <= (r - q`1)^2 + (s - q`2)^2 by AXIOMS:24;
then sqrt (s - q`2)^2 <= sqrt ((r - q`1)^2 + (s - q`2)^2)
by A22,SQUARE_1:94;
then sqrt (s - q`2)^2 <= min(s-G*(1,j)`2,G*
(1,j+1)`2-s) by A21,AXIOMS:22;
then abs(s-q`2) <= min(s-G*(1,j)`2,G*(1,j+1)`2-s) by SQUARE_1:91;
then A23: abs(s-q`2) <= s-G*(1,j)`2 & abs(s-q`2) <= G*
(1,j+1)`2-s by SQUARE_1:39;
per cases;
suppose
A24: s <= q`2;
then A25: q`2-s >= 0 by SQUARE_1:12;
abs(s-q`2) = abs(-(s-q`2)) by ABSVALUE:17
.= abs(q`2 - s) by XCMPLX_1:143
.= q`2 - s by A25,ABSVALUE:def 1;
then A26: q`2 <= G*(1,j+1)`2 by A23,REAL_1:54;
G*(1,j)`2 <= q`2 by A12,A24,AXIOMS:22;
hence y in h_strip(G,j) by A2,A18,A20,A26;
suppose
A27: s >= q`2;
then s-q`2 >= 0 by SQUARE_1:12;
then abs(s-q`2) = s - q`2 by ABSVALUE:def 1;
then A28: G*(1,j)`2 <= q`2 by A23,REAL_2:105;
q`2 <= G*(1,j+1)`2 by A13,A27,AXIOMS:22;
hence y in h_strip(G,j) by A2,A18,A20,A28;
end;
Ball(u,min(s-G*(1,j)`2,G*(1,j+1)`2-s))
is Subset of TOP-REAL2 by TOPREAL3:13;
then reconsider B = Ball(u,min(s-G*(1,j)`2,G*(1,j+1)`2-s))
as Subset of TOP-REAL2;
B is open by Th6;
hence x in Int h_strip(G,j) by A11,A15,A16,TOPS_1:54;
end;
theorem Th21:
Int cell(G,0,0) = { |[r,s]| : r < G*(1,1)`1 & s < G*(1,1)`2 }
proof cell(G,0,0) = v_strip(G,0) /\ h_strip(G,0) by GOBOARD5:def 3;
then A1: Int cell(G,0,0) = Int v_strip(G,0) /\ Int h_strip(G,0) by TOPS_1:46;
A2: Int v_strip(G,0) = { |[r,s]| : r < G*(1,1)`1 } by Th15;
A3: Int h_strip(G,0) = { |[r,s]| : s < G*(1,1)`2 } by Th18;
thus Int cell(G,0,0) c= { |[r,s]| : r < G*(1,1)`1 & s < G*(1,1)`2 }
proof let x be set;
assume
A4: x in Int cell(G,0,0);
then x in Int v_strip(G,0) by A1,XBOOLE_0:def 3;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: r1 < G*(1,1)`1 by A2;
x in Int h_strip(G,0) by A1,A4,XBOOLE_0:def 3;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: s2 < G*(1,1)`2 by A3;
r1 = r2 & s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be set;
assume x in { |[r,s]| : r < G*(1,1)`1 & s < G*(1,1)`2 };
then ex r,s st x = |[r,s]| & r < G*(1,1)`1 & s < G*(1,1)`2;
then x in Int v_strip(G,0) & x in Int h_strip(G,0) by A2,A3;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th22:
Int cell(G,0,width G) = { |[r,s]| : r < G*(1,1)`1 & G*(1,width G)`2 < s }
proof cell(G,0,width G) = v_strip(G,0) /\ h_strip(G,width G) by GOBOARD5:def 3
;
then A1: Int cell(G,0,width G) = Int v_strip(G,0) /\ Int h_strip(G,width G)
by TOPS_1:46;
A2: Int v_strip(G,0) = { |[r,s]| : r < G*(1,1)`1 } by Th15;
A3: Int h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 < s } by Th19;
thus Int cell(G,0,width G)
c= { |[r,s]| : r < G*(1,1)`1 & G*(1,width G)`2 < s }
proof let x be set;
assume
A4: x in Int cell(G,0,width G);
then x in Int v_strip(G,0) by A1,XBOOLE_0:def 3;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: r1 < G*(1,1)`1 by A2;
x in Int h_strip(G,width G) by A1,A4,XBOOLE_0:def 3;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: G*(1,width G)`2 < s2 by A3;
r1 = r2 & s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be set;
assume x in { |[r,s]| : r < G*(1,1)`1 & G*(1,width G)`2 < s };
then ex r,s st x = |[r,s]| & r < G*(1,1)`1 & G*(1,width G)`2 < s;
then x in Int v_strip(G,0) & x in Int h_strip(G,width G) by A2,A3;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th23:
1 <= j & j < width G
implies Int cell(G,0,j) =
{ |[r,s]| : r < G*(1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 }
proof assume
A1: 1 <= j & j < width G;
cell(G,0,j) = v_strip(G,0) /\ h_strip(G,j) by GOBOARD5:def 3;
then A2: Int cell(G,0,j) = Int v_strip(G,0) /\ Int h_strip(G,j) by TOPS_1:46
;
A3: Int v_strip(G,0) = { |[r,s]| : r < G*(1,1)`1 } by Th15;
A4: Int h_strip(G,j) = { |[r,s]| : G*(1,j)`2 < s & s < G*
(1,j+1)`2 } by A1,Th20
;
thus Int cell(G,0,j) c=
{ |[r,s]| : r < G*(1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 }
proof let x be set;
assume
A5: x in Int cell(G,0,j);
then x in Int v_strip(G,0) by A2,XBOOLE_0:def 3;
then consider r1,s1 such that
A6: x = |[r1,s1]| and
A7: r1 < G*(1,1)`1 by A3;
x in Int h_strip(G,j) by A2,A5,XBOOLE_0:def 3;
then consider r2,s2 such that
A8: x = |[r2,s2]| and
A9: G*(1,j)`2 < s2 & s2 < G*(1,j+1)`2 by A4;
r1 = r2 & s1 = s2 by A6,A8,SPPOL_2:1;
hence thesis by A6,A7,A9;
end;
let x be set;
assume x in { |[r,s]| : r < G*(1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 };
then ex r,s st
x = |[r,s]| & r < G*(1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2;
then x in Int v_strip(G,0) & x in Int h_strip(G,j) by A3,A4;
hence thesis by A2,XBOOLE_0:def 3;
end;
theorem Th24:
Int cell(G,len G,0) = { |[r,s]| : G*(len G,1)`1 < r & s < G*(1,1)`2 }
proof cell(G,len G,0) = v_strip(G,len G) /\ h_strip(G,0) by GOBOARD5:def 3;
then A1: Int cell(G,len G,0) = Int v_strip(G,len G) /\ Int h_strip(G,0) by
TOPS_1:46;
A2: Int v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 < r } by Th16;
A3: Int h_strip(G,0) = { |[r,s]| : s < G*(1,1)`2 } by Th18;
thus Int cell(G,len G,0) c= { |[r,s]| : G*(len G,1)`1 < r & s < G*(1,1)`2 }
proof let x be set;
assume
A4: x in Int cell(G,len G,0);
then x in Int v_strip(G,len G) by A1,XBOOLE_0:def 3;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: G*(len G,1)`1 < r1 by A2;
x in Int h_strip(G,0) by A1,A4,XBOOLE_0:def 3;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: s2 < G*(1,1)`2 by A3;
r1 = r2 & s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be set;
assume x in { |[r,s]| : G*(len G,1)`1 < r & s < G*(1,1)`2 };
then ex r,s st x = |[r,s]| & G*(len G,1)`1 < r & s < G*(1,1)`2;
then x in Int v_strip(G,len G) & x in Int h_strip(G,0) by A2,A3;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th25:
Int cell(G,len G,width G) =
{ |[r,s]| : G*(len G,1)`1 < r & G*(1,width G)`2 < s }
proof
cell(G,len G,width G) = v_strip(G,len G) /\ h_strip(G,width G)
by GOBOARD5:def 3;
then A1: Int cell(G,len G,width G) = Int v_strip(G,len G) /\ Int h_strip(G,
width G)
by TOPS_1:46;
A2: Int v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 < r } by Th16;
A3: Int h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 < s } by Th19;
thus Int cell(G,len G,width G) c=
{ |[r,s]| : G*(len G,1)`1 < r & G*(1,width G)`2 < s }
proof let x be set;
assume
A4: x in Int cell(G,len G,width G);
then x in Int v_strip(G,len G) by A1,XBOOLE_0:def 3;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: G*(len G,1)`1 < r1 by A2;
x in Int h_strip(G,width G) by A1,A4,XBOOLE_0:def 3;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: G*(1,width G)`2 < s2 by A3;
r1 = r2 & s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be set;
assume x in { |[r,s]| : G*(len G,1)`1 < r & G*(1,width G)`2 < s };
then ex r,s st x = |[r,s]| & G*(len G,1)`1 < r & G*(1,width G)`2 < s;
then x in Int v_strip(G,len G) & x in Int h_strip(G,width G) by A2,A3;
hence thesis by A1,XBOOLE_0:def 3;
end;
theorem Th26:
1 <= j & j < width G
implies Int cell(G,len G,j) =
{ |[r,s]| : G*(len G,1)`1 < r & G*(1,j)`2 < s & s < G*(1,j+1)`2 }
proof assume
A1: 1 <= j & j < width G;
cell(G,len G,j) = v_strip(G,len G) /\ h_strip(G,j) by GOBOARD5:def 3;
then A2: Int cell(G,len G,j) = Int v_strip(G,len G) /\ Int h_strip(G,j) by
TOPS_1:46;
A3: Int v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 < r } by Th16;
A4: Int h_strip(G,j) = { |[r,s]| : G*(1,j)`2 < s & s < G*
(1,j+1)`2 } by A1,Th20
;
thus Int cell(G,len G,j) c=
{ |[r,s]| : G*(len G,1)`1 < r & G*(1,j)`2 < s & s < G*(1,j+1)`2 }
proof let x be set;
assume
A5: x in Int cell(G,len G,j);
then x in Int v_strip(G,len G) by A2,XBOOLE_0:def 3;
then consider r1,s1 such that
A6: x = |[r1,s1]| and
A7: G*(len G,1)`1 < r1 by A3;
x in Int h_strip(G,j) by A2,A5,XBOOLE_0:def 3;
then consider r2,s2 such that
A8: x = |[r2,s2]| and
A9: G*(1,j)`2 < s2 & s2 < G*(1,j+1)`2 by A4;
r1 = r2 & s1 = s2 by A6,A8,SPPOL_2:1;
hence thesis by A6,A7,A9;
end;
let x be set;
assume x in { |[r,s]| : G*(len G,1)`1 < r & G*(1,j)`2 < s & s < G*
(1,j+1)`2 };
then ex r,s st
x = |[r,s]| & G*(len G,1)`1 < r & G*(1,j)`2 < s & s < G*(1,j+1)`2;
then x in Int v_strip(G,len G) & x in Int h_strip(G,j) by A3,A4;
hence thesis by A2,XBOOLE_0:def 3;
end;
theorem Th27:
1 <= i & i < len G
implies Int cell(G,i,0) =
{ |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & s < G*(1,1)`2 }
proof assume
A1: 1 <= i & i < len G;
cell(G,i,0) = v_strip(G,i) /\ h_strip(G,0) by GOBOARD5:def 3;
then A2: Int cell(G,i,0) = Int v_strip(G,i) /\ Int h_strip(G,0) by TOPS_1:46
;
A3: Int v_strip(G,i) = { |[r,s]| : G*(i,1)`1 < r & r < G*
(i+1,1)`1 } by A1,Th17
;
A4: Int h_strip(G,0) = { |[r,s]| : s < G*(1,1)`2 } by Th18;
thus Int cell(G,i,0) c=
{ |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & s < G*(1,1)`2 }
proof let x be set;
assume
A5: x in Int cell(G,i,0);
then x in Int v_strip(G,i) by A2,XBOOLE_0:def 3;
then consider r1,s1 such that
A6: x = |[r1,s1]| and
A7: G*(i,1)`1 < r1 & r1 < G*(i+1,1)`1 by A3;
x in Int h_strip(G,0) by A2,A5,XBOOLE_0:def 3;
then consider r2,s2 such that
A8: x = |[r2,s2]| and
A9: s2 < G*(1,1)`2 by A4;
r1 = r2 & s1 = s2 by A6,A8,SPPOL_2:1;
hence thesis by A6,A7,A9;
end;
let x be set;
assume x in { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & s < G*(1,1)`2 };
then ex r,s st
x = |[r,s]| & G*(i,1)`1 < r & r < G*(i+1,1)`1 & s < G*(1,1)`2;
then x in Int v_strip(G,i) & x in Int h_strip(G,0) by A3,A4;
hence thesis by A2,XBOOLE_0:def 3;
end;
theorem Th28:
1 <= i & i < len G
implies Int cell(G,i,width G) =
{ |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,width G)`2 < s }
proof assume
A1: 1 <= i & i < len G;
cell(G,i,width G) = v_strip(G,i) /\ h_strip(G,width G) by GOBOARD5:def 3;
then A2: Int cell(G,i,width G) = Int v_strip(G,i) /\ Int h_strip(G,width G)
by TOPS_1:46;
A3: Int v_strip(G,i) = { |[r,s]| : G*(i,1)`1 < r & r < G*
(i+1,1)`1 } by A1,Th17
;
A4: Int h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 < s } by Th19;
thus Int cell(G,i,width G) c=
{ |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,width G)`2 < s }
proof let x be set;
assume
A5: x in Int cell(G,i,width G);
then x in Int v_strip(G,i) by A2,XBOOLE_0:def 3;
then consider r1,s1 such that
A6: x = |[r1,s1]| and
A7: G*(i,1)`1 < r1 & r1 < G*(i+1,1)`1 by A3;
x in Int h_strip(G,width G) by A2,A5,XBOOLE_0:def 3;
then consider r2,s2 such that
A8: x = |[r2,s2]| and
A9: G*(1,width G)`2 < s2 by A4;
r1 = r2 & s1 = s2 by A6,A8,SPPOL_2:1;
hence thesis by A6,A7,A9;
end;
let x be set;
assume
x in { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,width G)`2 < s };
then ex r,s st
x = |[r,s]| & G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,width G)`2 < s;
then x in Int v_strip(G,i) & x in Int h_strip(G,width G) by A3,A4;
hence thesis by A2,XBOOLE_0:def 3;
end;
theorem Th29:
1 <= i & i < len G & 1 <= j & j < width G
implies Int cell(G,i,j) =
{ |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 &
G*(1,j)`2 < s & s < G*(1,j+1)`2 }
proof assume that
A1: 1 <= i & i < len G and
A2: 1 <= j & j < width G;
cell(G,i,j) = v_strip(G,i) /\ h_strip(G,j) by GOBOARD5:def 3;
then A3: Int cell(G,i,j) = Int v_strip(G,i) /\ Int h_strip(G,j) by TOPS_1:46
;
A4: Int v_strip(G,i) = { |[r,s]| : G*(i,1)`1 < r & r < G*
(i+1,1)`1 } by A1,Th17
;
A5: Int h_strip(G,j) = { |[r,s]| : G*(1,j)`2 < s & s < G*
(1,j+1)`2 } by A2,Th20
;
thus Int cell(G,i,j) c=
{ |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 &
G*(1,j)`2 < s & s < G*(1,j+1)`2 }
proof let x be set;
assume
A6: x in Int cell(G,i,j);
then x in Int v_strip(G,i) by A3,XBOOLE_0:def 3;
then consider r1,s1 such that
A7: x = |[r1,s1]| and
A8: G*(i,1)`1 < r1 & r1 < G*(i+1,1)`1 by A4;
x in Int h_strip(G,j) by A3,A6,XBOOLE_0:def 3;
then consider r2,s2 such that
A9: x = |[r2,s2]| and
A10: G*(1,j)`2 < s2 & s2 < G*(1,j+1)`2 by A5;
r1 = r2 & s1 = s2 by A7,A9,SPPOL_2:1;
hence thesis by A7,A8,A10;
end;
let x be set;
assume x in { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 &
G*(1,j)`2 < s & s < G*(1,j+1)`2 };
then ex r,s st x = |[r,s]| &
G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2;
then x in Int v_strip(G,i) & x in Int h_strip(G,j) by A4,A5;
hence thesis by A3,XBOOLE_0:def 3;
end;
theorem
1 <= j & j <= width G & p in Int h_strip(G,j) implies p`2 > G*(1,j)`2
proof assume that
A1: 1 <= j & j <= width G and
A2: p in Int h_strip(G,j);
per cases by A1,AXIOMS:21;
suppose j = width G;
then Int h_strip(G,j) = { |[r,s]| : G*(1,j)`2 < s } by Th19;
then consider r,s such that
A3: p = |[r,s]| and
A4: G*(1,j)`2 < s by A2;
thus p`2 > G*(1,j)`2 by A3,A4,EUCLID:56;
suppose j < width G;
then Int h_strip(G,j) = { |[r,s]| : G*(1,j)`2 < s & s < G*(1,j+1)`2 }
by A1,Th20;
then consider r,s such that
A5: p = |[r,s]| and
A6: G*(1,j)`2 < s and s < G*(1,j+1)`2 by A2;
thus p`2 > G*(1,j)`2 by A5,A6,EUCLID:56;
end;
theorem
j < width G & p in Int h_strip(G,j) implies p`2 < G*(1,j+1)`2
proof assume that
A1: j < width G and
A2: p in Int h_strip(G,j);
per cases by RLVECT_1:99;
suppose j = 0;
then Int h_strip(G,j) = { |[r,s]| : s < G*(1,j+1)`2 } by Th18;
then consider r,s such that
A3: p = |[r,s]| and
A4: G*(1,j+1)`2 > s by A2;
thus p`2 < G*(1,j+1)`2 by A3,A4,EUCLID:56;
suppose j >= 1;
then Int h_strip(G,j) = { |[r,s]| : G*(1,j)`2 < s & s < G*(1,j+1)`2 }
by A1,Th20;
then consider r,s such that
A5: p = |[r,s]| and G*(1,j)`2 < s and
A6: s < G*(1,j+1)`2 by A2;
thus p`2 < G*(1,j+1)`2 by A5,A6,EUCLID:56;
end;
theorem
1 <= i & i <= len G & p in Int v_strip(G,i) implies p`1 > G*(i,1)`1
proof assume that
A1: 1 <= i & i <= len G and
A2: p in Int v_strip(G,i);
per cases by A1,AXIOMS:21;
suppose i = len G;
then Int v_strip(G,i) = { |[r,s]| : G*(i,1)`1 < r } by Th16;
then consider r,s such that
A3: p = |[r,s]| and
A4: G*(i,1)`1 < r by A2;
thus p`1 > G*(i,1)`1 by A3,A4,EUCLID:56;
suppose i < len G;
then Int v_strip(G,i) = { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 }
by A1,Th17;
then consider r,s such that
A5: p = |[r,s]| and
A6: G*(i,1)`1 < r and r < G*(i+1,1)`1 by A2;
thus p`1 > G*(i,1)`1 by A5,A6,EUCLID:56;
end;
theorem
i < len G & p in Int v_strip(G,i) implies p`1 < G*(i+1,1)`1
proof assume that
A1: i < len G and
A2: p in Int v_strip(G,i);
per cases by RLVECT_1:99;
suppose i = 0;
then Int v_strip(G,i) = { |[r,s]| : r < G*(i+1,1)`1 } by Th15;
then consider r,s such that
A3: p = |[r,s]| and
A4: G*(i+1,1)`1 > r by A2;
thus p`1 < G*(i+1,1)`1 by A3,A4,EUCLID:56;
suppose i >= 1;
then Int v_strip(G,i) = { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 }
by A1,Th17;
then consider r,s such that
A5: p = |[r,s]| and G*(i,1)`1 < r and
A6: r < G*(i+1,1)`1 by A2;
thus p`1 < G*(i+1,1)`1 by A5,A6,EUCLID:56;
end;
theorem Th34:
1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies
1/2*(G*(i,j)+G*(i+1,j+1)) in Int cell(G,i,j)
proof assume that
A1: 1 <= i & i+1 <= len G and
A2: 1 <= j & j+1 <= width G;
set r1 = G*(i,j)`1, s1 = G*(i,j)`2, r2 = G*(i+1,j+1)`1, s2 = G*
(i+1,j+1)`2;
A3: G*(i,j) = |[r1,s1]| by EUCLID:57;
G*(i+1,j+1) = |[r2,s2]| by EUCLID:57;
then G*(i,j)+G*(i+1,j+1) = |[r1+r2,s1+s2]| by A3,EUCLID:60;
then A4: 1/2*(G*(i,j)+G*(i+1,j+1)) = |[1/2*(r1+r2),1/2*(s1+s2)]| by EUCLID:
62;
A5: 1/2*r1 = r1/2 by XCMPLX_1:100;
A6: 1/2*r2 = r2/2 by XCMPLX_1:100;
A7: 1/2*s1 = s1/2 by XCMPLX_1:100;
A8: 1/2*s2 = s2/2 by XCMPLX_1:100;
i <= i+1 & j <= j+1 by NAT_1:29;
then A9: i <= len G & j <= width G by A1,A2,AXIOMS:22;
A10: 1 <= i+1 & 1 <= j+1 by NAT_1:29;
A11: G*(i,1)`1 = r1 by A1,A2,A9,GOBOARD5:3;
A12: G*(i+1,1)`1 = r2 by A1,A2,A10,GOBOARD5:3;
A13: G*(1,j)`2 = s1 by A1,A2,A9,GOBOARD5:2;
A14: G*(1,j+1)`2 = s2 by A1,A2,A10,GOBOARD5:2;
1 <= width G & i < i+1 by A2,A9,AXIOMS:22,REAL_1:69;
then A15: r1 < r2 by A1,A11,A12,GOBOARD5:4;
then r1+r1 < r1+r2 by REAL_1:53;
then 1/2*(r1+r1) < 1/2*(r1+r2) by REAL_1:70;
then 1/2*r1+1/2*r1 < 1/2*(r1+r2) by XCMPLX_1:8;
then A16: G*(i,1)`1 < 1/2*(r1+r2) by A5,A11,XCMPLX_1:66;
r1+r2 < r2+r2 by A15,REAL_1:53;
then 1/2*(r1+r2) < 1/2*(r2+r2) by REAL_1:70;
then 1/2*(r1+r2) < 1/2*r2+1/2*r2 by XCMPLX_1:8;
then A17: 1/2*(r1+r2) < G*(i+1,1)`1 by A6,A12,XCMPLX_1:66;
1 <= len G & j < j+1 by A1,A9,AXIOMS:22,REAL_1:69;
then A18: s1 < s2 by A2,A13,A14,GOBOARD5:5;
then s1+s1 < s1+s2 by REAL_1:53;
then 1/2*(s1+s1) < 1/2*(s1+s2) by REAL_1:70;
then 1/2*s1+1/2*s1 < 1/2*(s1+s2) by XCMPLX_1:8;
then A19: G*(1,j)`2 < 1/2*(s1+s2) by A7,A13,XCMPLX_1:66;
s1+s2 < s2+s2 by A18,REAL_1:53;
then 1/2*(s1+s2) < 1/2*(s2+s2) by REAL_1:70;
then 1/2*(s1+s2) < 1/2*s2+1/2*s2 by XCMPLX_1:8;
then A20: 1/2*(s1+s2) < G*(1,j+1)`2 by A8,A14,XCMPLX_1:66;
A21: 1 <= i & i < len G by A1,NAT_1:38;
1 <= j & j < width G by A2,NAT_1:38;
then Int cell(G,i,j) =
{ |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 &
G*(1,j)`2 < s & s < G*(1,j+1)`2 } by A21,Th29;
hence 1/2*(G*(i,j)+G*(i+1,j+1)) in Int cell(G,i,j) by A4,A16,A17,A19,A20;
end;
theorem Th35:
1 <= i & i+1 <= len G implies
1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]| in Int cell(G,i,width G)
proof assume that
A1: 1 <= i & i+1 <= len G;
set r1 = G*(i,width G)`1, s1 = G*(i,width G)`2, r2 = G*(i+1,width G)`1;
A2: i < len G by A1,NAT_1:38;
width G <> 0 by GOBOARD1:def 5;
then A3: 1 <= i+1 & 1 <= width G by NAT_1:29,RLVECT_1:99;
A4: 1/2*s1 = s1/2 by XCMPLX_1:100;
A5: 1/2*(s1+s1) = 1/2*s1+1/2*s1 by XCMPLX_1:8 .= s1 by A4,XCMPLX_1:66;
A6: G*(i,width G) = |[r1,s1]| by EUCLID:57;
A7: G*(1,width G)`2 = s1 by A1,A2,A3,GOBOARD5:2;
G*(1,width G)`2 = G*(i+1,width G)`2 by A1,A3,GOBOARD5:2;
then G*(i+1,width G) = |[r2,s1]| by A7,EUCLID:57;
then G*(i,width G)+G*(i+1,width G) = |[r1+r2,s1+s1]| by A6,EUCLID:60;
then 1/2*(G*(i,width G)+G*(i+1,width G))= |[1/2*(r1+r2),s1]|
by A5,EUCLID:62;
then A8: 1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]| = |[1/2*(r1+r2)+0,s1+1
]|
by EUCLID:60;
A9: 1/2*r1 = r1/2 by XCMPLX_1:100;
A10: 1/2*r2 = r2/2 by XCMPLX_1:100;
A11: G*(i,1)`1 = r1 by A1,A2,A3,GOBOARD5:3;
A12: G*(i+1,1)`1 = r2 by A1,A3,GOBOARD5:3;
width G <> 0 by GOBOARD1:def 5;
then 1 <= width G & i < i+1 by REAL_1:69,RLVECT_1:99;
then A13: r1 < r2 by A1,GOBOARD5:4;
then r1+r1 < r1+r2 by REAL_1:53;
then 1/2*(r1+r1) < 1/2*(r1+r2) by REAL_1:70;
then 1/2*r1+1/2*r1 < 1/2*(r1+r2) by XCMPLX_1:8;
then A14: G*(i,1)`1 < 1/2*(r1+r2) by A9,A11,XCMPLX_1:66;
r1+r2 < r2+r2 by A13,REAL_1:53;
then 1/2*(r1+r2) < 1/2*(r2+r2) by REAL_1:70;
then 1/2*(r1+r2) < 1/2*r2+1/2*r2 by XCMPLX_1:8;
then A15: 1/2*(r1+r2) < G*(i+1,1)`1 by A10,A12,XCMPLX_1:66;
A16: G*(1,width G)`2 < s1+1 by A7,REAL_1:69;
1 <= i & i < len G by A1,NAT_1:38;
then Int cell(G,i,width G) =
{ |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*
(1,width G)`2 < s } by Th28
;
hence 1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]| in Int cell(G,i,width G)
by A8,A14,A15,A16;
end;
theorem Th36:
1 <= i & i+1 <= len G implies
1/2*(G*(i,1)+G*(i+1,1))-|[0,1]| in Int cell(G,i,0)
proof assume that
A1: 1 <= i & i+1 <= len G;
set r1 = G*(i,1)`1, s1 = G*(i,1)`2, r2 = G*(i+1,1)`1;
A2: i < len G by A1,NAT_1:38;
width G <> 0 by GOBOARD1:def 5;
then A3: 1 <= i+1 & 1 <= width G by NAT_1:29,RLVECT_1:99;
A4: 1/2*s1 = s1/2 by XCMPLX_1:100;
A5: 1/2*(s1+s1) = 1/2*s1+1/2*s1 by XCMPLX_1:8 .= s1 by A4,XCMPLX_1:66;
A6: G*(i,1) = |[r1,s1]| by EUCLID:57;
A7: G*(1,1)`2 = s1 by A1,A2,A3,GOBOARD5:2;
G*(1,1)`2 = G*(i+1,1)`2 by A1,A3,GOBOARD5:2;
then G*(i+1,1) = |[r2,s1]| by A7,EUCLID:57;
then G*(i,1)+G*(i+1,1) = |[r1+r2,s1+s1]| by A6,EUCLID:60;
then 1/2*(G*(i,1)+G*(i+1,1))= |[1/2*(r1+r2),s1]| by A5,EUCLID:62;
then A8: 1/2*(G*(i,1)+G*(i+1,1))-|[0,1]| = |[1/2*(r1+r2)-0,s1-1]| by EUCLID
:66
.= |[1/2*(r1+r2),s1-1]|;
A9: 1/2*r1 = r1/2 by XCMPLX_1:100;
A10: 1/2*r2 = r2/2 by XCMPLX_1:100;
width G <> 0 by GOBOARD1:def 5;
then 1 <= width G & i < i+1 by REAL_1:69,RLVECT_1:99;
then A11: r1 < r2 by A1,GOBOARD5:4;
then r1+r1 < r1+r2 by REAL_1:53;
then 1/2*(r1+r1) < 1/2*(r1+r2) by REAL_1:70;
then 1/2*r1+1/2*r1 < 1/2*(r1+r2) by XCMPLX_1:8;
then A12: G*(i,1)`1 < 1/2*(r1+r2) by A9,XCMPLX_1:66;
r1+r2 < r2+r2 by A11,REAL_1:53;
then 1/2*(r1+r2) < 1/2*(r2+r2) by REAL_1:70;
then 1/2*(r1+r2) < 1/2*r2+1/2*r2 by XCMPLX_1:8;
then A13: 1/2*(r1+r2) < G*(i+1,1)`1 by A10,XCMPLX_1:66;
s1 < G*(1,1)`2+1 by A7,REAL_1:69;
then A14: s1-1 < G*(1,1)`2 by REAL_1:84;
1 <= i & i < len G by A1,NAT_1:38;
then Int cell(G,i,0) =
{ |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & s < G*(1,1)`2 } by Th27;
hence 1/2*(G*(i,1)+G*(i+1,1))-|[0,1]| in Int cell(G,i,0) by A8,A12,A13,A14;
end;
theorem Th37:
1 <= j & j+1 <= width G implies
1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]| in Int cell(G,len G,j)
proof assume that
A1: 1 <= j & j+1 <= width G;
set s1 = G*(len G,j)`2, r1 = G*(len G,j)`1, s2 = G*(len G,j+1)`2;
A2: j < width G by A1,NAT_1:38;
len G <> 0 by GOBOARD1:def 5;
then A3: 1 <= j+1 & 1 <= len G by NAT_1:29,RLVECT_1:99;
A4: 1/2*r1 = r1/2 by XCMPLX_1:100;
A5: 1/2*(r1+r1) = 1/2*r1+1/2*r1 by XCMPLX_1:8 .= r1 by A4,XCMPLX_1:66;
A6: G*(len G,j) = |[r1,s1]| by EUCLID:57;
A7: G*(len G,1)`1 = r1 by A1,A2,A3,GOBOARD5:3;
G*(len G,1)`1 = G*(len G,j+1)`1 by A1,A3,GOBOARD5:3;
then G*(len G,j+1) = |[r1,s2]| by A7,EUCLID:57;
then G*(len G,j)+G*(len G,j+1) = |[r1+r1,s1+s2]| by A6,EUCLID:60;
then 1/2*(G*(len G,j)+G*(len G,j+1))= |[r1,1/2*(s1+s2)]|
by A5,EUCLID:62;
then A8: 1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]| = |[r1+1,1/2*(s1+s2)+0]|
by EUCLID:60;
A9: 1/2*s1 = s1/2 by XCMPLX_1:100;
A10: 1/2*s2 = s2/2 by XCMPLX_1:100;
A11: G*(1,j)`2 = s1 by A1,A2,A3,GOBOARD5:2;
A12: G*(1,j+1)`2 = s2 by A1,A3,GOBOARD5:2;
len G <> 0 by GOBOARD1:def 5;
then 1 <= len G & j < j+1 by REAL_1:69,RLVECT_1:99;
then A13: s1 < s2 by A1,GOBOARD5:5;
then s1+s1 < s1+s2 by REAL_1:53;
then 1/2*(s1+s1) < 1/2*(s1+s2) by REAL_1:70;
then 1/2*s1+1/2*s1 < 1/2*(s1+s2) by XCMPLX_1:8;
then A14: G*(1,j)`2 < 1/2*(s1+s2) by A9,A11,XCMPLX_1:66;
s1+s2 < s2+s2 by A13,REAL_1:53;
then 1/2*(s1+s2) < 1/2*(s2+s2) by REAL_1:70;
then 1/2*(s1+s2) < 1/2*s2+1/2*s2 by XCMPLX_1:8;
then A15: 1/2*(s1+s2) < G*(1,j+1)`2 by A10,A12,XCMPLX_1:66;
A16: G*(len G,1)`1 < r1+1 by A7,REAL_1:69;
1 <= j & j < width G by A1,NAT_1:38;
then Int cell(G,len G,j) =
{ |[r,s]| : G*(len G,1)`1 < r & G*(1,j)`2 < s & s < G*
(1,j+1)`2 } by Th26;
hence 1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]| in Int cell(G,len G,j)
by A8,A14,A15,A16;
end;
theorem Th38:
1 <= j & j+1 <= width G implies
1/2*(G*(1,j)+G*(1,j+1))-|[1,0]| in Int cell(G,0,j)
proof assume that
A1: 1 <= j & j+1 <= width G;
set s1 = G*(1,j)`2, r1 = G*(1,j)`1, s2 = G*(1,j+1)`2;
A2: j < width G by A1,NAT_1:38;
len G <> 0 by GOBOARD1:def 5;
then A3: 1 <= j+1 & 1 <= len G by NAT_1:29,RLVECT_1:99;
A4: 1/2*r1 = r1/2 by XCMPLX_1:100;
A5: 1/2*(r1+r1) = 1/2*r1+1/2*r1 by XCMPLX_1:8 .= r1 by A4,XCMPLX_1:66;
A6: G*(1,j) = |[r1,s1]| by EUCLID:57;
A7: G*(1,1)`1 = r1 by A1,A2,A3,GOBOARD5:3;
G*(1,1)`1 = G*(1,j+1)`1 by A1,A3,GOBOARD5:3;
then G*(1,j+1) = |[r1,s2]| by A7,EUCLID:57;
then G*(1,j)+G*(1,j+1) = |[r1+r1,s1+s2]| by A6,EUCLID:60;
then 1/2*(G*(1,j)+G*(1,j+1))= |[r1,1/2*(s1+s2)]| by A5,EUCLID:62;
then A8: 1/2*(G*(1,j)+G*(1,j+1))-|[1,0]| = |[r1-1,1/2*(s1+s2)-0]| by EUCLID
:66
.= |[r1-1,1/2*(s1+s2)]|;
A9: 1/2*s1 = s1/2 by XCMPLX_1:100;
A10: 1/2*s2 = s2/2 by XCMPLX_1:100;
len G <> 0 by GOBOARD1:def 5;
then 1 <= len G & j < j+1 by REAL_1:69,RLVECT_1:99;
then A11: s1 < s2 by A1,GOBOARD5:5;
then s1+s1 < s1+s2 by REAL_1:53;
then 1/2*(s1+s1) < 1/2*(s1+s2) by REAL_1:70;
then 1/2*s1+1/2*s1 < 1/2*(s1+s2) by XCMPLX_1:8;
then A12: G*(1,j)`2 < 1/2*(s1+s2) by A9,XCMPLX_1:66;
s1+s2 < s2+s2 by A11,REAL_1:53;
then 1/2*(s1+s2) < 1/2*(s2+s2) by REAL_1:70;
then 1/2*(s1+s2) < 1/2*s2+1/2*s2 by XCMPLX_1:8;
then A13: 1/2*(s1+s2) < G*(1,j+1)`2 by A10,XCMPLX_1:66;
r1 < G*(1,1)`1+1 by A7,REAL_1:69;
then A14: r1-1 < G*(1,1)`1 by REAL_1:84;
1 <= j & j < width G by A1,NAT_1:38;
then Int cell(G,0,j) =
{ |[r,s]| : r < G*(1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 } by Th23;
hence 1/2*(G*(1,j)+G*(1,j+1))-|[1,0]| in Int cell(G,0,j) by A8,A12,A13,A14;
end;
theorem Th39:
G*(1,1)-|[1,1]| in Int cell(G,0,0)
proof set s1 = G*(1,1)`2, r1 = G*(1,1)`1;
G*(1,1) = |[r1,s1]| by EUCLID:57;
then A1: G*(1,1)-|[1,1]| = |[r1-1,s1-1]| by EUCLID:66;
s1 < G*(1,1)`2+1 by REAL_1:69;
then A2: s1-1 < G*(1,1)`2 by REAL_1:84;
r1 < G*(1,1)`1+1 by REAL_1:69;
then A3: r1-1 < G*(1,1)`1 by REAL_1:84;
Int cell(G,0,0) = { |[r,s]| : r < G*(1,1)`1 & s < G*(1,1)`2 } by Th21;
hence G*(1,1)-|[1,1]| in Int cell(G,0,0) by A1,A2,A3;
end;
theorem Th40:
G*(len G,width G)+|[1,1]| in Int cell(G,len G,width G)
proof set s1 = G*(len G,width G)`2, r1 = G*(len G,width G)`1;
width G <> 0 by GOBOARD1:def 5;
then A1: 1 <= width G by RLVECT_1:99;
len G <> 0 by GOBOARD1:def 5;
then A2: 1 <= len G by RLVECT_1:99;
then A3: G*(len G,1)`1 = r1 by A1,GOBOARD5:3;
A4: G*(1,width G)`2 = s1 by A1,A2,GOBOARD5:2;
G*(len G,width G) = |[r1,s1]| by EUCLID:57;
then A5: G*(len G,width G)+|[1,1]| = |[r1+1,s1+1]| by EUCLID:60;
A6: s1+1 > G*(1,width G)`2 by A4,REAL_1:69;
A7: r1+1 > G*(len G,1)`1 by A3,REAL_1:69;
Int cell(G,len G,width G) =
{ |[r,s]| : G*(len G,1)`1 < r & G*(1,width G)`2 < s } by Th25;
hence G*(len G,width G)+|[1,1]| in Int cell(G,len G,width G) by A5,A6,A7;
end;
theorem Th41:
G*(1,width G)+|[-1,1]| in Int cell(G,0,width G)
proof set s1 = G*(1,width G)`2, r1 = G*(1,width G)`1;
width G <> 0 by GOBOARD1:def 5;
then A1: 1 <= width G by RLVECT_1:99;
len G <> 0 by GOBOARD1:def 5;
then 1 <= len G by RLVECT_1:99;
then A2: G*(1,1)`1 = r1 by A1,GOBOARD5:3;
G*(1,width G) = |[r1,s1]| by EUCLID:57;
then A3: G*(1,width G)+|[-1,1]| = |[r1+-1,s1+1]| by EUCLID:60
.= |[r1-1,s1+1]| by XCMPLX_0:def 8;
A4: s1+1 > G*(1,width G)`2 by REAL_1:69;
r1 < G*(1,1)`1+1 by A2,REAL_1:69;
then A5: r1-1 < G*(1,1)`1 by REAL_1:84;
Int cell(G,0,width G) = { |[r,s]| : r < G*(1,1)`1 & G*(1,width G)`2 < s }
by Th22;
hence G*(1,width G)+|[-1,1]| in Int cell(G,0,width G) by A3,A4,A5;
end;
theorem Th42:
G*(len G,1)+|[1,-1]| in Int cell(G,len G,0)
proof set s1 = G*(len G,1)`2, r1 = G*(len G,1)`1;
width G <> 0 by GOBOARD1:def 5;
then A1: 1 <= width G by RLVECT_1:99;
len G <> 0 by GOBOARD1:def 5;
then 1 <= len G by RLVECT_1:99;
then A2: G*(1,1)`2 = s1 by A1,GOBOARD5:2;
G*(len G,1) = |[r1,s1]| by EUCLID:57;
then A3: G*(len G,1)+|[1,-1]| = |[r1+1,s1+-1]| by EUCLID:60
.= |[r1+1,s1-1]| by XCMPLX_0:def 8;
s1 < G*(1,1)`2+1 by A2,REAL_1:69;
then A4: s1-1 < G*(1,1)`2 by REAL_1:84;
A5: r1+1 > G*(len G,1)`1 by REAL_1:69;
Int cell(G,len G,0) = { |[r,s]| : G*(len G,1)`1 < r & s < G*
(1,1)`2 } by Th24
;
hence G*(len G,1)+|[1,-1]| in Int cell(G,len G,0) by A3,A4,A5;
end;
theorem Th43:
1 <= i & i < len G & 1 <= j & j < width G implies
LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i,j+1)))
c= Int cell(G,i,j) \/ { 1/2*(G*(i,j)+G*(i,j+1)) }
proof
assume
A1: 1 <= i & i < len G & 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i,j+1)));
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,j)+G*(i+1,j+1)))+r*(1/2*(G*(i,j)+G*(i,j+1)))
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(1/2*(G*(i,j)+G*(i,j+1))) by A4,EUCLID:33
.= 1*(1/2*(G*(i,j)+G*(i,j+1))) by EUCLID:31
.= 1/2*(G*(i,j)+G*(i,j+1)) by EUCLID:33;
hence p in { 1/2*(G*(i,j)+G*(i,j+1)) } by TARSKI:def 1;
case
A5: r < 1;
set r1 = G*(i,1)`1, r2 = G*(i+1,1)`1,
s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
A7: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
A8: G*(i,j) = |[G*(i,j)`1,G*(i,j)`2]| by EUCLID:57
.= |[r1,G*(i,j)`2]| by A1,GOBOARD5:3
.= |[r1,s1]| by A1,GOBOARD5:2;
A9: G*(i+1,j+1) = |[G*(i+1,j+1)`1,G*(i+1,j+1)`2]| by EUCLID:57
.= |[r2,G*(i+1,j+1)`2]| by A6,A7,GOBOARD5:3
.= |[r2,s2]| by A6,A7,GOBOARD5:2;
A10: G*(i,j+1) = |[G*(i,j+1)`1,G*(i,j+1)`2]| by EUCLID:57
.= |[r1,G*(i,j+1)`2]| by A1,A6,GOBOARD5:3
.= |[r1,s2]| by A1,A6,GOBOARD5:2;
set r3 = (1-r)*(1/2), s3 = r*(1/2);
A11: (1/2)*r1 = r1/2 by XCMPLX_1:100;
A12: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A13: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A14: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A15: p = r3*(G*(i,j)+G*(i+1,j+1))+r*(1/2*(G*(i,j)+G*
(i,j+1))) by A4,EUCLID:34
.= r3*(G*(i,j)+G*(i+1,j+1))+s3*(G*(i,j)+G*(i,j+1)) by EUCLID:34
.= r3*|[r1+r2,s1+s2]|+s3*(G*(i,j)+G*(i,j+1)) by A8,A9,EUCLID:60
.= r3*|[r1+r2,s1+s2]|+s3*|[r1+r1,s1+s2]| by A8,A10,EUCLID:60
.= |[r3*(r1+r2),r3*(s1+s2)]|+s3*|[r1+r1,s1+s2]| by EUCLID:62
.= |[r3*(r1+r2),r3*(s1+s2)]|+|[s3*(r1+r1),s3*(s1+s2)]| by EUCLID:62
.= |[r3*(r1+r2)+s3*(r1+r1),r3*(s1+s2)+s3*(s1+s2)]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A16: r3 > (1/2)*0 by REAL_1:70;
0 <> width G by GOBOARD1:def 5;
then A17: 1 <= width G by RLVECT_1:99;
i < i+1 by REAL_1:69;
then A18: r1 < r2 by A1,A7,A17,GOBOARD5:4;
then r1+r1 < r1+r2 by REAL_1:53;
then A19: r3*(r1+r1) < r3*(r1+r2) by A16,REAL_1:70;
0 <> len G by GOBOARD1:def 5;
then A20: 1 <= len G by RLVECT_1:99;
j < j+1 by REAL_1:69;
then A21: s1 < s2 by A1,A6,A20,GOBOARD5:5;
r3*(r1+r1)+s3*(r1+r1)
= (r3+s3)*(r1+r1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r1+r1) by XCMPLX_1:8
.= 1*(1/2)*(r1+r1) by XCMPLX_1:27
.= (1/2)*r1+(1/2)*r1 by XCMPLX_1:8
.= r1 by A11,XCMPLX_1:66;
then A22: r1 < r3*(r1+r2)+s3*(r1+r1) by A19,REAL_1:53;
A23: s3 >= 0 by A3,REAL_2:121;
r1+r2 < r2+r2 by A18,REAL_1:53;
then A24: r3*(r1+r2) < r3*(r2+r2) by A16,REAL_1:70;
r1+r1 < r2+r2 by A18,REAL_1:67;
then A25: s3*(r1+r1) <= s3*(r2+r2) by A23,AXIOMS:25;
r3*(r2+r2)+s3*(r2+r2)
= (r3+s3)*(r2+r2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2 by XCMPLX_1:8
.= r2 by A12,XCMPLX_1:66;
then A26: r3*(r1+r2)+s3*(r1+r1) < r2 by A24,A25,REAL_1:67;
A27: s1+s1 < s1+s2 by A21,REAL_1:53;
then A28: r3*(s1+s1) < r3*(s1+s2) by A16,REAL_1:70;
A29: s3*(s1+s1) <= s3*(s1+s2) by A23,A27,AXIOMS:25;
r3*(s1+s1)+s3*(s1+s1)
= (r3+s3)*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A13,XCMPLX_1:66;
then A30: s1 < r3*(s1+s2)+s3*(s1+s2) by A28,A29,REAL_1:67;
A31: s1+s2 < s2+s2 by A21,REAL_1:53;
then A32: r3*(s1+s2) < r3*(s2+s2) by A16,REAL_1:70;
A33: s3*(s1+s2) <= s3*(s2+s2) by A23,A31,AXIOMS:25;
r3*(s2+s2)+s3*(s2+s2)
= (r3+s3)*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A14,XCMPLX_1:66;
then A34: r3*(s1+s2)+s3*(s1+s2) < s2 by A32,A33,REAL_1:67;
Int cell(G,i,j) =
{ |[r',s']| : r1 < r' & r' < r2 & s1 < s' & s' < s2 } by A1,Th29;
hence p in Int cell(G,i,j) by A15,A22,A26,A30,A34;
end;
hence x in Int cell(G,i,j) \/ { 1/2*(G*(i,j)+G*(i,j+1)) } by XBOOLE_0:def 2;
end;
theorem Th44:
1 <= i & i < len G & 1 <= j & j < width G implies
LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j+1)+G*(i+1,j+1))) c=
Int cell(G,i,j) \/ { 1/2*(G*(i,j+1)+G*(i+1,j+1)) }
proof
assume
A1: 1 <= i & i < len G & 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j+1)+G*(i+1,j+1)));
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,j)+G*(i+1,j+1)))+r*(1/2*(G*(i,j+1)+G*(i+1,j+1)))
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(1/2*(G*(i,j+1)+G*(i+1,j+1))) by A4,EUCLID:33
.= 1*(1/2*(G*(i,j+1)+G*(i+1,j+1))) by EUCLID:31
.= 1/2*(G*(i,j+1)+G*(i+1,j+1)) by EUCLID:33;
hence p in { 1/2*(G*(i,j+1)+G*(i+1,j+1)) } by TARSKI:def 1;
case
A5: r < 1;
set r1 = G*(i,1)`1, r2 = G*(i+1,1)`1,
s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
A7: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
A8: G*(i,j) = |[G*(i,j)`1,G*(i,j)`2]| by EUCLID:57
.= |[r1,G*(i,j)`2]| by A1,GOBOARD5:3
.= |[r1,s1]| by A1,GOBOARD5:2;
A9: G*(i+1,j+1) = |[G*(i+1,j+1)`1,G*(i+1,j+1)`2]| by EUCLID:57
.= |[r2,G*(i+1,j+1)`2]| by A6,A7,GOBOARD5:3
.= |[r2,s2]| by A6,A7,GOBOARD5:2;
A10: G*(i,j+1) = |[G*(i,j+1)`1,G*(i,j+1)`2]| by EUCLID:57
.= |[r1,G*(i,j+1)`2]| by A1,A6,GOBOARD5:3
.= |[r1,s2]| by A1,A6,GOBOARD5:2;
set r3 = (1-r)*(1/2), s3 = r*(1/2);
A11: (1/2)*r1 = r1/2 by XCMPLX_1:100;
A12: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A13: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A14: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A15: p = r3*(G*(i,j)+G*(i+1,j+1))+r*(1/2*(G*(i,j+1)+G*(i+1,j+1))) by A4,EUCLID
:34
.= r3*(G*(i,j)+G*(i+1,j+1))+s3*(G*(i,j+1)+G*(i+1,j+1)) by EUCLID:34
.= r3*|[r1+r2,s1+s2]|+s3*(G*(i,j+1)+G*(i+1,j+1)) by A8,A9,EUCLID:60
.= r3*|[r1+r2,s1+s2]|+s3*|[r1+r2,s2+s2]| by A9,A10,EUCLID:60
.= |[r3*(r1+r2),r3*(s1+s2)]|+s3*|[r1+r2,s2+s2]| by EUCLID:62
.= |[r3*(r1+r2),r3*(s1+s2)]|+|[s3*(r1+r2),s3*(s2+s2)]| by EUCLID:62
.= |[r3*(r1+r2)+s3*(r1+r2),r3*(s1+s2)+s3*(s2+s2)]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A16: r3 > (1/2)*0 by REAL_1:70;
0 <> width G by GOBOARD1:def 5;
then A17: 1 <= width G by RLVECT_1:99;
i < i+1 by REAL_1:69;
then A18: r1 < r2 by A1,A7,A17,GOBOARD5:4;
then A19: r1+r1 < r1+r2 by REAL_1:53;
then A20: r3*(r1+r1) < r3*(r1+r2) by A16,REAL_1:70;
0 <> len G by GOBOARD1:def 5;
then A21: 1 <= len G by RLVECT_1:99;
j < j+1 by REAL_1:69;
then A22: s1 < s2 by A1,A6,A21,GOBOARD5:5;
A23: s3 >= 0 by A3,REAL_2:121;
then A24: s3*(r1+r1) <= s3*(r1+r2) by A19,AXIOMS:25;
r3*(r1+r1)+s3*(r1+r1)
= (r3+s3)*(r1+r1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r1+r1) by XCMPLX_1:8
.= 1*(1/2)*(r1+r1) by XCMPLX_1:27
.= (1/2)*r1+(1/2)*r1 by XCMPLX_1:8
.= r1 by A11,XCMPLX_1:66;
then A25: r1 < r3*(r1+r2)+s3*(r1+r2) by A20,A24,REAL_1:67;
r1+r2 < r2+r2 by A18,REAL_1:53;
then A26: r3*(r1+r2) < r3*(r2+r2) by A16,REAL_1:70;
r1+r2 < r2+r2 by A18,REAL_1:67;
then A27: s3*(r1+r2) <= s3*(r2+r2) by A23,AXIOMS:25;
r3*(r2+r2)+s3*(r2+r2)
= (r3+s3)*(r2+r2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2 by XCMPLX_1:8
.= r2 by A12,XCMPLX_1:66;
then A28: r3*(r1+r2)+s3*(r1+r2) < r2 by A26,A27,REAL_1:67;
A29: s1+s1 < s1+s2 by A22,REAL_1:53;
then A30: r3*(s1+s1) < r3*(s1+s2) by A16,REAL_1:70;
s1+s2 < s2+s2 by A22,REAL_1:53;
then s1+s1 < s2+s2 by A29,AXIOMS:22;
then A31: s3*(s1+s1) <= s3*(s2+s2) by A23,AXIOMS:25;
r3*(s1+s1)+s3*(s1+s1)
= (r3+s3)*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A13,XCMPLX_1:66;
then A32: s1 < r3*(s1+s2)+s3*(s2+s2) by A30,A31,REAL_1:67;
s1+s2 < s2+s2 by A22,REAL_1:53;
then A33: r3*(s1+s2) < r3*(s2+s2) by A16,REAL_1:70;
r3*(s2+s2)+s3*(s2+s2)
= (r3+s3)*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A14,XCMPLX_1:66;
then A34: r3*(s1+s2)+s3*(s2+s2) < s2 by A33,REAL_1:67;
Int cell(G,i,j) =
{ |[r',s']| : r1 < r' & r' < r2 & s1 < s' & s' < s2 } by A1,Th29;
hence p in Int cell(G,i,j) by A15,A25,A28,A32,A34;
end;
hence x in Int cell(G,i,j) \/ { 1/2*(G*(i,j+1)+G*
(i+1,j+1)) } by XBOOLE_0:def 2;
end;
theorem Th45:
1 <= i & i < len G & 1 <= j & j < width G implies
LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i+1,j)+G*(i+1,j+1))) c=
Int cell(G,i,j) \/ { 1/2*(G*(i+1,j)+G*(i+1,j+1)) }
proof
assume
A1: 1 <= i & i < len G & 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i+1,j)+G*(i+1,j+1)));
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,j)+G*(i+1,j+1)))+r*(1/2*(G*(i+1,j)+G*(i+1,j+1)))
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(1/2*(G*(i+1,j)+G*(i+1,j+1))) by A4,EUCLID:33
.= 1*(1/2*(G*(i+1,j)+G*(i+1,j+1))) by EUCLID:31
.= 1/2*(G*(i+1,j)+G*(i+1,j+1)) by EUCLID:33;
hence p in { 1/2*(G*(i+1,j)+G*(i+1,j+1)) } by TARSKI:def 1;
case
A5: r < 1;
set r1 = G*(i,1)`1, r2 = G*(i+1,1)`1,
s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
A7: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
A8: G*(i,j) = |[G*(i,j)`1,G*(i,j)`2]| by EUCLID:57
.= |[r1,G*(i,j)`2]| by A1,GOBOARD5:3
.= |[r1,s1]| by A1,GOBOARD5:2;
A9: G*(i+1,j+1) = |[G*(i+1,j+1)`1,G*(i+1,j+1)`2]| by EUCLID:57
.= |[r2,G*(i+1,j+1)`2]| by A6,A7,GOBOARD5:3
.= |[r2,s2]| by A6,A7,GOBOARD5:2;
A10: G*(i+1,j) = |[G*(i+1,j)`1,G*(i+1,j)`2]| by EUCLID:57
.= |[r2,G*(i+1,j)`2]| by A1,A7,GOBOARD5:3
.= |[r2,s1]| by A1,A7,GOBOARD5:2;
set r3 = (1-r)*(1/2), s3 = r*(1/2);
A11: (1/2)*r1 = r1/2 by XCMPLX_1:100;
A12: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A13: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A14: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A15: p = r3*(G*(i,j)+G*(i+1,j+1))+r*(1/2*(G*(i+1,j)+G*(i+1,j+1))) by A4,EUCLID
:34
.= r3*(G*(i,j)+G*(i+1,j+1))+s3*(G*(i+1,j)+G*(i+1,j+1)) by EUCLID:34
.= r3*|[r1+r2,s1+s2]|+s3*(G*(i+1,j)+G*(i+1,j+1)) by A8,A9,EUCLID:60
.= r3*|[r1+r2,s1+s2]|+s3*|[r2+r2,s1+s2]| by A9,A10,EUCLID:60
.= |[r3*(r1+r2),r3*(s1+s2)]|+s3*|[r2+r2,s1+s2]| by EUCLID:62
.= |[r3*(r1+r2),r3*(s1+s2)]|+|[s3*(r2+r2),s3*(s1+s2)]| by EUCLID:62
.= |[r3*(r1+r2)+s3*(r2+r2),r3*(s1+s2)+s3*(s1+s2)]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A16: r3 > (1/2)*0 by REAL_1:70;
0 <> width G by GOBOARD1:def 5;
then A17: 1 <= width G by RLVECT_1:99;
i < i+1 by REAL_1:69;
then A18: r1 < r2 by A1,A7,A17,GOBOARD5:4;
then A19: r1+r1 < r1+r2 by REAL_1:53;
then A20: r3*(r1+r1) < r3*(r1+r2) by A16,REAL_1:70;
0 <> len G by GOBOARD1:def 5;
then A21: 1 <= len G by RLVECT_1:99;
j < j+1 by REAL_1:69;
then A22: s1 < s2 by A1,A6,A21,GOBOARD5:5;
A23: s3 >= 0 by A3,REAL_2:121;
r1+r2 < r2+r2 by A18,REAL_1:53;
then r1+r1 < r2+r2 by A19,AXIOMS:22;
then A24: s3*(r1+r1) <= s3*(r2+r2) by A23,AXIOMS:25;
r3*(r1+r1)+s3*(r1+r1)
= (r3+s3)*(r1+r1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r1+r1) by XCMPLX_1:8
.= 1*(1/2)*(r1+r1) by XCMPLX_1:27
.= (1/2)*r1+(1/2)*r1 by XCMPLX_1:8
.= r1 by A11,XCMPLX_1:66;
then A25: r1 < r3*(r1+r2)+s3*(r2+r2) by A20,A24,REAL_1:67;
r1+r2 < r2+r2 by A18,REAL_1:53;
then A26: r3*(r1+r2) < r3*(r2+r2) by A16,REAL_1:70;
r3*(r2+r2)+s3*(r2+r2)
= (r3+s3)*(r2+r2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2 by XCMPLX_1:8
.= r2 by A12,XCMPLX_1:66;
then A27: r3*(r1+r2)+s3*(r2+r2) < r2 by A26,REAL_1:67;
A28: s1+s1 < s1+s2 by A22,REAL_1:53;
then A29: r3*(s1+s1) < r3*(s1+s2) by A16,REAL_1:70;
A30: s3*(s1+s1) <= s3*(s1+s2) by A23,A28,AXIOMS:25;
r3*(s1+s1)+s3*(s1+s1)
= (r3+s3)*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A13,XCMPLX_1:66;
then A31: s1 < r3*(s1+s2)+s3*(s1+s2) by A29,A30,REAL_1:67;
A32: s1+s2 < s2+s2 by A22,REAL_1:53;
then A33: r3*(s1+s2) < r3*(s2+s2) by A16,REAL_1:70;
A34: s3*(s1+s2) <= s3*(s2+s2) by A23,A32,AXIOMS:25;
r3*(s2+s2)+s3*(s2+s2)
= (r3+s3)*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A14,XCMPLX_1:66;
then A35: r3*(s1+s2)+s3*(s1+s2) < s2 by A33,A34,REAL_1:67;
Int cell(G,i,j) =
{ |[r',s']| : r1 < r' & r' < r2 & s1 < s' & s' < s2 } by A1,Th29;
hence p in Int cell(G,i,j) by A15,A25,A27,A31,A35;
end;
hence x in Int cell(G,i,j) \/ { 1/2*(G*(i+1,j)+G*
(i+1,j+1)) } by XBOOLE_0:def 2;
end;
theorem Th46:
1 <= i & i < len G & 1 <= j & j < width G implies
LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i+1,j))) c=
Int cell(G,i,j) \/ { 1/2*(G*(i,j)+G*(i+1,j)) }
proof
assume
A1: 1 <= i & i < len G & 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i+1,j)));
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,j)+G*(i+1,j+1)))+r*(1/2*(G*(i,j)+G*(i+1,j)))
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(1/2*(G*(i,j)+G*(i+1,j))) by A4,EUCLID:33
.= 1*(1/2*(G*(i,j)+G*(i+1,j))) by EUCLID:31
.= 1/2*(G*(i,j)+G*(i+1,j)) by EUCLID:33;
hence p in { 1/2*(G*(i,j)+G*(i+1,j)) } by TARSKI:def 1;
case
A5: r < 1;
set r1 = G*(i,1)`1, r2 = G*(i+1,1)`1,
s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
A7: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
A8: G*(i,j) = |[G*(i,j)`1,G*(i,j)`2]| by EUCLID:57
.= |[r1,G*(i,j)`2]| by A1,GOBOARD5:3
.= |[r1,s1]| by A1,GOBOARD5:2;
A9: G*(i+1,j+1) = |[G*(i+1,j+1)`1,G*(i+1,j+1)`2]| by EUCLID:57
.= |[r2,G*(i+1,j+1)`2]| by A6,A7,GOBOARD5:3
.= |[r2,s2]| by A6,A7,GOBOARD5:2;
A10: G*(i+1,j) = |[G*(i+1,j)`1,G*(i+1,j)`2]| by EUCLID:57
.= |[r2,G*(i+1,j)`2]| by A1,A7,GOBOARD5:3
.= |[r2,s1]| by A1,A7,GOBOARD5:2;
set r3 = (1-r)*(1/2), s3 = r*(1/2);
A11: (1/2)*r1 = r1/2 by XCMPLX_1:100;
A12: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A13: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A14: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A15: p = r3*(G*(i,j)+G*(i+1,j+1))+r*(1/2*(G*(i,j)+G*
(i+1,j))) by A4,EUCLID:34
.= r3*(G*(i,j)+G*(i+1,j+1))+s3*(G*(i,j)+G*(i+1,j)) by EUCLID:34
.= r3*|[r1+r2,s1+s2]|+s3*(G*(i,j)+G*(i+1,j)) by A8,A9,EUCLID:60
.= r3*|[r1+r2,s1+s2]|+s3*|[r1+r2,s1+s1]| by A8,A10,EUCLID:60
.= |[r3*(r1+r2),r3*(s1+s2)]|+s3*|[r1+r2,s1+s1]| by EUCLID:62
.= |[r3*(r1+r2),r3*(s1+s2)]|+|[s3*(r1+r2),s3*(s1+s1)]| by EUCLID:62
.= |[r3*(r1+r2)+s3*(r1+r2),r3*(s1+s2)+s3*(s1+s1)]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A16: r3 > (1/2)*0 by REAL_1:70;
0 <> width G by GOBOARD1:def 5;
then A17: 1 <= width G by RLVECT_1:99;
i < i+1 by REAL_1:69;
then A18: r1 < r2 by A1,A7,A17,GOBOARD5:4;
then A19: r1+r1 < r1+r2 by REAL_1:53;
then A20: r3*(r1+r1) < r3*(r1+r2) by A16,REAL_1:70;
0 <> len G by GOBOARD1:def 5;
then A21: 1 <= len G by RLVECT_1:99;
j < j+1 by REAL_1:69;
then A22: s1 < s2 by A1,A6,A21,GOBOARD5:5;
A23: s3 >= 0 by A3,REAL_2:121;
then A24: s3*(r1+r1) <= s3*(r1+r2) by A19,AXIOMS:25;
r3*(r1+r1)+s3*(r1+r1)
= (r3+s3)*(r1+r1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r1+r1) by XCMPLX_1:8
.= 1*(1/2)*(r1+r1) by XCMPLX_1:27
.= (1/2)*r1+(1/2)*r1 by XCMPLX_1:8
.= r1 by A11,XCMPLX_1:66;
then A25: r1 < r3*(r1+r2)+s3*(r1+r2) by A20,A24,REAL_1:67;
r1+r2 < r2+r2 by A18,REAL_1:53;
then A26: r3*(r1+r2) < r3*(r2+r2) by A16,REAL_1:70;
r1+r2 < r2+r2 by A18,REAL_1:67;
then A27: s3*(r1+r2) <= s3*(r2+r2) by A23,AXIOMS:25;
r3*(r2+r2)+s3*(r2+r2)
= (r3+s3)*(r2+r2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2 by XCMPLX_1:8
.= r2 by A12,XCMPLX_1:66;
then A28: r3*(r1+r2)+s3*(r1+r2) < r2 by A26,A27,REAL_1:67;
A29: s1+s1 < s1+s2 by A22,REAL_1:53;
then A30: r3*(s1+s1) < r3*(s1+s2) by A16,REAL_1:70;
r3*(s1+s1)+s3*(s1+s1)
= (r3+s3)*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A13,XCMPLX_1:66;
then A31: s1 < r3*(s1+s2)+s3*(s1+s1) by A30,REAL_1:67;
s1+s2 < s2+s2 by A22,REAL_1:53;
then A32: r3*(s1+s2) < r3*(s2+s2) by A16,REAL_1:70;
s1+s2 < s2+s2 by A22,REAL_1:53;
then s1+s1 < s2+s2 by A29,AXIOMS:22;
then A33: s3*(s1+s1) <= s3*(s2+s2) by A23,AXIOMS:25;
r3*(s2+s2)+s3*(s2+s2)
= (r3+s3)*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A14,XCMPLX_1:66;
then A34: r3*(s1+s2)+s3*(s1+s1) < s2 by A32,A33,REAL_1:67;
Int cell(G,i,j) =
{ |[r',s']| : r1 < r' & r' < r2 & s1 < s' & s' < s2 } by A1,Th29;
hence p in Int cell(G,i,j) by A15,A25,A28,A31,A34;
end;
hence x in Int cell(G,i,j) \/ { 1/2*(G*(i,j)+G*(i+1,j)) } by XBOOLE_0:def 2;
end;
theorem Th47:
1 <= j & j < width G implies
LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1,0]|,1/2*(G*(1,j)+G*(1,j+1))) c=
Int cell(G,0,j) \/ { 1/2*(G*(1,j)+G*(1,j+1)) }
proof
assume
A1: 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|,1/2*(G*(1,j)+G*(1,j+1)));
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|)+r*(1/2*(G*(1,j)+G*
(1,j+1)))
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(1/2*(G*(1,j)+G*(1,j+1))) by A4,EUCLID:33
.= 1*(1/2*(G*(1,j)+G*(1,j+1))) by EUCLID:31
.= 1/2*(G*(1,j)+G*(1,j+1)) by EUCLID:33;
hence p in { 1/2*(G*(1,j)+G*(1,j+1)) } by TARSKI:def 1;
case
A5: r < 1;
set r2 = G*(1,1)`1,
s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
0 <> len G by GOBOARD1:def 5;
then A7: 1 <= len G by RLVECT_1:99;
A8: G*(1,j+1) = |[G*(1,j+1)`1,G*(1,j+1)`2]| by EUCLID:57
.= |[r2,s2]| by A6,A7,GOBOARD5:3;
A9: G*(1,j) = |[G*(1,j)`1,G*(1,j)`2]| by EUCLID:57
.= |[r2,s1]| by A1,A7,GOBOARD5:3;
set r3 = (1-r)*(1/2), s3 = r*(1/2);
A10: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A11: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A12: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(1,j)+G*(1,j+1)))-(1-r)*|[1,0]|
+r*(1/2*(G*(1,j)+G*(1,j+1))) by A4,EUCLID:53
.= r3*(G*(1,j)+G*(1,j+1))-(1-r)*|[1,0]|+r*(1/2*(G*(1,j)+G*(1,j+1)))
by EUCLID:34
.= r3*(G*(1,j)+G*(1,j+1))-|[(1-r)*1,(1-r)*0]|+r*(1/2*(G*(1,j)+G*
(1,j+1)))
by EUCLID:62
.= r3*(G*(1,j)+G*(1,j+1))-|[1-r,0]|+s3*(G*(1,j)+G*
(1,j+1)) by EUCLID:34
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+s3*(G*(1,j)+G*(1,j+1))
by A8,A9,EUCLID:60
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+s3*|[r2+r2,s1+s2]| by A8,A9,EUCLID:60
.= |[r3*(r2+r2),r3*(s1+s2)]|-|[1-r,0]|+s3*|[r2+r2,s1+s2]| by EUCLID:62
.= |[r3*(r2+r2),r3*(s1+s2)]|-|[1-r,0]|+|[s3*(r2+r2),s3*(s1+s2)]|
by EUCLID:62
.= |[r3*(r2+r2)-(1-r),r3*(s1+s2)-0]|+|[s3*(r2+r2),s3*(s1+s2)]|
by EUCLID:66
.= |[r3*(r2+r2)-(1-r)+s3*(r2+r2),r3*(s1+s2)+s3*(s1+s2)]| by EUCLID:60;
A14: 1 - r > 0 by A5,SQUARE_1:11;
then A15: r3 > (1/2)*0 by REAL_1:70;
j < j+1 by REAL_1:69;
then A16: s1 < s2 by A1,A6,A7,GOBOARD5:5;
A17: s3 >= 0 by A3,REAL_2:121;
r2 < r2+(1-r) by A14,REAL_1:69;
then A18: r2-(1-r) < r2 by REAL_1:84;
A19: r3*(r2+r2)-(1-r)+s3*(r2+r2)
= r3*(r2+r2)+s3*(r2+r2)-(1-r) by XCMPLX_1:29
.= (r3+s3)*(r2+r2)-(1-r) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2)-(1-r) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2)-(1-r) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2-(1-r) by XCMPLX_1:8
.= r2-(1-r) by A10,XCMPLX_1:66;
A20: s1+s1 < s1+s2 by A16,REAL_1:53;
then A21: r3*(s1+s1) < r3*(s1+s2) by A15,REAL_1:70;
A22: s3*(s1+s1) <= s3*(s1+s2) by A17,A20,AXIOMS:25;
r3*(s1+s1)+s3*(s1+s1)
= (r3+s3)*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A11,XCMPLX_1:66;
then A23: s1 < r3*(s1+s2)+s3*(s1+s2) by A21,A22,REAL_1:67;
A24: s1+s2 < s2+s2 by A16,REAL_1:53;
then A25: r3*(s1+s2) < r3*(s2+s2) by A15,REAL_1:70;
A26: s3*(s1+s2) <= s3*(s2+s2) by A17,A24,AXIOMS:25;
r3*(s2+s2)+s3*(s2+s2)
= (r3+s3)*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A12,XCMPLX_1:66;
then A27: r3*(s1+s2)+s3*(s1+s2) < s2 by A25,A26,REAL_1:67;
Int cell(G,0,j) =
{ |[r',s']| : r' < G*(1,1)`1 & G*(1,j)`2 < s' & s' < G*(1,j+1)`2 }
by A1,Th23;
hence p in Int cell(G,0,j) by A13,A18,A19,A23,A27;
end;
hence x in Int cell(G,0,j) \/ { 1/2*(G*(1,j)+G*(1,j+1)) } by XBOOLE_0:def 2;
end;
theorem Th48:
1 <= j & j < width G implies
LSeg(1/2*(G*(len G,j)+G*(len G,j+1))
+ |[1,0]|,1/2*(G*(len G,j)+G*(len G,j+1)))
c= Int cell(G,len G,j) \/ { 1/2*(G*(len G,j)+G*(len G,j+1)) }
proof
assume
A1: 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|,
1/2*(G*(len G,j)+G*(len G,j+1)));
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|)
+r*(1/2*(G*(len G,j)+G*(len G,j+1))) by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(1/2*(G*(len G,j)+G*(len G,j+1))) by A4,EUCLID:33
.= 1*(1/2*(G*(len G,j)+G*(len G,j+1))) by EUCLID:31
.= 1/2*(G*(len G,j)+G*(len G,j+1)) by EUCLID:33;
hence p in { 1/2*(G*(len G,j)+G*(len G,j+1)) } by TARSKI:def 1;
case
A5: r < 1;
set r2 = G*(len G,1)`1, s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
0 <> len G by GOBOARD1:def 5;
then A7: 1 <= len G by RLVECT_1:99;
A8: G*(len G,j+1) = |[G*(len G,j+1)`1,G*(len G,j+1)`2]| by EUCLID:57
.= |[r2,G*(len G,j+1)`2]| by A6,A7,GOBOARD5:3
.= |[r2,s2]| by A6,A7,GOBOARD5:2;
A9: G*(len G,j) = |[G*(len G,j)`1,G*(len G,j)`2]| by EUCLID:57
.= |[r2,G*(len G,j)`2]| by A1,A7,GOBOARD5:3
.= |[r2,s1]| by A1,A7,GOBOARD5:2;
set r3 = (1-r)*(1/2), s3 = r*(1/2);
A10: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A11: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A12: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(len G,j)+G*(len G,j+1)))+(1-r)*|[1,0]|
+r*(1/2*(G*(len G,j)+G*(len G,j+1))) by A4,EUCLID:36
.= r3*(G*(len G,j)+G*(len G,j+1))+(1-r)*|[1,0]|+
r*(1/2*(G*(len G,j)+G*(len G,j+1))) by EUCLID:34
.= r3*(G*(len G,j)+G*(len G,j+1))+|[(1-r)*1,(1-r)*0]|+
r*(1/2*(G*(len G,j)+G*(len G,j+1))) by EUCLID:62
.= r3*(G*(len G,j)+G*(len G,j+1))+|[1-r,0]|+
s3*(G*(len G,j)+G*(len G,j+1)) by EUCLID:34
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+s3*(G*(len G,j)+G*(len G,j+1))
by A8,A9,EUCLID:60
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+s3*|[r2+r2,s1+s2]| by A8,A9,EUCLID:60
.= |[r3*(r2+r2),r3*(s1+s2)]|+|[1-r,0]|+s3*|[r2+r2,s1+s2]| by EUCLID:62
.= |[r3*(r2+r2),r3*(s1+s2)]|+|[1-r,0]|+|[s3*(r2+r2),s3*(s1+s2)]|
by EUCLID:62
.= |[r3*(r2+r2)+(1-r),r3*(s1+s2)+0]|+|[s3*(r2+r2),s3*(s1+s2)]|
by EUCLID:60
.= |[r3*(r2+r2)+(1-r)+s3*(r2+r2),r3*(s1+s2)+s3*(s1+s2)]| by EUCLID:60;
A14: 1 - r > 0 by A5,SQUARE_1:11;
then A15: r3 > (1/2)*0 by REAL_1:70;
j < j+1 by REAL_1:69;
then A16: s1 < s2 by A1,A6,A7,GOBOARD5:5;
A17: s3 >= 0 by A3,REAL_2:121;
A18: r2+(1-r) > r2 by A14,REAL_1:69;
A19: r3*(r2+r2)+(1-r)+s3*(r2+r2)
= r3*(r2+r2)+s3*(r2+r2)+(1-r) by XCMPLX_1:1
.= (r3+s3)*(r2+r2)+(1-r) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2)+(1-r) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2)+(1-r) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2+(1-r) by XCMPLX_1:8
.= r2+(1-r) by A10,XCMPLX_1:66;
A20: s1+s1 < s1+s2 by A16,REAL_1:53;
then A21: r3*(s1+s1) < r3*(s1+s2) by A15,REAL_1:70;
A22: s3*(s1+s1) <= s3*(s1+s2) by A17,A20,AXIOMS:25;
r3*(s1+s1)+s3*(s1+s1)
= (r3+s3)*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A11,XCMPLX_1:66;
then A23: s1 < r3*(s1+s2)+s3*(s1+s2) by A21,A22,REAL_1:67;
A24: s1+s2 < s2+s2 by A16,REAL_1:53;
then A25: r3*(s1+s2) < r3*(s2+s2) by A15,REAL_1:70;
A26: s3*(s1+s2) <= s3*(s2+s2) by A17,A24,AXIOMS:25;
r3*(s2+s2)+s3*(s2+s2)
= (r3+s3)*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A12,XCMPLX_1:66;
then A27: r3*(s1+s2)+s3*(s1+s2) < s2 by A25,A26,REAL_1:67;
Int cell(G,len G,j) = { |[r',s']| :
G*(len G,1)`1 < r' & G*(1,j)`2 < s' & s' < G*(1,j+1)`2 } by A1,Th26;
hence p in Int cell(G,len G,j) by A13,A18,A19,A23,A27;
end;
hence x in Int cell(G,len G,j) \/ { 1/2*(G*(len G,j)+G*(len G,j+1)) }
by XBOOLE_0:def
2;
end;
theorem Th49:
1 <= i & i < len G implies
LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1]|,1/2*(G*(i,1)+G*(i+1,1))) c=
Int cell(G,i,0) \/ { 1/2*(G*(i,1)+G*(i+1,1)) }
proof
assume
A1: 1 <= i & i < len G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|,1/2*(G*(i,1)+G*(i+1,1)));
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|)+r*(1/2*(G*(i,1)+G*
(i+1,1)))
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(1/2*(G*(i,1)+G*(i+1,1))) by A4,EUCLID:33
.= 1*(1/2*(G*(i,1)+G*(i+1,1))) by EUCLID:31
.= 1/2*(G*(i,1)+G*(i+1,1)) by EUCLID:33;
hence p in { 1/2*(G*(i,1)+G*(i+1,1)) } by TARSKI:def 1;
case
A5: r < 1;
set s2 = G*(1,1)`2,
r1 = G*(i,1)`1, r2 = G*(i+1,1)`1;
A6: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
0 <> width G by GOBOARD1:def 5;
then A7: 1 <= width G by RLVECT_1:99;
A8: G*(i+1,1) = |[G*(i+1,1)`1,G*(i+1,1)`2]| by EUCLID:57
.= |[r2,s2]| by A6,A7,GOBOARD5:2;
A9: G*(i,1) = |[G*(i,1)`1,G*(i,1)`2]| by EUCLID:57
.= |[r1,s2]| by A1,A7,GOBOARD5:2;
set r3 = (1-r)*(1/2), s3 = r*(1/2);
A10: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A11: (1/2)*r1 = r1/2 by XCMPLX_1:100;
A12: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(i,1)+G*(i+1,1)))-(1-r)*|[0,1]|
+r*(1/2*(G*(i,1)+G*(i+1,1))) by A4,EUCLID:53
.= r3*(G*(i,1)+G*(i+1,1))-(1-r)*|[0,1]|+r*(1/2*(G*(i,1)+G*(i+1,1)))
by EUCLID:34
.= r3*(G*(i,1)+G*(i+1,1))-|[(1-r)*0,(1-r)*1]|+r*(1/2*(G*(i,1)+G*
(i+1,1)))
by EUCLID:62
.= r3*(G*(i,1)+G*(i+1,1))-|[0,1-r]|+s3*(G*(i,1)+G*
(i+1,1)) by EUCLID:34
.= r3*|[r1+r2,s2+s2]|-|[0,1-r]|+s3*(G*(i,1)+G*(i+1,1))
by A8,A9,EUCLID:60
.= r3*|[r1+r2,s2+s2]|-|[0,1-r]|+s3*|[r1+r2,s2+s2]| by A8,A9,EUCLID:60
.= |[r3*(r1+r2),r3*(s2+s2)]|-|[0,1-r]|+s3*|[r1+r2,s2+s2]| by EUCLID:62
.= |[r3*(r1+r2),r3*(s2+s2)]|-|[0,1-r]|+|[s3*(r1+r2),s3*(s2+s2)]|
by EUCLID:62
.= |[r3*(r1+r2)-0,r3*(s2+s2)-(1-r)]|+|[s3*(r1+r2),s3*(s2+s2)]|
by EUCLID:66
.= |[r3*(r1+r2)+s3*(r1+r2),r3*(s2+s2)-(1-r)+s3*(s2+s2)]| by EUCLID:60;
A14: 1 - r > 0 by A5,SQUARE_1:11;
then A15: r3 > (1/2)*0 by REAL_1:70;
i < i+1 by REAL_1:69;
then A16: r1 < r2 by A1,A6,A7,GOBOARD5:4;
A17: s3 >= 0 by A3,REAL_2:121;
s2 < s2+(1-r) by A14,REAL_1:69;
then A18: s2-(1-r) < s2 by REAL_1:84;
A19: r3*(s2+s2)-(1-r)+s3*(s2+s2)
= r3*(s2+s2)+s3*(s2+s2)-(1-r) by XCMPLX_1:29
.= (r3+s3)*(s2+s2)-(1-r) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2)-(1-r) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2)-(1-r) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2-(1-r) by XCMPLX_1:8
.= s2-(1-r) by A10,XCMPLX_1:66;
A20: r1+r1 < r1+r2 by A16,REAL_1:53;
then A21: r3*(r1+r1) < r3*(r1+r2) by A15,REAL_1:70;
A22: s3*(r1+r1) <= s3*(r1+r2) by A17,A20,AXIOMS:25;
r3*(r1+r1)+s3*(r1+r1)
= (r3+s3)*(r1+r1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r1+r1) by XCMPLX_1:8
.= 1*(1/2)*(r1+r1) by XCMPLX_1:27
.= (1/2)*r1+(1/2)*r1 by XCMPLX_1:8
.= r1 by A11,XCMPLX_1:66;
then A23: r1 < r3*(r1+r2)+s3*(r1+r2) by A21,A22,REAL_1:67;
A24: r1+r2 < r2+r2 by A16,REAL_1:53;
then A25: r3*(r1+r2) < r3*(r2+r2) by A15,REAL_1:70;
A26: s3*(r1+r2) <= s3*(r2+r2) by A17,A24,AXIOMS:25;
r3*(r2+r2)+s3*(r2+r2)
= (r3+s3)*(r2+r2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2 by XCMPLX_1:8
.= r2 by A12,XCMPLX_1:66;
then A27: r3*(r1+r2)+s3*(r1+r2) < r2 by A25,A26,REAL_1:67;
Int cell(G,i,0) =
{ |[r',s']| : G*(i,1)`1 < r' & r' < G*(i+1,1)`1 & s' < G*(1,1)`2 }
by A1,Th27;
hence p in Int cell(G,i,0) by A13,A18,A19,A23,A27;
end;
hence x in Int cell(G,i,0) \/ { 1/2*(G*(i,1)+G*(i+1,1)) } by XBOOLE_0:def 2;
end;
theorem Th50:
1 <= i & i < len G implies
LSeg(1/2*(G*(i,width G)+G*(i+1,width G))+ |[0,1]|,
1/2*(G*(i,width G)+G*(i+1,width G)))
c= Int cell(G,i,width G) \/ { 1/2*(G*(i,width G)+G*(i+1,width G)) }
proof
assume
A1: 1 <= i & i < len G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]|,
1/2*(G*(i,width G)+G*(i+1,width G)));
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]|)
+r*(1/2*(G*(i,width G)+G*(i+1,width G))) by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(1/2*(G*(i,width G)+G*(i+1,width G))) by A4,EUCLID:
33
.= 1*(1/2*(G*(i,width G)+G*(i+1,width G))) by EUCLID:31
.= 1/2*(G*(i,width G)+G*(i+1,width G)) by EUCLID:33;
hence p in { 1/2*(G*(i,width G)+G*(i+1,width G)) } by TARSKI:def 1;
case
A5: r < 1;
set s2 = G*(1,width G)`2, r1 = G*(i,1)`1, r2 = G*(i+1,1)`1;
A6: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
0 <> width G by GOBOARD1:def 5;
then A7: 1 <= width G by RLVECT_1:99;
A8: G*(i+1,width G) = |[G*(i+1,width G)`1,G*(i+1,width G)`2]| by EUCLID:57
.= |[G*(i+1,width G)`1,s2]| by A6,A7,GOBOARD5:2
.= |[r2,s2]| by A6,A7,GOBOARD5:3;
A9: G*(i,width G) = |[G*(i,width G)`1,G*(i,width G)`2]| by EUCLID:57
.= |[G*(i,width G)`1,s2]| by A1,A7,GOBOARD5:2
.= |[r1,s2]| by A1,A7,GOBOARD5:3;
set r3 = (1-r)*(1/2), s3 = r*(1/2);
A10: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A11: (1/2)*r1 = r1/2 by XCMPLX_1:100;
A12: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(i,width G)+G*(i+1,width G)))+(1-r)*|[0,1]|
+r*(1/2*(G*(i,width G)+G*
(i+1,width G))) by A4,EUCLID:36
.= r3*(G*(i,width G)+G*(i+1,width G))+(1-r)*|[0,1]|+
r*(1/2*(G*(i,width G)+G*(i+1,width G))) by EUCLID:34
.= r3*(G*(i,width G)+G*(i+1,width G))+|[(1-r)*0,(1-r)*1]|+
r*(1/2*(G*(i,width G)+G*(i+1,width G))) by EUCLID:62
.= r3*(G*(i,width G)+G*(i+1,width G))+|[0,1-r]|+
s3*(G*(i,width G)+G*(i+1,width G)) by EUCLID:34
.= r3*|[r1+r2,s2+s2]|+|[0,1-r]|+s3*(G*(i,width G)+G*(i+1,width G))
by A8,A9,EUCLID:60
.= r3*|[r1+r2,s2+s2]|+|[0,1-r]|+s3*|[r1+r2,s2+s2]| by A8,A9,EUCLID:60
.= |[r3*(r1+r2),r3*(s2+s2)]|+|[0,1-r]|+s3*|[r1+r2,s2+s2]| by EUCLID:62
.= |[r3*(r1+r2),r3*(s2+s2)]|+|[0,1-r]|+|[s3*(r1+r2),s3*(s2+s2)]|
by EUCLID:62
.= |[r3*(r1+r2)+0,r3*(s2+s2)+(1-r)]|+|[s3*(r1+r2),s3*(s2+s2)]|
by EUCLID:60
.= |[r3*(r1+r2)+s3*(r1+r2),r3*(s2+s2)+(1-r)+s3*(s2+s2)]| by EUCLID:60;
A14: 1 - r > 0 by A5,SQUARE_1:11;
then A15: r3 > (1/2)*0 by REAL_1:70;
i < i+1 by REAL_1:69;
then A16: r1 < r2 by A1,A6,A7,GOBOARD5:4;
A17: s3 >= 0 by A3,REAL_2:121;
A18: s2+(1-r) > s2 by A14,REAL_1:69;
A19: r3*(s2+s2)+(1-r)+s3*(s2+s2)
= r3*(s2+s2)+s3*(s2+s2)+(1-r) by XCMPLX_1:1
.= (r3+s3)*(s2+s2)+(1-r) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2)+(1-r) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2)+(1-r) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2+(1-r) by XCMPLX_1:8
.= s2+(1-r) by A10,XCMPLX_1:66;
A20: r1+r1 < r1+r2 by A16,REAL_1:53;
then A21: r3*(r1+r1) < r3*(r1+r2) by A15,REAL_1:70;
A22: s3*(r1+r1) <= s3*(r1+r2) by A17,A20,AXIOMS:25;
r3*(r1+r1)+s3*(r1+r1)
= (r3+s3)*(r1+r1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r1+r1) by XCMPLX_1:8
.= 1*(1/2)*(r1+r1) by XCMPLX_1:27
.= (1/2)*r1+(1/2)*r1 by XCMPLX_1:8
.= r1 by A11,XCMPLX_1:66;
then A23: r1 < r3*(r1+r2)+s3*(r1+r2) by A21,A22,REAL_1:67;
A24: r1+r2 < r2+r2 by A16,REAL_1:53;
then A25: r3*(r1+r2) < r3*(r2+r2) by A15,REAL_1:70;
A26: s3*(r1+r2) <= s3*(r2+r2) by A17,A24,AXIOMS:25;
r3*(r2+r2)+s3*(r2+r2)
= (r3+s3)*(r2+r2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2 by XCMPLX_1:8
.= r2 by A12,XCMPLX_1:66;
then A27: r3*(r1+r2)+s3*(r1+r2) < r2 by A25,A26,REAL_1:67;
Int cell(G,i,width G) = { |[r',s']| :
G*(i,1)`1 < r' & r' < G*(i+1,1)`1 & G*
(1,width G)`2 < s' } by A1,Th28;
hence p in Int cell(G,i,width G) by A13,A18,A19,A23,A27;
end;
hence x in Int cell(G,i,width G) \/ { 1/2*(G*(i,width G)+G*(i+1,width G)) }
by XBOOLE_0:def
2;
end;
theorem Th51:
1 <= j & j < width G implies
LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1,0]|,G*(1,j) - |[1,0]|) c=
Int cell(G,0,j) \/ { G*(1,j) - |[1,0]| }
proof
assume
A1: 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|,G*(1,j) - |[1,0]|);
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|)+r*(G*(1,j) - |[1,0]|)
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(G*(1,j) - |[1,0]|) by A4,EUCLID:33
.= 1*(G*(1,j) - |[1,0]|) by EUCLID:31
.= (G*(1,j) - |[1,0]|) by EUCLID:33;
hence p in { G*(1,j) - |[1,0]| } by TARSKI:def 1;
case
A5: r < 1;
set r2 = G*(1,1)`1,
s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
0 <> len G by GOBOARD1:def 5;
then A7: 1 <= len G by RLVECT_1:99;
A8: G*(1,j+1) = |[G*(1,j+1)`1,G*(1,j+1)`2]| by EUCLID:57
.= |[r2,s2]| by A6,A7,GOBOARD5:3;
A9: G*(1,j) = |[G*(1,j)`1,G*(1,j)`2]| by EUCLID:57
.= |[r2,s1]| by A1,A7,GOBOARD5:3;
set r3 = (1-r)*(1/2);
A10: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A11: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A12: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(1,j)+G*(1,j+1)))-(1-r)*|[1,0]|
+r*(G*(1,j) - |[1,0]|) by A4,EUCLID:53
.= r3*(G*(1,j)+G*(1,j+1))-(1-r)*|[1,0]|+r*(G*
(1,j) - |[1,0]|) by EUCLID:34
.= r3*(G*(1,j)+G*(1,j+1))-|[(1-r)*1,(1-r)*0]|+r*(G*(1,j) - |[1,0]|)
by EUCLID:62
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+r*(|[r2,s1]| - |[1,0]|)
by A8,A9,EUCLID:60
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+(r*|[r2,s1]| - r*|[1,0]|) by EUCLID:53
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+(|[r*r2,r*s1]| - r*|[1,0]|) by EUCLID:62
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+(|[r*r2,r*s1]| - |[r*1,r*0]|)
by EUCLID:62
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+|[r*r2-r,r*s1-0]| by EUCLID:66
.= |[r3*(r2+r2),r3*(s1+s2)]|-|[1-r,0]|+|[r*r2-r,r*s1-0]| by EUCLID:62
.= |[r3*(r2+r2)-(1-r),r3*(s1+s2)-0]|+|[r*r2-r,r*s1-0]| by EUCLID:66
.= |[r3*(r2+r2)-(1-r)+(r*r2-r),r3*(s1+s2)+r*s1]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A14: r3 > (1/2)*0 by REAL_1:70;
j < j+1 by REAL_1:69;
then A15: s1 < s2 by A1,A6,A7,GOBOARD5:5;
r2 < r2+1 by REAL_1:69;
then A16: r2-1 < r2 by REAL_1:84;
A17: r3*(r2+r2)-(1-r)+(r*r2-r)
= (1-r)*((1/2)*(r2+r2))-(1-r)+(r*r2-r) by XCMPLX_1:4
.= (1-r)*((1/2)*r2+(1/2)*r2)-(1-r)+(r*r2-r) by XCMPLX_1:8
.= (1-r)*r2-(1-r)+(r*r2-r) by A10,XCMPLX_1:66
.= (1-r)*r2-(1-r)+r*r2-r by XCMPLX_1:29
.= (1-r)*r2+r*r2-(1-r)-r by XCMPLX_1:29
.= ((1-r)+r)*r2-(1-r)-r by XCMPLX_1:8
.= 1*r2-(1-r)-r by XCMPLX_1:27
.= r2-((1-r)+r) by XCMPLX_1:36
.= r2-1 by XCMPLX_1:27;
s1+s1 < s1+s2 by A15,REAL_1:53;
then A18: r3*(s1+s1) < r3*(s1+s2) by A14,REAL_1:70;
r3*(s1+s1)+r*s1
= r3*(s1+s1)+r*(1/2*s1+1/2*s1) by A11,XCMPLX_1:66
.= r3*(s1+s1)+r*((1/2)*(s1+s1)) by XCMPLX_1:8
.= r3*(s1+s1)+(r*(1/2))*(s1+s1) by XCMPLX_1:4
.= (r3+r*(1/2))*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A11,XCMPLX_1:66;
then A19: s1 < r3*(s1+s2)+r*s1 by A18,REAL_1:53;
s1+s2 < s2+s2 by A15,REAL_1:53;
then A20: r3*(s1+s2) < r3*(s2+s2) by A14,REAL_1:70;
A21: r*s1 <= r*s2 by A3,A15,AXIOMS:25;
r3*(s2+s2)+r*s2
= r3*(s2+s2)+r*(1/2*s2+1/2*s2) by A12,XCMPLX_1:66
.= r3*(s2+s2)+r*((1/2)*(s2+s2)) by XCMPLX_1:8
.= r3*(s2+s2)+(r*(1/2))*(s2+s2) by XCMPLX_1:4
.= (r3+r*(1/2))*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A12,XCMPLX_1:66;
then A22: r3*(s1+s2)+r*s1 < s2 by A20,A21,REAL_1:67;
Int cell(G,0,j) =
{ |[r',s']| : r' < G*(1,1)`1 & G*(1,j)`2 < s' & s' < G*(1,j+1)`2 }
by A1,Th23;
hence p in Int cell(G,0,j) by A13,A16,A17,A19,A22;
end;
hence x in Int cell(G,0,j) \/ { G*(1,j) - |[1,0]| } by XBOOLE_0:def 2;
end;
theorem Th52:
1 <= j & j < width G implies
LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1,0]|,G*(1,j+1) - |[1,0]|) c=
Int cell(G,0,j) \/ { G*(1,j+1) - |[1,0]| }
proof
assume
A1: 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|,G*(1,j+1) - |[1,0]|);
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|)+r*(G*(1,j+1) - |[1,0]|)
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(G*(1,j+1) - |[1,0]|) by A4,EUCLID:33
.= 1*(G*(1,j+1) - |[1,0]|) by EUCLID:31
.= (G*(1,j+1) - |[1,0]|) by EUCLID:33;
hence p in { G*(1,j+1) - |[1,0]| } by TARSKI:def 1;
case
A5: r < 1;
set r2 = G*(1,1)`1,
s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
0 <> len G by GOBOARD1:def 5;
then A7: 1 <= len G by RLVECT_1:99;
A8: G*(1,j+1) = |[G*(1,j+1)`1,G*(1,j+1)`2]| by EUCLID:57
.= |[r2,s2]| by A6,A7,GOBOARD5:3;
A9: G*(1,j) = |[G*(1,j)`1,G*(1,j)`2]| by EUCLID:57
.= |[r2,s1]| by A1,A7,GOBOARD5:3;
set r3 = (1-r)*(1/2);
A10: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A11: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A12: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(1,j)+G*(1,j+1)))-(1-r)*|[1,0]|
+r*(G*(1,j+1) - |[1,0]|) by A4,EUCLID:53
.= r3*(G*(1,j)+G*(1,j+1))-(1-r)*|[1,0]|+r*(G*(1,j+1) - |[1,0]|)
by EUCLID:34
.= r3*(G*(1,j)+G*(1,j+1))-|[(1-r)*1,(1-r)*0]|+r*(G*(1,j+1) - |[1,0]|)
by EUCLID:62
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+r*(|[r2,s2]| - |[1,0]|)
by A8,A9,EUCLID:60
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+(r*|[r2,s2]| - r*|[1,0]|) by EUCLID:53
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+(|[r*r2,r*s2]| - r*|[1,0]|) by EUCLID:62
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+(|[r*r2,r*s2]| - |[r*1,r*0]|)
by EUCLID:62
.= r3*|[r2+r2,s1+s2]|-|[1-r,0]|+|[r*r2-r,r*s2-0]| by EUCLID:66
.= |[r3*(r2+r2),r3*(s1+s2)]|-|[1-r,0]|+|[r*r2-r,r*s2-0]| by EUCLID:62
.= |[r3*(r2+r2)-(1-r),r3*(s1+s2)-0]|+|[r*r2-r,r*s2-0]| by EUCLID:66
.= |[r3*(r2+r2)-(1-r)+(r*r2-r),r3*(s1+s2)+r*s2]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A14: r3 > (1/2)*0 by REAL_1:70;
j < j+1 by REAL_1:69;
then A15: s1 < s2 by A1,A6,A7,GOBOARD5:5;
r2 < r2+1 by REAL_1:69;
then A16: r2-1 < r2 by REAL_1:84;
A17: r3*(r2+r2)-(1-r)+(r*r2-r)
= (1-r)*((1/2)*(r2+r2))-(1-r)+(r*r2-r) by XCMPLX_1:4
.= (1-r)*((1/2)*r2+(1/2)*r2)-(1-r)+(r*r2-r) by XCMPLX_1:8
.= (1-r)*r2-(1-r)+(r*r2-r) by A10,XCMPLX_1:66
.= (1-r)*r2-(1-r)+r*r2-r by XCMPLX_1:29
.= (1-r)*r2+r*r2-(1-r)-r by XCMPLX_1:29
.= ((1-r)+r)*r2-(1-r)-r by XCMPLX_1:8
.= 1*r2-(1-r)-r by XCMPLX_1:27
.= r2-((1-r)+r) by XCMPLX_1:36
.= r2-1 by XCMPLX_1:27;
s1+s1 < s1+s2 by A15,REAL_1:53;
then A18: r3*(s1+s1) < r3*(s1+s2) by A14,REAL_1:70;
A19: r*s1 <= r*s2 by A3,A15,AXIOMS:25;
r3*(s1+s1)+r*s1
= r3*(s1+s1)+r*(1/2*s1+1/2*s1) by A11,XCMPLX_1:66
.= r3*(s1+s1)+r*((1/2)*(s1+s1)) by XCMPLX_1:8
.= r3*(s1+s1)+(r*(1/2))*(s1+s1) by XCMPLX_1:4
.= (r3+r*(1/2))*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A11,XCMPLX_1:66;
then A20: s1 < r3*(s1+s2)+r*s2 by A18,A19,REAL_1:67;
s1+s2 < s2+s2 by A15,REAL_1:53;
then A21: r3*(s1+s2) < r3*(s2+s2) by A14,REAL_1:70;
r3*(s2+s2)+r*s2
= r3*(s2+s2)+r*(1/2*s2+1/2*s2) by A12,XCMPLX_1:66
.= r3*(s2+s2)+r*((1/2)*(s2+s2)) by XCMPLX_1:8
.= r3*(s2+s2)+(r*(1/2))*(s2+s2) by XCMPLX_1:4
.= (r3+r*(1/2))*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A12,XCMPLX_1:66;
then A22: r3*(s1+s2)+r*s2 < s2 by A21,REAL_1:67;
Int cell(G,0,j) =
{ |[r',s']| : r' < G*(1,1)`1 & G*(1,j)`2 < s' & s' < G*(1,j+1)`2 }
by A1,Th23;
hence p in Int cell(G,0,j) by A13,A16,A17,A20,A22;
end;
hence x in Int cell(G,0,j) \/ { G*(1,j+1) - |[1,0]| } by XBOOLE_0:def 2;
end;
theorem Th53:
1 <= j & j < width G implies
LSeg(1/2*(G*(len G,j)+G*(len G,j+1)) + |[1,0]|,G*(len G,j) + |[1,0]|) c=
Int cell(G,len G,j) \/ { G*(len G,j) + |[1,0]| }
proof
assume
A1: 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|,G*
(len G,j) + |[1,0]|);
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|)+
r*(G*(len G,j) + |[1,0]|) by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(G*(len G,j) + |[1,0]|) by A4,EUCLID:33
.= 1*(G*(len G,j) + |[1,0]|) by EUCLID:31
.= (G*(len G,j) + |[1,0]|) by EUCLID:33;
hence p in { G*(len G,j) + |[1,0]| } by TARSKI:def 1;
case
A5: r < 1;
set r2 = G*(len G,1)`1, s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
0 <> len G by GOBOARD1:def 5;
then A7: 1 <= len G by RLVECT_1:99;
A8: G*(len G,j+1) = |[G*(len G,j+1)`1,G*(len G,j+1)`2]| by EUCLID:57
.= |[r2,G*(len G,j+1)`2]| by A6,A7,GOBOARD5:3
.= |[r2,s2]| by A6,A7,GOBOARD5:2;
A9: G*(len G,j) = |[G*(len G,j)`1,G*(len G,j)`2]| by EUCLID:57
.= |[r2,G*(len G,j)`2]| by A1,A7,GOBOARD5:3
.= |[r2,s1]| by A1,A7,GOBOARD5:2;
set r3 = (1-r)*(1/2);
A10: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A11: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A12: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(len G,j)+G*(len G,j+1)))+(1-r)*|[1,0]|
+r*(G*(len G,j) + |[1,0]|) by A4,EUCLID:36
.= r3*(G*(len G,j)+G*(len G,j+1))+(1-r)*|[1,0]|+r*(G*
(len G,j) + |[1,0]|)
by EUCLID:34
.= r3*(G*(len G,j)+G*(len G,j+1))+|[(1-r)*1,(1-r)*0]|+
r*(G*(len G,j) + |[1,0]|) by EUCLID:62
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+r*(|[r2,s1]| + |[1,0]|)
by A8,A9,EUCLID:60
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+(r*|[r2,s1]| + r*|[1,0]|) by EUCLID:36
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+(|[r*r2,r*s1]| + r*|[1,0]|) by EUCLID:62
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+(|[r*r2,r*s1]| + |[r*1,r*0]|)
by EUCLID:62
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+|[r*r2+r,r*s1+0]| by EUCLID:60
.= |[r3*(r2+r2),r3*(s1+s2)]|+|[1-r,0]|+|[r*r2+r,r*s1+0]| by EUCLID:62
.= |[r3*(r2+r2)+(1-r),r3*(s1+s2)+0]|+|[r*r2+r,r*s1+0]| by EUCLID:60
.= |[r3*(r2+r2)+(1-r)+(r*r2+r),r3*(s1+s2)+r*s1]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A14: r3 > (1/2)*0 by REAL_1:70;
j < j+1 by REAL_1:69;
then A15: s1 < s2 by A1,A6,A7,GOBOARD5:5;
A16: r2 < r2+1 by REAL_1:69;
A17: r3*(r2+r2)+(1-r)+(r*r2+r)
= (1-r)*((1/2)*(r2+r2))+(1-r)+(r*r2+r) by XCMPLX_1:4
.= (1-r)*((1/2)*r2+(1/2)*r2)+(1-r)+(r*r2+r) by XCMPLX_1:8
.= (1-r)*r2+(1-r)+(r*r2+r) by A10,XCMPLX_1:66
.= (1-r)*r2+(1-r)+r*r2+r by XCMPLX_1:1
.= (1-r)*r2+r*r2+(1-r)+r by XCMPLX_1:1
.= ((1-r)+r)*r2+(1-r)+r by XCMPLX_1:8
.= 1*r2+(1-r)+r by XCMPLX_1:27
.= r2+((1-r)+r) by XCMPLX_1:1
.= r2+1 by XCMPLX_1:27;
s1+s1 < s1+s2 by A15,REAL_1:53;
then A18: r3*(s1+s1) < r3*(s1+s2) by A14,REAL_1:70;
r3*(s1+s1)+r*s1
= r3*(s1+s1)+r*(1/2*s1+1/2*s1) by A11,XCMPLX_1:66
.= r3*(s1+s1)+r*((1/2)*(s1+s1)) by XCMPLX_1:8
.= r3*(s1+s1)+(r*(1/2))*(s1+s1) by XCMPLX_1:4
.= (r3+r*(1/2))*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A11,XCMPLX_1:66;
then A19: s1 < r3*(s1+s2)+r*s1 by A18,REAL_1:53;
s1+s2 < s2+s2 by A15,REAL_1:53;
then A20: r3*(s1+s2) < r3*(s2+s2) by A14,REAL_1:70;
A21: r*s1 <= r*s2 by A3,A15,AXIOMS:25;
r3*(s2+s2)+r*s2
= r3*(s2+s2)+r*(1/2*s2+1/2*s2) by A12,XCMPLX_1:66
.= r3*(s2+s2)+r*((1/2)*(s2+s2)) by XCMPLX_1:8
.= r3*(s2+s2)+(r*(1/2))*(s2+s2) by XCMPLX_1:4
.= (r3+r*(1/2))*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A12,XCMPLX_1:66;
then A22: r3*(s1+s2)+r*s1 < s2 by A20,A21,REAL_1:67;
Int cell(G,len G,j) =
{ |[r',s']| : G*(len G,1)`1 < r' & G*(1,j)`2 < s' & s' < G*(1,j+1)`2 }
by A1,Th26;
hence p in Int cell(G,len G,j) by A13,A16,A17,A19,A22;
end;
hence x in Int cell(G,len G,j) \/ { G*(len G,j) + |[1,0]| } by XBOOLE_0:def 2
;
end;
theorem Th54:
1 <= j & j < width G implies
LSeg(1/2*(G*(len G,j)+G*(len G,j+1)) + |[1,0]|,G*(len G,j+1) + |[1,0]|) c=
Int cell(G,len G,j) \/ { G*(len G,j+1) + |[1,0]| }
proof
assume
A1: 1 <= j & j < width G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|,G*
(len G,j+1) + |[1,0]|);
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|)+
r*(G*(len G,j+1) + |[1,0]|) by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(G*(len G,j+1) + |[1,0]|) by A4,EUCLID:33
.= 1*(G*(len G,j+1) + |[1,0]|) by EUCLID:31
.= (G*(len G,j+1) + |[1,0]|) by EUCLID:33;
hence p in { G*(len G,j+1) + |[1,0]| } by TARSKI:def 1;
case
A5: r < 1;
set r2 = G*(len G,1)`1, s1 = G*(1,j)`2, s2 = G*(1,j+1)`2;
A6: 1 <= j+1 & j+1 <= width G by A1,NAT_1:38;
0 <> len G by GOBOARD1:def 5;
then A7: 1 <= len G by RLVECT_1:99;
A8: G*(len G,j+1) = |[G*(len G,j+1)`1,G*(len G,j+1)`2]| by EUCLID:57
.= |[r2,G*(len G,j+1)`2]| by A6,A7,GOBOARD5:3
.= |[r2,s2]| by A6,A7,GOBOARD5:2;
A9: G*(len G,j) = |[G*(len G,j)`1,G*(len G,j)`2]| by EUCLID:57
.= |[r2,G*(len G,j)`2]| by A1,A7,GOBOARD5:3
.= |[r2,s1]| by A1,A7,GOBOARD5:2;
set r3 = (1-r)*(1/2);
A10: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A11: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A12: (1/2)*s2 = s2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(len G,j)+G*(len G,j+1)))+(1-r)*|[1,0]|
+r*(G*(len G,j+1) + |[1,0]|) by A4,EUCLID:36
.= r3*(G*(len G,j)+G*(len G,j+1))+(1-r)*|[1,0]|+
r*(G*(len G,j+1) + |[1,0]|) by EUCLID:34
.= r3*(G*(len G,j)+G*(len G,j+1))+|[(1-r)*1,(1-r)*0]|+
r*(G*(len G,j+1) + |[1,0]|) by EUCLID:62
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+r*(|[r2,s2]| + |[1,0]|)
by A8,A9,EUCLID:60
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+(r*|[r2,s2]| + r*|[1,0]|) by EUCLID:36
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+(|[r*r2,r*s2]| + r*|[1,0]|) by EUCLID:62
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+(|[r*r2,r*s2]| + |[r*1,r*0]|)
by EUCLID:62
.= r3*|[r2+r2,s1+s2]|+|[1-r,0]|+|[r*r2+r,r*s2+0]| by EUCLID:60
.= |[r3*(r2+r2),r3*(s1+s2)]|+|[1-r,0]|+|[r*r2+r,r*s2+0]| by EUCLID:62
.= |[r3*(r2+r2)+(1-r),r3*(s1+s2)+0]|+|[r*r2+r,r*s2+0]| by EUCLID:60
.= |[r3*(r2+r2)+(1-r)+(r*r2+r),r3*(s1+s2)+r*s2]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A14: r3 > (1/2)*0 by REAL_1:70;
j < j+1 by REAL_1:69;
then A15: s1 < s2 by A1,A6,A7,GOBOARD5:5;
A16: r2+1 > r2 by REAL_1:69;
A17: r3*(r2+r2)+(1-r)+(r*r2+r)
= (1-r)*((1/2)*(r2+r2))+(1-r)+(r*r2+r) by XCMPLX_1:4
.= (1-r)*((1/2)*r2+(1/2)*r2)+(1-r)+(r*r2+r) by XCMPLX_1:8
.= (1-r)*r2+(1-r)+(r*r2+r) by A10,XCMPLX_1:66
.= (1-r)*r2+(1-r)+r*r2+r by XCMPLX_1:1
.= (1-r)*r2+r*r2+(1-r)+r by XCMPLX_1:1
.= ((1-r)+r)*r2+(1-r)+r by XCMPLX_1:8
.= 1*r2+(1-r)+r by XCMPLX_1:27
.= r2+((1-r)+r) by XCMPLX_1:1
.= r2+1 by XCMPLX_1:27;
s1+s1 < s1+s2 by A15,REAL_1:53;
then A18: r3*(s1+s1) < r3*(s1+s2) by A14,REAL_1:70;
A19: r*s1 <= r*s2 by A3,A15,AXIOMS:25;
r3*(s1+s1)+r*s1
= r3*(s1+s1)+r*(1/2*s1+1/2*s1) by A11,XCMPLX_1:66
.= r3*(s1+s1)+r*((1/2)*(s1+s1)) by XCMPLX_1:8
.= r3*(s1+s1)+(r*(1/2))*(s1+s1) by XCMPLX_1:4
.= (r3+r*(1/2))*(s1+s1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s1+s1) by XCMPLX_1:8
.= 1*(1/2)*(s1+s1) by XCMPLX_1:27
.= (1/2)*s1+(1/2)*s1 by XCMPLX_1:8
.= s1 by A11,XCMPLX_1:66;
then A20: s1 < r3*(s1+s2)+r*s2 by A18,A19,REAL_1:67;
s1+s2 < s2+s2 by A15,REAL_1:53;
then A21: r3*(s1+s2) < r3*(s2+s2) by A14,REAL_1:70;
r3*(s2+s2)+r*s2
= r3*(s2+s2)+r*(1/2*s2+1/2*s2) by A12,XCMPLX_1:66
.= r3*(s2+s2)+r*((1/2)*(s2+s2)) by XCMPLX_1:8
.= r3*(s2+s2)+(r*(1/2))*(s2+s2) by XCMPLX_1:4
.= (r3+r*(1/2))*(s2+s2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(s2+s2) by XCMPLX_1:8
.= 1*(1/2)*(s2+s2) by XCMPLX_1:27
.= (1/2)*s2+(1/2)*s2 by XCMPLX_1:8
.= s2 by A12,XCMPLX_1:66;
then A22: r3*(s1+s2)+r*s2 < s2 by A21,REAL_1:67;
Int cell(G,len G,j) =
{ |[r',s']| : G*(len G,1)`1 < r' & G*(1,j)`2 < s' & s' < G*(1,j+1)`2 }
by A1,Th26;
hence p in Int cell(G,len G,j) by A13,A16,A17,A20,A22;
end;
hence x in Int cell(G,len G,j) \/ { G*(len G,j+1) + |[1,0]| } by XBOOLE_0:def
2;
end;
theorem Th55:
1 <= i & i < len G implies
LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1]|,G*(i,1) - |[0,1]|) c=
Int cell(G,i,0) \/ { G*(i,1) - |[0,1]| }
proof
assume
A1: 1 <= i & i < len G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|,G*(i,1) - |[0,1]|);
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|)+r*(G*(i,1) - |[0,1]|)
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(G*(i,1) - |[0,1]|) by A4,EUCLID:33
.= 1*(G*(i,1) - |[0,1]|) by EUCLID:31
.= (G*(i,1) - |[0,1]|) by EUCLID:33;
hence p in { G*(i,1) - |[0,1]| } by TARSKI:def 1;
case
A5: r < 1;
set s1 = G*(1,1)`2,
r1 = G*(i,1)`1, r2 = G*(i+1,1)`1;
A6: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
0 <> width G by GOBOARD1:def 5;
then A7: 1 <= width G by RLVECT_1:99;
A8: G*(i+1,1) = |[G*(i+1,1)`1,G*(i+1,1)`2]| by EUCLID:57
.= |[r2,s1]| by A6,A7,GOBOARD5:2;
A9: G*(i,1) = |[G*(i,1)`1,G*(i,1)`2]| by EUCLID:57
.= |[r1,s1]| by A1,A7,GOBOARD5:2;
set r3 = (1-r)*(1/2);
A10: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A11: (1/2)*r1 = r1/2 by XCMPLX_1:100;
A12: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(i,1)+G*(i+1,1)))-(1-r)*|[0,1]|
+r*(G*(i,1) - |[0,1]|) by A4,EUCLID:53
.= r3*(G*(i,1)+G*(i+1,1))-(1-r)*|[0,1]|+r*(G*
(i,1) - |[0,1]|) by EUCLID:34
.= r3*(G*(i,1)+G*(i+1,1))-|[(1-r)*0,(1-r)*1]|+r*(G*(i,1) - |[0,1]|)
by EUCLID:62
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+r*(|[r1,s1]| - |[0,1]|)
by A8,A9,EUCLID:60
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+(r*|[r1,s1]| - r*|[0,1]|) by EUCLID:53
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+(|[r*r1,r*s1]| - r*|[0,1]|) by EUCLID:62
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+(|[r*r1,r*s1]| - |[r*0,r*1]|)
by EUCLID:62
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+|[r*r1-0,r*s1-r]| by EUCLID:66
.= |[r3*(r1+r2),r3*(s1+s1)]|-|[0,1-r]|+|[r*r1-0,r*s1-r]| by EUCLID:62
.= |[r3*(r1+r2)-0,r3*(s1+s1)-(1-r)]|+|[r*r1-0,r*s1-r]| by EUCLID:66
.= |[r3*(r1+r2)+r*r1,r3*(s1+s1)-(1-r)+(r*s1-r)]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A14: r3 > (1/2)*0 by REAL_1:70;
i < i+1 by REAL_1:69;
then A15: r1 < r2 by A1,A6,A7,GOBOARD5:4;
s1 < s1+1 by REAL_1:69;
then A16: s1-1 < s1 by REAL_1:84;
A17: r3*(s1+s1)-(1-r)+(r*s1-r)
= (1-r)*((1/2)*(s1+s1))-(1-r)+(r*s1-r) by XCMPLX_1:4
.= (1-r)*((1/2)*s1+(1/2)*s1)-(1-r)+(r*s1-r) by XCMPLX_1:8
.= (1-r)*s1-(1-r)+(r*s1-r) by A10,XCMPLX_1:66
.= (1-r)*s1-(1-r)+r*s1-r by XCMPLX_1:29
.= (1-r)*s1+r*s1-(1-r)-r by XCMPLX_1:29
.= ((1-r)+r)*s1-(1-r)-r by XCMPLX_1:8
.= 1*s1-(1-r)-r by XCMPLX_1:27
.= s1-((1-r)+r) by XCMPLX_1:36
.= s1-1 by XCMPLX_1:27;
r1+r1 < r1+r2 by A15,REAL_1:53;
then A18: r3*(r1+r1) < r3*(r1+r2) by A14,REAL_1:70;
r3*(r1+r1)+r*r1
= r3*(r1+r1)+r*(1/2*r1+1/2*r1) by A11,XCMPLX_1:66
.= r3*(r1+r1)+r*((1/2)*(r1+r1)) by XCMPLX_1:8
.= r3*(r1+r1)+(r*(1/2))*(r1+r1) by XCMPLX_1:4
.= (r3+r*(1/2))*(r1+r1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r1+r1) by XCMPLX_1:8
.= 1*(1/2)*(r1+r1) by XCMPLX_1:27
.= (1/2)*r1+(1/2)*r1 by XCMPLX_1:8
.= r1 by A11,XCMPLX_1:66;
then A19: r1 < r3*(r1+r2)+r*r1 by A18,REAL_1:53;
r1+r2 < r2+r2 by A15,REAL_1:53;
then A20: r3*(r1+r2) < r3*(r2+r2) by A14,REAL_1:70;
A21: r*r1 <= r*r2 by A3,A15,AXIOMS:25;
r3*(r2+r2)+r*r2
= r3*(r2+r2)+r*(1/2*r2+1/2*r2) by A12,XCMPLX_1:66
.= r3*(r2+r2)+r*((1/2)*(r2+r2)) by XCMPLX_1:8
.= r3*(r2+r2)+(r*(1/2))*(r2+r2) by XCMPLX_1:4
.= (r3+r*(1/2))*(r2+r2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2 by XCMPLX_1:8
.= r2 by A12,XCMPLX_1:66;
then A22: r3*(r1+r2)+r*r1 < r2 by A20,A21,REAL_1:67;
Int cell(G,i,0) =
{ |[r',s']| : G*(i,1)`1 < r' & r' < G*(i+1,1)`1 & s' < G*(1,1)`2 }
by A1,Th27;
hence p in Int cell(G,i,0) by A13,A16,A17,A19,A22;
end;
hence x in Int cell(G,i,0) \/ { G*(i,1) - |[0,1]| } by XBOOLE_0:def 2;
end;
theorem Th56:
1 <= i & i < len G implies
LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1]|,G*(i+1,1) - |[0,1]|) c=
Int cell(G,i,0) \/ { G*(i+1,1) - |[0,1]| }
proof
assume
A1: 1 <= i & i < len G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|,G*(i+1,1) - |[0,1]|);
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|)+r*(G*(i+1,1) - |[0,1]|)
by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(G*(i+1,1) - |[0,1]|) by A4,EUCLID:33
.= 1*(G*(i+1,1) - |[0,1]|) by EUCLID:31
.= (G*(i+1,1) - |[0,1]|) by EUCLID:33;
hence p in { G*(i+1,1) - |[0,1]| } by TARSKI:def 1;
case
A5: r < 1;
set s1 = G*(1,1)`2,
r1 = G*(i,1)`1, r2 = G*(i+1,1)`1;
A6: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
0 <> width G by GOBOARD1:def 5;
then A7: 1 <= width G by RLVECT_1:99;
A8: G*(i+1,1) = |[G*(i+1,1)`1,G*(i+1,1)`2]| by EUCLID:57
.= |[r2,s1]| by A6,A7,GOBOARD5:2;
A9: G*(i,1) = |[G*(i,1)`1,G*(i,1)`2]| by EUCLID:57
.= |[r1,s1]| by A1,A7,GOBOARD5:2;
set r3 = (1-r)*(1/2);
A10: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A11: (1/2)*r1 = r1/2 by XCMPLX_1:100;
A12: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(i,1)+G*(i+1,1)))-(1-r)*|[0,1]|
+r*(G*(i+1,1) - |[0,1]|) by A4,EUCLID:53
.= r3*(G*(i,1)+G*(i+1,1))-(1-r)*|[0,1]|+r*(G*(i+1,1) - |[0,1]|)
by EUCLID:34
.= r3*(G*(i,1)+G*(i+1,1))-|[(1-r)*0,(1-r)*1]|+r*(G*(i+1,1) - |[0,1]|)
by EUCLID:62
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+r*(|[r2,s1]| - |[0,1]|)
by A8,A9,EUCLID:60
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+(r*|[r2,s1]| - r*|[0,1]|) by EUCLID:53
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+(|[r*r2,r*s1]| - r*|[0,1]|) by EUCLID:62
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+(|[r*r2,r*s1]| - |[r*0,r*1]|)
by EUCLID:62
.= r3*|[r1+r2,s1+s1]|-|[0,1-r]|+|[r*r2-0,r*s1-r]| by EUCLID:66
.= |[r3*(r1+r2),r3*(s1+s1)]|-|[0,1-r]|+|[r*r2-0,r*s1-r]| by EUCLID:62
.= |[r3*(r1+r2)-0,r3*(s1+s1)-(1-r)]|+|[r*r2-0,r*s1-r]| by EUCLID:66
.= |[r3*(r1+r2)+r*r2,r3*(s1+s1)-(1-r)+(r*s1-r)]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A14: r3 > (1/2)*0 by REAL_1:70;
i < i+1 by REAL_1:69;
then A15: r1 < r2 by A1,A6,A7,GOBOARD5:4;
s1 < s1+1 by REAL_1:69;
then A16: s1-1 < s1 by REAL_1:84;
A17: r3*(s1+s1)-(1-r)+(r*s1-r)
= (1-r)*((1/2)*(s1+s1))-(1-r)+(r*s1-r) by XCMPLX_1:4
.= (1-r)*((1/2)*s1+(1/2)*s1)-(1-r)+(r*s1-r) by XCMPLX_1:8
.= (1-r)*s1-(1-r)+(r*s1-r) by A10,XCMPLX_1:66
.= (1-r)*s1-(1-r)+r*s1-r by XCMPLX_1:29
.= (1-r)*s1+r*s1-(1-r)-r by XCMPLX_1:29
.= ((1-r)+r)*s1-(1-r)-r by XCMPLX_1:8
.= 1*s1-(1-r)-r by XCMPLX_1:27
.= s1-((1-r)+r) by XCMPLX_1:36
.= s1-1 by XCMPLX_1:27;
r1+r1 < r1+r2 by A15,REAL_1:53;
then A18: r3*(r1+r1) < r3*(r1+r2) by A14,REAL_1:70;
A19: r*r1 <= r*r2 by A3,A15,AXIOMS:25;
r3*(r1+r1)+r*r1
= r3*(r1+r1)+r*(1/2*r1+1/2*r1) by A11,XCMPLX_1:66
.= r3*(r1+r1)+r*((1/2)*(r1+r1)) by XCMPLX_1:8
.= r3*(r1+r1)+(r*(1/2))*(r1+r1) by XCMPLX_1:4
.= (r3+r*(1/2))*(r1+r1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r1+r1) by XCMPLX_1:8
.= 1*(1/2)*(r1+r1) by XCMPLX_1:27
.= (1/2)*r1+(1/2)*r1 by XCMPLX_1:8
.= r1 by A11,XCMPLX_1:66;
then A20: r1 < r3*(r1+r2)+r*r2 by A18,A19,REAL_1:67;
r1+r2 < r2+r2 by A15,REAL_1:53;
then A21: r3*(r1+r2) < r3*(r2+r2) by A14,REAL_1:70;
r3*(r2+r2)+r*r2
= r3*(r2+r2)+r*(1/2*r2+1/2*r2) by A12,XCMPLX_1:66
.= r3*(r2+r2)+r*((1/2)*(r2+r2)) by XCMPLX_1:8
.= r3*(r2+r2)+(r*(1/2))*(r2+r2) by XCMPLX_1:4
.= (r3+r*(1/2))*(r2+r2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2 by XCMPLX_1:8
.= r2 by A12,XCMPLX_1:66;
then A22: r3*(r1+r2)+r*r2 < r2 by A21,REAL_1:67;
Int cell(G,i,0) =
{ |[r',s']| : G*(i,1)`1 < r' & r' < G*(i+1,1)`1 & s' < G*(1,1)`2 }
by A1,Th27;
hence p in Int cell(G,i,0) by A13,A16,A17,A20,A22;
end;
hence x in Int cell(G,i,0) \/ { G*(i+1,1) - |[0,1]| } by XBOOLE_0:def 2;
end;
theorem Th57:
1 <= i & i < len G implies
LSeg(1/2*(G*(i,width G)+G*(i+1,width G)) + |[0,1]|,G*
(i,width G) + |[0,1]|) c=
Int cell(G,i,width G) \/ { G*(i,width G) + |[0,1]| }
proof
assume
A1: 1 <= i & i < len G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]|,
G*(i,width G) + |[0,1]|);
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]|)+
r*(G*(i,width G) + |[0,1]|) by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(G*(i,width G) + |[0,1]|) by A4,EUCLID:33
.= 1*(G*(i,width G) + |[0,1]|) by EUCLID:31
.= (G*(i,width G) + |[0,1]|) by EUCLID:33;
hence p in { G*(i,width G) + |[0,1]| } by TARSKI:def 1;
case
A5: r < 1;
set s1 = G*(1,width G)`2, r1 = G*(i,1)`1, r2 = G*(i+1,1)`1;
A6: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
0 <> width G by GOBOARD1:def 5;
then A7: 1 <= width G by RLVECT_1:99;
A8: G*(i+1,width G) = |[G*(i+1,width G)`1,G*(i+1,width G)`2]| by EUCLID:57
.= |[G*(i+1,width G)`1,s1]| by A6,A7,GOBOARD5:2
.= |[r2,s1]| by A6,A7,GOBOARD5:3;
A9: G*(i,width G) = |[G*(i,width G)`1,G*(i,width G)`2]| by EUCLID:57
.= |[G*(i,width G)`1,s1]| by A1,A7,GOBOARD5:2
.= |[r1,s1]| by A1,A7,GOBOARD5:3;
set r3 = (1-r)*(1/2);
A10: (1/2)*s1 = s1/2 by XCMPLX_1:100;
A11: (1/2)*r1 = r1/2 by XCMPLX_1:100;
A12: (1/2)*r2 = r2/2 by XCMPLX_1:100;
A13: p = (1-r)*(1/2*(G*(i,width G)+G*(i+1,width G)))+(1-r)*|[0,1]|
+r*(G*(i,width G) + |[0,1]|) by A4,EUCLID:36
.= r3*(G*(i,width G)+G*(i+1,width G))+(1-r)*|[0,1]|+
r*(G*(i,width G) + |[0,1]|) by EUCLID:34
.= r3*(G*(i,width G)+G*(i+1,width G))+|[(1-r)*0,(1-r)*1]|+
r*(G*(i,width G) + |[0,1]|) by EUCLID:62
.= r3*|[r1+r2,s1+s1]|+|[0,1-r]|+r*(|[r1,s1]| + |[0,1]|)
by A8,A9,EUCLID:60
.= r3*|[r1+r2,s1+s1]|+|[0,1-r]|+(r*|[r1,s1]| + r*|[0,1]|) by EUCLID:36
.= r3*|[r1+r2,s1+s1]|+|[0,1-r]|+(|[r*r1,r*s1]| + r*|[0,1]|) by EUCLID:62
.= r3*|[r1+r2,s1+s1]|+|[0,1-r]|+(|[r*r1,r*s1]| + |[r*0,r*1]|)
by EUCLID:62
.= r3*|[r1+r2,s1+s1]|+|[0,1-r]|+|[r*r1+0,r*s1+r]| by EUCLID:60
.= |[r3*(r1+r2),r3*(s1+s1)]|+|[0,1-r]|+|[r*r1+0,r*s1+r]| by EUCLID:62
.= |[r3*(r1+r2)+0,r3*(s1+s1)+(1-r)]|+|[r*r1+0,r*s1+r]| by EUCLID:60
.= |[r3*(r1+r2)+r*r1,r3*(s1+s1)+(1-r)+(r*s1+r)]| by EUCLID:60;
1 - r > 0 by A5,SQUARE_1:11;
then A14: r3 > (1/2)*0 by REAL_1:70;
i < i+1 by REAL_1:69;
then A15: r1 < r2 by A1,A6,A7,GOBOARD5:4;
A16: s1 < s1+1 by REAL_1:69;
A17: r3*(s1+s1)+(1-r)+(r*s1+r)
= (1-r)*((1/2)*(s1+s1))+(1-r)+(r*s1+r) by XCMPLX_1:4
.= (1-r)*((1/2)*s1+(1/2)*s1)+(1-r)+(r*s1+r) by XCMPLX_1:8
.= (1-r)*s1+(1-r)+(r*s1+r) by A10,XCMPLX_1:66
.= (1-r)*s1+(1-r)+r*s1+r by XCMPLX_1:1
.= (1-r)*s1+r*s1+(1-r)+r by XCMPLX_1:1
.= ((1-r)+r)*s1+(1-r)+r by XCMPLX_1:8
.= 1*s1+(1-r)+r by XCMPLX_1:27
.= s1+((1-r)+r) by XCMPLX_1:1
.= s1+1 by XCMPLX_1:27;
r1+r1 < r1+r2 by A15,REAL_1:53;
then A18: r3*(r1+r1) < r3*(r1+r2) by A14,REAL_1:70;
r3*(r1+r1)+r*r1
= r3*(r1+r1)+r*(1/2*r1+1/2*r1) by A11,XCMPLX_1:66
.= r3*(r1+r1)+r*((1/2)*(r1+r1)) by XCMPLX_1:8
.= r3*(r1+r1)+(r*(1/2))*(r1+r1) by XCMPLX_1:4
.= (r3+r*(1/2))*(r1+r1) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r1+r1) by XCMPLX_1:8
.= 1*(1/2)*(r1+r1) by XCMPLX_1:27
.= (1/2)*r1+(1/2)*r1 by XCMPLX_1:8
.= r1 by A11,XCMPLX_1:66;
then A19: r1 < r3*(r1+r2)+r*r1 by A18,REAL_1:53;
r1+r2 < r2+r2 by A15,REAL_1:53;
then A20: r3*(r1+r2) < r3*(r2+r2) by A14,REAL_1:70;
A21: r*r1 <= r*r2 by A3,A15,AXIOMS:25;
r3*(r2+r2)+r*r2
= r3*(r2+r2)+r*(1/2*r2+1/2*r2) by A12,XCMPLX_1:66
.= r3*(r2+r2)+r*((1/2)*(r2+r2)) by XCMPLX_1:8
.= r3*(r2+r2)+(r*(1/2))*(r2+r2) by XCMPLX_1:4
.= (r3+r*(1/2))*(r2+r2) by XCMPLX_1:8
.= ((1-r)+r)*(1/2)*(r2+r2) by XCMPLX_1:8
.= 1*(1/2)*(r2+r2) by XCMPLX_1:27
.= (1/2)*r2+(1/2)*r2 by XCMPLX_1:8
.= r2 by A12,XCMPLX_1:66;
then A22: r3*(r1+r2)+r*r1 < r2 by A20,A21,REAL_1:67;
Int cell(G,i,width G) =
{ |[r',s']| : G*(i,1)`1 < r' & r' < G*(i+1,1)`1 & G*(1,width G)`2 < s' }
by A1,Th28;
hence p in Int cell(G,i,width G) by A13,A16,A17,A19,A22;
end;
hence x in Int cell(G,i,width G) \/
{ G*(i,width G) + |[0,1]| } by XBOOLE_0:def 2;
end;
theorem Th58:
1 <= i & i < len G implies
LSeg(1/2*(G*(i,width G)+G*(i+1,width G)) + |[0,1]|,G*
(i+1,width G) + |[0,1]|)
c= Int cell(G,i,width G) \/ { G*(i+1,width G) + |[0,1]| }
proof
assume
A1: 1 <= i & i < len G;
let x be set;
assume
A2: x in LSeg(1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]|,
G*(i+1,width G) + |[0,1]|);
then reconsider p = x as Point of TOP-REAL 2;
consider r such that
A3: 0<=r & r<=1 and
A4: p = (1-r)*(1/2*(G*(i,width G)+G*(i+1,width G))+|[0,1]|)+
r*(G*(i+1,width G) + |[0,1]|) by A2,SPPOL_1:21;
now per cases by A3,AXIOMS:21;
case r = 1;
then p = 0.REAL 2 + 1*(G*(i+1,width G) + |[0,1]|) by A4,EUCLID:33
.= 1*(G*(i+1,width G) + |[0,1]|) by EUCLID:31
.= (G*(i+1,width G) + |[0,1]|) by EUCLID:33;
hence p in { G*(i+1,width G) + |[0,1]| } by TARSKI:def 1;
case
A5: r < 1;
set s1 = G*(1,width G)`2, r1 = G*(i,1)`1, r2 = G*(i+1,1)`1;
A6: 1 <= i+1 & i+1 <= len G by A1,NAT_1:38;
0 <> width G by GOBOARD1:def 5;
then A7: 1 <= width G by RLVECT_1:99;
A8: G*(i+1,width G) = |[G*(i+1,