:: Classical and Non--classical Pasch Configurations in Ordered Affine Planes
:: by Henryk Oryszczyszyn, Krzysztof Pra\.zmowski and
:: Ma{\l}gorzata Pra\.zmowska
::
:: Received May 16, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ANALOAF, SUBSET_1, DIRAF, PARSP_1, VECTSP_1, PASCH, PENCIL_1;
notations STRUCT_0, ANALOAF, DIRAF;
constructors DIRAF;
registrations STRUCT_0;
theorems DIRAF, ANALOAF;
begin
reserve OAS for OAffinSpace;
reserve a,a9,b,b9,c,c9,d,d1,d2,e1,e2,e3,e4,e5,e6,p,p9,q,r,x,y,z for Element of
OAS;
definition
let OAS;
attr OAS is satisfying_Int_Par_Pasch means
for a,b,c,d,p st not p,b,c are_collinear &
Mid b,p,a & p,c,d are_collinear & b,c '||' d,a holds Mid c,p,d;
end;
definition
let OAS;
attr OAS is satisfying_Ext_Par_Pasch means
for a,b,c,d,p st Mid p,b,c & p,a,d are_collinear & a,b '||' c,d &
not p,a,b are_collinear holds Mid p,a,d;
end;
definition
let OAS;
attr OAS is satisfying_Gen_Par_Pasch means
for a,b,c,a9,b9,c9 st not a,b,a9 are_collinear & a,a9 '||' b,b9 &
a,a9 '||' c,c9 & Mid a,b,c & a9,b9,c9 are_collinear holds Mid a9,b9,c9;
end;
definition
let OAS;
attr OAS is satisfying_Ext_Bet_Pasch means
for a,b,c,d,x,y st Mid a,b,d &
Mid b,x,c & not a,b,c are_collinear holds ex y st Mid a,y,c & Mid y,x,d;
end;
definition
let OAS;
attr OAS is satisfying_Int_Bet_Pasch means
for a,b,c,d,x,y st Mid a,b,d &
Mid a,x,c & not a,b,c are_collinear holds ex y st Mid b,y,c & Mid x,y,d;
end;
definition
let OAS;
attr OAS is Fanoian means
for a,b,c,d st a,b // c,d & a,c // b,d & not a,b,c are_collinear
ex x st Mid a,x,d & Mid b,x,c;
end;
theorem Th1:
b,p // p,c & p<>c & b<>p implies ex d st a,p // p,d & a,b '||' c,
d & c <>d & p<>d
proof
assume that
A1: b,p // p,c and
A2: p<>c and
A3: b<>p;
A4: now
A5: now
Mid b,p,c by A1,DIRAF:def 3;
then b,p,c are_collinear by DIRAF:28;
then
A6: p,c,b are_collinear by DIRAF:30;
assume p,a // p,b;
then
A7: a,p // b,p by DIRAF:2;
then a,p // p,c by A1,A3,DIRAF:3;
then Mid a,p,c by DIRAF:def 3;
then a,p,c are_collinear by DIRAF:28;
then p,c,a are_collinear by DIRAF:30;
then
A8: p,c '||' a,b by A6,DIRAF:34;
A9: p,c // b,p by A1,DIRAF:2;
A10: p,c,c are_collinear by DIRAF:31;
consider d such that
A11: Mid p,c,d and
A12: c <>d by DIRAF:13;
A13: p<>d by A11,A12,DIRAF:8;
p,c // c,d by A11,DIRAF:def 3;
then p,c // p,d by ANALOAF:def 5;
then
A14: b,p // p,d by A2,A9,ANALOAF:def 5;
p,c,d are_collinear by A11,DIRAF:28;
then p,c '||' c,d by A10,DIRAF:34;
then a,b '||' c,d by A2,A8,DIRAF:23;
hence thesis by A3,A7,A12,A13,A14,DIRAF:3;
end;
A15: now
assume p,a // b,p;
then
A16: a,p // p,b by DIRAF:2;
then Mid a,p,b by DIRAF:def 3;
then a,p,b are_collinear by DIRAF:28;
then
A17: p,b,a are_collinear by DIRAF:30;
Mid b,p,c by A1,DIRAF:def 3;
then b,p,c are_collinear by DIRAF:28;
then
A18: p,b,c are_collinear by DIRAF:30;
A19: a,b,b are_collinear by DIRAF:31;
A20: b <> c by A1,A2,ANALOAF:def 5;
p,b,b are_collinear by DIRAF:31;
then a,b,c are_collinear by A3,A17,A18,DIRAF:32;
hence thesis by A3,A16,A20,A19,DIRAF:34;
end;
assume a,b,p are_collinear;
then p,a,b are_collinear by DIRAF:30;
then p,a '||' p,b by DIRAF:def 5;
hence thesis by A5,A15,DIRAF:def 4;
end;
now
consider d such that
A21: a,p // p,d and
A22: a,b // c,d by A1,A3,ANALOAF:def 5;
assume
A23: not a,b,p are_collinear;
A24: now
assume d=p;
then p,c // b,a by A22,DIRAF:2;
then b,p // b,a by A1,A2,DIRAF:3;
then b,p '||' b,a by DIRAF:def 4;
then b,p,a are_collinear by DIRAF:def 5;
hence contradiction by A23,DIRAF:30;
end;
A25: now
assume d=c;
then p,d // b,p by A1,DIRAF:2;
then a,p // b,p by A21,A24,DIRAF:3;
then p,a // p,b by DIRAF:2;
then p,a '||' p,b by DIRAF:def 4;
then p,a,b are_collinear by DIRAF:def 5;
hence contradiction by A23,DIRAF:30;
end;
a,b '||' c,d by A22,DIRAF:def 4;
hence thesis by A21,A24,A25;
end;
hence thesis by A4;
end;
theorem Th2:
p,b // p,c & p<>c & b<>p implies ex d st p,a // p,d & a,b '||' c, d & c <>d
proof
assume that
A1: p,b // p,c and
A2: p<>c and
A3: b<>p;
consider q such that
A4: Mid b,p,q and
A5: p<>q by DIRAF:13;
A6: b,p // p,q by A4,DIRAF:def 3;
then consider r such that
A7: a,p // p,r and
A8: a,b '||' q,r and
A9: q<>r and
A10: r<>p by A3,A5,Th1;
b,p // c,p by A1,DIRAF:2;
then p,q // c,p by A3,A6,ANALOAF:def 5;
then q,p // p,c by DIRAF:2;
then consider d such that
A11: r,p // p,d and
A12: r,q '||' c,d and
A13: c <>d and
d<>p by A2,A5,Th1;
p,r // d,p by A11,DIRAF:2;
then a,p // d,p by A7,A10,DIRAF:3;
then
A14: p,a // p,d by DIRAF:2;
q,r '||' c,d by A12,DIRAF:22;
then a,b '||' c,d by A8,A9,DIRAF:23;
hence thesis by A13,A14;
end;
theorem
p,b '||' p,c & p<>b implies ex d st p,a '||' p,d & a,b '||' c,d
proof
assume that
A1: p,b '||' p,c and
A2: p<>b;
A3: now
assume
A4: p<>c;
A5: now
assume p,b // c,p;
then b,p // p,c by DIRAF:2;
then consider d such that
A6: a,p // p,d and
A7: a,b '||' c,d and
c <>d and
d<>p by A2,A4,Th1;
p,a // d,p by A6,DIRAF:2;
then p,a '||' p,d by DIRAF:def 4;
hence thesis by A7;
end;
now
assume p,b // p,c;
then consider d such that
A8: p,a // p,d and
A9: a,b '||' c,d and
c <>d by A2,A4,Th2;
p,a '||' p,d by A8,DIRAF:def 4;
hence thesis by A9;
end;
hence thesis by A1,A5,DIRAF:def 4;
end;
now
A10: a,b '||' p,p by DIRAF:20;
A11: p,a '||' p,p by DIRAF:20;
assume p=c;
hence thesis by A11,A10;
end;
hence thesis by A3;
end;
theorem Th4:
not p,a,b are_collinear & p,b,c are_collinear & p,a,d1 are_collinear &
p,a,d2 are_collinear & a,b '||' c,d1 & a,b '||' c,d2 implies d1=d2
proof
assume that
A1: not p,a,b are_collinear and
A2: p,b,c are_collinear and
A3: p,a,d1 are_collinear and
A4: p,a,d2 are_collinear and
A5: a,b '||' c,d1 and
A6: a,b '||' c,d2;
A7: p<>a by A1,DIRAF:31;
A8: a<>b by A1,DIRAF:31;
A9: now
p,a,a are_collinear by DIRAF:31;
then
A10: d1,d2,a are_collinear by A3,A4,A7,DIRAF:32;
A11: d1,d2,d1 are_collinear by DIRAF:31;
A12: p,c,b are_collinear by A2,DIRAF:30;
A13: d1,d2,d2 are_collinear by DIRAF:31;
A14: p,a,p are_collinear by DIRAF:31;
then
A15: d1,d2,p are_collinear by A3,A4,A7,DIRAF:32;
c,d1 '||' c,d2 by A5,A6,A8,DIRAF:23;
then
A16: c,d1,d2 are_collinear by DIRAF:def 5;
then
A17: d1,d2,c are_collinear by DIRAF:30;
assume
A18: p<>c;
assume
A19: d1<>d2;
d1,d2,p are_collinear by A3,A4,A7,A14,DIRAF:32;
then
A20: p,c,d1 are_collinear by A19,A17,A11,DIRAF:32;
d1,d2,c are_collinear by A16,DIRAF:30;
then p,c,d2 are_collinear by A19,A15,A13,DIRAF:32;
then d1,d2,b are_collinear by A18,A20,A12,DIRAF:32;
hence contradiction by A1,A19,A15,A10,DIRAF:32;
end;
A21: p,d2,a are_collinear by A4,DIRAF:30;
A22: p,d1,a are_collinear by A3,DIRAF:30;
now
A23: p,d2,p are_collinear by DIRAF:31;
assume
A24: c =p;
then
A25: p,d2 '||' a,b by A6,DIRAF:22;
A26: now
assume
A27: p<>d2;
then p,d2,b are_collinear by A21,A25,DIRAF:33;
hence contradiction by A1,A21,A23,A27,DIRAF:32;
end;
A28: p,d1,p are_collinear by DIRAF:31;
A29: p,d1 '||' a,b by A5,A24,DIRAF:22;
now
assume
A30: p<>d1;
then p,d1,b are_collinear by A22,A29,DIRAF:33;
hence contradiction by A1,A22,A28,A30,DIRAF:32;
end;
hence thesis by A26;
end;
hence thesis by A9;
end;
theorem Th5:
not a,b,c are_collinear & a,b '||' c,d1 & a,b '||' c,d2 & a,c '||' b,d1 &
a,c '||' b,d2 implies d1=d2
proof
assume that
A1: not a,b,c are_collinear and
A2: a,b '||' c,d1 and
A3: a,b '||' c,d2 and
A4: a,c '||' b,d1 and
A5: a,c '||' b,d2;
assume
A6: d1<>d2;
a<>c by A1,DIRAF:31;
then b,d1 '||' b,d2 by A4,A5,DIRAF:23;
then b,d1,d2 are_collinear by DIRAF:def 5;
then
A7: d1,d2,b are_collinear by DIRAF:30;
A8: now
assume c =d1;
then c,a '||' c,b by A4,DIRAF:22;
then c,a,b are_collinear by DIRAF:def 5;
hence contradiction by A1,DIRAF:30;
end;
A9: d1,d2,d1 are_collinear by DIRAF:31;
a<>b by A1,DIRAF:31;
then c,d1 '||' c,d2 by A2,A3,DIRAF:23;
then
A10: c,d1,d2 are_collinear by DIRAF:def 5;
then
A11: d1,d2,c are_collinear by DIRAF:30;
d1,d2,c are_collinear by A10,DIRAF:30;
then d1,d2 '||' c,d1 by A9,DIRAF:34;
then d1,d2 '||' a,b or c =d1 by A2,DIRAF:23;
then d1,d2 '||' b,a by A8,DIRAF:22;
then d1,d2,a are_collinear by A6,A7,DIRAF:33;
hence contradiction by A1,A6,A11,A7,DIRAF:32;
end;
theorem Th6:
not p,b,c are_collinear & Mid b,p,a & p,c,d are_collinear & b,c '||' d,a
implies Mid c,p,d
proof
assume that
A1: not p,b,c are_collinear and
A2: Mid b,p,a and
A3: p,c,d are_collinear and
A4: b,c '||' d,a;
A5: p,d,c are_collinear by A3,DIRAF:30;
b,p,a are_collinear by A2,DIRAF:28;
then
A6: p,b,a are_collinear by DIRAF:30;
p,c '||' p,d by A3,DIRAF:def 5;
then
A7: p,c // p,d or p,c // d,p by DIRAF:def 4;
assume
A8: not Mid c,p,d;
then
A9: d<>p by DIRAF:10;
A10: now
assume p,c // d,p;
then c,p // p,d by DIRAF:2;
hence contradiction by A8,DIRAF:def 3;
end;
p<>c by A8,DIRAF:10;
then consider q such that
A11: p,b // p,q and
A12: b,c '||' d,q and
d<>q by A9,A7,A10,Th2;
A13: p,d,p are_collinear by DIRAF:31;
p,b '||' p,q by A11,DIRAF:def 4;
then p,b,q are_collinear by DIRAF:def 5;
then a=q by A1,A3,A4,A12,A6,Th4;
then b,p // p,q by A2,DIRAF:def 3;
then p,q // b,p by DIRAF:2;
then p,b // b,p or p=q by A11,DIRAF:3;
then p=b or p=q by ANALOAF:def 5;
then p,d '||' c,b by A1,A12,DIRAF:22,31;
then p,d,b are_collinear by A9,A5,DIRAF:33;
hence contradiction by A1,A9,A5,A13,DIRAF:32;
end;
theorem
OAS is satisfying_Int_Par_Pasch
by Th6;
theorem Th8:
Mid p,b,c & p,a,d are_collinear & a,b '||' c,d & not p,a,b are_collinear
implies Mid p,a,d
proof
assume that
A1: Mid p,b,c and
A2: p,a,d are_collinear and
A3: a,b '||' c,d and
A4: not p,a,b are_collinear;
A5: now
d,a,p are_collinear by A2,DIRAF:30;
then d,a '||' d,p by DIRAF:def 5;
then
A6: a,d '||' d,p by DIRAF:22;
assume
A7: b<>c;
A8: b<>a by A4,DIRAF:31;
A9: not d,b,a are_collinear
proof
assume d,b,a are_collinear;
then
A10: a,b,d are_collinear by DIRAF:30;
a,b '||' d,c by A3,DIRAF:22;
then a,b,c are_collinear by A8,A10,DIRAF:33;
then
A11: b,c,a are_collinear by DIRAF:30;
p,b,c are_collinear by A1,DIRAF:28;
then
A12: b,c,p are_collinear by DIRAF:30;
b,c,b are_collinear by DIRAF:31;
hence contradiction by A4,A7,A11,A12,DIRAF:32;
end;
then d<>a by DIRAF:31;
then consider q such that
A13: b,d '||' d,q and
A14: b,a '||' p,q by A6,DIRAF:27;
A15: p,b,c are_collinear by A1,DIRAF:28;
A16: p<>c by A1,A7,DIRAF:8;
A17: not b,c,d are_collinear
proof
A18: p,c,c are_collinear by DIRAF:31;
p,b,c are_collinear by A1,DIRAF:28;
then
A19: p,c,b are_collinear by DIRAF:30;
assume
A20: b,c,d are_collinear;
A21: b,c,b are_collinear by DIRAF:31;
A22: now
assume a,b '||' c,b;
then b,c '||' b,a by DIRAF:22;
then b,c,a are_collinear by DIRAF:def 5;
hence contradiction by A7,A9,A20,A21,DIRAF:32;
end;
c,d,b are_collinear by A20,DIRAF:30;
then c,d '||' c,b by DIRAF:def 5;
then p,a,c are_collinear by A2,A3,A22,DIRAF:23;
then p,c,a are_collinear by DIRAF:30;
then b,c,a are_collinear by A16,A19,A18,DIRAF:32;
hence contradiction by A7,A9,A20,A21,DIRAF:32;
end;
a,b '||' q,p by A14,DIRAF:22;
then
A23: c,d '||' q,p by A3,A8,DIRAF:23;
d,b '||' d,q by A13,DIRAF:22;
then d,b,q are_collinear by DIRAF:def 5;
then
A24: b,d,q are_collinear by DIRAF:30;
A25: d<>p
proof
A26: p,c,p are_collinear by DIRAF:31;
p,b,c are_collinear by A1,DIRAF:28;
then
A27: p,c,b are_collinear by DIRAF:30;
assume d=p;
then p,c '||' b,a by A3,DIRAF:22;
then p,c,a are_collinear by A16,A27,DIRAF:33;
hence contradiction by A4,A16,A27,A26,DIRAF:32;
end;
A28: not d,p,q are_collinear
proof
A29: now
assume p=q;
then d,b '||' d,p by A13,DIRAF:22;
then d,b,p are_collinear by DIRAF:def 5;
then
A30: d,p,b are_collinear by DIRAF:30;
A31: d,p,d are_collinear by DIRAF:31;
d,p,a are_collinear by A2,DIRAF:30;
hence contradiction by A9,A25,A31,A30,DIRAF:32;
end;
A32: p,q,p are_collinear by DIRAF:31;
A33: d,p,p are_collinear by DIRAF:31;
assume
A34: d,p,q are_collinear;
d,p,a are_collinear by A2,DIRAF:30;
then
A35: p,q,a are_collinear by A25,A34,A33,DIRAF:32;
p,q '||' a,b by A14,DIRAF:22;
then p,q,b are_collinear by A35,A29,DIRAF:33;
hence contradiction by A4,A35,A29,A32,DIRAF:32;
end;
Mid c,b,p by A1,DIRAF:9;
then
A36: Mid d,b,q by A17,A24,A23,Th6;
A37: now
d,b '||' d,q by A13,DIRAF:22;
then d,b,q are_collinear by DIRAF:def 5;
then
A38: d,q,b are_collinear by DIRAF:30;
assume
A39: Mid p,d,a;
p,q '||' b,a by A14,DIRAF:22;
then Mid q,d,b by A28,A39,A38,Th6;
then Mid b,d,q by DIRAF:9;
then b=d by A36,DIRAF:14;
hence contradiction by A9,DIRAF:31;
end;
assume not Mid p,a,d;
then Mid a,p,d by A2,A37,DIRAF:29;
then Mid b,p,c by A3,A4,A15,Th6;
then p=b by A1,DIRAF:14;
hence contradiction by A4,DIRAF:31;
end;
now
A40: a,b '||' b,a by DIRAF:19;
A41: p,a,a are_collinear by DIRAF:31;
A42: p,b,b are_collinear by DIRAF:31;
assume b=c;
then a=d by A2,A3,A4,A42,A41,A40,Th4;
hence thesis by DIRAF:10;
end;
hence thesis by A5;
end;
theorem
OAS is satisfying_Ext_Par_Pasch
by Th8;
theorem Th10:
not a,b,a9 are_collinear & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c &
a9,b9,c9 are_collinear implies Mid a9,b9,c9
proof
assume that
A1: not a,b,a9 are_collinear and
A2: a,a9 '||' b,b9 and
A3: a,a9 '||' c,c9 and
A4: Mid a,b,c and
A5: a9,b9,c9 are_collinear;
A6: a,b,c are_collinear by A4,DIRAF:28;
A7: b9,c9,a9 are_collinear by A5,DIRAF:30;
A8: c9,b9,a9 are_collinear by A5,DIRAF:30;
A9: a<>a9 by A1,DIRAF:31;
then
A10: b,b9 '||' c,c9 by A2,A3,DIRAF:23;
A11: a<>b by A1,DIRAF:31;
then
A12: a<>c by A4,DIRAF:8;
A13: now
assume that
A14: b9<>c9 and
a9<>b9 and
A15: b<>b9;
A16: not b,b9,a9 are_collinear
proof
A17: b,b9,b are_collinear by DIRAF:31;
assume
A18: b,b9,a9 are_collinear;
b,b9 '||' a9,a by A2,DIRAF:22;
then b,b9,a are_collinear by A15,A18,DIRAF:33;
hence contradiction by A1,A15,A18,A17,DIRAF:32;
end;
A19: now
a,b '||' a,c by A6,DIRAF:def 5;
then c,a '||' a,b by DIRAF:22;
then consider x such that
A20: c9,a '||' a,x and
A21: c9,c '||' b,x by A12,DIRAF:27;
a,c9 '||' a,x by A20,DIRAF:22;
then
A22: a,c9,x are_collinear by DIRAF:def 5;
assume
A23: c <>c9;
A24: x<>b
proof
assume x=b;
then
A25: a,b,c9 are_collinear by A22,DIRAF:30;
a,b,b are_collinear by DIRAF:31;
then
A26: c,c9,b are_collinear by A11,A6,A25,DIRAF:32;
a,b,a are_collinear by DIRAF:31;
then c,c9,a are_collinear by A11,A6,A25,DIRAF:32;
then c,c9 '||' a,b by A26,DIRAF:34;
then b,b9 '||' a,b by A10,A23,DIRAF:23;
then a,a9 '||' a,b by A2,A15,DIRAF:23;
then a,a9,b are_collinear by DIRAF:def 5;
hence contradiction by A1,DIRAF:30;
end;
c,c9 '||' b,x by A21,DIRAF:22;
then b,b9 '||' b,x by A10,A23,DIRAF:23;
then
A27: b,b9,x are_collinear by DIRAF:def 5;
then b,x,b9 are_collinear by DIRAF:30;
then b,x '||' b,b9 by DIRAF:def 5;
then b,x '||' c,c9 by A10,A15,DIRAF:23;
then
A28: x,b '||' c,c9 by DIRAF:22;
A29: x<>b9
proof
assume x=b9;
then
A30: b9,c9,a are_collinear by A22,DIRAF:30;
A31: a,a9 '||' b9,b by A2,DIRAF:22;
b9,c9,b9 are_collinear by DIRAF:31;
then a,a9,b9 are_collinear by A7,A14,A30,DIRAF:32;
then a,a9,b are_collinear by A9,A31,DIRAF:33;
hence contradiction by A1,DIRAF:30;
end;
A32: not c9,b9,x are_collinear
proof
assume c9,b9,x are_collinear;
then
A33: b9,x,c9 are_collinear by DIRAF:30;
A34: b9,x,b9 are_collinear by DIRAF:31;
A35: c9,b9,b9 are_collinear by DIRAF:31;
b9,x,b are_collinear by A27,DIRAF:30;
then c9,b9,b are_collinear by A29,A33,A34,DIRAF:32;
hence contradiction by A8,A14,A16,A35,DIRAF:32;
end;
A36: x,b,b9 are_collinear by A27,DIRAF:30;
A37: not a,x,b are_collinear
proof
assume a,x,b are_collinear;
then
A38: x,b,a are_collinear by DIRAF:30;
A39: b,b9 '||' a,a9 by A2,DIRAF:22;
x,b,b are_collinear by DIRAF:31;
then b,b9,a are_collinear by A36,A24,A38,DIRAF:32;
hence contradiction by A15,A16,A39,DIRAF:33;
end;
b9,b,x are_collinear by A27,DIRAF:30;
then b9,b '||' b9,x by DIRAF:def 5;
then b,b9 '||' b9,x by DIRAF:22;
then
A40: b9,x '||' a,a9 by A2,A15,DIRAF:23;
a,x,c9 are_collinear by A22,DIRAF:30;
then Mid a,x,c9 by A4,A28,A37,Th8;
then Mid c9,x,a by DIRAF:9;
then Mid c9,b9,a9 by A8,A40,A32,Th8;
hence thesis by DIRAF:9;
end;
c =c9 implies thesis
proof
A41: not c9,b9,b are_collinear
proof
A42: c9,b9,b9 are_collinear by DIRAF:31;
assume c9,b9,b are_collinear;
hence contradiction by A8,A14,A16,A42,DIRAF:32;
end;
assume c =c9;
then
A43: Mid c9,b,a by A4,DIRAF:9;
b9,b '||' a,a9 by A2,DIRAF:22;
then Mid c9,b9,a9 by A8,A43,A41,Th8;
hence thesis by DIRAF:9;
end;
hence thesis by A19;
end;
b=b9 implies thesis
proof
A44: a,a9 '||' c9,c by A3,DIRAF:22;
A45: b9,a9,c9 are_collinear by A5,DIRAF:30;
assume
A46: b=b9;
then not b9,a,a9 are_collinear by A1,DIRAF:30;
hence thesis by A4,A46,A45,A44,Th6;
end;
hence thesis by A13,DIRAF:10;
end;
theorem
OAS is satisfying_Gen_Par_Pasch
by Th10;
theorem
not p,a,b are_collinear & a,p // p,a9 & b,p // p,b9 & a,b '||' a9,b9
implies a,b
// b9,a9
proof
assume that
A1: not p,a,b are_collinear and
A2: a,p // p,a9 and
A3: b,p // p,b9 and
A4: a,b '||' a9,b9;
A5: not p,b,a are_collinear by A1,DIRAF:30;
Mid b,p,b9 by A3,DIRAF:def 3;
then b,p,b9 are_collinear by DIRAF:28;
then
A6: p,b,b9 are_collinear by DIRAF:30;
Mid a,p,a9 by A2,DIRAF:def 3;
then a,p,a9 are_collinear by DIRAF:28;
then
A7: p,a,a9 are_collinear by DIRAF:30;
A8: b,a '||' a9,b9 by A4,DIRAF:22;
a<>p by A1,DIRAF:31;
then consider q such that
A9: b,p // p,q and
A10: b,a // a9,q by A2,ANALOAF:def 5;
Mid b,p,q by A9,DIRAF:def 3;
then b,p,q are_collinear by DIRAF:28;
then
A11: p,b,q are_collinear by DIRAF:30;
b,a '||' a9,q by A10,DIRAF:def 4;
then b,a // a9,b9 by A10,A5,A7,A6,A11,A8,Th4;
hence thesis by DIRAF:2;
end;
theorem
not p,a,a9 are_collinear & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9
implies a,a9 // b,b9
proof
assume that
A1: not p,a,a9 are_collinear and
A2: p,a // p,b and
A3: p,a9 // p,b9 and
A4: a,a9 '||' b,b9;
consider c such that
A5: Mid a,p,c and
A6: p<>c by DIRAF:13;
A7: a,p // p,c by A5,DIRAF:def 3;
A8: a<>p by A1,DIRAF:31;
then consider c9 such that
A9: a9,p // p,c9 and
A10: a9,a // c,c9 by A7,ANALOAF:def 5;
A11: a9,a '||' c9,c by A10,DIRAF:def 4;
A12: c <>c9
proof
assume c =c9;
then Mid a9,p,c by A9,DIRAF:def 3;
then a9,p,c are_collinear by DIRAF:28;
then
A13: p,c,a9 are_collinear by DIRAF:30;
a,p,c are_collinear by A5,DIRAF:28;
then
A14: p,c,a are_collinear by DIRAF:30;
p,c,p are_collinear by DIRAF:31;
hence contradiction by A1,A6,A14,A13,DIRAF:32;
end;
p,a // c,p by A7,DIRAF:2;
then c,p // p,b by A2,A8,ANALOAF:def 5;
then consider b99 be Element of OAS such that
A15: c9,p // p,b99 and
A16: c9,c // b,b99 by A6,ANALOAF:def 5;
A17: a9,a '||' b,b9 by A4,DIRAF:22;
A18: p<>c9
proof
assume p=c9;
then a9,a '||' c,p by A10,DIRAF:def 4;
then
A19: p,c '||' a,a9 by DIRAF:22;
a,p '||' p,c by A7,DIRAF:def 4;
then a,p '||' a,a9 by A6,A19,DIRAF:23;
then a,p,a9 are_collinear by DIRAF:def 5;
hence contradiction by A1,DIRAF:30;
end;
p,a '||' p,b by A2,DIRAF:def 4;
then
A20: p,a,b are_collinear by DIRAF:def 5;
A21: c9,c // a,a9 by A10,DIRAF:2;
a9,p '||' p,c9 by A9,DIRAF:def 4;
then
A22: p,a9 '||' p,c9 by DIRAF:22;
p,a9 '||' p,b9 by A3,DIRAF:def 4;
then
A23: p,a9,b9 are_collinear by DIRAF:def 5;
c9,p '||' p,b99 by A15,DIRAF:def 4;
then p,c9 '||' p,b99 by DIRAF:22;
then p,a9 '||' p,b99 by A18,A22,DIRAF:23;
then
A24: p,a9,b99 are_collinear by DIRAF:def 5;
c9,c '||' b,b99 by A16,DIRAF:def 4;
then
A25: a9,a '||' b,b99 by A12,A11,DIRAF:23;
not p,a9,a are_collinear by A1,DIRAF:30;
then c9,c // b,b9 by A20,A23,A17,A16,A24,A25,Th4;
hence thesis by A12,A21,ANALOAF:def 5;
end;
theorem Th14:
not p,a,b are_collinear & p,a '||' b,c & p,b '||' a,c implies
p,a // b,c & p,b // a,c
proof
assume that
A1: not p,a,b are_collinear and
A2: p,a '||' b,c and
A3: p,b '||' a,c;
consider d such that
A4: p,a // b,d and
A5: p,b // a,d and
a<>d by ANALOAF:def 5;
A6: p,b '||' a,d by A5,DIRAF:def 4;
p,a '||' b,d by A4,DIRAF:def 4;
hence thesis by A1,A2,A3,A4,A5,A6,Th5;
end;
theorem Th15:
Mid p,c,b & c,d // b,a & p,d // p,a & not p,a,b are_collinear & p<>c
implies Mid p,d,a
proof
assume that
A1: Mid p,c,b and
A2: c,d // b,a and
A3: p,d // p,a and
A4: not p,a,b are_collinear and
A5: p<>c;
A6: p,c,b are_collinear by A1,DIRAF:28;
now
assume
A7: Mid p,a,d;
A8: now
A9: p<>a by A4,DIRAF:31;
assume that
A10: b<>c and
A11: d<>a;
assume not Mid p,d,a;
then Mid p,a,d by A3,DIRAF:7;
then p,a // a,d by DIRAF:def 3;
then consider e1 such that
A12: c,a // a,e1 and
A13: c,p // d,e1 by A9,ANALOAF:def 5;
A14: d,e1 // c,p by A13,DIRAF:2;
A15: c <>e1
by A12,DIRAF:def 3,A4,A6,DIRAF:8;
Mid b,c,p by A1,DIRAF:9;
then
A16: b,c // c,p by DIRAF:def 3;
then
A17: c,p // b,c by DIRAF:2;
consider e2 such that
A18: b,a // a,e2 and
A19: b,c // e1,e2 by A4,A6,A12,ANALOAF:def 5;
consider e3 such that
A20: b,c // e2,e3 and
A21: b,e2 // c,e3 and
c <>e3 by ANALOAF:def 5;
A22: a<>b by A4,DIRAF:31;
A23: Mid c,a,e1 by A12,DIRAF:def 3;
A24: d<>e1
proof
Mid p,d,a or Mid p,a,d by A3,DIRAF:7;
then p,d,a are_collinear or p,a,d are_collinear by DIRAF:28;
then
A25: d,a,p are_collinear by DIRAF:30;
A26: d,a,a are_collinear by DIRAF:31;
assume d=e1;
then c,a,d are_collinear by A23,DIRAF:28;
then d,a,c are_collinear by DIRAF:30;
then d,a,b are_collinear by A5,A6,A25,DIRAF:35;
hence contradiction by A4,A11,A25,A26,DIRAF:32;
end;
b,a // b,e2 by A18,ANALOAF:def 5;
then
A27: c,d // b,e2 by A2,A22,DIRAF:3;
b<>e2 by A22,A18,ANALOAF:def 5;
then c,d // c,e3 by A21,A27,DIRAF:3;
then Mid c,d,e3 or Mid c,e3,d by DIRAF:7;
then c,d,e3 are_collinear or c,e3,d are_collinear by DIRAF:28;
then
A28: d,e3,c are_collinear by DIRAF:30;
e1,e2 // c,p by A10,A19,A16,ANALOAF:def 5;
then
A29: e1,e2 // d,e1 by A5,A13,DIRAF:3;
then d,e1 // e1,e2 by DIRAF:2;
then
A30: d,e1 // d,e2 by ANALOAF:def 5;
then d,e2 // d,e1 by DIRAF:2;
then d,e2 // c,p by A24,A14,DIRAF:3;
then d,e2 // b,c by A5,A17,DIRAF:3;
then
A31: d,e2 // e2,e3 by A10,A20,DIRAF:3;
then Mid d,e2,e3 by DIRAF:def 3;
then d,e2,e3 are_collinear by DIRAF:28;
then
A32: d,e3,e2 are_collinear by DIRAF:30;
A33: d<>e2 by A24,A29,ANALOAF:def 5;
then
A34: d<>e3 by A31,ANALOAF:def 5;
d,e2 // d,e3 by A31,ANALOAF:def 5;
then d,e1 // d,e3 by A30,A33,DIRAF:3;
then Mid d,e1,e3 or Mid d,e3,e1 by DIRAF:7;
then d,e1,e3 are_collinear or d,e3,e1 are_collinear by DIRAF:28;
then
A35: d,e3,e1 are_collinear by DIRAF:30;
c,a,e1 are_collinear by A23,DIRAF:28;
then c,e1,a are_collinear by DIRAF:30;
then
A36: d,e3,a are_collinear by A15,A28,A35,DIRAF:35;
A37: a<>e1
proof
p,a // a,d by A7,DIRAF:def 3;
then
A38: d,a // a,p by DIRAF:2;
assume a=e1;
then c,p // a,p by A11,A13,A38,DIRAF:3;
then p,c // p,a by DIRAF:2;
then Mid p,c,a or Mid p,a,c by DIRAF:7;
then p,c,a are_collinear or p,a,c are_collinear by DIRAF:28;
then
A39: p,c,a are_collinear by DIRAF:30;
p,c,p are_collinear by DIRAF:31;
hence contradiction by A4,A5,A6,A39,DIRAF:32;
end;
A40: a<>e2
proof
assume
A41: a=e2;
e1,a // a,c by A12,DIRAF:2;
then b,c // a,c by A19,A37,A41,DIRAF:3;
then c,b // c,a by DIRAF:2;
then Mid c,b,a or Mid c,a,b by DIRAF:7;
then c,b,a are_collinear or c,a,b are_collinear by DIRAF:28;
then
A42: c,b,a are_collinear by DIRAF:30;
A43: c,b,b are_collinear by DIRAF:31;
c,b,p are_collinear by A6,DIRAF:30;
hence contradiction by A4,A10,A42,A43,DIRAF:32;
end;
Mid b,a,e2 by A18,DIRAF:def 3;
then b,a,e2 are_collinear by DIRAF:28;
then a,e2,b are_collinear by DIRAF:30;
then
A44: d,e3,b are_collinear by A40,A36,A32,DIRAF:35;
c,b,p are_collinear by A6,DIRAF:30;
then d,e3,p are_collinear by A10,A28,A44,DIRAF:35;
hence contradiction by A4,A34,A36,A44,DIRAF:32;
end;
A45: p,a,d are_collinear by A7,DIRAF:28;
now
assume b=c;
then Mid b,d,a or Mid b,a,d by A2,DIRAF:7;
then b,d,a are_collinear or b,a,d are_collinear by DIRAF:28;
then
A46: d,a,b are_collinear by DIRAF:30;
A47: d,a,a are_collinear by DIRAF:31;
d,a,p are_collinear by A45,DIRAF:30;
hence a=d by A4,A46,A47,DIRAF:32;
end;
hence thesis by A8,DIRAF:10;
end;
hence thesis by A3,DIRAF:7;
end;
theorem Th16:
Mid p,d,a & c,d // b,a & p,c // p,b & not p,a,b are_collinear & p<>c
implies Mid p,c,b
proof
assume that
A1: Mid p,d,a and
A2: c,d // b,a and
A3: p,c // p,b and
A4: not p,a,b are_collinear and
A5: p<>c;
A6: p<>d
proof
assume
A7: p=d;
c,p // b,p by A3,DIRAF:2;
then b,p // b,a by A2,A5,A7,ANALOAF:def 5;
then Mid b,p,a or Mid b,a,p by DIRAF:7;
then b,p,a are_collinear or b,a,p are_collinear by DIRAF:28;
hence contradiction by A4,DIRAF:30;
end;
Mid p,c,b or Mid p,b,c by A3,DIRAF:7;
then
A8: p,c,b are_collinear or p,b,c are_collinear by DIRAF:28;
then
A9: p,c,b are_collinear by DIRAF:30;
now
A10: not p,d,c are_collinear
proof
assume p,d,c are_collinear;
then
A11: p,c,d are_collinear by DIRAF:30;
p,c,p are_collinear by DIRAF:31;
then
A12: p,d,b are_collinear by A5,A9,A11,DIRAF:32;
A13: p,d,p are_collinear by DIRAF:31;
p,d,a are_collinear by A1,DIRAF:28;
hence contradiction by A4,A6,A12,A13,DIRAF:32;
end;
assume
A14: Mid p,b,c;
p,d // d,a by A1,DIRAF:def 3;
then p,d // p,a by ANALOAF:def 5;
then
A15: p,a // p,d by DIRAF:2;
A16: p<>b by A4,DIRAF:31;
b,a // c,d by A2,DIRAF:2;
then Mid p,a,d by A14,A15,A16,A10,Th15;
then
A17: Mid d,a,p by DIRAF:9;
Mid a,d,p by A1,DIRAF:9;
then c,a // b,a by A2,A17,DIRAF:14;
then a,c // a,b by DIRAF:2;
then Mid a,c,b or Mid a,b,c by DIRAF:7;
then a,c,b are_collinear or a,b,c are_collinear by DIRAF:28;
then
A18: b,c,a are_collinear by DIRAF:30;
A19: b,c,b are_collinear by DIRAF:31;
b,c,p are_collinear by A8,DIRAF:30;
then b=c by A4,A18,A19,DIRAF:32;
hence thesis by DIRAF:10;
end;
hence thesis by A3,DIRAF:7;
end;
theorem Th17:
not p,a,b are_collinear & p,b // p,c & b,a // c,d & p<>d
implies not Mid a ,p,d
proof
assume that
A1: not p,a,b are_collinear and
A2: p,b // p,c and
A3: b,a // c,d and
A4: p<>d;
assume Mid a,p,d;
then Mid d,p,a by DIRAF:9;
then
A5: d,p // p,a by DIRAF:def 3;
then
A6: p,d // a,p by DIRAF:2;
consider b9 such that
A7: c,p // p,b9 and
A8: c,d // a,b9 by A4,A5,ANALOAF:def 5;
A9: p<>c
proof
assume p=c;
then b,a // a,p by A3,A4,A6,DIRAF:3;
then Mid b,a,p by DIRAF:def 3;
hence contradiction by A1,DIRAF:9,28;
end;
A10: a<>b9
proof
assume
A11: a=b9;
b,p // c,p by A2,DIRAF:2;
then b,p // p,a by A9,A7,A11,DIRAF:3;
then Mid b,p,a by DIRAF:def 3;
then b,p,a are_collinear by DIRAF:28;
hence contradiction by A1,DIRAF:30;
end;
p,c // b9,p by A7,DIRAF:2;
then p,b // b9,p by A2,A9,DIRAF:3;
then
A12: b9,p // p,b by DIRAF:2;
A13: c <>d
proof
assume c =d;
then p,b // a,p by A2,A4,A6,DIRAF:3;
then b,p // p,a by DIRAF:2;
then Mid b,p,a by DIRAF:def 3;
then b,p,a are_collinear by DIRAF:28;
hence contradiction by A1,DIRAF:30;
end;
p<>b9
proof
assume p=b9;
then b,a // a,p by A3,A13,A8,DIRAF:3;
then Mid b,a,p by DIRAF:def 3;
hence contradiction by A1,DIRAF:9,28;
end;
then consider b99 be Element of OAS such that
A14: a,p // p,b99 and
A15: a,b9 // b,b99 by A12,ANALOAF:def 5;
a<>p by A1,DIRAF:31;
then
A16: a<>b99 by A14,ANALOAF:def 5;
b,a // a,b9 by A3,A13,A8,DIRAF:3;
then b,a // b,b99 by A15,A10,DIRAF:3;
then Mid b,a,b99 or Mid b,b99,a by DIRAF:7;
then b,a,b99 are_collinear or b,b99,a are_collinear by DIRAF:28;
then
A17: a,b99,b are_collinear by DIRAF:30;
Mid a,p,b99 by A14,DIRAF:def 3;
then a,p,b99 are_collinear by DIRAF:28;
then
A18: a,b99,p are_collinear by DIRAF:30;
a,b99, a are_collinear by DIRAF:31;
hence contradiction by A1,A18,A16,A17,DIRAF:32;
end;
theorem Th18:
p,b // p,c & b<>p implies ex x st p,a // p,x & b,a // c,x
proof
assume that
A1: p,b // p,c and
A2: b<>p;
A3: b,p // c,p by A1,DIRAF:2;
A4: now
assume that
p<>c and
A5: p<>a;
consider e1 such that
A6: Mid a,p,e1 and
A7: p<>e1 by DIRAF:13;
a,p // p,e1 by A6,DIRAF:def 3;
then consider e2 such that
A8: b,p // p,e2 and
A9: b,a // e1,e2 by A5,ANALOAF:def 5;
Mid e1,p,a by A6,DIRAF:9;
then
A10: e1,p // p,a by DIRAF:def 3;
A11: now
A12: now
A13: now
assume b,p // a,p;
then a,p // c,p by A2,A3,ANALOAF:def 5;
hence p,a // p,c & b,a // c,c by DIRAF:2,4;
end;
assume
A14: a,b // b,p;
then a,b // a,p by ANALOAF:def 5;
then b,p // a,p or a=b by A14,ANALOAF:def 5;
hence thesis by A13,DIRAF:1;
end;
A15: now
assume
A16: a,p // p,b;
then a,p // a,b by ANALOAF:def 5;
then a,b // p,b by A5,A16,ANALOAF:def 5;
then b,a // b,p by DIRAF:2;
hence p,a // p,p & b,a // c,p by A2,A3,DIRAF:3,4;
end;
assume p=e2;
then b,a // p,a by A7,A10,A9,DIRAF:3;
then a,b // a,p by DIRAF:2;
hence thesis by A12,A15,DIRAF:6;
end;
A17: now
A18: now
assume that
p,a // a,b and
A19: p,c // c,a;
p,c // p,a by A19,ANALOAF:def 5;
hence p,a // p,c & b,a // c,c by DIRAF:2,4;
end;
A20: now
assume that
p,b // b,a and
A21: p,c // c,a;
p,c // p,a by A21,ANALOAF:def 5;
hence p,a // p,c & b,a // c,c by DIRAF:2,4;
end;
A22: now
assume that
A23: p,a // a,b and
A24: p,a // a,c;
a,b // a,c by A5,A23,A24,ANALOAF:def 5;
hence p,a // p,a & b,a // c,a by DIRAF:1,2;
end;
A25: p,b // b,a & p,a // a,c implies p,a // p,c & b,a // c,c by ANALOAF:def 5;
assume that
A26: e1=e2 and
A27: e2<>p;
p,e2 // a,p by A10,A26,DIRAF:2;
then b,p // a,p by A8,A27,DIRAF:3;
then
A28: p,b // p,a by DIRAF:2;
then p,a // p,c by A1,A2,ANALOAF:def 5;
hence thesis by A28,A25,A20,A22,A18,DIRAF:6;
end;
now
assume that
A29: e1<>e2 and
A30: e2<>p;
p,b // e2,p by A8,DIRAF:2;
then e2,p // p,c by A1,A2,ANALOAF:def 5;
then consider x such that
A31: e1,p // p,x and
A32: e1,e2 // c,x by A30,ANALOAF:def 5;
A33: p,a // p,x by A7,A10,A31,ANALOAF:def 5;
b,a // c,x by A9,A29,A32,DIRAF:3;
hence thesis by A33;
end;
hence thesis by A17,A11;
end;
A34: p=c implies p,a // p,c & b,a // c,c by DIRAF:4;
p=a implies p,a // p,a & b,a // c,a by A1,DIRAF:1,2;
hence thesis by A34,A4;
end;
theorem Th19:
Mid p,c,b implies ex x st Mid p,x,a & b,a // c,x
proof
A1: b=c implies Mid p,a,a & b,a // c,a by DIRAF:1,10;
assume
A2: Mid p,c,b;
A3: now
assume p=b;
then p=c by A2,DIRAF:8;
hence Mid p,p,a & b,a // c,p by DIRAF:4,10;
end;
A4: p,c // c,b by A2,DIRAF:def 3;
A5: now
assume that
A6: p<>c and
A7: p<>b and
A8: b<>c;
Mid b,c,p by A2,DIRAF:9;
then
A9: b,c // c,p by DIRAF:def 3;
then
A10: b,c // b,p by ANALOAF:def 5;
then
A11: b,p // c,p by A8,A9,ANALOAF:def 5;
A12: now
A13: now
assume
A14: Mid p,a,b;
A15: now
Mid b,a,p by A14,DIRAF:9;
then b,a // a,p by DIRAF:def 3;
then
A16: a,p // b,a by DIRAF:2;
assume Mid p,a,c;
then Mid c,a,p by DIRAF:9;
then c,a // a,p by DIRAF:def 3;
then
A17: a,p // c,a by DIRAF:2;
A18: b,a // c,a implies Mid p,a,a & b,a // c,a by DIRAF:10;
a=p implies Mid p,p,a & b,a // c,p by A8,A9,A10,ANALOAF:def 5
,DIRAF:10;
hence thesis by A17,A16,A18,ANALOAF:def 5;
end;
Mid p,c,a implies Mid p,c,a & b,a // c,c by DIRAF:4;
hence thesis by A2,A14,A15,DIRAF:17;
end;
A19: now
assume Mid a,p,b;
then Mid b,p,a by DIRAF:9;
then b,p // p,a by DIRAF:def 3;
then b,p // b,a by ANALOAF:def 5;
hence Mid p,p,a & b,a // c,p by A7,A11,ANALOAF:def 5,DIRAF:10;
end;
A20: now
A21: p,c // p,b by A4,ANALOAF:def 5;
assume
A22: Mid p,b,a;
then p,b // b,a by DIRAF:def 3;
then p,c // b,a by A7,A21,DIRAF:3;
then b,a // c,b by A4,A6,ANALOAF:def 5;
hence thesis by A22;
end;
assume p,a,b are_collinear;
hence thesis by A13,A19,A20,DIRAF:29;
end;
now
A23: p,b // p,c by A2,DIRAF:7;
assume
A24: not p,a,b are_collinear;
then p<>b by DIRAF:31;
then consider x such that
A25: p,a // p,x and
A26: b,a // c,x by A23,Th18;
A27: p,x // p,a by A25,DIRAF:2;
c,x // b,a by A26,DIRAF:2;
hence thesis by A2,A6,A24,A26,A27,Th15;
end;
hence thesis by A12;
end;
p=c implies Mid p,p,a & b,a // c,p by DIRAF:4,10;
hence thesis by A3,A1,A5;
end;
theorem Th20:
p<>b & Mid p,b,c implies ex x st Mid p,a,x & b,a // c,x
proof
assume that
A1: p<>b and
A2: Mid p,b,c;
A3: p,b // b,c by A2,DIRAF:def 3;
then
A4: p,b // p,c by ANALOAF:def 5;
A5: now
assume
A6: not p,a,b are_collinear;
consider x such that
A7: p,a // p,x and
A8: b,a // c,x by A1,A4,Th18;
A9: p<>c by A1,A2,DIRAF:8;
A10: p<>x
proof
p,b // p,c by A2,DIRAF:7;
then
A11: c,p // b,p by DIRAF:2;
assume p=x;
then b,a // b,p by A8,A9,A11,DIRAF:3;
then Mid b,a,p or Mid b,p,a by DIRAF:7;
then b,a,p are_collinear or b,p,a are_collinear by DIRAF:28;
hence contradiction by A6,DIRAF:30;
end;
not p,x,c are_collinear
proof
Mid p,a,x or Mid p,x,a by A7,DIRAF:7;
then p,a,x are_collinear or p,x,a are_collinear by DIRAF:28;
then
A12: p,x,a are_collinear by DIRAF:30;
A13: p,x,p are_collinear by DIRAF:31;
p,b,c are_collinear by A2,DIRAF:28;
then
A14: p,c,b are_collinear by DIRAF:30;
A15: p,c,p are_collinear by DIRAF:31;
assume p,x,c are_collinear;
then p,c,a are_collinear by A10,A12,A13,DIRAF:32;
hence contradiction by A6,A9,A14,A15,DIRAF:32;
end;
hence thesis by A1,A2,A7,A8,Th15;
end;
A16: now
assume that
A17: p,a,b are_collinear and
A18: c <>b;
A19: now
assume Mid p,a,b;
then Mid a,b,c by A2,DIRAF:11;
then Mid c,b,a by DIRAF:9;
then
A20: c,b // b,a by DIRAF:def 3;
then c,b // c,a by ANALOAF:def 5;
hence Mid p,a,a & b,a // c,a by A18,A20,ANALOAF:def 5,DIRAF:10;
end;
A21: now
assume Mid p,b,a;
then
A22: p,b // b,a by DIRAF:def 3;
A23: now
A24: now
assume p,a // a,c;
then Mid p,a,c by DIRAF:def 3;
hence thesis by DIRAF:4;
end;
A25: now
assume a=b;
then b,a // c,a by DIRAF:4;
hence thesis by DIRAF:10;
end;
p,b // p,a by A22,ANALOAF:def 5;
then
A26: b,a // p,a by A1,A22,ANALOAF:def 5;
assume b,a // a,c;
hence thesis by A26,A25,A24,ANALOAF:def 5;
end;
A27: now
assume
A28: b,c // c,a;
then b,c // b,a by ANALOAF:def 5;
hence Mid p,a,a & b,a // c,a by A18,A28,ANALOAF:def 5,DIRAF:10;
end;
b,a // b,c by A1,A3,A22,ANALOAF:def 5;
hence thesis by A23,A27,ANALOAF:def 5;
end;
now
assume Mid a,p,b;
then Mid a,b,c by A1,A2,DIRAF:12;
then Mid c,b,a by DIRAF:9;
then
A29: c,b // b,a by DIRAF:def 3;
then c,b // c,a by ANALOAF:def 5;
hence Mid p,a,a & b,a // c,a by A18,A29,ANALOAF:def 5,DIRAF:10;
end;
hence thesis by A17,A19,A21,DIRAF:29;
end;
c =b implies Mid p,a,a & b,a // c,a by DIRAF:1,10;
hence thesis by A5,A16;
end;
theorem Th21:
not p,a,b are_collinear & Mid p,c,b implies ex x st Mid p,x,a & a,b // x,c
proof
assume that
A1: not p,a,b are_collinear and
A2: Mid p,c,b;
A3: p<>a by A1,DIRAF:31;
A4: p,c,b are_collinear by A2,DIRAF:28;
A5: Mid b,c,p by A2,DIRAF:9;
then
A6: b,c // c,p by DIRAF:def 3;
A7: a<>b by A1,DIRAF:31;
A8: now
assume that
A9: b<>c and
A10: a<>c and
A11: p<>c;
consider e1 such that
A12: Mid b,e1,a and
A13: p,a // c,e1 by A5,Th19;
A14: not p,c,a are_collinear
proof
A15: p,c,p are_collinear by DIRAF:31;
assume p,c,a are_collinear;
hence contradiction by A1,A4,A11,A15,DIRAF:32;
end;
A16: a<>e1
proof
assume a=e1;
then a,p // a,c by A13,DIRAF:2;
then Mid a,p,c or Mid a,c,p by DIRAF:7;
then a,p,c are_collinear or a,c,p are_collinear by DIRAF:28;
hence contradiction by A14,DIRAF:30;
end;
consider e4 such that
A17: e1,c // c,e4 and
A18: e1,b // p,e4 by A6,A9,ANALOAF:def 5;
consider e2 such that
A19: a,c // c,e2 and
A20: a,b // p,e2 by A6,A9,ANALOAF:def 5;
consider e3 such that
A21: p,c // c,e3 and
A22: p,a // e2,e3 by A10,A19,ANALOAF:def 5;
A23: not a,b,c are_collinear
proof
assume a,b,c are_collinear;
then
A24: b,c,a are_collinear by DIRAF:30;
A25: b,c,b are_collinear by DIRAF:31;
b,c,p are_collinear by A4,DIRAF:30;
hence contradiction by A1,A9,A24,A25,DIRAF:32;
end;
A26: c <>e2
proof
assume
A27: c =e2;
p,c // c,b by A6,DIRAF:2;
then a,b // c,b by A11,A20,A27,DIRAF:3;
then b,a // b,c by DIRAF:2;
then Mid b,a,c or Mid b,c,a by DIRAF:7;
then b,a,c are_collinear or b,c,a are_collinear by DIRAF:28;
hence contradiction by A23,DIRAF:30;
end;
A28: e2<>e3
proof
assume e2=e3;
then c,e2 // p,c by A21,DIRAF:2;
then a,c // p,c by A19,A26,DIRAF:3;
then c,a // c,p by DIRAF:2;
then Mid c,a,p or Mid c,p,a by DIRAF:7;
then c,a,p are_collinear or c,p,a are_collinear by DIRAF:28;
hence contradiction by A14,DIRAF:30;
end;
A29: c <>e1
proof
assume c =e1;
then b,c,a are_collinear by A12,DIRAF:28;
hence contradiction by A23,DIRAF:30;
end;
A30: p<>e4
proof
assume p=e4;
then c,e1 // p,c by A17,DIRAF:2;
then p,a // p,c by A13,A29,DIRAF:3;
then Mid p,a,c or Mid p,c,a by DIRAF:7;
then p,a,c are_collinear or p,c,a are_collinear by DIRAF:28;
hence contradiction by A14,DIRAF:30;
end;
Mid e1,c,e4 by A17,DIRAF:def 3;
then Mid e4,c,e1 by DIRAF:9;
then
A31: e4,c // c,e1 by DIRAF:def 3;
c,e1 // e2,e3 by A3,A13,A22,ANALOAF:def 5;
then
A32: e4,c // e2,e3 by A29,A31,DIRAF:3;
A33: e2<>e4
proof
assume e2=e4;
then c,e2 // e1,c by A17,DIRAF:2;
then a,c // e1,c by A19,A26,DIRAF:3;
then c,e1 // c,a by DIRAF:2;
then p,a // c,a by A13,A29,DIRAF:3;
then a,p // a,c by DIRAF:2;
then Mid a,p,c or Mid a,c,p by DIRAF:7;
then a,p,c are_collinear or a,c,p are_collinear by DIRAF:28;
hence contradiction by A14,DIRAF:30;
end;
A34: c <>e3
proof
assume c =e3;
then c,e2 // a,p by A22,DIRAF:2;
then a,c // a,p by A19,A26,DIRAF:3;
then Mid a,c,p or Mid a,p,c by DIRAF:7;
then a,c,p are_collinear or a,p,c are_collinear by DIRAF:28;
hence contradiction by A14,DIRAF:30;
end;
A35: p<>e3 by A11,A21,ANALOAF:def 5;
A36: not p,e3,e2 are_collinear
proof
p,c // c,b by A2,DIRAF:def 3;
then
A37: p,c // p,b by ANALOAF:def 5;
p,c // p,e3 by A21,ANALOAF:def 5;
then p,b // p,e3 by A11,A37,ANALOAF:def 5;
then Mid p,b,e3 or Mid p,e3,b by DIRAF:7;
then p,b,e3 are_collinear or p,e3,b are_collinear by DIRAF:28;
then
A38: p,e3,b are_collinear by DIRAF:30;
A39: p,e3,p are_collinear by DIRAF:31;
a,c // a,e2 by A19,ANALOAF:def 5;
then Mid a,c,e2 or Mid a,e2,c by DIRAF:7;
then a,c,e2 are_collinear or a,e2,c are_collinear by DIRAF:28;
then
A40: c,e2,a are_collinear by DIRAF:30;
p,c // p,e3 by A21,ANALOAF:def 5;
then Mid p,c,e3 or Mid p,e3,c by DIRAF:7;
then p,c,e3 are_collinear or p,e3,c are_collinear by DIRAF:28;
then
A41: p,e3,c are_collinear by DIRAF:30;
assume p,e3,e2 are_collinear ;
then p,e3,a are_collinear by A26,A41,A40,DIRAF:35;
hence contradiction by A1,A35,A38,A39,DIRAF:32;
end;
then
A42: not e3,e2,p are_collinear by DIRAF:30;
consider e5 such that
A43: e4,e2 // c,e5 and
A44: e4,c // e2,e5 and
A45: e2<>e5 by ANALOAF:def 5;
A46: b<>e1
proof
p,c // c,b by A2,DIRAF:def 3;
then
A47: c,b // p,c by DIRAF:2;
assume b=e1;
then p,a // p,c by A9,A13,A47,DIRAF:3;
then Mid p,a,c or Mid p,c,a by DIRAF:7;
then p,a,c are_collinear or p,c,a are_collinear by DIRAF:28;
hence contradiction by A14,DIRAF:30;
end;
A48: c <>e4
proof
assume
A49: c =e4;
p,c // c,b by A2,DIRAF:def 3;
then e1,b // c,b by A11,A18,A49,DIRAF:3;
then b,e1 // b,c by DIRAF:2;
then Mid b,e1,c or Mid b,c,e1 by DIRAF:7;
then b,e1,c are_collinear or b,c,e1 are_collinear by DIRAF:28;
then
A50: b,e1,c are_collinear by DIRAF:30;
A51: b,e1,b are_collinear by DIRAF:31;
b,e1,a are_collinear by A12,DIRAF:28;
hence contradiction by A23,A46,A50,A51,DIRAF:32;
end;
A52: c <>e5
proof
assume c =e5;
then c,e4 // c,e2 by A44,DIRAF:2;
then e1,c // c,e2 by A17,A48,DIRAF:3;
then c,e2 // e1,c by DIRAF:2;
then a,c // e1,c by A19,A26,DIRAF:3;
then c,e1 // c,a by DIRAF:2;
then p,a // c,a by A13,A29,DIRAF:3;
then a,p // a,c by DIRAF:2;
then Mid a,p,c or Mid a,c,p by DIRAF:7;
then a,p,c are_collinear or a,c,p are_collinear by DIRAF:28;
hence contradiction by A14,DIRAF:30;
end;
Mid a,e1,b by A12,DIRAF:9;
then
A53: a,e1 // e1,b by DIRAF:def 3;
then a,e1 // a,b by ANALOAF:def 5;
then a,b // e1,b by A16,A53,ANALOAF:def 5;
then e1,b // p,e2 by A7,A20,ANALOAF:def 5;
then
A54: p,e4 // p,e2 by A18,A46,ANALOAF:def 5;
Mid p,c,e3 by A21,DIRAF:def 3;
then Mid p,e4,e2 by A36,A32,A30,A54,Th16;
then
A55: p,e4 // e4,e2 by DIRAF:def 3;
then p,e4 // p,e2 by ANALOAF:def 5;
then
A56: p,e2 // e4,e2 by A30,A55,ANALOAF:def 5;
then
A57: p,e2 // c,e5 by A43,A33,DIRAF:3;
p<>e2
proof
assume p=e2;
then Mid a,c,p by A19,DIRAF:def 3;
hence contradiction by A14,DIRAF:9,28;
end;
then
A58: a,b // e4,e2 by A20,A56,DIRAF:3;
then
A59: a,b // c,e5 by A43,A33,DIRAF:3;
A60: e5<>e3
proof
assume e5=e3;
then c,e3 // a,b by A59,DIRAF:2;
then p,c // a,b by A21,A34,DIRAF:3;
then c,p // b,a by DIRAF:2;
then b,c // b,a by A6,A11,DIRAF:3;
then Mid b,c,a or Mid b,a,c by DIRAF:7;
then b,c,a are_collinear or b,a,c are_collinear by DIRAF:28;
hence contradiction by A23,DIRAF:30;
end;
c,e1 // e4,c by A17,DIRAF:2;
then c,e1 // e2,e5 by A44,A48,DIRAF:3;
then p,a // e2,e5 by A13,A29,DIRAF:3;
then e2,e3 // e2,e5 by A3,A22,ANALOAF:def 5;
then Mid e2,e3,e5 or Mid e2,e5,e3 by DIRAF:7;
then e2,e3,e5 are_collinear or e2,e5,e3 are_collinear by DIRAF:28;
then
A61: e2,e3,e5 are_collinear by DIRAF:30;
Mid p,c,e3 by A21,DIRAF:def 3;
then
A62: Mid e3,c,p by DIRAF:9;
e3,c // c,p by A21,DIRAF:2;
then consider x such that
A63: e5,c // c,x and
A64: e5,e3 // p,x by A34,ANALOAF:def 5;
A65: c,e5 // x,c by A63,DIRAF:2;
Mid p,c,e3 by A21,DIRAF:def 3;
then Mid e3,c,p by DIRAF:9;
then e3,c // c,p by DIRAF:def 3;
then e3,c // e3,p by ANALOAF:def 5;
then e3,p // e3,c by DIRAF:2;
then not Mid e2,e3,e5 by A60,A57,A42,Th17;
then Mid e3,e2,e5 or Mid e2,e5,e3 by A61,DIRAF:29;
then e3,e2 // e2,e5 or Mid e3,e5,e2 by DIRAF:9,def 3;
then e3,e2 // e3,e5 or e3,e5 // e5,e2 by ANALOAF:def 5,DIRAF:def 3;
then
A66: e3,e5 // e3,e2 by ANALOAF:def 5,DIRAF:2;
c,e5 // p,e2 by A57,DIRAF:2;
then Mid e3,e5,e2 by A34,A42,A66,A62,Th15;
then Mid e2,e5,e3 by DIRAF:9;
then
A67: e2,e5 // e5,e3 by DIRAF:def 3;
then e2,e5 // e2,e3 by ANALOAF:def 5;
then e2,e3 // e5,e3 by A45,A67,ANALOAF:def 5;
then p,a // e5,e3 by A22,A28,DIRAF:3;
then p,a // p,x by A64,A60,DIRAF:3;
then
A68: p,x // p,a by DIRAF:2;
a,b // c,e5 by A43,A33,A58,DIRAF:3;
then
A69: a,b // x,c by A52,A65,DIRAF:3;
then c,x // b,a by DIRAF:2;
hence thesis by A1,A2,A11,A69,A68,Th15;
end;
A70: a=c implies a,b // a,c & Mid p,a,a by DIRAF:4,10;
A71: p=c implies a,b // c,c & Mid p,c,a by DIRAF:4,10;
b=c implies a,b // a,c & Mid p,a,a by DIRAF:1,10;
hence thesis by A8,A70,A71;
end;
theorem
ex x st a,x // b,c & a,b // x,c
proof
A1: now
consider e3 such that
A2: Mid b,c,e3 and
A3: c <>e3 by DIRAF:13;
A4: b,c // c,e3 by A2,DIRAF:def 3;
assume
A5: not a,b,c are_collinear;
then
A6: b<>c by DIRAF:31;
then consider e4 such that
A7: a,c // c,e4 and
A8: a,b // e3,e4 by A4,ANALOAF:def 5;
A9: Mid a,c,e4 by A7,DIRAF:def 3;
then Mid e4,c,a by DIRAF:9;
then
A10: e4,c // c,a by DIRAF:def 3;
A11: e4<>c
proof
assume
A12: e4=c;
e3,c // c,b by A4,DIRAF:2;
then a,b // c,b by A3,A8,A12,DIRAF:3;
then b,a // b,c by DIRAF:2;
then Mid b,a,c or Mid b,c,a by DIRAF:7;
then b,a,c are_collinear or b,c,a are_collinear by DIRAF:28;
hence contradiction by A5,DIRAF:30;
end;
A13: not e4,c,e3 are_collinear
proof
b,c,e3 are_collinear by A2,DIRAF:28;
then
A14: c,e3,b are_collinear by DIRAF:30;
assume
A15: e4,c,e3 are_collinear ;
A16: c,e3,c are_collinear by DIRAF:31;
A17: e4,c,c are_collinear by DIRAF:31;
e4,c,a are_collinear by A9,DIRAF:9,28;
then c,e3,a are_collinear by A11,A15,A17,DIRAF:32;
hence contradiction by A5,A3,A14,A16,DIRAF:32;
end;
b,c // c,e3 by A2,DIRAF:def 3;
then
A18: c,e3 // b,c by DIRAF:2;
consider e1 such that
A19: Mid c,a,e1 and
A20: a<>e1 by DIRAF:13;
A21: c,a // a,e1 by A19,DIRAF:def 3;
A22: a<>c by A5,DIRAF:31;
then consider e2 such that
A23: b,a // a,e2 and
A24: b,c // e1,e2 by A21,ANALOAF:def 5;
c,a // c,e1 by A21,ANALOAF:def 5;
then e4,c // c,e1 by A22,A10,DIRAF:3;
then
A25: Mid e4,c,e1 by DIRAF:def 3;
then consider e5 such that
A26: Mid e4,e3,e5 and
A27: c,e3 // e1,e5 by A11,Th20;
A28: e4<>e3
proof
assume e4=e3;
then Mid a,c,e3 by A7,DIRAF:def 3;
then
A29: e3,c,a are_collinear by DIRAF:9,28;
A30: e3,c,c are_collinear by DIRAF:31;
e3,c,b are_collinear by A2,DIRAF:9,28;
hence contradiction by A5,A3,A29,A30,DIRAF:32;
end;
then
A31: e4<>e5 by A26,DIRAF:8;
A32: e1<>e4 by A25,A11,DIRAF:8;
A33: not e1,e4,e3 are_collinear
proof
e4,c,e1 are_collinear by A25,DIRAF:28;
then
A34: e4,e1,c are_collinear by DIRAF:30;
assume e1,e4,e3 are_collinear ;
then
A35: e4,e1,e3 are_collinear by DIRAF:30;
e4,e1,e4 are_collinear by DIRAF:31;
hence contradiction by A32,A13,A35,A34,DIRAF:32;
end;
A36: not e1,e5,e4 are_collinear
proof
e4,e3,e5 are_collinear by A26,DIRAF:28;
then
A37: e5,e4,e3 are_collinear by DIRAF:30;
assume e1,e5,e4 are_collinear;
then
A38: e5,e4,e1 are_collinear by DIRAF:30;
e5,e4,e4 are_collinear by DIRAF:31;
hence contradiction by A31,A33,A38,A37,DIRAF:32;
end;
then
A39: e1<>e5 by DIRAF:31;
Mid e1,c,e4 by A25,DIRAF:9;
then consider e6 such that
A40: Mid e1,e6,e5 and
A41: e5,e4 // e6,c by A36,Th21;
A42: c <>e1 by A19,A20,DIRAF:8;
A43: not c,e1,b are_collinear
proof
c,a,e1 are_collinear by A19,DIRAF:28;
then
A44: c,e1,a are_collinear by DIRAF:30;
A45: c,e1,c are_collinear by DIRAF:31;
assume c,e1,b are_collinear;
hence contradiction by A5,A42,A44,A45,DIRAF:32;
end;
A46: e5<>e3
proof
assume e5=e3;
then e3,c // e3,e1 by A27,DIRAF:2;
then Mid e3,c,e1 or Mid e3,e1,c by DIRAF:7;
then e3,c,e1 are_collinear or e3,e1,c are_collinear by DIRAF:28;
then
A47: e3,c,e1 are_collinear by DIRAF:30;
A48: e3,c,c are_collinear by DIRAF:31;
e3,c,b are_collinear by A2,DIRAF:9,28;
hence contradiction by A3,A43,A47,A48,DIRAF:32;
end;
A49: e1<>e6
proof
Mid e5,e3,e4 by A26,DIRAF:9;
then
A50: e5,e3 // e3,e4 by DIRAF:def 3;
then e5,e3 // e5,e4 by ANALOAF:def 5;
then
A51: e5,e4 // e3,e4 by A46,A50,ANALOAF:def 5;
assume e1=e6;
then e3,e4 // e1,c by A31,A41,A51,ANALOAF:def 5;
then
A52: a,b // e1,c by A8,A28,DIRAF:3;
Mid e1,a,c by A19,DIRAF:9;
then
A53: e1,a // a,c by DIRAF:def 3;
then e1,a // e1,c by ANALOAF:def 5;
then e1,c // a,c by A20,A53,ANALOAF:def 5;
then a,b // a,c by A42,A52,DIRAF:3;
then a,b // b,c or a,c // c,b by DIRAF:6;
then Mid a,b,c or Mid a,c,b by DIRAF:def 3;
then a,b,c are_collinear or a,c,b are_collinear by DIRAF:28;
hence contradiction by A5,DIRAF:30;
end;
consider x such that
A54: Mid c,x,e6 and
A55: e1,e6 // a,x by A19,Th19;
e1,e6 // e6,e5 by A40,DIRAF:def 3;
then e1,e6 // e1,e5 by ANALOAF:def 5;
then e1,e5 // a,x by A55,A49,ANALOAF:def 5;
then c,e3 // a,x by A27,A39,DIRAF:3;
then
A56: a,x // b,c by A3,A18,ANALOAF:def 5;
A57: e6<>c
proof
assume e6=c;
then x=c by A54,DIRAF:8;
then c,a // c,b by A56,DIRAF:2;
then Mid c,a,b or Mid c,b,a by DIRAF:7;
then c,a,b are_collinear or c,b,a are_collinear by DIRAF:28;
hence contradiction by A5,DIRAF:30;
end;
A58: a<>e2
proof
assume
A59: a=e2;
e1,a // a,c by A21,DIRAF:2;
then b,c // a,c by A20,A24,A59,DIRAF:3;
then c,b // c,a by DIRAF:2;
then Mid c,b,a or Mid c,a,b by DIRAF:7;
then c,b,a are_collinear or c,a,b are_collinear by DIRAF:28;
hence contradiction by A5,DIRAF:30;
end;
A60: e6<>x
proof
assume e6=x;
then e6,e1 // e6,a by A55,DIRAF:2;
then Mid e6,e1,a or Mid e6,a,e1 by DIRAF:7;
then e6,e1,a are_collinear or e6,a,e1 are_collinear by DIRAF:28;
then
A61: e6,e1,a are_collinear by DIRAF:30;
e1,e6,e5 are_collinear by A40,DIRAF:28;
then
A62: e6,e1,e5 are_collinear by DIRAF:30;
b,c // e1,e5 by A3,A4,A27,DIRAF:3;
then e1,e2 // e1,e5 by A6,A24,ANALOAF:def 5;
then Mid e1,e2,e5 or Mid e1,e5,e2 by DIRAF:7;
then e1,e2,e5 are_collinear or e1,e5,e2 are_collinear by DIRAF:28;
then
A63: e1,e5,e2 are_collinear by DIRAF:30;
A64: e1,e5,e1 are_collinear by DIRAF:31;
Mid b,a,e2 by A23,DIRAF:def 3;
then b,a,e2 are_collinear by DIRAF:28;
then
A65: a,e2,b are_collinear by DIRAF:30;
c,a,e1 are_collinear by A19,DIRAF:28;
then
A66: a,e1,c are_collinear by DIRAF:30;
e6,e1,e1 are_collinear by DIRAF:31;
then e1,e5,a are_collinear by A49,A61,A62,DIRAF:32;
then
A67: a,e1,e2 are_collinear by A39,A63,A64,DIRAF:32;
A68: a,e2,a are_collinear by DIRAF:31;
a,e1,a are_collinear by DIRAF:31;
then a,e2,c are_collinear by A20,A67,A66,DIRAF:32;
hence contradiction by A5,A58,A65,A68,DIRAF:32;
end;
Mid e6,x,c by A54,DIRAF:9;
then
A69: e6,x // x,c by DIRAF:def 3;
then e6,x // e6,c by ANALOAF:def 5;
then
A70: e6,c // x,c by A60,A69,ANALOAF:def 5;
Mid e5,e3,e4 by A26,DIRAF:9;
then
A71: e5,e3 // e3,e4 by DIRAF:def 3;
then e5,e3 // e5,e4 by ANALOAF:def 5;
then e3,e4 // e5,e4 by A46,A71,ANALOAF:def 5;
then a,b // e5,e4 by A8,A28,DIRAF:3;
then a,b // e6,c by A31,A41,DIRAF:3;
then a,b // x,c by A57,A70,DIRAF:3;
hence thesis by A56;
end;
now
A72: now
assume Mid a,c,b;
then a,c // c,b by DIRAF:def 3;
then a,c // a,b by ANALOAF:def 5;
hence a,a // b,c & a,b // a,c by DIRAF:2,4;
end;
A73: now
assume Mid b,a,c;
then Mid c,a,b by DIRAF:9;
then c,a // a,b by DIRAF:def 3;
then c,a // c,b by ANALOAF:def 5;
hence a,c // b,c & a,b // c,c by DIRAF:2,4;
end;
A74: Mid a,b,c implies a,b // b,c & a,b // b,c by DIRAF:def 3;
assume a,b,c are_collinear;
hence thesis by A74,A73,A72,DIRAF:29;
end;
hence thesis by A1;
end;
theorem Th23:
a,b // c,d & not a,b,c are_collinear implies ex x st Mid a,x,d & Mid b,x,c
proof
assume that
A1: a,b // c,d and
A2: not a,b,c are_collinear;
A3: now
consider e1 such that
A4: a,b // d,e1 and
A5: a,d // b,e1 and
A6: b<>e1 by ANALOAF:def 5;
A7: a<>b by A2,DIRAF:31;
then c,d // d,e1 by A1,A4,ANALOAF:def 5;
then
A8: Mid c,d,e1 by DIRAF:def 3;
A9: a<>d
proof
assume a=d;
then b,a // a,c by A1,DIRAF:2;
then Mid b,a,c by DIRAF:def 3;
then b,a,c are_collinear by DIRAF:28;
hence contradiction by A2,DIRAF:30;
end;
A10: not a,b,d are_collinear
proof
A11: now
assume a,b // a,d;
then c,d // a,d by A1,A7,ANALOAF:def 5;
then d,c // d,a by DIRAF:2;
then d,c '||' d,a by DIRAF:def 4;
hence d,c,a are_collinear by DIRAF:def 5;
end;
A12: d,a,a are_collinear by DIRAF:31;
A13: now
assume a,b // d,a;
then c,d // d,a by A1,A7,ANALOAF:def 5;
then Mid c,d,a by DIRAF:def 3;
then c,d,a are_collinear by DIRAF:28;
hence d,c,a are_collinear by DIRAF:30;
end;
assume
A14: a,b,d are_collinear;
then
A15: d,a,b are_collinear by DIRAF:30;
a,b '||' a,d by A14,DIRAF:def 5;
then d,a,c are_collinear by A11,A13,DIRAF:30,def 4;
hence contradiction by A2,A9,A12,A15,DIRAF:32;
end;
consider e2 such that
A16: c,d // b,e2 and
A17: c,b // d,e2 and
A18: d<>e2 by ANALOAF:def 5;
assume
A19: c <>d;
then a,b // b,e2 by A1,A16,DIRAF:3;
then
A20: Mid a,b,e2 by DIRAF:def 3;
A21: not c,d,b are_collinear
proof
A22: now
assume c,d // c,b;
then a,b // c,b by A1,A19,DIRAF:3;
then b,a // b,c by DIRAF:2;
then Mid b,a,c or Mid b,c,a by DIRAF:7;
then b,a,c are_collinear or b,c,a are_collinear by DIRAF:28;
hence contradiction by A2,DIRAF:30;
end;
assume c,d,b are_collinear;
then c,d '||' c,b by DIRAF:def 5;
then c,d // c,b or c,d // b,c by DIRAF:def 4;
then a,b // b,c by A1,A19,A22,DIRAF:3;
then Mid a,b,c by DIRAF:def 3;
hence contradiction by A2,DIRAF:28;
end;
A23: b,c,c are_collinear by DIRAF:31;
A24: d,a,a are_collinear by DIRAF:31;
A25: c <>e1
proof
assume c =e1;
then c,d // d,c by A1,A4,A7,ANALOAF:def 5;
hence contradiction by A19,ANALOAF:def 5;
end;
not c,b,e1 are_collinear
proof
c,d,e1 are_collinear by A8,DIRAF:28;
then
A26: c,e1,d are_collinear by DIRAF:30;
assume c,b,e1 are_collinear;
then
A27: c,e1,b are_collinear by DIRAF:30;
c,e1,c are_collinear by DIRAF:31;
hence contradiction by A25,A21,A27,A26,DIRAF:32;
end;
then consider x such that
A28: Mid c,x,b and
A29: b,e1 // x,d by A8,Th21;
A30: Mid b,x,c by A28,DIRAF:9;
a,d // x,d by A5,A6,A29,DIRAF:3;
then d,a // d,x by DIRAF:2;
then Mid d,a,x or Mid d,x,a by DIRAF:7;
then d,a,x are_collinear or d,x,a are_collinear by DIRAF:28;
then
A31: d,a,x are_collinear by DIRAF:30;
A32: b<>c by A2,DIRAF:31;
A33: a<>e2
proof
assume a=e2;
then a,b // b,a by A1,A19,A16,DIRAF:3;
hence contradiction by A7,ANALOAF:def 5;
end;
not a,d,e2 are_collinear
proof
a,b,e2 are_collinear by A20,DIRAF:28;
then
A34: a,e2,b are_collinear by DIRAF:30;
assume a,d,e2 are_collinear;
then
A35: a,e2,d are_collinear by DIRAF:30;
a,e2,a are_collinear by DIRAF:31;
hence contradiction by A33,A10,A35,A34,DIRAF:32;
end;
then consider y such that
A36: Mid a,y,d and
A37: d,e2 // y,b by A20,Th21;
A38: b,c,b are_collinear by DIRAF:31;
c,b // y,b by A17,A18,A37,DIRAF:3;
then b,c // b,y by DIRAF:2;
then Mid b,c,y or Mid b,y,c by DIRAF:7;
then b,c,y are_collinear or b,y,c are_collinear by DIRAF:28;
then
A39: b,c,y are_collinear by DIRAF:30;
A40: c,x,b are_collinear by A28,DIRAF:28;
then b,c,x are_collinear by DIRAF:30;
then
A41: x,y,c are_collinear by A32,A39,A23,DIRAF:32;
a,y,d are_collinear by A36,DIRAF:28;
then d,a,y are_collinear by DIRAF:30;
then
A42: x,y,a are_collinear by A9,A31,A24,DIRAF:32;
b,c,x are_collinear by A40,DIRAF:30;
then x,y,b are_collinear by A32,A39,A38,DIRAF:32;
then Mid a,x,d by A2,A36,A42,A41,DIRAF:32;
hence thesis by A30;
end;
now
assume
A43: c =d;
take x=c;
thus Mid a,x,d & Mid b,x,c by A43,DIRAF:10;
end;
hence thesis by A3;
end;
theorem
OAS is Fanoian
by Th23;
theorem
a,b '||' c,d & a,c '||' b,d & not a,b,c are_collinear implies
ex x st x,a,d are_collinear
& x,b,c are_collinear
proof
assume that
A1: a,b '||' c,d and
A2: a,c '||' b,d and
A3: not a,b,c are_collinear;
a,b // c,d by A1,A2,A3,Th14;
then consider x such that
A4: Mid a,x,d and
A5: Mid b,x,c by A3,Th23;
b,x,c are_collinear by A5,DIRAF:28;
then
A6: x,b,c are_collinear by DIRAF:30;
a,x,d are_collinear by A4,DIRAF:28;
then x,a,d are_collinear by DIRAF:30;
hence thesis by A6;
end;
theorem
a,b '||' c,d & not a,b,c are_collinear & p,a,d are_collinear &
p,b,c are_collinear implies not p,a,b are_collinear
proof
assume that
A1: a,b '||' c,d and
A2: not a,b,c are_collinear and
A3: p,a,d are_collinear and
A4: p,b,c are_collinear;
A5: p,a,a are_collinear by DIRAF:31;
assume p,a,b are_collinear;
then
A6: a,b,d are_collinear by A2,A3,A4,A5,DIRAF:32;
A7: a,b '||' d,c by A1,DIRAF:22;
a<>b by A2,DIRAF:31;
hence contradiction by A2,A6,A7,DIRAF:33;
end;
theorem Th27:
Mid a,b,d & Mid b,x,c & not a,b,c are_collinear implies
ex y st Mid a,y,c & Mid y,x,d
proof
assume that
A1: Mid a,b,d and
A2: Mid b,x,c and
A3: not a,b,c are_collinear;
A4: now
assume
A5: b=d;
take y=c;
thus Mid a,y,c & Mid d,x,y by A2,A5,DIRAF:10;
thus Mid a,y,c & Mid y,x,d by A2,A5,DIRAF:9,10;
end;
A6: Mid d,b,a by A1,DIRAF:9;
A7: now
assume that
A8: b<>d and
A9: x<>b;
d,b // b,a by A6,DIRAF:def 3;
then consider e1 such that
A10: x,b // b,e1 and
A11: x,d // a,e1 by A8,ANALOAF:def 5;
A12: Mid x,b,e1 by A10,DIRAF:def 3;
then
A13: Mid e1,b,x by DIRAF:9;
then
A14: Mid e1,x,c by A2,A9,DIRAF:12;
A15: c <>e1
proof
assume c =e1;
then Mid x,b,x by A2,A9,A13,DIRAF:8,12;
hence contradiction by A9,DIRAF:8;
end;
A16: x<>e1 by A9,A12,DIRAF:8;
A17: not c,a,e1 are_collinear
proof
x,b,e1 are_collinear by A12,DIRAF:28;
then
A18: x,e1,b are_collinear by DIRAF:30;
assume c,a,e1 are_collinear;
then
A19: c,e1,a are_collinear by DIRAF:30;
c,x,e1 are_collinear by A14,DIRAF:9,28;
then
A20: c,e1,x are_collinear by DIRAF:30;
A21: c,e1,c are_collinear by DIRAF:31;
c,e1,e1 are_collinear by DIRAF:31;
then c,e1,b are_collinear by A16,A20,A18,DIRAF:35;
hence contradiction by A3,A15,A19,A21,DIRAF:32;
end;
Mid c,x,e1 by A14,DIRAF:9;
then consider y such that
A22: Mid c,y,a and
A23: a,e1 // y,x by A17,Th21;
a<>e1 by A17,DIRAF:31;
then x,d // y,x by A11,A23,DIRAF:3;
then d,x // x,y by DIRAF:2;
then Mid d,x,y by DIRAF:def 3;
then
A24: Mid y,x,d by DIRAF:9;
Mid a,y,c by A22,DIRAF:9;
hence thesis by A24;
end;
now
assume that
b<>d and
A25: x=b;
take y=a;
thus Mid a,y,c & Mid y,x,d by A1,A25,DIRAF:10;
end;
hence thesis by A7,A4;
end;
theorem
OAS is satisfying_Ext_Bet_Pasch
by Th27;
theorem Th29:
Mid a,b,d & Mid a,x,c & not a,b,c are_collinear implies
ex y st Mid b,y,c & Mid x,y,d
proof
assume that
A1: Mid a,b,d and
A2: Mid a,x,c and
A3: not a,b,c are_collinear;
A4: b<>c by A3,DIRAF:31;
A5: a<>b by A3,DIRAF:31;
A6: now
assume that
A7: b<>d and
A8: x<>c and
A9: a<>x;
A10: a<>d by A1,A7,DIRAF:8;
consider e1 such that
A11: Mid a,d,e1 and
A12: x,d // c,e1 by A2,A9,Th20;
A13: Mid e1,d,a by A11,DIRAF:9;
A14: d,b,a are_collinear by A1,DIRAF:9,28;
A15: not a,x,b are_collinear
proof
A16: a,x,a are_collinear by DIRAF:31;
assume
A17: a,x,b are_collinear;
a,x,c are_collinear by A2,DIRAF:28;
hence contradiction by A3,A9,A17,A16,DIRAF:32;
end;
A18: not x,d,a are_collinear
proof
assume x,d,a are_collinear;
then
A19: d,a,x are_collinear by DIRAF:30;
A20: d,a,a are_collinear by DIRAF:31;
d,a,b are_collinear by A14,DIRAF:30;
hence contradiction by A10,A15,A19,A20,DIRAF:32;
end;
then
A21: x<>d by DIRAF:31;
A22: Mid d,b,a by A1,DIRAF:9;
Mid b,d,e1 by A1,A11,DIRAF:11;
then Mid e1,d,b by DIRAF:9;
then Mid e1,b,a by A22,A13,DIRAF:12;
then
A23: e1,b // b,a by DIRAF:def 3;
e1<>b by A7,A22,A13,DIRAF:14;
then consider e2 such that
A24: c,b // b,e2 and
A25: c,e1 // a,e2 by A23,ANALOAF:def 5;
A26: Mid c,b,e2 by A24,DIRAF:def 3;
then
A27: c,b,e2 are_collinear by DIRAF:28;
Mid c,x,a by A2,DIRAF:9;
then consider y such that
A28: Mid c,y,e2 and
A29: a,e2 // x,y by Th19;
A30: Mid c,b,y or Mid c,y,b by A26,A28,DIRAF:17;
A31: c <>e2 by A4,A24,ANALOAF:def 5;
A32: now
c,b,e2 are_collinear by A26,DIRAF:28;
then
A33: c,e2,b are_collinear by DIRAF:30;
c,y,e2 are_collinear by A28,DIRAF:28;
then
A34: c,e2,y are_collinear by DIRAF:30;
c,e2,c are_collinear by DIRAF:31;
then
A35: b,y,c are_collinear by A31,A34,A33,DIRAF:32;
a,x,c are_collinear by A2,DIRAF:28;
then
A36: x,a,c are_collinear by DIRAF:30;
A37: Mid c,x,a by A2,DIRAF:9;
assume
A38: Mid x,d,y;
then consider c9 such that
A39: Mid x,c9,a and
A40: Mid c9,b,y by A22,A18,Th27;
x,c9,a are_collinear by A39,DIRAF:28;
then
A41: x,a,c9 are_collinear by DIRAF:30;
A42: b<>y
proof
assume b=y;
then x,d,b are_collinear by A38,DIRAF:28;
then
A43: d,b,x are_collinear by DIRAF:30;
A44: d,b,b are_collinear by DIRAF:31;
a,x,c are_collinear by A2,DIRAF:28;
then d,b,c are_collinear by A9,A14,A43,DIRAF:35;
hence contradiction by A3,A7,A14,A44,DIRAF:32;
end;
c9,b,y are_collinear by A40,DIRAF:28;
then
A45: b,y,c9 are_collinear by DIRAF:30;
then
A46: c,c9,c are_collinear by A42,A35,DIRAF:32;
b,y,b are_collinear by DIRAF:31;
then
A47: c,c9,b are_collinear by A42,A35,A45,DIRAF:32;
x,a,a are_collinear by DIRAF:31;
then c,c9,a are_collinear by A9,A36,A41,DIRAF:32;
then Mid x,c,a by A3,A39,A47,A46,DIRAF:32;
hence contradiction by A8,A37,DIRAF:14;
end;
A48: a<>e2
proof
assume a=e2;
then Mid c,b,a by A24,DIRAF:def 3;
hence contradiction by A3,DIRAF:9,28;
end;
A49: e1,d,a are_collinear by A11,DIRAF:9,28;
A50: c <>e1
proof
assume c =e1;
then
A51: d,a,c are_collinear by A49,DIRAF:30;
A52: d,a,a are_collinear by DIRAF:31;
d,a,b are_collinear by A14,DIRAF:30;
hence contradiction by A3,A10,A51,A52,DIRAF:32;
end;
then x,d // a,e2 by A12,A25,DIRAF:3;
then x,d // x,y by A48,A29,DIRAF:3;
then
A53: Mid x,d,y or Mid x,y,d by DIRAF:7;
then
A54: Mid d,y,x by A32,DIRAF:9;
now
A55: b<>e2
proof
A56: a,b // b,d by A1,DIRAF:def 3;
assume
A57: b=e2;
c,e1 // x,d by A12,DIRAF:2;
then a,b // x,d by A25,A50,A57,ANALOAF:def 5;
then x,d // b,d by A5,A56,ANALOAF:def 5;
then d,x // d,b by DIRAF:2;
then Mid d,x,b or Mid d,b,x by DIRAF:7;
then d,x,b are_collinear or d,b,x are_collinear by DIRAF:28;
then
A58: d,b,x are_collinear by DIRAF:30;
d,b,b are_collinear by DIRAF:31;
then
A59: a,x,b are_collinear by A7,A14,A58,DIRAF:32;
A60: a,x,c are_collinear by A2,DIRAF:28;
a,x,a are_collinear by A7,A14,A58,DIRAF:32;
hence contradiction by A3,A9,A59,A60,DIRAF:32;
end;
A61: b,d,a are_collinear by A14,DIRAF:30;
A62: y<>d
proof
A63: c,e2,c are_collinear by DIRAF:31;
A64: c,e2,b are_collinear by A27,DIRAF:30;
assume y=d;
then c,d,e2 are_collinear by A28,DIRAF:28;
then c,e2,d are_collinear by DIRAF:30;
then c,e2,a are_collinear by A7,A14,A64,DIRAF:35;
hence contradiction by A3,A31,A64,A63,DIRAF:32;
end;
A65: b,e2,c are_collinear by A27,DIRAF:30;
assume
A66: not Mid c,y,b;
then
A67: y<>b by DIRAF:10;
Mid b,y,e2 by A28,A30,A66,DIRAF:11;
then consider z such that
A68: Mid b,d,z and
A69: y,d // e2,z by A67,Th20;
A70: a,e2,a are_collinear by DIRAF:31;
A71: now
assume
A72: a=z;
Mid d,b,a by A1,DIRAF:9;
hence contradiction by A7,A68,A72,DIRAF:14;
end;
d,y // y,x by A54,DIRAF:def 3;
then d,y // d,x by ANALOAF:def 5;
then y,d // x,d by DIRAF:2;
then y,d // c,e1 by A12,A21,DIRAF:3;
then c,e1 // e2,z by A69,A62,ANALOAF:def 5;
then a,e2 // e2,z by A25,A50,ANALOAF:def 5;
then Mid a,e2,z by DIRAF:def 3;
then a,e2,z are_collinear by DIRAF:28;
then
A73: a,z,e2 are_collinear by DIRAF:30;
A74: b,d,z are_collinear by A68,DIRAF:28;
then
A75: a,z,a are_collinear by A7,A61,DIRAF:32;
b,d,b are_collinear by DIRAF:31;
then a,z,b are_collinear by A7,A74,A61,DIRAF:32;
then
A76: a,e2,b are_collinear by A73,A75,A71,DIRAF:32;
a,e2,e2 are_collinear by A73,A75,A71,DIRAF:32;
then a,e2,c are_collinear by A55,A76,A65,DIRAF:35;
hence contradiction by A3,A48,A76,A70,DIRAF:32;
end;
then Mid b,y,c by DIRAF:9;
hence thesis by A53,A32;
end;
A77: b=d implies Mid b,d,c & Mid x,d,d by DIRAF:10;
A78: x=c implies Mid b,c,c & Mid x,c,d by DIRAF:10;
a=x implies Mid b,b,c & Mid x,b,d by A1,DIRAF:10;
hence thesis by A6,A77,A78;
end;
theorem
OAS is satisfying_Int_Bet_Pasch
by Th29;
theorem
Mid p,a,b & p,a // p9,a9 & not p,a,p9 are_collinear &
p9,a9,b9 are_collinear & p,p9 // a,a9 & p,p9 // b,b9 implies Mid p9,a9,b9
proof
assume that
A1: Mid p,a,b and
A2: p,a // p9,a9 and
A3: not p,a,p9 are_collinear and
A4: p9,a9,b9 are_collinear and
A5: p,p9 // a,a9 and
A6: p,p9 // b,b9;
A7: p<>a by A3,DIRAF:31;
A8: p<>p9 by A3,DIRAF:31;
A9: p,a,b are_collinear by A1,DIRAF:28;
then
A10: p,b,a are_collinear by DIRAF:30;
now
A11: p<>b by A1,A7,DIRAF:8;
A12: p9<>b9
proof
assume
A13: p9=b9;
then b9,p // b9,b by A6,DIRAF:2;
then Mid b9,p,b or Mid b9,b,p by DIRAF:7;
then b9,p,b are_collinear or b9,b,p are_collinear by DIRAF:28;
then
A14: p,b,b9 are_collinear by DIRAF:30;
p,b,p are_collinear by DIRAF:31;
hence contradiction by A3,A10,A11,A13,A14,DIRAF:32;
end;
A15: not p,a,a9 are_collinear
proof
assume
A16: p,a,a9 are_collinear;
p,a '||' a9,p9 by A2,DIRAF:def 4;
hence contradiction by A3,A7,A16,DIRAF:33;
end;
then
A17: a<>a9 by DIRAF:31;
A18: now
a,a9 // p,p9 by A5,DIRAF:2;
then
A19: a,a9 '||' p9,p by DIRAF:def 4;
assume a,a9,p9 are_collinear;
then a,a9,p are_collinear by A17,A19,DIRAF:33;
hence contradiction by A15,DIRAF:30;
end;
assume that
A20: p9<>a9 and
a9<>b9;
consider x such that
A21: Mid p,x,b9 and
A22: b,b9 // a,x by A1,Th19;
Mid b9,x,p by A21,DIRAF:9;
then consider y such that
A23: Mid b9,y,p9 and
A24: p,p9 // x,y by Th19;
b9,y,p9 are_collinear by A23,DIRAF:28;
then
A25: p9,b9,y are_collinear by DIRAF:30;
A26: b<>b9
proof
assume b=b9;
then a9,p9,b are_collinear by A4,DIRAF:30;
then a9,p9 '||' a9,b by DIRAF:def 5;
then a9,p9 // a9,b or a9,p9 // b,a9 by DIRAF:def 4;
then p9,a9 // a9,b or p9,a9 // b,a9 by DIRAF:2;
then p,a // a9,b or p,a // b,a9 by A2,A20,DIRAF:3;
then p,a '||' b,a9 by DIRAF:def 4;
hence contradiction by A1,A7,A15,DIRAF:28,33;
end;
A27: x<>a
proof
assume x=a;
then
A28: p,a,b9 are_collinear by A21,DIRAF:28;
p,a,a are_collinear by DIRAF:31;
then
A29: b,b9,a are_collinear by A7,A9,A28,DIRAF:32;
p,a,p are_collinear by DIRAF:31;
then
A30: b,b9,p are_collinear by A7,A9,A28,DIRAF:32;
b,b9 // p,p9 by A6,DIRAF:2;
then b,b9 '||' p,p9 by DIRAF:def 4;
then b,b9,p9 are_collinear by A26,A30,DIRAF:33;
hence contradiction by A3,A26,A29,A30,DIRAF:32;
end;
A31: p9,b9,a9 are_collinear by A4,DIRAF:30;
then
A32: y,a9,a9 are_collinear by A12,A25,DIRAF:32;
A33: p,p9 // a,x by A6,A22,A26,DIRAF:3;
then a,x // x,y by A8,A24,ANALOAF:def 5;
then a,x // a,y by ANALOAF:def 5;
then p,p9 // a,y by A27,A33,DIRAF:3;
then a,y // a,a9 by A5,A8,ANALOAF:def 5;
then a,y '||' a,a9 by DIRAF:def 4;
then a,y,a9 are_collinear by DIRAF:def 5;
then
A34: y,a9,a are_collinear by DIRAF:30;
p9,b9,p9 are_collinear by DIRAF:31;
then y,a9,p9 are_collinear by A12,A25,A31,DIRAF:32;
then y=a9 or a,a9,p9 are_collinear by A34,A32,DIRAF:32;
hence thesis by A23,A18,DIRAF:9;
end;
hence thesis by DIRAF:10;
end;