:: Introduction to {D}iophantine Approximation
:: by Yasushige Watase
::
:: Received April 19, 2015
:: Copyright (c) 2015 Association of Mizar Users
:: Approximation an irrational by its simple continued fraction
theorem
Th1
:
:: DIOPHAN1:1
for
n
being
Nat
for
r
being
Real
holds
(
r
=
(
rfs
r
)
.
0
&
r
=
(
(
scf
r
)
.
0
)
+
(
1
/
(
(
rfs
r
)
.
1
)
)
&
(
rfs
r
)
.
n
=
(
(
scf
r
)
.
n
)
+
(
1
/
(
(
rfs
r
)
.
(
n
+
1
)
)
)
)
proof
end;
theorem
Th2
:
:: DIOPHAN1:2
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
rfs
r
)
.
n
is
irrational
proof
end;
theorem
Th3
:
:: DIOPHAN1:3
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
(
rfs
r
)
.
n
<>
0
&
(
(
rfs
r
)
.
1
)
*
(
(
rfs
r
)
.
2
)
<>
0
&
(
(
(
scf
r
)
.
1
)
*
(
(
rfs
r
)
.
2
)
)
+
1
<>
0
)
proof
end;
theorem
Th4
:
:: DIOPHAN1:4
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
(
scf
r
)
.
n
<
(
rfs
r
)
.
n
&
(
rfs
r
)
.
n
<
(
(
scf
r
)
.
n
)
+
1 & 1
<
(
rfs
r
)
.
(
n
+
1
)
)
proof
end;
theorem
Th5
:
:: DIOPHAN1:5
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
0
<
(
scf
r
)
.
(
n
+
1
)
proof
end;
theorem
Th6
:
:: DIOPHAN1:6
for
r
being
Real
for
n
being
Nat
holds
(
c_n
r
)
.
n
is
Integer
proof
end;
theorem
Th7
:
:: DIOPHAN1:7
for
r
being
Real
st
r
is
irrational
holds
for
n
being
Nat
holds
(
c_d
r
)
.
(
n
+
1
)
>=
(
c_d
r
)
.
n
proof
end;
theorem
Th8
:
:: DIOPHAN1:8
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
c_d
r
)
.
n
>=
1
proof
end;
::[Hardy&Wrigt] Irrational case of Ch.10 Th155
theorem
:: DIOPHAN1:9
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
c_d
r
)
.
(
n
+
2
)
>
(
c_d
r
)
.
(
n
+
1
)
proof
end;
::[Hard&Wrigt] Ch.10 Th156
theorem
Th10
:
:: DIOPHAN1:10
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
c_d
r
)
.
n
>=
n
proof
end;
::[Hard&Wrigt] Ch.10 Th157
theorem
:: DIOPHAN1:11
for
n
being
Nat
for
r
being
Real
for
cn
,
cd
being
Integer
st
cn
=
(
c_n
r
)
.
n
&
cd
=
(
c_d
r
)
.
n
&
cn
<>
0
holds
cn
,
cd
are_coprime
proof
end;
theorem
Th12
:
:: DIOPHAN1:12
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
(
(
(
c_d
r
)
.
(
n
+
1
)
)
*
(
(
rfs
r
)
.
(
n
+
2
)
)
)
+
(
(
c_d
r
)
.
n
)
>
0
&
(
(
(
c_d
r
)
.
(
n
+
1
)
)
*
(
(
rfs
r
)
.
(
n
+
2
)
)
)
-
(
(
c_d
r
)
.
n
)
>
0
)
proof
end;
theorem
Th13
:
:: DIOPHAN1:13
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
(
c_d
r
)
.
(
n
+
1
)
)
*
(
(
(
(
c_d
r
)
.
(
n
+
1
)
)
*
(
(
rfs
r
)
.
(
n
+
2
)
)
)
+
(
(
c_d
r
)
.
n
)
)
>
0
proof
end;
theorem
Th14
:
:: DIOPHAN1:14
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
r
=
(
(
(
(
c_n
r
)
.
(
n
+
1
)
)
*
(
(
rfs
r
)
.
(
n
+
2
)
)
)
+
(
(
c_n
r
)
.
n
)
)
/
(
(
(
(
c_d
r
)
.
(
n
+
1
)
)
*
(
(
rfs
r
)
.
(
n
+
2
)
)
)
+
(
(
c_d
r
)
.
n
)
)
proof
end;
::[Hard&Wrigt] Ch.10 Th158
theorem
Th15
:
:: DIOPHAN1:15
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
(
(
c_n
r
)
.
(
n
+
1
)
)
/
(
(
c_d
r
)
.
(
n
+
1
)
)
)
-
r
=
(
(
-
1
)
|^
n
)
/
(
(
(
c_d
r
)
.
(
n
+
1
)
)
*
(
(
(
(
c_d
r
)
.
(
n
+
1
)
)
*
(
(
rfs
r
)
.
(
n
+
2
)
)
)
+
(
(
c_d
r
)
.
n
)
)
)
proof
end;
theorem
Th16
:
:: DIOPHAN1:16
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
&
n
is
natural
even
number
&
n
>
0
holds
r
>
(
(
c_n
r
)
.
n
)
/
(
(
c_d
r
)
.
n
)
proof
end;
theorem
Th17
:
:: DIOPHAN1:17
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
&
n
is
natural
odd
number
holds
r
<
(
(
c_n
r
)
.
n
)
/
(
(
c_d
r
)
.
n
)
proof
end;
theorem
:: DIOPHAN1:18
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
&
n
>
0
holds
|.
(
r
-
(
(
(
c_n
r
)
.
n
)
/
(
(
c_d
r
)
.
n
)
)
)
.|
+
|.
(
r
-
(
(
(
c_n
r
)
.
(
n
+
1
)
)
/
(
(
c_d
r
)
.
(
n
+
1
)
)
)
)
.|
=
|.
(
(
(
(
c_n
r
)
.
n
)
/
(
(
c_d
r
)
.
n
)
)
-
(
(
(
c_n
r
)
.
(
n
+
1
)
)
/
(
(
c_d
r
)
.
(
n
+
1
)
)
)
)
.|
proof
end;
theorem
Th19
:
:: DIOPHAN1:19
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
|.
(
r
-
(
(
(
c_n
r
)
.
n
)
/
(
(
c_d
r
)
.
n
)
)
)
.|
>
0
proof
end;
theorem
:: DIOPHAN1:20
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
c_d
r
)
.
(
n
+
2
)
>=
2
*
(
(
c_d
r
)
.
n
)
proof
end;
theorem
Th21
:
:: DIOPHAN1:21
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
|.
(
r
-
(
(
(
c_n
r
)
.
(
n
+
1
)
)
/
(
(
c_d
r
)
.
(
n
+
1
)
)
)
)
.|
<
1
/
(
(
(
c_d
r
)
.
(
n
+
1
)
)
*
(
(
c_d
r
)
.
(
n
+
2
)
)
)
proof
end;
theorem
Th22
:
:: DIOPHAN1:22
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
(
|.
(
(
r
*
(
(
c_d
r
)
.
(
n
+
1
)
)
)
-
(
(
c_n
r
)
.
(
n
+
1
)
)
)
.|
<
|.
(
(
r
*
(
(
c_d
r
)
.
n
)
)
-
(
(
c_n
r
)
.
n
)
)
.|
&
|.
(
r
-
(
(
(
c_n
r
)
.
(
n
+
1
)
)
/
(
(
c_d
r
)
.
(
n
+
1
)
)
)
)
.|
<
|.
(
r
-
(
(
(
c_n
r
)
.
n
)
/
(
(
c_d
r
)
.
n
)
)
)
.|
)
proof
end;
theorem
Th23
:
:: DIOPHAN1:23
for
m
,
n
being
Nat
for
r
being
Real
st
r
is
irrational
&
m
>
n
holds
|.
(
r
-
(
(
(
c_n
r
)
.
n
)
/
(
(
c_d
r
)
.
n
)
)
)
.|
>
|.
(
r
-
(
(
(
c_n
r
)
.
m
)
/
(
(
c_d
r
)
.
m
)
)
)
.|
proof
end;
::[Hardy&Wright] Ch.10 Th164
theorem
Th24
:
:: DIOPHAN1:24
for
n
being
Nat
for
r
being
Real
st
r
is
irrational
holds
|.
(
r
-
(
(
(
c_n
r
)
.
n
)
/
(
(
c_d
r
)
.
n
)
)
)
.|
<
1
/
(
(
(
c_d
r
)
.
n
)
|^
2
)
proof
end;
theorem
:: DIOPHAN1:25
for
S
being
Subset
of
RAT
for
r
being
Real
st
r
is
irrational
&
S
=
{
p
where
p
is
Element
of
RAT
:
|.
(
r
-
p
)
.|
<
1
/
(
(
denominator
p
)
|^
2
)
}
holds
S
is
infinite
proof
end;
theorem
:: DIOPHAN1:26
for
r
being
Real
st
r
is
irrational
holds
(
cocf
r
is
convergent
&
lim
(
cocf
r
)
=
r
)
proof
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Proof of an existance of a solution of|. x*a -y .| < 1/t x < t
:: Dirichlet's argument
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
registration
cluster
ordinal
natural
V19
()
V20
()
ext-real
non
negative
integer
dim-like
finite
cardinal
non
irrational
1
_greater
for
set
;
existence
ex
b
1
being
Nat
st
b
1
is 1
_greater
proof
end;
end;
theorem
Lm1
:
:: DIOPHAN1:27
for
t
being 1
_greater
Nat
holds
(
t
>
0
&
t
>
1 &
t
"
>
0
&
t
*
(
t
"
)
=
1 )
proof
end;
definition
let
t
be 1
_greater
Nat
;
func
Equal_Div_interval
t
->
SetSequence
of
REAL
means
:
Def1
:
:: DIOPHAN1:def 1
for
n
being
Element
of
NAT
holds
it
.
n
=
halfline_fin
(
(
n
*
(
t
"
)
)
,
(
(
n
*
(
t
"
)
)
+
(
t
"
)
)
);
existence
ex
b
1
being
SetSequence
of
REAL
st
for
n
being
Element
of
NAT
holds
b
1
.
n
=
halfline_fin
(
(
n
*
(
t
"
)
)
,
(
(
n
*
(
t
"
)
)
+
(
t
"
)
)
)
proof
end;
uniqueness
for
b
1
,
b
2
being
SetSequence
of
REAL
st ( for
n
being
Element
of
NAT
holds
b
1
.
n
=
halfline_fin
(
(
n
*
(
t
"
)
)
,
(
(
n
*
(
t
"
)
)
+
(
t
"
)
)
) ) & ( for
n
being
Element
of
NAT
holds
b
2
.
n
=
halfline_fin
(
(
n
*
(
t
"
)
)
,
(
(
n
*
(
t
"
)
)
+
(
t
"
)
)
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def1
defines
Equal_Div_interval
DIOPHAN1:def 1 :
for
t
being 1
_greater
Nat
for
b
2
being
SetSequence
of
REAL
holds
(
b
2
=
Equal_Div_interval
t
iff for
n
being
Element
of
NAT
holds
b
2
.
n
=
halfline_fin
(
(
n
*
(
t
"
)
)
,
(
(
n
*
(
t
"
)
)
+
(
t
"
)
)
) );
theorem
Lm2
:
:: DIOPHAN1:28
for
k
being
Nat
for
t
being 1
_greater
Nat
holds
[.
0
,
(
(
k
+
1
)
*
(
t
"
)
)
.[
\/
[.
(
(
k
+
1
)
*
(
t
"
)
)
,
(
(
k
+
2
)
*
(
t
"
)
)
.[
=
[.
0
,
(
(
k
+
2
)
*
(
t
"
)
)
.[
proof
end;
theorem
Lm3
:
:: DIOPHAN1:29
for
i
being
Nat
for
t
being 1
_greater
Nat
holds
(
Partial_Union
(
Equal_Div_interval
t
)
)
.
i
=
[.
0
,
(
(
i
+
1
)
*
(
t
"
)
)
.[
proof
end;
theorem
Lm4
:
:: DIOPHAN1:30
for
t
being 1
_greater
Nat
for
r
being
Real
for
i
being
Nat
st
[\
(
r
*
t
)
/]
=
i
holds
r
in
(
Equal_Div_interval
t
)
.
i
proof
end;
theorem
Lm5
:
:: DIOPHAN1:31
for
i
being
Nat
for
r1
,
r2
being
Real
for
t
being 1
_greater
Nat
st
r1
in
(
Equal_Div_interval
t
)
.
i
&
r2
in
(
Equal_Div_interval
t
)
.
i
holds
|.
(
r1
-
r2
)
.|
<
t
"
proof
end;
theorem
Lm6
:
:: DIOPHAN1:32
for
t
being 1
_greater
Nat
holds
(
Partial_Union
(
Equal_Div_interval
t
)
)
.
(
t
-
1
)
=
[.
0
,1
.[
proof
end;
theorem
Lm7
:
:: DIOPHAN1:33
for
t
being 1
_greater
Nat
for
r
being
Real
st
r
in
[.
0
,1
.[
holds
ex
i
being
Nat
st
(
i
<=
t
-
1 &
r
in
(
Equal_Div_interval
t
)
.
i
)
proof
end;
theorem
Lm8
:
:: DIOPHAN1:34
for
t
being 1
_greater
Nat
for
r
being
Real
for
i
being
Nat
st
r
in
(
Equal_Div_interval
t
)
.
i
holds
[\
(
r
*
t
)
/]
=
i
proof
end;
theorem
Lm9
:
:: DIOPHAN1:35
for
t
being 1
_greater
Nat
for
r
being
Real
st
r
in
[.
0
,1
.[
holds
ex
i
being
Nat
st
(
i
<=
t
-
1 &
[\
(
r
*
t
)
/]
=
i
)
proof
end;
definition
let
t
be 1
_greater
Nat
;
let
a
be
Real
;
func
F_dp1
(
t
,
a
)
->
FinSequence
of
Segm
t
means
:
Def4
:
:: DIOPHAN1:def 2
(
len
it
=
t
+
1 & ( for
i
being
Nat
st
i
in
dom
it
holds
it
.
i
=
[\
(
(
frac
(
(
i
-
1
)
*
a
)
)
*
t
)
/]
) );
existence
ex
b
1
being
FinSequence
of
Segm
t
st
(
len
b
1
=
t
+
1 & ( for
i
being
Nat
st
i
in
dom
b
1
holds
b
1
.
i
=
[\
(
(
frac
(
(
i
-
1
)
*
a
)
)
*
t
)
/]
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
FinSequence
of
Segm
t
st
len
b
1
=
t
+
1 & ( for
i
being
Nat
st
i
in
dom
b
1
holds
b
1
.
i
=
[\
(
(
frac
(
(
i
-
1
)
*
a
)
)
*
t
)
/]
) &
len
b
2
=
t
+
1 & ( for
i
being
Nat
st
i
in
dom
b
2
holds
b
2
.
i
=
[\
(
(
frac
(
(
i
-
1
)
*
a
)
)
*
t
)
/]
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def4
defines
F_dp1
DIOPHAN1:def 2 :
for
t
being 1
_greater
Nat
for
a
being
Real
for
b
3
being
FinSequence
of
Segm
t
holds
(
b
3
=
F_dp1
(
t
,
a
) iff (
len
b
3
=
t
+
1 & ( for
i
being
Nat
st
i
in
dom
b
3
holds
b
3
.
i
=
[\
(
(
frac
(
(
i
-
1
)
*
a
)
)
*
t
)
/]
) ) );
theorem
Lm10
:
:: DIOPHAN1:36
for
a
being
Real
for
t
being 1
_greater
Nat
holds
(
card
(
rng
(
F_dp1
(
t
,
a
)
)
)
in
card
(
dom
(
F_dp1
(
t
,
a
)
)
)
&
rng
(
F_dp1
(
t
,
a
)
)
<>
{}
)
proof
end;
theorem
Th27
:
:: DIOPHAN1:37
for
a
being
Real
for
t
being 1
_greater
Nat
ex
x1
,
x2
being
object
st
(
x1
in
dom
(
F_dp1
(
t
,
a
)
)
&
x2
in
dom
(
F_dp1
(
t
,
a
)
)
&
x1
<>
x2
&
(
F_dp1
(
t
,
a
)
)
.
x1
=
(
F_dp1
(
t
,
a
)
)
.
x2
)
proof
end;
::[Baker] Chapter 6.1
::
Dirichlet's approximation theorem
theorem
:: DIOPHAN1:38
for
a
being
Real
for
t
being 1
_greater
Nat
ex
x
,
y
being
Integer
st
(
|.
(
(
x
*
a
)
-
y
)
.|
<
1
/
t
&
0
<
x
&
x
<=
t
)
proof
end;