let r be Real; ( r is irrational implies ( cocf r is convergent & lim (cocf r) = r ) )
assume A1:
r is irrational
; ( cocf r is convergent & lim (cocf r) = r )
A2:
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((cocf r) . m) - r).| < p
proof
let p be
Real;
( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((cocf r) . m) - r).| < p )
assume A3:
p > 0
;
ex n being Nat st
for m being Nat st n <= m holds
|.(((cocf r) . m) - r).| < p
then A4:
sqrt p > 0
by SQUARE_1:25;
A7:
[/(1 / (sqrt p))\] >= 1
/ (sqrt p)
by INT_1:def 7;
[/(1 / (sqrt p))\] > 0
by A4, INT_1:def 7;
then
[/(1 / (sqrt p))\] in NAT
by INT_1:3;
then consider n being
Nat such that A9:
n = [/(1 / (sqrt p))\]
;
A10:
n > 0
by A4, INT_1:def 7, A9;
for
k being
Nat st
k >= n holds
|.(((cocf r) . k) - r).| < p
proof
let k be
Nat;
( k >= n implies |.(((cocf r) . k) - r).| < p )
assume A12:
k >= n
;
|.(((cocf r) . k) - r).| < p
A13:
(cocf r) . k =
((c_n r) /" (c_d r)) . k
by REAL_3:def 7
.=
((c_n r) . k) * (((c_d r) ") . k)
by SEQ_1:8
.=
((c_n r) . k) / ((c_d r) . k)
by VALUED_1:10
;
A14:
|.(((cocf r) . k) - r).| =
|.(- (((cocf r) . k) - r)).|
by COMPLEX1:52
.=
|.(r - (((c_n r) . k) / ((c_d r) . k))).|
by A13
;
(1 / (sqrt p)) ^2 =
((sqrt p) ") * ((sqrt p) ")
by SQUARE_1:def 1
.=
((sqrt p) * (sqrt p)) "
by XCMPLX_1:204
.=
((sqrt p) ^2) "
by SQUARE_1:def 1
.=
p "
by A3, SQUARE_1:def 2
;
then
n ^2 >= p "
by A4, A7, SQUARE_1:15, A9;
then A16:
(n ^2) " <= (p ") "
by A3, XREAL_1:85;
k ^2 >= n ^2
by A12, SQUARE_1:15;
then A18:
(k ^2) " <= (n ^2) "
by A10, SQUARE_1:12, XREAL_1:85;
A19:
((c_d r) . k) ^2 =
((c_d r) . k) * ((c_d r) . k)
by SQUARE_1:def 1
.=
((c_d r) . k) |^ 2
by WSIERP_1:1
;
A20:
((c_d r) . k) ^2 >= k ^2
by A1, Th10, SQUARE_1:15;
(((c_d r) . k) ^2) " =
(((c_d r) . k) |^ 2) "
by A19
.=
1
/ (((c_d r) . k) |^ 2)
;
then
1
/ (((c_d r) . k) |^ 2) <= (k ^2) "
by A12, A10, SQUARE_1:12, XREAL_1:85, A20;
then
1
/ (((c_d r) . k) |^ 2) <= (n ^2) "
by A18, XXREAL_0:2;
then
1
/ (((c_d r) . k) |^ 2) <= p
by A16, XXREAL_0:2;
hence
|.(((cocf r) . k) - r).| < p
by XXREAL_0:2, A1, Th24, A14;
verum
end;
hence
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.(((cocf r) . m) - r).| < p
;
verum
end;
cocf r is convergent
by A2, SEQ_2:def 6;
hence
( cocf r is convergent & lim (cocf r) = r )
by A2, SEQ_2:def 7; verum