:: Tarski Geometry Axioms -- Part {II} :: by Roland Coghetto and Adam Grabowski :: :: Received June 30, 2016 :: Copyright (c) 2016 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 TARSKI, NUMBERS, SUBSET_1, COMPLEX1, REAL_1, RELAT_1, CARD_1, ARYTM_1, SUPINF_2, XXREAL_2, NAT_1, ARYTM_3, SQUARE_1, XXREAL_0, XBOOLE_0, RLTOPSP1, PRE_TOPC, MCART_1, EUCLID, INCSP_1, METRIC_1, SIN_COS, COMPLEX2, PROJPL_1, GTARSKI1, PBOOLE, FINSEQ_2, QC_LANG1, GTARSKI2, FUNCT_1, ROUGHS_4, RELAT_2, LATTICE3, EUCLIDLP, EUCLID12, MEMBERED, ORDINAL2, ANALOAF, PASCH, RLVECT_1, ZFMISC_1, DIRAF, PENCIL_1, PARSP_1; notations XBOOLE_0, ORDINAL1, SUBSET_1, XXREAL_2, MEMBERED, TARSKI, XCMPLX_0, NUMBERS, XREAL_0, COMPLEX1, METRIC_1, STRUCT_0, FINSEQ_2, SQUARE_1, RVSUM_1, PRE_TOPC, XXREAL_0, RLVECT_1, SIN_COS, EUCLID_3, EUCLID_6, GTARSKI1, EUCLID, BINOP_1, TOPREAL6, ANALOAF, DIRAF, PASCH, EUCLID12, EUCLIDLP, EUCLID_4, RLTOPSP1; constructors SQUARE_1, COMPLEX1, MONOID_0, SIN_COS, EUCLID_3, TOPREAL6, GTARSKI1, SEQ_4, PASCH, DIRAF, EUCLID12, EUCLID_4; registrations EUCLIDLP, RLTOPSP1, MONOID_0, RELSET_1, XXREAL_0, XREAL_0, EUCLID, VALUED_0, SQUARE_1, ORDINAL1, SIN_COS, GTARSKI1, XCMPLX_0, RLVECT_1, STRUCT_0, ZFMISC_1, ANALOAF, XXREAL_2, MEMBERED; requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL; definitions TARSKI, GTARSKI1, MEMBERED, XXREAL_2; equalities XBOOLE_0, EUCLID, VALUED_1, XCMPLX_0, RLVECT_1, ANALOAF; expansions TARSKI, XBOOLE_0, GTARSKI1, SUBSET_1, ANALOAF, DIRAF, PASCH; theorems XREAL_1, XXREAL_0, ZFMISC_1, XBOOLE_0, XBOOLE_1, EUCLID11, SQUARE_1, XCMPLX_1, RVSUM_1, TARSKI, EUCLID, RLTOPSP1, EUCLID_6, SIN_COS, EUCLID10, TOPREAL6, METRIC_1, COMPLEX1, GTARSKI1, TOPREAL3, EUCLID12, XCMPLX_0, XXREAL_2, ANALOAF, PASCH, RLVECT_1, FINSEQ_1, DIRAF, XTUPLE_0, EUCLIDLP, TOPREAL9; begin :: Preliminaries theorem Th1: for r,s,t,u being Real st s <> 0 & t <> 0 & r^2 = s^2 + t^2 - 2*s*t*u holds u = (r^2 - s^2 - t^2)/(-2*s*t) proof let r,s,t,u be Real; assume that A1: s <> 0 and A2: t <> 0 and A3: r^2 = s^2+t^2-2*s*t*u; r^2-s^2-t^2 = u * (-2*s*t) by A3; hence thesis by A1,A2,XCMPLX_1:89; end; theorem THJE: for n being Nat for u,v being Element of TOP-REAL n holds u + 0 * v = u proof let n be Nat; let u,v be Element of TOP-REAL n; 0.TOP-REAL n = 0 * v by RLVECT_1:10; hence thesis; end; theorem THJC: for n being Nat for r,s being Real, u,v,w being Element of TOP-REAL n st r * u - r * v = s * w - s * u holds (r + s) * u = r * v + s * w proof let n be Nat; let r,s be Real, u,v,w be Element of TOP-REAL n; assume r * u - r * v = s * w - s * u; then r * u - r * v + s * u = s * w + (- s * u + s * u) by RVSUM_1:15 .= s * w + ((- 1)* s * u + s * u) by RVSUM_1:49 .= s * w + (- s + s) * u by RVSUM_1:50 .= s * w by THJE; then s * w + r * v = r * u + ((-1)* r * v) + s * u + r * v by RVSUM_1:49 .= r * u + s * u + ((-1)* r * v) + r * v by RVSUM_1:15 .= r * u + s * u + (((-1)* r * v) + r * v) by RVSUM_1:15 .= r * u + s * u + (- r + r) * v by RVSUM_1:50 .= (r * u + s * u) by THJE; hence thesis by RVSUM_1:50; end; theorem THJD: for r,s being Real st 0 < r & 0 < s holds 0 <= r / (r+s) <= 1 proof let r,s be Real; assume that A1: 0 < r and A2: 0 < s; thus 0 <= r/(r+s) by A1,A2; 0 + r <= s + r by A2,XREAL_1:6; then r / (r+s) <= (r+s) / (r+s) by A1,XREAL_1:72; hence r / (r+s) <= 1 by A1,A2,XCMPLX_1:60; end; theorem Th2: for a being Real holds cos (3*PI - a) = -cos a proof let a be Real; cos(3*PI - a) = cos (2*PI + (PI -a)) .= cos (PI - a) by SIN_COS:79 .= - cos a by EUCLID10:2; hence thesis; end; theorem THSD2: for n being Nat for a,b,c being Element of TOP-REAL n st a - c = b - c holds a = b proof let n be Nat; let a,b,c be Element of TOP-REAL n; assume a - c = b - c; then a + (-c + c) = b - c + c by RLVECT_1:def 3; then a + 0.TOP-REAL n = b - c + c by RLVECT_1:5; then a = b + (- c + c) by RLVECT_1:def 3; then a = b + 0.TOP-REAL n by RLVECT_1:5; hence thesis; end; theorem ThWW: for n being Nat for a,b,c being Element of TOP-REAL n holds c - a - (b - a) = c - b proof let n be Nat; let a,b,c be Element of TOP-REAL n; thus c - a - (b - a) = (c - a) - b + a by RLVECT_1:29 .= c - a + a + - b by RLVECT_1:def 3 .= c + (- a + a) + - b by RLVECT_1:def 3 .= c + 0.TOP-REAL n + - b by RLVECT_1:5 .= c - b; end; theorem THYQ: for a,b,c,d being Real holds dist(|[a,b]|,|[c,d]|) = sqrt ((a-c)^2+(b-d)^2) proof let a,b,c,d be Real; A1: |[a,b]|`1 = a & |[a,b]|`2 = b & |[c,d]|`1 = c & |[c,d]|`2 = d by EUCLID:52; reconsider P = |[a,b]|,Q = |[c,d]| as Point of Euclid 2 by EUCLID:22; dist(|[a,b]|,|[c,d]|) = dist(P,Q) by TOPREAL6:def 1 .= (Pitag_dist 2).(P,Q) by METRIC_1:def 1 .= sqrt ((a-c)^2+(b - d)^2) by A1,TOPREAL3:7; hence thesis; end; theorem THY1: dist(|[0,0]|,|[1,0]|) = 1 proof dist(|[0,0]|,|[1,0]|) = sqrt ((0-1)^2+(0 - 0)^2) by THYQ .= sqrt ((-1) * (-1) + 0^2) by SQUARE_1:def 1 .= sqrt (1 + 0 * 0) by SQUARE_1:def 1 .= 1 by SQUARE_1:18; hence thesis; end; theorem THY2: dist(|[0,0]|,|[0,1]|) = 1 proof dist(|[0,0]|,|[0,1]|) = sqrt ((0-0)^2+(0 - 1)^2) by THYQ .= sqrt (0 * 0 + (-1)^2) by SQUARE_1:def 1 .= sqrt (0 + (-1) * (-1)) by SQUARE_1:def 1 .= 1 by SQUARE_1:18; hence thesis; end; theorem THY3: dist(|[1,0]|,|[0,1]|) = sqrt 2 proof dist(|[1,0]|,|[0,1]|) = sqrt ((1-0)^2+(0 - 1)^2) by THYQ .= sqrt (1^2+(1)^2) by SQUARE_1:3 .= sqrt (1 * 1 + 1^2) by SQUARE_1:def 1 .= sqrt (1 * 1 + 1 * 1) by SQUARE_1:def 1 .= sqrt 2; hence thesis; end; definition let n be Nat; func TarskiEuclidSpace n -> MetrTarskiStr equals the naturally_generated TarskiExtension of Euclid n; coherence; end; definition func TarskiEuclid2Space -> MetrTarskiStr equals TarskiEuclidSpace 2; :: the naturally_generated TarskiExtension of Euclid 2; coherence; end; begin registration let n be Nat; cluster TarskiEuclidSpace n -> non empty; coherence; end; registration cluster TarskiEuclid2Space -> Reflexive symmetric discerning; coherence; end; registration let n be Nat; cluster TarskiEuclidSpace n -> Reflexive symmetric discerning; coherence; end; definition let n be Nat; let P be POINT of TarskiEuclidSpace n; func #P -> Element of TOP-REAL n equals P; coherence proof the MetrStruct of TarskiEuclidSpace n = the MetrStruct of Euclid n by GTARSKI1:def 13; hence thesis by EUCLID:22; end; end; definition let P be POINT of TarskiEuclid2Space; func #P -> Element of TOP-REAL 2 equals P; coherence proof the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; hence thesis by EUCLID:22; end; end; definition let P be POINT of TarskiEuclid2Space; func @P -> Point of Euclid 2 equals P; coherence proof the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; hence thesis; end; end; definition let P be POINT of TarskiEuclid2Space; func %P -> Element of REAL 2 equals P; coherence proof the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; hence thesis; end; end; theorem ThEquiv: for n being Nat for p,q being POINT of TarskiEuclidSpace n, p1,q1 being Element of TOP-REAL n st p = p1 & q = q1 holds dist(p,q) = (Pitag_dist n).(p1, q1) & dist(p,q) = |. p1 - q1 .| proof let n be Nat; let p,q be POINT of TarskiEuclidSpace n, p1,q1 being Element of TOP-REAL n; assume A0: p = p1 & q = q1; A1: the MetrStruct of TarskiEuclidSpace n = the MetrStruct of Euclid n by GTARSKI1:def 13; then (Pitag_dist n).(p1, q1) = |. p1 - q1 .| by A0,EUCLID:def 6; hence thesis by A1,METRIC_1:def 1,A0; end; theorem ThLawOfCosines: for a, b, c, x being POINT of TarskiEuclid2Space holds (dist(c,a))^2 = (dist(a,b))^2 + (dist(b,c))^2 - 2 * dist(a,b) * dist(b,c) * cos angle( #a, #b, #c) proof let a, b, c, x be POINT of TarskiEuclid2Space; set ta = |.#a - #b.|, tb = |. #c - #b .|, tc = |.#c - #a.|; |.#a - #b.| = dist(a,b) & |. #c - #b .| = dist(c,b) & |.#c - #a.| = dist(c,a) by ThEquiv; hence thesis by EUCLID_6:7; end; theorem for a,b,c,d,e,f,g being POINT of TarskiEuclid2Space st #a, #b, #c is_a_triangle & angle( #a, #b, #c) < PI & angle( #e, #c, #a) = angle( #b,#c,#a) / 3 & angle( #c, #a, #e) = angle( #c, #a, #b) / 3 & angle( #a, #b, #f) = angle( #a, #b, #c) / 3 & angle( #f, #a, #b) = angle( #c, #a, #b) / 3 & angle( #b, #c, #g) = angle( #b, #c, #a) / 3 & angle( #g, #b, #c) = angle( #a, #b, #c) / 3 holds dist(f,e) = dist(g,f) & dist(f,e) = dist(e,g) & dist(g,f) = dist(e,g) proof let a,b,c,d,e,f,g be POINT of TarskiEuclid2Space; assume A1: #a, #b, #c is_a_triangle & angle( #a, #b, #c) < PI & angle( #e, #c, #a) = angle( #b,#c,#a) / 3 & angle( #c, #a, #e) = angle( #c, #a, #b) / 3 & angle( #a, #b, #f) = angle( #a, #b, #c) / 3 & angle( #f, #a, #b) = angle( #c, #a, #b) / 3 & angle( #b,#c, #g) = angle( #b, #c, #a) / 3 & angle( #g, #b, #c) = angle( #a, #b, #c) / 3; |.#f - #e.| = dist(f,e) & |. #g - #f .| = dist(g,f) & |.#e - #g.| = dist(e,g) by ThEquiv; hence thesis by A1,EUCLID11:23; end; theorem ThConv: for n being Nat for p,q being Element of TarskiEuclidSpace n, p1, q1 being Element of Euclid n st p = p1 & q = q1 holds dist(p,q) = dist(p1, q1) proof let n be Nat; let p,q be Element of TarskiEuclidSpace n; let p1,q1 be Element of Euclid n; assume A1: p = p1 & q = q1; thus dist(p,q) = (the distance of the MetrStruct of TarskiEuclidSpace n).(p,q) by METRIC_1:def 1 .= (the distance of the MetrStruct of Euclid n).(p,q) by GTARSKI1:def 13 .= dist(p1,q1) by METRIC_1:def 1,A1; end; theorem ThConv2: for p,q being POINT of TarskiEuclid2Space holds dist(p,q) = sqrt((( #p)`1-( #q)`1)^2 + ((( #p)`2-( #q)`2)^2)) proof let p,q be POINT of TarskiEuclid2Space; A1: the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; (Pitag_dist 2).( @p, @q) = sqrt(( ( #p)`1 - ( #q)`1)^2 + ( ( #p)`2 - ( #q)`2)^2) by TOPREAL3:7; hence thesis by A1,METRIC_1:def 1; end; theorem ThConv3: for A,B being POINT of TarskiEuclid2Space holds dist(A,B) = |. #A - #B .| & dist(A,B) = |. %A - %B .| proof let A,B be POINT of TarskiEuclid2Space; the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; then dist(A,B) = (Pitag_dist 2).( #A, #B) by METRIC_1:def 1 .= |. %A - %B .| by EUCLID:def 6; hence thesis; end; theorem ThConv4: for a,b,c,d being POINT of TarskiEuclid2Space holds |. #a - #b .| = |. #c - #d .| iff a,b equiv c,d proof let a,b,c,d be POINT of TarskiEuclid2Space; A1: dist(a,b) = |. #a - #b .| & dist(c,d) = |. #c - #d .| by ThConv3; thus |. #a - #b .|= |. #c - #d .| implies a,b equiv c,d by A1,GTARSKI1:def 15; assume a,b equiv c,d; hence thesis by A1,GTARSKI1:def 15; end; theorem ThConv5: for p,q,r being POINT of TarskiEuclid2Space holds p is_Between q,r iff #p in LSeg( #q, #r ) proof let p,q,r be POINT of TarskiEuclid2Space; A1: dist( #q,#p) = dist(@q,@p) & dist( #p,#r)=dist(@p,@r) & dist( #q, #r) = dist(@q,@r) by TOPREAL6:def 1; dist(q,p) = dist(@q,@p) & dist(p,r)=dist(@p,@r) & dist(q,r)=dist(@q,@r) by ThConv; hence thesis by A1,EUCLID12:12; end; reserve n for Nat; theorem ThConv6: for p,q,r being POINT of TarskiEuclid2Space holds between p,q,r iff #q in LSeg( #p, #r ) proof let p,q,r be POINT of TarskiEuclid2Space; hereby assume between p,q,r; then q is_Between p,r by GTARSKI1:def 15; hence #q in LSeg( #p,#r) by ThConv5; end; assume #q in LSeg( #p, #r); then q is_Between p,r by ThConv5; hence thesis by GTARSKI1:def 15; end; theorem ThConv7: for a,b being Point of TarskiEuclid2Space holds between a,a,b & between a,b,b proof let a,b be Point of TarskiEuclid2Space; #a in LSeg( #a,#b) by RLTOPSP1:68; hence between a,a,b by ThConv6; #b in LSeg( #a,#b) by RLTOPSP1:68; hence between a,b,b by ThConv6; end; theorem ThConv7bis: for a,b,c being Point of TarskiEuclid2Space st between a,b,c holds between c,b,a proof let a,b,c be Point of TarskiEuclid2Space; assume between a,b,c; then #b in LSeg( #a,#c) by ThConv6; hence thesis by ThConv6; end; theorem ThConv7ter: for a,b being Point of TarskiEuclid2Space st between a,b,a holds a = b proof let a,b be Point of TarskiEuclid2Space; assume between a,b,a; then #b in LSeg( #a,#a) by ThConv6; then #b in { #a } by RLTOPSP1:70; hence thesis by TARSKI:def 1; end; theorem ThEgal: for a, b being POINT of TarskiEuclid2Space holds a = b iff dist(a,b) = 0 proof let a, b be POINT of TarskiEuclid2Space; hereby assume a = b; then %a = %b; then 0 = |. #a - #b .|; hence dist(a,b) = 0 by ThEquiv; end; assume dist(a,b) = 0; hence thesis by METRIC_1:2; end; theorem ThNull: for a,b,c,d being POINT of TarskiEuclid2Space st dist(a,b) + dist(c,d) = 0 holds a = b & c = d proof let a,b,c,d be POINT of TarskiEuclid2Space; assume A1: dist(a,b) + dist(c,d) = 0; 0 <= dist(a,b) & 0 <= dist(c,d) by METRIC_1:5; then dist(a,b) = 0 & dist(c,d) = 0 by A1; hence thesis by ThEgal; end; theorem for a,b,c,a1,b1,c1 being POINT of TarskiEuclid2Space holds a,b,c cong a1,b1,c1 iff (dist(a,b) = dist(a1,b1) & dist(a,c) = dist(a1,c1) & dist(b,c) = dist(b1,c1)) by GTARSKI1:def 15; theorem ThConv8: for a,b,c being POINT of TarskiEuclid2Space holds between a,b,c iff dist(a,c) = dist(a,b) + dist(b,c) proof let a,b,c be POINT of TarskiEuclid2Space; hereby assume between a,b,c; then b is_Between a,c by GTARSKI1:def 15; hence dist(a,c) = dist(a,b) + dist(b,c); end; assume dist(a,c) = dist(a,b) + dist(b,c); then b is_Between a,c; hence thesis by GTARSKI1:def 15; end; theorem ThConv9: for a,b,c,d being POINT of TarskiEuclid2Space holds dist(a,b)^2 = dist(c,d)^2 iff a,b equiv c,d proof let a,b,c,d be POINT of TarskiEuclid2Space; hereby assume A1: dist(a,b)^2 = dist(c,d)^2; sqrt dist(a,b)^2 = dist(a,b) & sqrt dist(c,d)^2 = dist(c,d) by METRIC_1:5,SQUARE_1:22; hence a,b equiv c,d by A1,GTARSKI1:def 15; end; assume a,b equiv c,d; hence thesis by GTARSKI1:def 15; end; theorem for a being Point of TarskiEuclid2Space holds between a,a,a by ThConv7; ThCongruenceSymmetry: TarskiEuclid2Space is satisfying_CongruenceSymmetry proof for a,b being POINT of TarskiEuclid2Space holds a,b equiv b,a proof let a,b be POINT of TarskiEuclid2Space; dist(a,b) = dist(b,a); hence thesis by GTARSKI1:def 15; end; hence thesis; end; ThCongruenceEquivalenceRelation: TarskiEuclid2Space is satisfying_CongruenceEquivalenceRelation proof let a, b, p, q, r, s be POINT of TarskiEuclid2Space; assume a,b equiv p,q & a,b equiv r,s; then dist (a,b) = dist (p,q) & dist (a,b) = dist (r,s) by GTARSKI1:def 15; hence thesis by GTARSKI1:def 15; end; ThCongruenceIdentity: TarskiEuclid2Space is satisfying_CongruenceIdentity proof let a, b, c be POINT of TarskiEuclid2Space; assume a,b equiv c,c; then dist (a,b) = dist (c,c) by GTARSKI1:def 15; hence thesis by METRIC_1:2,1; end; ThSegmentConstruction: TarskiEuclid2Space is satisfying_SegmentConstruction proof A1: the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; let a, q, b, c be POINT of TarskiEuclid2Space; per cases; suppose A1bis: a = q; now set alpha = |. #b - #c .|; reconsider P = |[alpha,0]| as Element of TOP-REAL 2; reconsider x = |[ ( #a)`1 + alpha, ( #a)`2 ]| as POINT of TarskiEuclid2Space by A1,EUCLID:67; A2: ( #x)`1 = ( #a)`1 + alpha & ( #x)`2 = ( #a)`2 by EUCLID:52; A3: |. #a - #x .| = dist(a,x) by ThEquiv .= sqrt((( #a)`1 - (( #a)`1 + alpha))^2 + (( #a)`2 - ( #a)`2)^2) by A2,ThConv2 .= sqrt((0 - alpha)^2 + 0 * 0) by SQUARE_1:def 1 .= sqrt(alpha^2) by SQUARE_1:3 .= alpha by SQUARE_1:22; take x; thus between q,a,x by A1bis,ThConv7; thus a,x equiv b,c by A3,ThConv4; end; hence thesis; end; suppose A4: a <> q; A5: b = c implies thesis proof assume A6: b = c; set x = a; thus ex x being POINT of TarskiEuclid2Space st between q,a,x & a,x equiv b,c proof take x; A7: %a = %x; %b = %c by A6; then |. #b - #c .| = 0; then |. #a - #x .| = |. #b - #c .| by A7; hence thesis by ThConv7,ThConv4; end; end; b <> c implies thesis proof assume b <> c; then %b <> %c; then reconsider alpha = |. #b - #c .| as positive Real by EUCLID:17; %a <> %q by A4; then reconsider mu = |. #a - #q .| as positive Real by EUCLID:17; reconsider nu = alpha / mu as positive Real; reconsider y = |[ ( #a)`1 + nu * (( #a)`1 -( #q)`1), ( #a)`2 + nu * (( #a)`2 - ( #q)`2)]| as POINT of TarskiEuclid2Space by A1,EUCLID:67; reconsider x = #a + nu * ( #a - #q) as POINT of TarskiEuclid2Space by A1,EUCLID:67; ex x being POINT of TarskiEuclid2Space st between q,a,x & a,x equiv b,c proof take x; reconsider t1 = (-nu*( #a -#q)), t2 = #a as Element of 2-tuples_on REAL by EUCLID:22; #a - #x = #a + ( - #a + - nu * ( #a - #q)) by RVSUM_1:26 .= t1 + t2 - t2 by RVSUM_1:15 .= - nu * ( #a - #q) by RVSUM_1:42; then A8: |. #a - #x .| = |. nu * ( #a - #q).| by EUCLID:10 .= |. nu .| * |.#a - #q.| by EUCLID:11 .= alpha / mu * mu by COMPLEX1:43 .= alpha by XCMPLX_1:87; reconsider aq = #a - #q, qa = #q - #a as Element of 2-tuples_on REAL by EUCLID:22; A9: #q - #x = #q + ( - #a + - nu * ( #a - #q)) by RVSUM_1:26 .= - nu *( #a - #q) + ( - - #q + - #a) by RVSUM_1:15 .= - nu *( #a - #q) - ( - #q + #a) by RVSUM_1:26 .= ((-1) * nu) * aq + (-1) * aq by RVSUM_1:49 .= (-1 - nu) * ( #a - #q) by RVSUM_1:50; |. #q - #x .| = |. -(1 + nu) .| * |. #a - #q.| by A9,EUCLID:11 .= |. 1 + nu .| * |. #a - #q.| by COMPLEX1:52 .= (1 + nu) * |. #a - #q.| by COMPLEX1:43 .= mu + alpha / mu * mu .= mu + alpha by XCMPLX_1:87; then |. #q - #x .| = |. %q - %a .| + |. #a - #x .| by A8,EUCLID:18 .= |. #q - #a .| + |. #a - #x .|; then #a in LSeg( #q, #x) by EUCLID12:11; hence thesis by ThConv6,A8,ThConv4; end; hence thesis; end; hence thesis by A5; end; end; ThSAS: TarskiEuclid2Space is satisfying_SAS proof set TP = TarskiEuclid2Space; let a, b, c, x, a1, b1, c1, x1 be POINT of TP; assume that A1: a <> b and A2: a,b,c cong a1,b1,c1 and A3: between a,b,x and A4: between a1,b1,x1 and A5: b,x equiv b1,x1; A6: (dist(a,b) = dist(a1,b1) & dist(a,c) = dist(a1,c1) & dist(b,c) = dist(b1,c1)) by A2,GTARSKI1:def 15; A7: dist(a,x) = dist(a,b)+dist(b,x) by A3,ThConv8; A8: dist(a1,x1) = dist(a1,b1)+dist(b1,x1) by A4,ThConv8; A9: dist(b,x) = dist(b1,x1) by A5,GTARSKI1:def 15; A10: (dist(c1,x1))^2 = (dist(x1,b1))^2 + (dist(c1,b1))^2 - 2 * dist(x1,b1) * dist(c1,b1) * cos angle( #x1, #b1, #c1) by ThLawOfCosines; dist(c,x)^2 = dist(c1,x1)^2 proof per cases; suppose x = b; then A11: 0 = dist(x,b) by ThEgal; then A12: dist(x1,b1) = 0 by A5,GTARSKI1:def 15; A12bis: dist(c,x)^2 = 0^2 + dist(c,b)^2 - 2 * 0 * dist(c,b) * cos angle( #x,#b,#c) by A11,ThLawOfCosines .= 0 * 0 + dist(c,b)^2 by SQUARE_1:def 1; dist(c1,x1)^2 = 0^2 + dist(c1,b1)^2 - 2 * 0 * dist(c1,b1) * cos angle( #x1,#b1,#c1) by ThLawOfCosines,A12 .= 0 * 0 + dist(c1,b1)^2 by SQUARE_1:def 1; hence thesis by A12bis,A2,GTARSKI1:def 15; end; suppose A13: c = b; then 0 = dist(c,b) by ThEgal; then dist(c1,b1) = 0 by A2,GTARSKI1:def 15; then dist(c1,x1)^2 = 0 * 0 + dist(x1,b1)^2 by A10,SQUARE_1:def 1; hence thesis by A13,A5,GTARSKI1:def 15; end; suppose A14: x <> b & c <> b; A15: a <> x proof assume a = x; then dist(a,b) + dist(b,x) = 0 by A7,ThEgal; hence contradiction by A1,ThNull; end; dist(a,b) <> 0 & dist(a,x) <>0 & dist(b,x) <>0 by A1,A14,A15,ThEgal; then A16: #a1 <> #b1 & #a1 <> #x1 & #b1 <> #x1 by ThEgal,A6,A7,A8,A9; #b in LSeg( #a,#x ) by A3,ThConv6; then angle( #a,#b,#c ) + angle( #c,#b,#x ) = PI or angle( #a,#b,#c ) + angle( #c,#b,#x ) = 3 * PI by A1,A14,EUCLID_6:13; then cos angle ( #a,#b,#c ) = cos (PI - angle( #c,#b,#x)) or cos angle ( #a,#b,#c ) = cos (3 * PI - angle( #c,#b,#x)); then A17: cos angle ( #a,#b,#c ) = - cos (angle( #c,#b,#x)) by Th2,EUCLID10:2; #b1 in LSeg( #a1,#x1 ) by A4,ThConv6; then angle( #a1,#b1,#c1 ) + angle( #c1,#b1,#x1 ) = PI or angle( #a1,#b1,#c1 ) + angle( #c1,#b1,#x1 ) = 3 * PI by A16,EUCLID_6:13; then cos angle ( #a1,#b1,#c1 ) = cos (PI - angle( #c1,#b1,#x1)) or cos angle ( #a1,#b1,#c1 ) = cos (3 * PI - angle( #c1,#b1,#x1)); then A18: cos angle ( #a1,#b1,#c1 ) = - cos (angle( #c1,#b1,#x1)) by Th2,EUCLID10:2; A19: dist(a,b) <> 0 & dist(c,b) <> 0 by A1,A14,ThEgal; A20: dist(c,a)^2 = dist(a,b)^2+dist(c,b)^2 - 2*dist(a,b)*dist(c,b) * cos angle( #a,#b,#c) by ThLawOfCosines; A21: dist(a1,b1) <> 0 & dist(c1,b1) <> 0 by A1,A6,A14,ThEgal; dist(c1,a1)^2 = dist(a1,b1)^2+dist(c1,b1)^2 - 2*dist(a1,b1)*dist(c1,b1) * cos angle( #a1,#b1,#c1) by ThLawOfCosines; then A22: cos angle( #a1,#b1,#c1) = (dist(c,a)^2-dist(a,b)^2-dist(c,b)^2)/(-2*dist(a,b)*dist(c,b)) by A6,Th1,A21 .= cos angle( #a,#b,#c) by A20,A19,Th1; (dist(c,x))^2 = (dist(x,b))^2 + (dist(c,b))^2 - 2 * dist(x,b) * dist(c,b) * cos angle( #x, #b, #c) by ThLawOfCosines .= (dist(x1,b1))^2 + (dist(c1,b1))^2 - 2 * dist(x1,b1) * dist(c1,b1) * (-cos angle( #a1, #b1, #c1)) by A17,EUCLID_6:3,A6,A9,A22 .= (dist(x1,b1))^2 + (dist(c1,b1))^2 - 2 * dist(x1,b1) * dist(c1,b1) * cos angle( #x1, #b1, #c1) by A18,EUCLID_6:3 .= (dist(c1,x1))^2 by ThLawOfCosines; hence thesis; end; end; hence thesis by ThConv9; end; ThBetweennessIdentity: TarskiEuclid2Space is satisfying_BetweennessIdentity proof let a,b be POINT of TarskiEuclid2Space; assume between a,b,a; then #b in LSeg( #a,#a) by ThConv6; then #b in { #a} by RLTOPSP1:70; hence thesis by TARSKI:def 1; end; begin :: Ordered Affine Space Generated by TOP-REAL 2 theorem THQQ: OASpace(TOP-REAL 2) is OAffinSpace proof (ex u,v be VECTOR of TOP-REAL 2 st for a,b being Real st a*u + b*v = 0.(TOP-REAL 2) holds a=0 & b=0) proof reconsider u = |[1,0]|, v = |[0,1]| as VECTOR of TOP-REAL 2; now let a,b be Real; assume A1: a * u + b * v = 0.(TOP-REAL 2); A2: a * u + b * v = |[a * 1,a * 0]| + b * v by EUCLID:58 .= |[a * 1,a * 0]| + |[b * 0, b * 1]| by EUCLID:58 .= |[a + 0,0 + b]| by EUCLID:56 .= |[a,b]|; |[a,b]|`1 = a & |[a,b]|`2 = b & |[0,0]|`1 = 0 & |[0,0]|`2 = 0 by EUCLID:52; hence a = 0 & b = 0 by A1,A2,EUCLID:54; end; hence thesis; end; hence thesis by ANALOAF:26; end; theorem THSS: for a,b,c being Element of OASpace(TOP-REAL 2) holds Mid a,b,c iff a = b or b = c or (ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v)) proof let a,b,c be Element of OASpace(TOP-REAL 2); A1: now assume Mid a,b,c; then a,b // b,c; then consider u,v,w,y be VECTOR of TOP-REAL 2 such that A2: [a,b] = [u,v] and A3: [b,c] = [w,y] and A4: u,v // w,y by ANALOAF:def 3; A5: a = u & b = v & b = w & c = y by A2,A3,XTUPLE_0:1; per cases by A4; suppose u = v; hence a = b or b = c or (ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v)) by A5; end; suppose w = y; hence a = b or b = c or (ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v)) by A5; end; suppose ex r,s be Real st 0 < r & 0 < s & r * (v-u) = s * (y - w); then consider r,s be Real such that A6: 0 < r and A7: 0 < s and A8: r * (v - u) = s * (y - w); r * v - r * u = r * (v - u) by RLVECT_1:34 .= s * y - s * v by A5,A8,RLVECT_1:34; then A9: (r + s) * v = r * u + s * y by THJC; reconsider t = 1/(r+s) as Real; A10: 1 - s/(r+s) = (r+s)/(r+s) - s/(r+s) by A6,A7,XCMPLX_1:60 .= r/(r+s); A11: 1/(r+s)*(r+s) = (r+s)/(r+s) .= 1 by A6,A7,XCMPLX_1:60; A12: v = 1 * v by RVSUM_1:52 .= t * ((r+s) * v) by A11,RVSUM_1:49 .= t * (r * u) + t *(s * y) by RVSUM_1:51,A9 .= (t * r) * u + t * (s * y) by RVSUM_1:49 .= (1-s/(r+s)) * u + s/(r+s) * y by A10,RVSUM_1:49; reconsider l = s/(r+s) as Real; 0 <= l <= 1 & v = (1-l) * u + l * y by A12,A6,A7,THJD; then v in {(1-l) * u + l * y where l is Real : 0 <= l & l <= 1}; then b in LSeg(u,y) by A5,RLTOPSP1:def 2; hence a = b or b = c or (ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v)) by A5; end; end; now assume A13: a = b or b = c or (ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v)); reconsider OAS = OASpace(TOP-REAL 2) as OAffinSpace by THQQ; per cases by A13; suppose A14: a = b; a is Element of OAS & b is Element of OAS; hence Mid a,b,c by A14,DIRAF:10; end; suppose A15: b = c; b is Element of OAS & c is Element of OAS; hence Mid a,b,c by A15,DIRAF:10; end; suppose ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v); then consider u,v be Point of TOP-REAL 2 such that A16: u = a and A17: v = c and A18: b in LSeg(u,v); b in {(1-l) * u + l * v where l is Real: 0 <= l & l <= 1} by RLTOPSP1:def 2,A18; then consider l be Real such that A19: b = (1-l) * u + l * v and A20: 0 <= l and A21: l <= 1; reconsider w = b,y = b as Point of TOP-REAL 2; now take u,w,y,v; thus [a,b] = [u,w] & [b,c] = [y,v] by A16,A17; A22: w - (1-l)*u = l * v + (1-l) * u + ((-1)*(1-l)) * u by A19,RVSUM_1:49 .= l * v + ((1-l) * u + (-(1-l)) * u) by RVSUM_1:15 .= l * v + ((1-l) + (-(1-l))) * u by RVSUM_1:50 .= l * v by THJE; |[l * v`1,l * v`2]| = l * v by EUCLID:57 .= |[w`1,w`2]| - (1-l)*u by A22,EUCLID:53 .= |[w`1,w`2]| - |[ (1-l)*u`1,(1-l)*u`2]| by EUCLID:57 .= |[w`1-(1-l)*u`1,w`2-(1-l)*u`2]| by EUCLID:62; then A23: l * v`1 = w`1-(1-l)*u`1 & l * v`2 = w`2-(1-l)*u`2 by FINSEQ_1:77; A24: (1-l) * w - (1-l) * u = l * v - l * w proof A25: (1-l) * w - (1-l) * u = (1-l) * |[w`1,w`2]| - (1-l)* u by EUCLID:53 .= (1-l) * |[w`1,w`2]| - (1-l)*|[u`1,u`2]| by EUCLID:53 .= |[(1-l) * w`1,(1-l)*w`2]| - (1-l)*|[u`1,u`2]| by EUCLID:58 .= |[(1-l) * w`1,(1-l)*w`2]| - |[(1-l)*u`1,(1-l)*u`2]| by EUCLID:58 .= |[(1-l)*w`1-(1-l)*u`1,(1-l)*w`2-(1-l)*u`2]| by EUCLID:62 .= |[l*v`1 - l*w`1,l*v`2 - l*w`2]| by A23; l * v - l * w = l * |[v`1,v`2]| - l * w by EUCLID:53 .= l * |[v`1,v`2]| - l * |[w`1,w`2]| by EUCLID:53 .= |[l * v`1,l * v`2]| - l * |[w`1,w`2]| by EUCLID:58 .= |[l * v`1,l * v`2]| - |[l * w`1,l * w`2]| by EUCLID:58 .= |[l * v`1 - l * w`1,l * v`2 - l * w`2]| by EUCLID:62; hence thesis by A25; end; A26: (1-l)*(w - u) = (1-l) * w + (1-l) * (-u) by RVSUM_1:51 .= (1-l) * w + ((1-l) * (-1)) * u by RVSUM_1:49 .= (1-l) * w - (1-l) * u by RVSUM_1:49 .= l * v + ((-1) * l) * w by A24,RVSUM_1:49 .= l * v + l * ((-1)*w) by RVSUM_1:49 .= l * (v - w) by RVSUM_1:51; per cases by A20,A21,XXREAL_0:1; suppose l = 1; then w = v + 0 * u by A19,RVSUM_1:52 .= v by THJE; hence u,w // y,v; end; suppose l = 0; then w = u + 0 * v by A19,RVSUM_1:52 .= u by THJE; hence u,w // y,v; end; suppose A27: 0 < l < 1; then l - l < 1 - l by XREAL_1:9; hence u,w // y,v by A27,A26; end; end; then a,b // b,c by ANALOAF:def 3; hence Mid a,b,c; end; end; hence thesis by A1; end; theorem THSS2: for a,b,c being Element of OASpace(TOP-REAL 2) holds Mid a,b,c iff (ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v)) proof let a,b,c be Element of OASpace(TOP-REAL 2); hereby assume Mid a,b,c; then per cases by THSS; suppose A1: a = b; reconsider u = a, v = c as Point of TOP-REAL 2; u in LSeg(u,v) by RLTOPSP1:68; hence ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v) by A1; end; suppose A2: b = c; reconsider u = a, v = c as Point of TOP-REAL 2; v in LSeg(u,v) by RLTOPSP1:68; hence ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v) by A2; end; suppose ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v); hence ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v); end; end; assume ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v); hence Mid a,b,c by THSS; end; theorem THSS3: for a,b,c being Element of OASpace(TOP-REAL 2), ap,bp,cp being POINT of TarskiEuclid2Space st a = ap & b = bp & c = cp holds Mid a,b,c iff between ap,bp,cp proof let a,b,c be Element of OASpace(TOP-REAL 2), ap,bp,cp be POINT of TarskiEuclid2Space; assume that A1: a = ap and A2: b = bp and A3: c = cp; hereby assume Mid a,b,c; then ex u,v be Point of TOP-REAL 2 st u = a & v = c & b in LSeg(u,v) by THSS2; then #bp in LSeg( #ap, #cp) by A1,A2,A3; hence between ap,bp,cp by ThConv6; end; assume between ap,bp,cp; then #bp in LSeg( #ap, #cp) by ThConv6; hence Mid a,b,c by A1,A2,A3,THSS2; end; begin theorem THORANGE: for A,B,C,D being Element of TOP-REAL 2 st B in LSeg(A,C) & C in LSeg(A,D) holds B in LSeg(A,D) proof let A,B,C,D be Element of TOP-REAL 2; assume that A1: B in LSeg(A,C) and A2: C in LSeg(A,D); B in {(1-r)*A+r*C where r is Real : 0 <= r & r <= 1} by A1,RLTOPSP1:def 2; then consider r be Real such that A3: B = (1-r)*A+r*C and A4: 0 <= r and A5: r <= 1; C in {(1-r)*A+r*D where r is Real : 0 <= r & r <= 1} by A2,RLTOPSP1:def 2; then consider s be Real such that A6: C = (1-s)*A+s*D and A7: 0 <= s and A8: s <= 1; reconsider t = r * s as Real; A9: r * s <= 1 * 1 by A4,A5,A7,A8,XREAL_1:66; s * D = |[s*D`1,s*D`2]| by EUCLID:57; then A10: r*((1-s)*A+s*D) = r * ( |[(1-s)*A`1,(1-s)*A`2]| + |[s*D`1,s*D`2]| ) by EUCLID:57 .= r * ( |[(1-s)*A`1 + s * D`1,(1-s)*A`2 + s * D`2]| ) by EUCLID:56 .= ( |[ r * ((1-s)*A`1 + s * D`1), r * ((1-s)*A`2 + s * D`2)]| ) by EUCLID:58; B = |[(1-r)*A`1,(1-r)*A`2]| + |[ r * ((1-s)*A`1 + s * D`1), r * ((1-s)*A`2 + s * D`2)]| by A3,A6,A10,EUCLID:57 .= |[(1-r)*A`1 + r * ((1-s)*A`1 + s * D`1), (1-r)*A`2 + r * ((1-s)*A`2 + s * D`2)]| by EUCLID:56 .= |[ (1-r*s)*A`1+r*s*D`1,(1-r*s)*A`2+r*s*D`2]| .= |[ (1-r*s)*A`1,(1-r*s)*A`2]| +|[r*s*D`1,r*s*D`2]| by EUCLID:56 .= (1-r*s)*A + |[r*s*D`1,r*s*D`2]| by EUCLID:57 .= (1-t)*A+t*D by EUCLID:57; then B in {(1-r)*A+r*D where r is Real:0 <= r & r <= 1} by A9,A4,A7; hence thesis by RLTOPSP1:def 2; end; theorem THORANGE2: for A,B,C,D being Element of TOP-REAL 2 st B <> C & B in LSeg(A,C) & C in LSeg(B,D) holds C in LSeg(A,D) proof let A,B,C,D be Element of TOP-REAL 2; assume that A1: B <> C and A2: B in LSeg(A,C) and A3: C in LSeg(B,D); reconsider OAS = OASpace(TOP-REAL 2) as OAffinSpace by THQQ; reconsider ta = A,tb = B,tc = C,td = D as Element of OAS; Mid ta,tb,tc & Mid tb,tc,td by A2,A3,THSS2; then ex u,v be Point of TOP-REAL 2 st u = ta & v = td & tc in LSeg(u,v) by A1,DIRAF:12,THSS2; hence thesis; end; theorem THPOIRE: for p,q,r,s being Point of TarskiEuclid2Space st between p,q,r & between p,r,s holds between p,q,s proof let p,q,r,s be Point of TarskiEuclid2Space; assume that A1: between p,q,r and A2: between p,r,s; #q in LSeg( #p, #r) & #r in LSeg( #p, #s) by A1,A2,ThConv6; hence thesis by ThConv6,THORANGE; end; theorem THNOIX: for A,B,C,D being Point of TOP-REAL 2 st B in LSeg(A,C) & D in LSeg(A,B) holds B in LSeg(D,C) proof let A,B,C,D be Point of TOP-REAL 2; assume that A1: B in LSeg(A,C) and A2: D in LSeg(A,B); A3: dist(A,D) + dist(D,C) = dist(A,C) by A1,A2,THORANGE,EUCLID12:12; A4: dist(A,B) + dist(B,C) = dist(A,C) by A1,EUCLID12:12; dist(A,D) + dist(D,B) = dist(A,B) by A2,EUCLID12:12; then dist(D,B) + dist(B,C)= dist(D,C) by A3,A4; hence thesis by EUCLID12:12; end; theorem THNOIX2: for p,q,r,s being Point of TarskiEuclid2Space st between p,q,r & between p,s,q holds between s,q,r proof let p,q,r,s be Point of TarskiEuclid2Space; assume that A1: between p,q,r and A2: between p,s,q; A3: #q in LSeg ( #p, #r) by A1,ThConv6; #s in LSeg ( #p, #q) by A2,ThConv6; then #q in LSeg( #s, #r) by A3,THNOIX; hence thesis by ThConv6; end; theorem THNOIX3: for p,q,r,s being Point of TarskiEuclid2Space st q <> r & between p,q,r & between q,r,s holds between p,q,s proof let p,q,r,s be Point of TarskiEuclid2Space; assume that A1: q <> r and A2: between p,q,r and A3: between q,r,s; A4: #q in LSeg( #p,#r) by A2,ThConv6; then A5: dist( #p, #q)+dist( #q, #r)=dist( #p, #r) by EUCLID12:12; A6: #r in LSeg( #q,#s) by A3,ThConv6; A7: #r in LSeg( #p, #s) by A1,A4,A6,THORANGE2; dist( #p, #q) + dist( #q, #s) = dist( #p, #r) - dist( #q, #r) + (dist( #q, #r) + dist( #r, #s)) by A5,A6,EUCLID12:12 .= dist( #p, #r) + dist( #r, #s) .= dist( #p, #s) by A7,EUCLID12:12; then #q in LSeg( #p, #s) by EUCLID12:12; hence thesis by ThConv6; end; theorem for p,q,r,s being Point of TarskiEuclid2Space st q <> r & between p,q,r & between q,r,s holds between p,r,s proof let p,q,r,s be Point of TarskiEuclid2Space; assume that A1: q <> r and A2: between p,q,r and A3: between q,r,s; A4: #q in LSeg( #p,#r) by A2,ThConv6; A6: #r in LSeg( #q,#s) by A3,ThConv6; #r in LSeg( #p, #s) by A1,A4,A6,THORANGE2; hence thesis by ThConv6; end; ThPasch: TarskiEuclid2Space is satisfying_Pasch proof set S = TarskiEuclid2Space; now let a, b, p, q, z be POINT of S; assume that A1: between a,p,z and A2: between b,q,z; reconsider OAS = OASpace(TOP-REAL 2) as OAffinSpace by THQQ; A3: OAS is satisfying_Int_Bet_Pasch by PASCH:30; #a is Element of REAL 2 & #b is Element of REAL 2 & #p is Element of REAL 2 & #z is Element of REAL 2 & #q is Element of REAL 2 by EUCLID:22; then reconsider a1 = a,b1 = b,p1 = p,z1 = z,q1 = q as Element of OAS; Mid a1,p1,z1 by A1,THSS3; then A4: Mid z1,p1,a1 by DIRAF:9; Mid b1,q1,z1 by A2,THSS3; then A5: Mid z1,q1,b1 by DIRAF:9; per cases; suppose z1,p1,b1 are_collinear; then z1,p1 '||' z1,b1; then per cases by DIRAF:2; suppose z1,p1 // z1,b1; then consider u,v,w,y be VECTOR of TOP-REAL 2 such that A6: [z1,p1] = [u,v] and A7: [z1,b1] = [w,y] and A8: u,v // w,y by ANALOAF:def 3; A9: u = z1 & p1 = v & z1 = w & b1 = y by A6,A7,XTUPLE_0:1; then per cases by A8; suppose u = v; then A10: between p,q,b by A9,A2,ThConv7bis; between q,q,a by ThConv7; hence ex x being POINT of S st between p,x,b & between q,x,a by A10; end; suppose u = y; then A11: b = q by A2,A9,ThConv7ter; A12: between p,b,b by ThConv7; between q,b,a by A11,ThConv7; hence ex x being POINT of S st between p,x,b & between q,x,a by A12; end; suppose ex a,b be Real st 0 < a & 0 < b & a * (v-u)= b*(y-u); then consider r,s be Real such that A13: 0 < r and A14: 0 < s and A15: r * (v - u) = s * (y - u); per cases by XXREAL_0:1; suppose r = s; then v - u = y - u by A13,A15,RLVECT_1:36; then A16: v = y by THSD2; A17: between p,p,b by ThConv7; #p in LSeg ( #z,#a) by A1,ThConv6; then A18: between z,b,a by A16,A9,ThConv6; #q in LSeg ( #b,#z) by A2,ThConv6; then A19: between z,q,b by ThConv6; between q,p,a by A16,A9,A18,A19,THNOIX2; hence ex x being POINT of S st between p,x,b & between q,x,a by A17; end; suppose A20: r < s; reconsider t = r / s as Real; A21: r / s < s / s by A13,A20,XREAL_1:74; A22: t * v - t * u = |[t * v`1,t * v`2]| - t * u by EUCLID:57 .= |[t * v`1,t * v`2]| - |[t * u`1,t * u`2]| by EUCLID:57 .= |[ 1/s * r * v`1 -1/s * r * u`1,t * v`2 - t * u`2]| by EUCLID:62 .= |[(1/s) * (r * v`1 - r * u`1),(1/s) * (r * v`2-r*u`2)]| .= (1/s) *|[r * v`1 - r * u`1,r * v`2-r*u`2]| by EUCLID:58; A23: |[r * v`1-r*u`1,r*v`2-r*u`2]| = |[r*(v`1-u`1),r*(v`2-u`2)]| .= r*|[v`1-u`1,v`2-u`2]| by EUCLID:58 .= s * (y-u) by A15,EUCLID:61; A24: t * v - t * u = (1/s) * |[ s*(y-u)`1,s*(y-u)`2]| by A23,A22,EUCLID:57 .= |[ (1/s)*(s*(y-u)`1),(1/s)*(s*(y-u)`2)]| by EUCLID:58 .= |[ s*(1/s)*(y-u)`1,s*(1/s)*(y-u)`2]| .= |[ 1*(y-u)`1,s*(1/s)*(y-u)`2]| by XCMPLX_1:106,A14 .= |[(y-u)`1,1 * (y-u)`2]| by XCMPLX_1:106,A14 .= y - u by EUCLID:53; y = |[y`1-u`1+u`1,y`2-u`2+u`2]| by EUCLID:53 .= |[y`1-u`1,y`2-u`2]| + |[u`1,u`2]| by EUCLID:56 .= |[y`1,y`2]| - |[u`1,u`2]| + |[u`1,u`2]| by EUCLID:62 .= y - |[u`1,u`2]| + |[u`1,u`2]| by EUCLID:53 .= y - u + |[u`1,u`2]| by EUCLID:53 .= y - u + u by EUCLID:53 .= |[t*v`1,t*v`2]| - t * u + u by A24,EUCLID:57 .= (|[t*v`1,t*v`2]| - |[t*u`1,t*u`2]|) + u by EUCLID:57 .= (|[t*v`1,t*v`2]| - |[t*u`1,t*u`2]|) + |[u`1,u`2]| by EUCLID:53 .= |[t*v`1-t*u`1,t*v`2-t*u`2]| + |[u`1,u`2]| by EUCLID:62 .= |[t*v`1-t*u`1+u`1,t*v`2-t*u`2+u`2]| by EUCLID:56 .= |[t*v`1+ (1-t)*u`1,t*v`2+ (1-t)*u`2]| .= |[(1-t)*u`1,(1-t)*u`2]| + |[t*v`1,t*v`2]| by EUCLID:56 .= (1-t) * u + |[t*v`1,t*v`2]| by EUCLID:57 .= (1-t) * u + t * v by EUCLID:57; then (1-t) * u + t * v = y & 0 < t & t < 1 by A21,A13,A14,XCMPLX_1:60; then y in {(1-t)*u+t*v where t is Real: 0 <= t & t <= 1}; then #b in LSeg( #z, #p) by A9,RLTOPSP1:def 2; then A25: between z,b,p by ThConv6; A26: between z,p,a by A1,ThConv7bis; A27: between z,q,b by A2,ThConv7bis; then A28: between z,q,p by A25,THPOIRE; #p in LSeg( #z,#a) by A1,ThConv6; then A29: dist( #z,#p) + dist( #p,#a) = dist( #z,#a) by EUCLID12:12; #q in LSeg( #z,#p) by A27,A25,THPOIRE,ThConv6; then A30: dist( #z,#q) + dist( #q,#p) = dist( #z,#p) by EUCLID12:12; #q in LSeg( #z,#a) by A28,A26,THPOIRE,ThConv6; then dist( #z,#q) + dist( #q,#a) = dist( #z,#a) by EUCLID12:12; then dist( #q,#p) + dist( #p,#a) = dist( #q, #a) by A29,A30; then A31: #p in LSeg( #q,#a) by EUCLID12:12; A32: between p,p,b by ThConv7; between q,p,a by A31,ThConv6; hence ex x being POINT of S st between p,x,b & between q,x,a by A32; end; suppose A33: s < r; set t = s / r; t < r / r by A33,A13,XREAL_1:74; then A34: t < 1 by A13,XCMPLX_1:60; A35: t * y - t * u = |[t * y`1,t * y`2]| - t * u by EUCLID:57 .= |[t * y`1,t * y`2]| - |[t * u`1,t * u`2]| by EUCLID:57 .= |[ 1/r * s * y`1 -1/r * s * u`1, (1/r)*s * y`2 - (1/r)*s * u`2]| by EUCLID:62 .= |[(1/r) * (s * y`1 - s * u`1),(1/r) * (s * y`2-s*u`2)]| .= (1/r) *|[s * y`1 - s * u`1,s * y`2-s*u`2]| by EUCLID:58; A36: |[s * y`1-s*u`1,s*y`2-s*u`2]| = |[s*(y`1-u`1),s*(y`2-u`2)]| .= s*|[y`1-u`1,y`2-u`2]| by EUCLID:58 .= r * (v-u) by A15,EUCLID:61; A37: t * y - t * u = (1/r) * |[ r*(v-u)`1,r*(v-u)`2]| by A36,A35,EUCLID:57 .= |[ (1/r)*(r*(v-u)`1),(1/r)*(r*(v-u)`2)]| by EUCLID:58 .= |[ r*(1/r)*(v-u)`1,r*(1/r)*(v-u)`2]| .= |[ 1*(v-u)`1,r*(1/r)*(v-u)`2]| by XCMPLX_1:106,A13 .= |[(v-u)`1,1 * (v-u)`2]| by XCMPLX_1:106,A13 .= v - u by EUCLID:53; v = |[v`1-u`1+u`1,v`2-u`2+u`2]| by EUCLID:53 .= |[v`1-u`1,v`2-u`2]| + |[u`1,u`2]| by EUCLID:56 .= |[v`1,v`2]| - |[u`1,u`2]| + |[u`1,u`2]| by EUCLID:62 .= v - |[u`1,u`2]| + |[u`1,u`2]| by EUCLID:53 .= v - u + |[u`1,u`2]| by EUCLID:53 .= t * y - t * u + u by A37,EUCLID:53 .= |[t*y`1,t*y`2]| - t * u + u by EUCLID:57 .= (|[t*y`1,t*y`2]| - |[t*u`1,t*u`2]|) + u by EUCLID:57 .= (|[t*y`1,t*y`2]| - |[t*u`1,t*u`2]|) + |[u`1,u`2]| by EUCLID:53 .= |[t*y`1-t*u`1,t*y`2-t*u`2]| + |[u`1,u`2]| by EUCLID:62 .= |[t*y`1-t*u`1+u`1,t*y`2-t*u`2+u`2]| by EUCLID:56 .= |[t*y`1+ (1-t)*u`1,t*y`2+ (1-t)*u`2]| .= |[(1-t)*u`1,(1-t)*u`2]| + |[t*y`1,t*y`2]| by EUCLID:56 .= (1-t) * u + |[t*y`1,t*y`2]| by EUCLID:57 .= (1-t) * u + t * y by EUCLID:57; then v in {(1-t)*u+t*y where t is Real: 0 <= t & t <= 1} by A13,A14,A34; then #p in LSeg( #z, #b) by A9,RLTOPSP1:def 2; then A38: between z,p,b by ThConv6; A39: between z,p,a by A1,ThConv7bis; A40: between z,q,b by A2,ThConv7bis; A41: Mid z1,p1,b1 & Mid z1,q1,b1 by A38,A40,THSS3; per cases; suppose A42: z <> p; Mid z1,p1,b1 & Mid z1,p1,a1 by A38,A39,THSS3; then per cases by A42,DIRAF:15; suppose Mid p1,b1,a1; per cases by A41,DIRAF:17; suppose Mid z1,p1,q1; then between z,p,q by THSS3; then A43: between p,q,b by A40,THNOIX2; between q,q,a by ThConv7; hence ex x being POINT of S st between p,x,b & between q,x,a by A43; end; suppose Mid z1,q1,p1; then between z,q,p by THSS3; then A44: between q,p,a by A39,THNOIX2; between p,p,b by ThConv7; hence ex x being POINT of S st between p,x,b & between q,x,a by A44; end; end; suppose Mid p1,a1,b1; per cases by A41,DIRAF:17; suppose Mid z1,p1,q1; then between z,p,q by THSS3; then A45: between p,q,b by A40,THNOIX2; between q,q,a by ThConv7; hence ex x being POINT of S st between p,x,b & between q,x,a by A45; end; suppose Mid z1,q1,p1; then between z,q,p by THSS3; then A46: between q,p,a by A39,THNOIX2; between p,p,b by ThConv7; hence ex x being POINT of S st between p,x,b & between q,x,a by A46; end; end; end; suppose A47: z = p; between q,q,a by ThConv7; hence ex x being POINT of S st between p,x,b & between q,x,a by A47,A40; end; end; end; end; suppose b1,z1 // z1,p1; then Mid b1,z1,p1; then Mid p1,z1,b1 by DIRAF:9; then A48: between p,z,b by THSS3; then A49: between b,z,p by ThConv7bis; A50: between q,z,p by A2,A49,THNOIX2; A51: between z,p,a by A1,ThConv7bis; per cases; suppose z = p; then A52: between p,q,b by A2,ThConv7bis; between q,q,a by ThConv7; hence ex x being POINT of S st between p,x,b & between q,x,a by A52; end; suppose z <> p; then between q,z,a by A50,A51,THNOIX3; hence ex x being POINT of S st between p,x,b & between q,x,a by A48; end; end; end; suppose A53: not z1,p1,b1 are_collinear; consider y be Element of OAS such that A54: Mid p1,y,b1 and A55: Mid q1,y,a1 by A3,A53,A4,A5; the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; then reconsider yt = y as POINT of S by EUCLID:22; A56: between p,yt,b by A54,THSS3; between q,yt,a by A55,THSS3; hence ex x being POINT of S st between p,x,b & between q,x,a by A56; end; end; hence thesis; end; registration cluster TarskiEuclid2Space -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch; coherence by ThCongruenceSymmetry, ThCongruenceEquivalenceRelation, ThCongruenceIdentity, ThSegmentConstruction, ThSAS, ThBetweennessIdentity, ThPasch; end; registration cluster TarskiEuclid2Space -> satisfying_Tarski-model; coherence; end; begin :: Preparatory Work for The Rest of Tarski's Axioms theorem ThAZ9: for P,Q,R being Point of TOP-REAL 2, L being Element of line_of_REAL 2 st P in L & Q in L & R in L holds P in LSeg(Q,R) or Q in LSeg(R,P) or R in LSeg(P,Q) proof let P,Q,R be Point of TOP-REAL 2, L be Element of line_of_REAL 2; assume that A1: P in L and A2: Q in L and A3: R in L; L in line_of_REAL 2; then L in the set of all Line(x1,x2) where x1,x2 is Element of REAL 2 by EUCLIDLP:def 4; then consider x1,x2 be Element of REAL 2 such that A4: L = Line(x1,x2); reconsider tx1 = x1,tx2 = x2 as Element of TOP-REAL 2 by EUCLID:22; P in Line(tx1,tx2) & Q in Line(tx1,tx2) & R in Line(tx1,tx2) by A1,A2,A3,A4,EUCLID12:4; hence thesis by RLTOPSP1:def 16,TOPREAL9:67; end; theorem ThConvAG: for a,b,c being Element of TarskiEuclid2Space holds #b in LSeg ( #a,#c) implies ex jj being Real st 0 <= jj & jj <= 1 & #b - #a = jj * ( #c - #a) proof let a,b,c be Element of TarskiEuclid2Space; assume #b in LSeg ( #a,#c); then consider jj being Real such that G2: 0 <= jj & jj <= 1 & #b = (1-jj)*#a + jj*#c by RLTOPSP1:76; set v = #a, w = #c; #b - #a = (1-jj)*v - v + jj*w by RVSUM_1:15,G2 .= (1-jj+(-1))*v + jj*w by RVSUM_1:50 .= jj*w + (jj*(-1))*v .= jj*w + jj*((-1)*v) by RVSUM_1:49 .= jj * (w - v) by RVSUM_1:51; hence thesis by G2; end; theorem for n being Nat for a,b,c being Element of TarskiEuclidSpace n holds #b in LSeg ( #a,#c) implies ex jj being Real st 0 <= jj & jj <= 1 & #b - #a = jj * ( #c - #a) proof let n be Nat; let a,b,c be Element of TarskiEuclidSpace n; assume #b in LSeg ( #a,#c); then consider jj being Real such that G2: 0 <= jj & jj <= 1 & #b = (1-jj)*#a + jj*#c by RLTOPSP1:76; set v = #a, w = #c; #b - #a = (1-jj)*v - v + jj*w by RVSUM_1:15,G2 .= (1-jj+(-1))*v + jj*w by RVSUM_1:50 .= jj*w + (jj*(-1))*v .= jj*w + jj*((-1)*v) by RVSUM_1:49 .= jj * (w - v) by RVSUM_1:51; hence thesis by G2; end; theorem ThConvAGI: for a,b,c being Element of TarskiEuclid2Space holds (ex jj being Real st 0 <= jj & jj <= 1 & #b - #a = jj * ( #c - #a)) implies #b in LSeg ( #a,#c) proof let a,b,c be Element of TarskiEuclid2Space; given jj being Real such that G2: 0 <= jj & jj <= 1 & #b - #a = jj * ( #c - #a); set v = #a, w = #c; SS: #b + (v - v) = #b + 0.TOP-REAL 2 by RLVECT_1:5 .= #b; G3: v = 1 * v by RVSUM_1:52; #b + (- v + v) = jj * ( #c - #a) + v by G2,RVSUM_1:15; then #b = jj*w + jj * (-v) + v by RVSUM_1:51,SS .= jj*w + (jj * (-1))*v + v by RVSUM_1:49 .= jj*w + (-1) * (jj*v) + v by RVSUM_1:49 .= jj*w + (- jj*v + 1*v) by RVSUM_1:15,G3 .= jj*w + (((-1) * jj)*v + 1*v) by RVSUM_1:49 .= ((1 - jj)*v) + jj*w by RVSUM_1:50; then #b in {(1-r)*v + r*w where r is Real : 0 <= r & r <= 1 } by G2; hence thesis by RLTOPSP1:def 2; end; begin :: Four Remaining Axioms of Tarski definition let S be TarskiPlane; attr S is satisfying_A8 means ::: Axiom A8 ex a,b,c being POINT of S st not between a,b,c & not between b,c,a & not between c,a,b; attr S is satisfying_A9 means ::: Axiom A9 for a,b,c,p,q being POINT of S st p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q holds between a, b, c or between b, c, a or between c, a, b; attr S is satisfying_A10 means ::: Axiom A10 for a,b,c,d,t being POINT of S st between a,d,t & between b,d,c & a <> d holds ex x,y being POINT of S st between a,b,x & between a,c,y & between x,t,y; attr S is satisfying_A11 means ::: Axiom A11 for X,Y being Subset of S st (ex a being POINT of S st for x,y being POINT of S st x in X & y in Y holds between a,x,y) holds (ex b being POINT of S st for x,y being POINT of S st x in X & y in Y holds between x,b,y); end; notation let S be TarskiPlane; synonym S is satisfying_Lower_Dimension_Axiom for S is satisfying_A8; synonym S is satisfying_Upper_Dimension_Axiom for S is satisfying_A9; synonym S is satisfying_Euclid_Axiom for S is satisfying_A10; synonym S is satisfying_Continuity_Axiom for S is satisfying_A11; end; :: Axiom A8 -- Lower Dimension Axiom ::$N Lower dimension axiom theorem AxiomA8: :: Axiom A8 ex a,b,c being Point of TarskiEuclid2Space st not between a,b,c & not between b,c,a & not between c,a,b proof the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; then reconsider a = |[0,0]|, b = |[1,0]|, c = |[0,1]| as Point of TarskiEuclid2Space by EUCLID:22; take a,b,c; thus not between a,b,c proof assume between a,b,c; then #b in LSeg( #a,#c) by ThConv6; then dist( #a,#b) + dist( #b,#c) = dist( #a,#c) by EUCLID12:12; hence thesis by SQUARE_1:19,THY1,THY2,THY3; end; thus not between b,c,a proof assume between b,c,a; then #c in LSeg( #b,#a) by ThConv6; then dist( #b,#c) + dist( #c,#a) = dist( #b,#a) by EUCLID12:12; hence thesis by SQUARE_1:19,THY1,THY2,THY3; end; assume between c,a,b; then #a in LSeg( #c,#b) by ThConv6; then dist( #c,#a) + dist( #a,#b) = dist( #c,#b) by EUCLID12:12; hence thesis by SQUARE_1:21,THY1,THY2,THY3; end; :: Axiom A9 -- Upper Dimension Axiom ::$N Upper dimension axiom theorem AxiomA9: :: Axiom A9 for a,b,c,p,q being Point of TarskiEuclid2Space st p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q holds between a, b, c or between b, c, a or between c, a, b proof let a,b,c,p,q be Point of TarskiEuclid2Space; assume that A1: p <> q and A2: a,p equiv a,q and A3: b,p equiv b,q and A4: c,p equiv c,q; |. #a - #p.| = |. #a - #q.| by A2,ThConv4; then A5: #a in the_perpendicular_bisector( #p,#q) by A1,EUCLID12:60; |. #b - #p.| = |. #b - #q.| by A3,ThConv4; then A6: #b in the_perpendicular_bisector( #p,#q) by A1,EUCLID12:60; |. #c - #p.| = |. #c - #q.| by A4,ThConv4; then #c in the_perpendicular_bisector( #p,#q) by A1,EUCLID12:60; then #a in LSeg( #b,#c) or #b in LSeg( #c,#a) or #c in LSeg( #a,#b) by A5,A6,ThAZ9; hence thesis by ThConv6; end; :: Axiom A10 -- Axiom of Euclid ::$N Axiom of Euclid theorem AxiomA10: :: Axiom A10 -- Axiom of Euclid for a,b,c,d,t being Element of TarskiEuclid2Space st between a,d,t & between b,d,c & a <> d holds ex x,y being Element of TarskiEuclid2Space st between a,b,x & between a,c,y & between x,t,y proof let a,b,c,d,t be Element of TarskiEuclid2Space; assume that A1: between a,d,t and A2: between b,d,c and A3: a <> d; G0: #d in LSeg( #a, #t ) by A1,ThConv6; set v = #a, w = #t; consider jj being Real such that G2: 0 <= jj & jj <= 1 & #d = (1-jj)*v + jj*w by RLTOPSP1:76,G0; g1: #d - #a = (1-jj)*v - v + jj*w by RVSUM_1:15,G2 .= (1-jj + (-1)) * v + jj*w by RVSUM_1:50 .= jj*w + (jj * (-1))*v .= jj*w + jj * ((-1)*v) by RVSUM_1:49 .= jj * (w - v) by RVSUM_1:51; set jt = 1 / jj; JJ: jj <> 0 proof assume jj = 0; then #d - #a = 0.TOP-REAL 2 by g1,RLVECT_1:10; hence thesis by A3,RLVECT_1:21; end; set xxx = jt * ( #b - #a) + #a; ww: the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; then reconsider xx = xxx as Element of TarskiEuclid2Space by EUCLID:22; jj * (xxx - #a) = jj * (jt * ( #b - #a) + ( #a - #a)) by RLVECT_1:28 .= jj * ((1 / jj) * ( #b - #a) + 0.TOP-REAL 2) by RLVECT_1:15 .= (jj * (1 / jj)) * ( #b - #a) by RLVECT_1:def 7 .= 1 * ( #b - #a) by XCMPLX_0:def 7,JJ .= #b - #a by RVSUM_1:52; then #b in LSeg ( #a, #xx) by G2,ThConvAGI; then T1: between a,b,xx by ThConv6; set yyy = jt * ( #c - #a) + #a; reconsider yy = yyy as Element of TarskiEuclid2Space by ww,EUCLID:22; jj * (yyy - #a) = jj * (jt * ( #c - #a) + ( #a - #a)) by RLVECT_1:28 .= jj * (jt * ( #c - #a) + 0.TOP-REAL 2) by RLVECT_1:15 .= (jj * jt) * ( #c - #a) by RLVECT_1:def 7 .= 1 * ( #c - #a) by XCMPLX_0:def 7,JJ .= ( #c - #a) by RVSUM_1:52; then #c in LSeg ( #a, #yy) by G2,ThConvAGI; then T2: between a,c,yy by ThConv6; #d in LSeg ( #b, #c) by A2,ThConv6; then consider kk being Real such that Y1: 0 <= kk & kk <= 1 & #d - #b = kk * ( #c - #b) by ThConvAG; jt * ( #d - #a) = (1 / jj) * jj * ( #t - #a) by g1,RLVECT_1:def 7 .= 1 * ( #t - #a) by JJ,XCMPLX_0:def 7 .= #t - #a by RVSUM_1:52; then w1: jt * ( #d - #a) + #a = #t + (- #a + #a) by RLVECT_1:def 3 .= #t + 0.TOP-REAL 2 by RLVECT_1:5; W2: #yy - #xx = (1 / jj) * ( #c - #a) + #a - #a - (1 / jj) * ( #b - #a) by RLVECT_1:27 .= jt * ( #c - #a) + ( #a - #a) - (1 / jj) * ( #b - #a) by RLVECT_1:28 .= jt * ( #c - #a) + 0.TOP-REAL 2 - (1 / jj) * ( #b - #a) by RLVECT_1:15 .= jt * (( #c - #a) - ( #b - #a)) by RLVECT_1:34 .= jt * ( #c - #b) by ThWW; #t - #xx = jt * ( #d - #a) + #a - #a - (1 / jj) * ( #b - #a) by RLVECT_1:27,w1 .= jt * ( #d - #a) + ( #a - #a) - (1 / jj) * ( #b - #a) by RLVECT_1:def 3 .= jt * ( #d - #a) + 0.TOP-REAL 2 - (1 / jj) * ( #b - #a) by RLVECT_1:5 .= jt * (( #d - #a) - ( #b - #a)) by RLVECT_1:34 .= jt * ( #d - #b) by ThWW .= jt * kk * ( #c - #b) by RLVECT_1:def 7,Y1 .= kk * ( #yy - #xx) by W2,RLVECT_1:def 7; then #t in LSeg ( #xx, #yy) by Y1,ThConvAGI; then between xx,t,yy by ThConv6; hence thesis by T1,T2; end; begin :: Axiom A11 -- Axiom Schema of Continuity ::$N Axiom schema of continuity theorem AxiomA11: :: Axiom A11 for X,Y being Subset of TarskiEuclid2Space st (ex a being Element of TarskiEuclid2Space st for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds between a,x,y) holds (ex b being Element of TarskiEuclid2Space st for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds between x,b,y) proof let X,Y being Subset of TarskiEuclid2Space; given a be Element of TarskiEuclid2Space such that A1: for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds between a,x,y; per cases; suppose SS: X c= {a} or Y = {}; ex b being Element of TarskiEuclid2Space st for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds between x,b,y proof take b = a; let x,y be Element of TarskiEuclid2Space; assume x in X & y in Y; then x = a by SS,TARSKI:def 1; hence thesis by GTARSKI1:17; end; hence thesis; end; suppose SSS: not X c= {a} & Y <> {}; X \ {a} <> {} by XBOOLE_1:37,SSS; then consider c being object such that G9: c in X \ {a} by XBOOLE_0:def 1; reconsider c as Element of TarskiEuclid2Space by G9; su: X \ {a} c= X by XBOOLE_1:36; set S = { j where j is Real : j >= 1 & #a + j * ( #c - #a) in Y }; S is real-membered proof let w be object; assume w in S; then consider j1 being Real such that G1: w = j1 & j1 >= 1 & #a + j1 * ( #c - #a) in Y; thus thesis by G1; end; then reconsider S as real-membered set; gg: 1 is LowerBound of S proof let x be ExtReal; assume x in S; then consider j1 being Real such that G1: x = j1 & j1 >= 1 & #a + j1 * ( #c - #a) in Y; thus thesis by G1; end; consider d being object such that G2: d in Y by XBOOLE_0:def 1,SSS; reconsider d as Element of TarskiEuclid2Space by G2; #c in LSeg ( #a,#d) by ThConv6,su,G9,A1,G2; then consider jda being Real such that G0: 0 <= jda & jda <= 1 & #c - #a = jda * ( #d - #a) by ThConvAG; set jd = 1 / jda; hh: jda <> 0 proof assume jda = 0; then #c - #a = 0.TOP-REAL 2 + 0 * ( #d - #a) by G0 .= 0.TOP-REAL 2 by THJE; hence thesis by G9,ZFMISC_1:56,RLVECT_1:21; end; Lem: for y being Element of TarskiEuclid2Space st y in Y holds ex j1 being Real st j1 >= 1 & #y - #a = j1 * ( #c - #a) proof let y be Element of TarskiEuclid2Space; assume y in Y; then #c in LSeg ( #a,#y) by A1,su,G9,ThConv6; then consider j being Real such that H1: 0 <= j & j <= 1 & #c - #a = j * ( #y - #a) by ThConvAG; set j1 = 1 / j; H2: j <> 0 proof assume j = 0; then #c - #a = 0.TOP-REAL 2 + 0 * ( #y - #a) by H1 .= 0.TOP-REAL 2 by THJE; hence thesis by G9,ZFMISC_1:56,RLVECT_1:21; end; then H5: j1 >= 1 by H1,XREAL_1:181; j1 * ( #c - #a) = j1 * j * ( #y - #a) by RLVECT_1:def 7,H1 .= 1 * ( #y - #a) by H2,XCMPLX_0:def 7 .= #y - #a by RVSUM_1:52; hence thesis by H5; end; Gy: jd * ( #c - #a) = jd * jda * ( #d - #a) by RLVECT_1:def 7,G0 .= 1 * ( #d - #a) by hh,XCMPLX_0:def 7 .= #d - #a by RVSUM_1:52; J2: jd >= 1 by XREAL_1:181,G0,hh; jd * ( #c - #a) + #a = #d + (- #a + #a) by RLVECT_1:def 3,Gy .= #d + 0.TOP-REAL 2 by RLVECT_1:5; then J1: jd in S by J2,G2; reconsider S as non empty bounded_below real-membered set by J1,gg,XXREAL_2:def 9; set k = inf S; set bb = #a + k * ( #c - #a); p2: the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 by GTARSKI1:def 13; reconsider bb as Element of TarskiEuclid2Space by p2,EUCLID:67; ex b being Element of TarskiEuclid2Space st for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds between x,b,y proof take b = bb; let x,y be Element of TarskiEuclid2Space; assume T1: x in X & y in Y; then consider j1 being Real such that HH: j1 >= 1 & #y - #a = j1 * ( #c - #a) by Lem; #y + (- #a + #a) = #a + j1 * ( #c - #a) by HH,RLVECT_1:def 3; then hH: #y + 0.TOP-REAL 2 = #a + j1 * ( #c - #a) by RLVECT_1:5; #x in LSeg ( #a,#d) by T1,A1,G2,ThConv6; then consider l being Real such that z1: 0 <= l & l <= 1 & #x - #a = l * ( #d - #a) by ThConvAG; z2: #x - #a = l * jd * ( #c - #a) by RLVECT_1:def 7,z1,Gy; set i = l * jd; #x + (- #a + #a) = i * ( #c - #a) + #a by z2,RLVECT_1:def 3; then E3: #x + 0.TOP-REAL 2 = i * ( #c - #a) + #a by RLVECT_1:5; for h being ExtReal st h in S holds i <= h proof let h be ExtReal; assume h in S; then consider j1 being Real such that G1: h = j1 & j1 >= 1 & #a + j1 * ( #c - #a) in Y; set z = #a + j1 * ( #c - #a); reconsider z as Element of TarskiEuclid2Space by EUCLID:67,p2; #x in LSeg ( #a,#z) by T1,A1,G1,ThConv6; then consider ll being Real such that z1: 0 <= ll & ll <= 1 & #x - #a = ll * ( #z - #a) by ThConvAG; z0: #c - #a <> 0.TOP-REAL 2 proof assume #c - #a = 0.TOP-REAL 2; then #c + (-#a + #a) = 0.TOP-REAL 2 + #a by RLVECT_1:def 3; then #c + 0.TOP-REAL 2 = 0.TOP-REAL 2 + #a by RLVECT_1:5; hence thesis by G9,ZFMISC_1:56; end; #z - #a = j1 * ( #c - #a) + ( #a + -#a) by RLVECT_1:def 3 .= j1 * ( #c - #a) + 0.TOP-REAL 2 by RLVECT_1:5 .= j1 * ( #c - #a); then #x - #a = ll * j1 * ( #c - #a) by z1,RLVECT_1:def 7; then ll * j1 = i by RLVECT_1:37,z0,z2; hence thesis by G1,XREAL_1:153,z1; end; then fF: i is LowerBound of S by XXREAL_2:def 2; then f1: i <= k by XXREAL_2:def 4; j1 in S by hH,HH,T1; then F0: k <= j1 by XXREAL_2:3; then f2: i <= j1 by f1,XXREAL_0:2; ff: #b - #x = #a + k * ( #c - #a) + (-i * ( #c - #a) + -#a) by E3,RLVECT_1:31 .= (k * ( #c - #a) + #a) +- #a + -i * ( #c - #a) by RLVECT_1:def 3 .= k * ( #c - #a) + ( #a +- #a) + -i * ( #c - #a) by RLVECT_1:def 3 .= k * ( #c - #a) + 0.TOP-REAL 2 + -i * ( #c - #a) by RLVECT_1:5 .= k * ( #c - #a) - i * ( #c - #a) .= (k - i) * ( #c - #a) by RLVECT_1:35; set l = (k - i) / (j1 - i); per cases; suppose i = j1; then k = i by F0,f1,XXREAL_0:1; then #b - #x = 0.TOP-REAL 2 + 0 * ( #c - #a) by ff .= 0.TOP-REAL 2 by THJE; then #b + (- #x + #x) = 0.TOP-REAL 2 + #x by RLVECT_1:def 3; then #b + 0.TOP-REAL 2 = 0.TOP-REAL 2 + #x by RLVECT_1:5; hence thesis by GTARSKI1:17; end; suppose i <> j1; then i < j1 by f2,XXREAL_0:1; then R1: j1 - i > 0 by XREAL_1:50; #y - #x = ( #a + j1 * ( #c - #a)) + (- i * ( #c - #a) + -#a) by RLVECT_1:31,E3,hH .= (j1 * ( #c - #a) + #a) +- #a - i * ( #c - #a) by RLVECT_1:def 3 .= j1 * ( #c - #a) + ( #a +- #a) - i * ( #c - #a) by RLVECT_1:def 3 .= j1 * ( #c - #a) + 0.TOP-REAL 2 - i * ( #c - #a) by RLVECT_1:5 .= (j1 - i) * ( #c - #a) by RLVECT_1:35; then (1 / (j1 - i)) * ( #y - #x) = (1 / (j1 - i)) * (j1 - i) * ( #c - #a) by RLVECT_1:def 7; then (1 / (j1 - i)) * ( #y - #x) = 1 * ( #c - #a) by XCMPLX_0:def 7,R1; then #c - #a = (1 / (j1 - i)) * ( #y - #x) by RVSUM_1:52; then S2: #b - #x = l * ( #y - #x) by RLVECT_1:def 7,ff; R4: k - i <= j1 - i by XREAL_1:13,F0; k - i >= 0 by fF,XREAL_1:48,XXREAL_2:def 4; then #b in LSeg ( #x,#y) by S2,ThConvAGI,R4,XREAL_1:183; hence thesis by ThConv6; end; end; hence thesis; end; end; registration cluster TarskiEuclid2Space -> satisfying_Lower_Dimension_Axiom satisfying_Upper_Dimension_Axiom satisfying_Euclid_Axiom satisfying_Continuity_Axiom; coherence by AxiomA8,AxiomA9,AxiomA10,AxiomA11; end; begin :: Corrolaries reserve X,Y for Subset of TarskiEuclid2Space; theorem for a being Element of TarskiEuclid2Space st (for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds between a,x,y) & a in Y holds X = {a} or X is empty proof let a be Element of TarskiEuclid2Space; assume that A1: for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds between a,x,y and A2: a in Y; M1: X c= {a} proof let x be object; assume L1: x in X; then reconsider x as Element of TarskiEuclid2Space; a = x by GTARSKI1:def 10,A1,A2,L1; hence thesis by TARSKI:def 1; end; per cases; suppose X is empty; hence thesis; end; suppose X is non empty; then consider x be object such that A3: x in X; reconsider x as Element of TarskiEuclid2Space by A3; a = x by GTARSKI1:def 10,A1,A2,A3; then {a} c= X by TARSKI:def 1,A3; hence thesis by M1; end; end; theorem for a being Element of TarskiEuclid2Space st (for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds between a,x,y) & X is non empty & Y is non empty & (X is trivial implies X <> {a}) holds ex b being Element of TarskiEuclid2Space st X c= Line( #a, #b) & Y c= Line( #a, #b) proof let a be Element of TarskiEuclid2Space such that A1: for x,y being Element of TarskiEuclid2Space st x in X & y in Y holds between a,x,y and A1A: X is non empty and A1B: Y is non empty and A3: X is trivial implies X <> {a}; consider x0 be object such that K1: x0 in X by A1A; reconsider x0 as Element of TarskiEuclid2Space by K1; consider c be object such that MM: c in Y by A1B; reconsider c as Element of TarskiEuclid2Space by MM; V1: X c= LSeg( #a,#c) proof let x be object; assume DA: x in X; then reconsider x1 = x as Element of TarskiEuclid2Space; #x1 in LSeg( #a,#c) by ThConv6,A1,DA,MM; hence x in LSeg( #a,#c); end; t2: LSeg( #a,#c) c= Line( #a,#c) by RLTOPSP1:73; then T1: X c= Line( #a, #c) by V1; T2: x0 in Line( #a, #c) by t2,V1,K1; Y c= Line( #a, #c) proof let y be object; assume V2: y in Y; then reconsider y0 = y as Element of TarskiEuclid2Space; per cases; suppose MU: x0 = a; per cases; suppose X is trivial; then consider xx be object such that KL: X = {xx} by A1A,ZFMISC_1:131; thus thesis by MU,K1,KL,TARSKI:def 1,A3; end; suppose X is non trivial; then consider a0,b0 be object such that LO1: a0 in X and LO2: b0 in X and LO3: a0 <> b0; ex x1 be object st x1 in X & x1 <> a proof assume AA: for x1 be object holds not x1 in X or x1 = a; a0 <> a or b0 <> a by LO3; hence contradiction by LO1,LO2,AA; end; then consider x1 be object such that K1: x1 in X and VAL: x1 <> a; reconsider x1 as Element of TarskiEuclid2Space by K1; N1: #x1 in LSeg( #a,#y0) by ThConv6,V2,K1,A1; n2: LSeg( #a,#y0) c= Line( #a,#y0) by RLTOPSP1:73; #a in Line( #a,#y0) by RLTOPSP1:72; then ff: Line( #x1,#a) = Line( #a,#y0) by N1,n2,VAL,RLTOPSP1:75; #a in Line( #a,#c) by RLTOPSP1:72; then Line( #a,#x1) c= Line( #a,#c) by K1,T1,RLTOPSP1:74; hence thesis by ff,RLTOPSP1:72; end; end; suppose VAL: x0 <> a; N1: #x0 in LSeg( #a,#y0) by ThConv6,V2,K1,A1; n2: LSeg( #a,#y0) c= Line( #a,#y0) by RLTOPSP1:73; #a in Line( #a,#y0) by RLTOPSP1:72; then ff: Line( #x0,#a) = Line( #a,#y0) by N1,n2,VAL,RLTOPSP1:75; #a in Line( #a,#c) by RLTOPSP1:72; then Line( #a,#x0) c= Line( #a,#c) by T2,RLTOPSP1:74; hence thesis by ff,RLTOPSP1:72; end; end; hence thesis by T1; end;