:: Lines in $n$-Dimensional Euclidean Spaces
:: by Akihiro Kubo
::
:: Received August 8, 2003
:: Copyright (c) 2003 Association of Mizar Users
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
)
proof
end;
theorem
Th2
:
:: EUCLID_4:2
for
a
being
Real
for
n
being
Nat
holds
a
*
(
0*
n
)
=
0*
n
proof
end;
theorem
Th3
:
:: EUCLID_4:3
for
n
being
Nat
for
x
being
Element
of
REAL
n
holds
( 1
*
x
=
x
&
0
*
x
=
0*
n
)
proof
end;
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:71
;
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
)
proof
end;
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:73
;
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:72
;
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
)
proof
end;
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
)
proof
end;
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
proof
end;
end;
Lm1
: for
n
being
Nat
for
x1
,
x2
being
Element
of
REAL
n
holds
Line
x1
,
x2
c=
Line
x2
,
x1
proof
end;
theorem
Th9
:
:: EUCLID_4:9
for
n
being
Nat
for
x1
,
x2
being
Element
of
REAL
n
holds
Line
x1
,
x2
=
Line
x2
,
x1
proof
end;
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
by
Th9
;
end;
theorem
Th10
:
:: EUCLID_4:10
for
n
being
Nat
for
x1
,
x2
being
Element
of
REAL
n
holds
(
x1
in
Line
x1
,
x2
&
x2
in
Line
x1
,
x2
)
proof
end;
Lm2
: for
n
being
Nat
for
x1
,
x2
,
x3
being
Element
of
REAL
n
holds
x1
+
(
x2
+
x3
)
=
(
x1
+
x2
)
+
x3
by
FINSEQOP:29
;
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
holds
Line
y1
,
y2
c=
Line
x1
,
x2
proof
end;
theorem
Th12
:
:: EUCLID_4:12
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
proof
end;
definition
let
n
be
Nat
;
let
A
be
Subset
of
(
REAL
n
)
;
attr
A
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
proof
end;
theorem
:: EUCLID_4:13
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
proof
end;
theorem
Th14
:
:: EUCLID_4:14
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
)
proof
end;
theorem
:: EUCLID_4:15
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
)
proof
end;
definition
canceled;
canceled;
canceled;
end;
::
deftheorem
EUCLID_4:def 3 :
canceled;
::
deftheorem
EUCLID_4:def 4 :
canceled;
::
deftheorem
EUCLID_4:def 5 :
canceled;
theorem
:: EUCLID_4:16
canceled;
theorem
:: EUCLID_4:17
canceled;
theorem
:: EUCLID_4:18
canceled;
theorem
:: EUCLID_4:19
canceled;
theorem
:: EUCLID_4:20
for
n
being
Nat
for
x
being
Element
of
REAL
n
holds
|.
x
.|
=
sqrt
|(
x
,
x
)|
proof
end;
theorem
Th21
:
:: EUCLID_4:21
for
n
being
Nat
for
x
being
Element
of
REAL
n
holds
(
|(
x
,
x
)|
=
0
iff
|.
x
.|
=
0
)
proof
end;
theorem
Th22
:
:: EUCLID_4:22
for
n
being
Nat
for
x
being
Element
of
REAL
n
holds
(
|(
x
,
x
)|
=
0
iff
x
=
0*
n
)
proof
end;
theorem
Th23
:
:: EUCLID_4:23
for
n
being
Nat
for
x
being
Element
of
REAL
n
holds
|(
x
,
(
0*
n
)
)|
=
0
proof
end;
theorem
:: EUCLID_4:24
for
n
being
Nat
for
x
being
Element
of
REAL
n
holds
|(
(
0*
n
)
,
x
)|
=
0
by
Th23
;
theorem
Th25
:
:: EUCLID_4:25
for
n
being
Nat
for
x1
,
x2
,
x3
being
Element
of
REAL
n
holds
|(
(
x1
+
x2
)
,
x3
)|
=
|(
x1
,
x3
)|
+
|(
x2
,
x3
)|
proof
end;
theorem
Th26
:
:: EUCLID_4:26
for
n
being
Nat
for
x1
,
x2
being
Element
of
REAL
n
for
a
being
real
number
holds
|(
(
a
*
x1
)
,
x2
)|
=
a
*
|(
x1
,
x2
)|
proof
end;
theorem
:: EUCLID_4:27
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
Th26
;
theorem
Th28
:
:: EUCLID_4:28
for
n
being
Nat
for
x1
,
x2
being
Element
of
REAL
n
holds
|(
(
-
x1
)
,
x2
)|
=
-
|(
x1
,
x2
)|
proof
end;
theorem
:: EUCLID_4:29
for
n
being
Nat
for
x1
,
x2
being
Element
of
REAL
n
holds
|(
x1
,
(
-
x2
)
)|
=
-
|(
x1
,
x2
)|
by
Th28
;
theorem
:: EUCLID_4:30
for
n
being
Nat
for
x1
,
x2
being
Element
of
REAL
n
holds
|(
(
-
x1
)
,
(
-
x2
)
)|
=
|(
x1
,
x2
)|
proof
end;
theorem
Th31
:
:: EUCLID_4:31
for
n
being
Nat
for
x1
,
x2
,
x3
being
Element
of
REAL
n
holds
|(
(
x1
-
x2
)
,
x3
)|
=
|(
x1
,
x3
)|
-
|(
x2
,
x3
)|
proof
end;
theorem
:: EUCLID_4:32
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
)|
)
proof
end;
theorem
:: EUCLID_4:33
for
n
being
Nat
for
x1
,
y1
,
y2
being
Element
of
REAL
n
holds
|(
x1
,
(
y1
+
y2
)
)|
=
|(
x1
,
y1
)|
+
|(
x1
,
y2
)|
by
Th25
;
theorem
:: EUCLID_4:34
for
n
being
Nat
for
x1
,
y1
,
y2
being
Element
of
REAL
n
holds
|(
x1
,
(
y1
-
y2
)
)|
=
|(
x1
,
y1
)|
-
|(
x1
,
y2
)|
by
Th31
;
theorem
Th35
:
:: EUCLID_4:35
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
)|
proof
end;
theorem
Th36
:
:: EUCLID_4:36
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
)|
proof
end;
theorem
Th37
:
:: EUCLID_4:37
for
n
being
Nat
for
x
,
y
being
Element
of
REAL
n
holds
|(
(
x
+
y
)
,
(
x
+
y
)
)|
=
(
|(
x
,
x
)|
+
(
2
*
|(
x
,
y
)|
)
)
+
|(
y
,
y
)|
proof
end;
theorem
Th38
:
:: EUCLID_4:38
for
n
being
Nat
for
x
,
y
being
Element
of
REAL
n
holds
|(
(
x
-
y
)
,
(
x
-
y
)
)|
=
(
|(
x
,
x
)|
-
(
2
*
|(
x
,
y
)|
)
)
+
|(
y
,
y
)|
proof
end;
theorem
:: EUCLID_4:39
for
n
being
Nat
for
x
,
y
being
Element
of
REAL
n
holds
|.
(
x
+
y
)
.|
^2
=
(
(
|.
x
.|
^2
)
+
(
2
*
|(
x
,
y
)|
)
)
+
(
|.
y
.|
^2
)
proof
end;
theorem
:: EUCLID_4:40
for
n
being
Nat
for
x
,
y
being
Element
of
REAL
n
holds
|.
(
x
-
y
)
.|
^2
=
(
(
|.
x
.|
^2
)
-
(
2
*
|(
x
,
y
)|
)
)
+
(
|.
y
.|
^2
)
proof
end;
theorem
:: EUCLID_4:41
for
n
being
Nat
for
x
,
y
being
Element
of
REAL
n
holds
(
|.
(
x
+
y
)
.|
^2
)
+
(
|.
(
x
-
y
)
.|
^2
)
=
2
*
(
(
|.
x
.|
^2
)
+
(
|.
y
.|
^2
)
)
proof
end;
theorem
:: EUCLID_4:42
for
n
being
Nat
for
x
,
y
being
Element
of
REAL
n
holds
(
|.
(
x
+
y
)
.|
^2
)
-
(
|.
(
x
-
y
)
.|
^2
)
=
4
*
|(
x
,
y
)|
proof
end;
theorem
:: EUCLID_4:43
for
n
being
Nat
for
x
,
y
being
Element
of
REAL
n
holds
abs
|(
x
,
y
)|
<=
|.
x
.|
*
|.
y
.|
proof
end;
theorem
:: EUCLID_4:44
for
n
being
Nat
for
x
,
y
being
Element
of
REAL
n
holds
|.
(
x
+
y
)
.|
<=
|.
x
.|
+
|.
y
.|
proof
end;
definition
canceled;
end;
::
deftheorem
EUCLID_4:def 6 :
canceled;
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
)
)
proof
end;
Lm5
: for
n
being
Nat
for
x1
,
x2
being
Element
of
REAL
n
st
x1
<>
x2
holds
|.
(
x1
-
x2
)
.|
<>
0
proof
end;
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
)
proof
end;
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
)
.|
) )
proof
end;
theorem
:: EUCLID_4:45
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
)
proof
end;
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 7
{
(
(
(
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
)
proof
end;
end;
::
deftheorem
defines
Line
EUCLID_4:def 7 :
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
proof
end;
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
)
proof
end;
theorem
Th46
:
:: EUCLID_4:46
for
n
being
Nat
for
p1
,
p2
being
Point
of
(
TOP-REAL
n
)
holds
Line
p1
,
p2
=
Line
p2
,
p1
proof
end;
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
by
Th46
;
end;
theorem
Th47
:
:: EUCLID_4:47
for
n
being
Nat
for
p1
,
p2
being
Point
of
(
TOP-REAL
n
)
holds
(
p1
in
Line
p1
,
p2
&
p2
in
Line
p1
,
p2
)
proof
end;
theorem
Th48
:
:: EUCLID_4:48
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
proof
end;
theorem
Th49
:
:: EUCLID_4:49
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
proof
end;
definition
let
n
be
Nat
;
let
A
be
Subset
of
(
TOP-REAL
n
)
;
attr
A
is
being_line
means
:
Def8
:
:: EUCLID_4:def 8
ex
p1
,
p2
being
Point
of
(
TOP-REAL
n
)
st
(
p1
<>
p2
&
A
=
Line
p1
,
p2
);
end;
::
deftheorem
Def8
defines
being_line
EUCLID_4:def 8 :
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
proof
end;
theorem
:: EUCLID_4:50
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
proof
end;
theorem
Th51
:
:: EUCLID_4:51
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
)
proof
end;
theorem
:: EUCLID_4:52
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
)
proof
end;
definition
let
n
be
Nat
;
let
p
be
Point
of
(
TOP-REAL
n
)
;
func
TPn2Rn
p
->
Element
of
REAL
n
equals
:: EUCLID_4:def 9
p
;
correctness
coherence
p
is
Element
of
REAL
n
;
by
EUCLID:25
;
end;
::
deftheorem
defines
TPn2Rn
EUCLID_4:def 9 :
for
n
being
Nat
for
p
being
Point
of
(
TOP-REAL
n
)
holds
TPn2Rn
p
=
p
;
theorem
:: EUCLID_4:53
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
)
proof
end;