defpred S1[ Nat] means for x being Point of (REAL-NS $1)
for xs being Element of REAL $1
for seq being sequence of (REAL-NS $1)
for xseq being sequence of (REAL $1) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg $1 holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) );
A1:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume A2:
S1[
n]
;
S1[n + 1]now for x being Point of (REAL-NS (n + 1))
for xs being Element of REAL (n + 1)
for seq being sequence of (REAL-NS (n + 1))
for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )let x be
Point of
(REAL-NS (n + 1));
for xs being Element of REAL (n + 1)
for seq being sequence of (REAL-NS (n + 1))
for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )let xs be
Element of
REAL (n + 1);
for seq being sequence of (REAL-NS (n + 1))
for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )let seq be
sequence of
(REAL-NS (n + 1));
for xseq being sequence of (REAL (n + 1)) st xs = x & xseq = seq holds
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )let xseq be
sequence of
(REAL (n + 1));
( xs = x & xseq = seq implies ( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) )assume A3:
(
xs = x &
xseq = seq )
;
( ( seq is convergent & lim seq = x ) iff for i being Nat st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) )A4:
now ( ( for i being Nat st i in Seg (n + 1) holds
ex rseqi being Real_Sequence st
for k being Nat holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) ) implies ( seq is convergent & lim seq = x ) )assume A5:
for
i being
Nat st
i in Seg (n + 1) holds
ex
rseqi being
Real_Sequence st
for
k being
Nat holds
(
rseqi . k = (xseq . k) . i &
rseqi is
convergent &
xs . i = lim rseqi )
;
( seq is convergent & lim seq = x )thus
(
seq is
convergent &
lim seq = x )
verumproof
len xs = n + 1
by CARD_1:def 7;
then
len (xs | n) = n
by FINSEQ_1:59, NAT_1:11;
then
dom (xs | n) = Seg n
by FINSEQ_1:def 3;
then reconsider xsn =
xs | n as
Element of
REAL n by Th6;
reconsider xn =
xsn as
Point of
(REAL-NS n) by Def4;
defpred S2[
Nat,
Element of
REAL n]
means $2
= (xseq . $1) | n;
set seq2 =
||.(seq - x).|| (#) ||.(seq - x).||;
consider rseqn1 being
Real_Sequence such that A6:
for
k being
Nat holds
(
rseqn1 . k = (xseq . k) . (n + 1) &
rseqn1 is
convergent &
xs . (n + 1) = lim rseqn1 )
by A5, FINSEQ_1:4;
A7:
for
i being
Element of
NAT ex
y being
Element of
REAL n st
S2[
i,
y]
consider xseqn being
sequence of
(REAL n) such that A8:
for
i being
Element of
NAT holds
S2[
i,
xseqn . i]
from FUNCT_2:sch 3(A7);
reconsider seqn =
xseqn as
sequence of
(REAL-NS n) by Def4;
set seqn2 =
||.(seqn - xn).|| (#) ||.(seqn - xn).||;
deffunc H1(
Nat)
-> object =
|.((rseqn1 . $1) - (xs . (n + 1))).|;
consider absrseq being
Real_Sequence such that A9:
for
i being
Nat holds
absrseq . i = H1(
i)
from SEQ_1:sch 1();
A10:
for
i being
Nat st
i in Seg n holds
ex
rseqi being
Real_Sequence st
for
k being
Nat holds
(
rseqi . k = (xseqn . k) . i &
rseqi is
convergent &
xsn . i = lim rseqi )
then A15:
xn = lim seqn
by A2;
set rseqn2 =
absrseq (#) absrseq;
xsn = xn
;
then A16:
seqn is
convergent
by A2, A10;
then A17:
||.(seqn - xn).|| is
convergent
by A15, NORMSP_1:24;
then A18:
||.(seqn - xn).|| (#) ||.(seqn - xn).|| is
convergent
by SEQ_2:14;
now for k being Nat holds (||.(seq - x).|| (#) ||.(seq - x).||) . k = ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k)reconsider rxs =
xs as
Element of
(n + 1) -tuples_on REAL by EUCLID:def 1;
let k be
Nat;
(||.(seq - x).|| (#) ||.(seq - x).||) . k = ((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k)A19:
k in NAT
by ORDINAL1:def 12;
A20:
||.(seq - x).|| . k =
||.((seq - x) . k).||
by NORMSP_0:def 4
.=
||.((seq . k) - x).||
by NORMSP_1:def 4
;
reconsider rxseqk =
xseq . k as
Element of
(n + 1) -tuples_on REAL by EUCLID:def 1;
A21:
||.(seqn - xn).|| . k =
||.((seqn - xn) . k).||
by NORMSP_0:def 4
.=
||.((seqn . k) - xn).||
by NORMSP_1:def 4
;
len ((xseqn . k) - xsn) = n
by CARD_1:def 7;
then A22:
dom ((xseqn . k) - xsn) = Seg n
by FINSEQ_1:def 3;
A23:
((xseq . k) - xs) . (n + 1) =
(rxseqk . (n + 1)) - (rxs . (n + 1))
by RVSUM_1:27
.=
(rseqn1 . k) - (xs . (n + 1))
by A6
;
len ((xseq . k) - xs) = n + 1
by CARD_1:def 7;
then A24:
len (((xseq . k) - xs) | n) = n
by FINSEQ_1:59, NAT_1:11;
A25:
now for i being Nat st i in dom (((xseq . k) - xs) | n) holds
(((xseq . k) - xs) | n) . i = ((xseqn . k) - xsn) . iend;
dom (((xseq . k) - xs) | n) = Seg n
by A24, FINSEQ_1:def 3;
then A29:
((xseq . k) - xs) | n = (xseqn . k) - xsn
by A22, A25, FINSEQ_1:13;
A30:
0 <= ((rseqn1 . k) - (xs . (n + 1))) ^2
by XREAL_1:63;
A31:
absrseq . k = |.((rseqn1 . k) - (xs . (n + 1))).|
by A9;
||.((seq . k) - x).|| = |.((xseq . k) - xs).|
by A3, Th1, Th5;
hence (||.(seq - x).|| (#) ||.(seq - x).||) . k =
|.((xseq . k) - xs).| ^2
by A20, SEQ_1:8
.=
(|.((xseqn . k) - xsn).| ^2) + (((rseqn1 . k) - (xs . (n + 1))) ^2)
by A23, A29, Th10
.=
(||.((seqn . k) - xn).|| ^2) + (((rseqn1 . k) - (xs . (n + 1))) ^2)
by Th1, Th5
.=
((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + (((rseqn1 . k) - (xs . (n + 1))) ^2)
by A21, SEQ_1:8
.=
((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + |.(((rseqn1 . k) - (xs . (n + 1))) * ((rseqn1 . k) - (xs . (n + 1)))).|
by A30, ABSVALUE:def 1
.=
((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + (|.((rseqn1 . k) - (xs . (n + 1))).| * |.((rseqn1 . k) - (xs . (n + 1))).|)
by COMPLEX1:65
.=
((||.(seqn - xn).|| (#) ||.(seqn - xn).||) . k) + ((absrseq (#) absrseq) . k)
by A31, SEQ_1:8
;
verum end;
then A32:
||.(seq - x).|| (#) ||.(seq - x).|| = (||.(seqn - xn).|| (#) ||.(seqn - xn).||) + (absrseq (#) absrseq)
by SEQ_1:7;
then A35:
absrseq is
convergent
by SEQ_2:def 6;
then
lim absrseq = 0
by A33, SEQ_2:def 7;
then A36:
lim (absrseq (#) absrseq) =
0 * 0
by A35, SEQ_2:15
.=
0
;
A37:
absrseq (#) absrseq is
convergent
by A35, SEQ_2:14;
then A38:
||.(seq - x).|| (#) ||.(seq - x).|| is
convergent
by A18, A32, SEQ_2:5;
lim ||.(seqn - xn).|| = 0
by A16, A15, NORMSP_1:24;
then lim (||.(seqn - xn).|| (#) ||.(seqn - xn).||) =
0 * 0
by A17, SEQ_2:15
.=
0
;
then A39:
lim (||.(seq - x).|| (#) ||.(seq - x).||) =
0 + 0
by A18, A37, A36, A32, SEQ_2:6
.=
0
;
A40:
for
e being
Real st
e > 0 holds
ex
m being
Nat st
for
k being
Nat st
k >= m holds
||.((seq . k) - x).|| < e
then
seq is
convergent
by NORMSP_1:def 6;
hence
(
seq is
convergent &
lim seq = x )
by A40, NORMSP_1:def 7;
verum
end; end; hence
( (
seq is
convergent &
lim seq = x ) iff for
i being
Nat st
i in Seg (n + 1) holds
ex
rseqi being
Real_Sequence st
for
k being
Nat holds
(
rseqi . k = (xseq . k) . i &
rseqi is
convergent &
xs . i = lim rseqi ) )
by A4;
verum end; hence
S1[
n + 1]
;
verum end;
A55:
S1[ 0 ]
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A55, A1); verum