:: Lines in $n$-Dimensional Euclidean Spaces :: by Akihiro Kubo :: :: Received August 8, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin theorem Th1: :: EUCLID_4:1 for n being Nat for x being Element of REAL n holds ( (0 * x) + x = x & x + (0* n) = x ) proofend; theorem Th2: :: EUCLID_4:2 for a being Real for n being Nat holds a * (0* n) = 0* n proofend; theorem Th3: :: EUCLID_4:3 for n being Nat for x being Element of REAL n holds ( 1 * x = x & 0 * x = 0* n ) proofend; theorem :: EUCLID_4:4 for a, b being Real for n being Nat for x being Element of REAL n holds (a * b) * x = a * (b * x) by RVSUM_1:49; theorem :: EUCLID_4:5 for a being Real for n being Nat for x being Element of REAL n holds ( not a * x = 0* n or a = 0 or x = 0* n ) proofend; theorem :: EUCLID_4:6 for a being Real for n being Nat for x1, x2 being Element of REAL n holds a * (x1 + x2) = (a * x1) + (a * x2) by RVSUM_1:51; theorem :: EUCLID_4:7 for a, b being Real for n being Nat for x being Element of REAL n holds (a + b) * x = (a * x) + (b * x) by RVSUM_1:50; theorem :: EUCLID_4:8 for a being Real for n being Nat for x1, x2 being Element of REAL n holds ( not a * x1 = a * x2 or a = 0 or x1 = x2 ) proofend; definition let n be Nat; let x1, x2 be Element of REAL n; func Line (x1,x2) -> Subset of (REAL n) equals :: EUCLID_4:def 1 { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ; coherence { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } is Subset of (REAL n) proofend; end; :: deftheorem defines Line EUCLID_4:def_1_:_ for n being Nat for x1, x2 being Element of REAL n holds Line (x1,x2) = { (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum } ; registration let n be Nat; let x1, x2 be Element of REAL n; cluster Line (x1,x2) -> non empty ; coherence not Line (x1,x2) is empty proofend; end; Lm1: for n being Nat for x1, x2 being Element of REAL n holds Line (x1,x2) c= Line (x2,x1) proofend; definition let n be Nat; let x1, x2 be Element of REAL n; :: original:Line redefine func Line (x1,x2) -> Subset of (REAL n); commutativity for x1, x2 being Element of REAL n holds Line (x1,x2) = Line (x2,x1) proofend; end; theorem Th9: :: EUCLID_4:9 for n being Nat for x1, x2 being Element of REAL n holds ( x1 in Line (x1,x2) & x2 in Line (x1,x2) ) proofend; Lm2: for n being Nat for x1, x2, x3 being Element of REAL n holds x1 + (x2 + x3) = (x1 + x2) + x3 by FINSEQOP:28; theorem Th10: :: EUCLID_4:10 for n being Nat for y1, x1, x2, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds Line (y1,y2) c= Line (x1,x2) proofend; theorem Th11: :: EUCLID_4:11 for n being Nat for y1, x1, x2, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 holds Line (x1,x2) c= Line (y1,y2) proofend; definition let n be Nat; let A be Subset of (REAL n); attrA is being_line means :Def2: :: EUCLID_4:def 2 ex x1, x2 being Element of REAL n st ( x1 <> x2 & A = Line (x1,x2) ); end; :: deftheorem Def2 defines being_line EUCLID_4:def_2_:_ for n being Nat for A being Subset of (REAL n) holds ( A is being_line iff ex x1, x2 being Element of REAL n st ( x1 <> x2 & A = Line (x1,x2) ) ); Lm3: for n being Nat for A being Subset of (REAL n) for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds A = Line (x1,x2) proofend; theorem :: EUCLID_4:12 for n being Nat for A, C being Subset of (REAL n) for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds A = C proofend; theorem Th13: :: EUCLID_4:13 for n being Nat for A being Subset of (REAL n) st A is being_line holds ex x1, x2 being Element of REAL n st ( x1 in A & x2 in A & x1 <> x2 ) proofend; theorem :: EUCLID_4:14 for n being Nat for x1 being Element of REAL n for A being Subset of (REAL n) st A is being_line holds ex x2 being Element of REAL n st ( x1 <> x2 & x2 in A ) proofend; theorem :: EUCLID_4:15 for n being Nat for x being Element of REAL n holds |.x.| = sqrt |(x,x)| ; theorem Th16: :: EUCLID_4:16 for n being Nat for x being Element of REAL n holds ( |(x,x)| = 0 iff |.x.| = 0 ) proofend; theorem Th17: :: EUCLID_4:17 for n being Nat for x being Element of REAL n holds ( |(x,x)| = 0 iff x = 0* n ) proofend; theorem Th18: :: EUCLID_4:18 for n being Nat for x being Element of REAL n holds |(x,(0* n))| = 0 proofend; theorem :: EUCLID_4:19 for n being Nat for x being Element of REAL n holds |((0* n),x)| = 0 by Th18; theorem Th20: :: EUCLID_4:20 for n being Nat for x1, x2, x3 being Element of REAL n holds |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)| proofend; theorem Th21: :: EUCLID_4:21 for n being Nat for x1, x2 being Element of REAL n for a being real number holds |((a * x1),x2)| = a * |(x1,x2)| proofend; theorem :: EUCLID_4:22 for n being Nat for x1, x2 being Element of REAL n for a being real number holds |(x1,(a * x2))| = a * |(x1,x2)| by Th21; theorem Th23: :: EUCLID_4:23 for n being Nat for x1, x2 being Element of REAL n holds |((- x1),x2)| = - |(x1,x2)| proofend; theorem :: EUCLID_4:24 for n being Nat for x1, x2 being Element of REAL n holds |(x1,(- x2))| = - |(x1,x2)| by Th23; theorem :: EUCLID_4:25 for n being Nat for x1, x2 being Element of REAL n holds |((- x1),(- x2))| = |(x1,x2)| proofend; theorem Th26: :: EUCLID_4:26 for n being Nat for x1, x2, x3 being Element of REAL n holds |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| proofend; theorem :: EUCLID_4:27 for n being Nat for a, b being real number for x1, x2, x3 being Element of REAL n holds |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|) proofend; theorem :: EUCLID_4:28 for n being Nat for x1, y1, y2 being Element of REAL n holds |(x1,(y1 + y2))| = |(x1,y1)| + |(x1,y2)| by Th20; theorem :: EUCLID_4:29 for n being Nat for x1, y1, y2 being Element of REAL n holds |(x1,(y1 - y2))| = |(x1,y1)| - |(x1,y2)| by Th26; theorem Th30: :: EUCLID_4:30 for n being Nat for x1, x2, y1, y2 being Element of REAL n holds |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| proofend; theorem Th31: :: EUCLID_4:31 for n being Nat for x1, x2, y1, y2 being Element of REAL n holds |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| proofend; theorem Th32: :: EUCLID_4:32 for n being Nat for x, y being Element of REAL n holds |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| proofend; theorem Th33: :: EUCLID_4:33 for n being Nat for x, y being Element of REAL n holds |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| proofend; theorem :: EUCLID_4:34 for n being Nat for x, y being Element of REAL n holds |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2) proofend; theorem :: EUCLID_4:35 for n being Nat for x, y being Element of REAL n holds |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(x,y)|)) + (|.y.| ^2) proofend; theorem :: EUCLID_4:36 for n being Nat for x, y being Element of REAL n holds (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2)) proofend; theorem :: EUCLID_4:37 for n being Nat for x, y being Element of REAL n holds (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| proofend; theorem :: EUCLID_4:38 for n being Nat for x, y being Element of REAL n holds abs |(x,y)| <= |.x.| * |.y.| proofend; theorem :: EUCLID_4:39 for n being Nat for x, y being Element of REAL n holds |.(x + y).| <= |.x.| + |.y.| proofend; Lm4: for a being Real for n being Nat for x being Element of REAL n holds ( - (a * x) = (- a) * x & - (a * x) = a * (- x) ) proofend; Lm5: for n being Nat for x1, x2 being Element of REAL n st x1 <> x2 holds |.(x1 - x2).| <> 0 proofend; Lm6: for n being Nat for y1, y2, x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds ex a being Real st y1 - y2 = a * (x1 - x2) proofend; Lm7: for n being Nat for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal & ( for x being Element of REAL n st x in Line (x1,x2) holds |.(y1 - y2).| <= |.(y1 - x).| ) ) proofend; theorem :: EUCLID_4:40 for n being Nat for R being Subset of REAL for x1, x2, y1 being Element of REAL n st R = { |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2) } holds ex y2 being Element of REAL n st ( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal ) proofend; definition let n be Nat; let p1, p2 be Point of (TOP-REAL n); func Line (p1,p2) -> Subset of (TOP-REAL n) equals :: EUCLID_4:def 3 { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } ; coherence { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } is Subset of (TOP-REAL n) proofend; end; :: deftheorem defines Line EUCLID_4:def_3_:_ for n being Nat for p1, p2 being Point of (TOP-REAL n) holds Line (p1,p2) = { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum } ; registration let n be Nat; let p1, p2 be Point of (TOP-REAL n); cluster Line (p1,p2) -> non empty ; coherence not Line (p1,p2) is empty proofend; end; Lm8: for n being Nat for p1, p2 being Point of (TOP-REAL n) ex x1, x2 being Element of REAL n st ( p1 = x1 & p2 = x2 & Line (x1,x2) = Line (p1,p2) ) proofend; definition let n be Nat; let p1, p2 be Point of (TOP-REAL n); :: original:Line redefine func Line (p1,p2) -> Subset of (TOP-REAL n); commutativity for p1, p2 being Point of (TOP-REAL n) holds Line (p1,p2) = Line (p2,p1) proofend; end; theorem Th41: :: EUCLID_4:41 for n being Nat for p1, p2 being Point of (TOP-REAL n) holds ( p1 in Line (p1,p2) & p2 in Line (p1,p2) ) proofend; theorem Th42: :: EUCLID_4:42 for n being Nat for q1, p1, p2, q2 being Point of (TOP-REAL n) st q1 in Line (p1,p2) & q2 in Line (p1,p2) holds Line (q1,q2) c= Line (p1,p2) proofend; theorem Th43: :: EUCLID_4:43 for n being Nat for q1, p1, p2, q2 being Point of (TOP-REAL n) st q1 in Line (p1,p2) & q2 in Line (p1,p2) & q1 <> q2 holds Line (p1,p2) c= Line (q1,q2) proofend; definition let n be Nat; let A be Subset of (TOP-REAL n); attrA is being_line means :Def4: :: EUCLID_4:def 4 ex p1, p2 being Point of (TOP-REAL n) st ( p1 <> p2 & A = Line (p1,p2) ); end; :: deftheorem Def4 defines being_line EUCLID_4:def_4_:_ for n being Nat for A being Subset of (TOP-REAL n) holds ( A is being_line iff ex p1, p2 being Point of (TOP-REAL n) st ( p1 <> p2 & A = Line (p1,p2) ) ); Lm9: for n being Nat for A being Subset of (TOP-REAL n) for p1, p2 being Point of (TOP-REAL n) st A is being_line & p1 in A & p2 in A & p1 <> p2 holds A = Line (p1,p2) proofend; theorem :: EUCLID_4:44 for n being Nat for p1, p2 being Point of (TOP-REAL n) for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds A = C proofend; theorem Th45: :: EUCLID_4:45 for n being Nat for A being Subset of (TOP-REAL n) st A is being_line holds ex p1, p2 being Point of (TOP-REAL n) st ( p1 in A & p2 in A & p1 <> p2 ) proofend; theorem :: EUCLID_4:46 for n being Nat for p1 being Point of (TOP-REAL n) for A being Subset of (TOP-REAL n) st A is being_line holds ex p2 being Point of (TOP-REAL n) st ( p1 <> p2 & p2 in A ) proofend; theorem :: EUCLID_4:47 for n being Nat for R being Subset of REAL for p1, p2, q1 being Point of (TOP-REAL n) st R = { |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2) } holds ex q2 being Point of (TOP-REAL n) st ( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal ) proofend;