let N be Nat; :: thesis: for seq being Real_Sequence of N
for n being Nat ex r being Real st
( 0 < r & ( for m being Nat st m <= n holds
|.(seq . m).| < r ) )
let seq be Real_Sequence of N; :: thesis: for n being Nat ex r being Real st
( 0 < r & ( for m being Nat st m <= n holds
|.(seq . m).| < r ) )
defpred S1[ Nat] means ex r1 being Real st
( 0 < r1 & ( for m being Nat st m <= $1 holds
|.(seq . m).| < r1 ) );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
given r1 being Real such that A2: 0 < r1 and
A3: for m being Nat st m <= n holds
|.(seq . m).| < r1 ; :: thesis: S1[n + 1]
A4: now :: thesis: ( r1 <= |.(seq . (n + 1)).| implies ex r being set st
( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) ) )
assume A5: r1 <= |.(seq . (n + 1)).| ; :: thesis: ex r being set st
( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) )
take r = |.(seq . (n + 1)).| + 1; :: thesis: ( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) )
thus 0 < r ; :: thesis: for m being Nat st m <= n + 1 holds
|.(seq . m).| < r
let m be Nat; :: thesis: ( m <= n + 1 implies |.(seq . m).| < r )
assume A6: m <= n + 1 ; :: thesis: |.(seq . m).| < r
A7: now :: thesis: ( m <= n implies |.(seq . m).| < r )
assume m <= n ; :: thesis: |.(seq . m).| < r
then |.(seq . m).| < r1 by A3;
then |.(seq . m).| < |.(seq . (n + 1)).| by A5, XXREAL_0:2;
then |.(seq . m).| + 0 < r by XREAL_1:8;
hence |.(seq . m).| < r ; :: thesis: verum
end;
now :: thesis: ( m = n + 1 implies |.(seq . m).| < r )
assume m = n + 1 ; :: thesis: |.(seq . m).| < r
then |.(seq . m).| + 0 < r by XREAL_1:8;
hence |.(seq . m).| < r ; :: thesis: verum
end;
hence |.(seq . m).| < r by A6, A7, NAT_1:8; :: thesis: verum
end;
now :: thesis: ( |.(seq . (n + 1)).| <= r1 implies ex r being set st
( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) ) )
assume A8: |.(seq . (n + 1)).| <= r1 ; :: thesis: ex r being set st
( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) )
take r = r1 + 1; :: thesis: ( 0 < r & ( for m being Nat st m <= n + 1 holds
|.(seq . m).| < r ) )
thus 0 < r by A2; :: thesis: for m being Nat st m <= n + 1 holds
|.(seq . m).| < r
let m be Nat; :: thesis: ( m <= n + 1 implies |.(seq . m).| < r )
assume A9: m <= n + 1 ; :: thesis: |.(seq . m).| < r
A10: now :: thesis: ( m <= n implies |.(seq . m).| < r )
assume m <= n ; :: thesis: |.(seq . m).| < r
then A11: |.(seq . m).| < r1 by A3;
r1 + 0 < r by XREAL_1:8;
hence |.(seq . m).| < r by A11, XXREAL_0:2; :: thesis: verum
end;
now :: thesis: ( m = n + 1 implies |.(seq . m).| < r )
A12: r1 + 0 < r by XREAL_1:8;
assume m = n + 1 ; :: thesis: |.(seq . m).| < r
hence |.(seq . m).| < r by A8, A12, XXREAL_0:2; :: thesis: verum
end;
hence |.(seq . m).| < r by A9, A10, NAT_1:8; :: thesis: verum
end;
hence S1[n + 1] by A4; :: thesis: verum
end;
A13: S1[ 0 ]
proof
take r = |.(seq . 0).| + 1; :: thesis: ( 0 < r & ( for m being Nat st m <= 0 holds
|.(seq . m).| < r ) )
thus 0 < r ; :: thesis: for m being Nat st m <= 0 holds
|.(seq . m).| < r
let m be Nat; :: thesis: ( m <= 0 implies |.(seq . m).| < r )
assume m <= 0 ; :: thesis: |.(seq . m).| < r
then 0 = m ;
then |.(seq . m).| + 0 < r by XREAL_1:8;
hence |.(seq . m).| < r ; :: thesis: verum
end;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A13, A1); :: thesis: verum