let f be Real_Sequence; :: thesis: for K being Real
for N being Nat st f is convergent & ( for n being Nat st N <= n holds
K <= f . n ) holds
K <= lim f
let K be Real; :: thesis: for N being Nat st f is convergent & ( for n being Nat st N <= n holds
K <= f . n ) holds
K <= lim f
let N be Nat; :: thesis: ( f is convergent & ( for n being Nat st N <= n holds
K <= f . n ) implies K <= lim f )
assume that
A1: f is convergent and
A2: for n being Nat st N <= n holds
K <= f . n ; :: thesis: K <= lim f
set e = (K - (lim f)) / 2;
assume K > lim f ; :: thesis: contradiction
then B2: 0 < K - (lim f) by XREAL_1:50;
then A3: ( 0 < (K - (lim f)) / 2 & (K - (lim f)) / 2 < K - (lim f) ) by XREAL_1:216;
consider N1 being Nat such that
A4: for m being Nat st N1 <= m holds
|.((f . m) - (lim f)).| < (K - (lim f)) / 2 by A1, B2, SEQ_2:def 7;
reconsider N2 = max (N,N1) as Nat by XXREAL_0:16;
|.((f . N2) - (lim f)).| < (K - (lim f)) / 2 by A4, XXREAL_0:25;
then ( - ((K - (lim f)) / 2) <= (f . N2) - (lim f) & (f . N2) - (lim f) <= (K - (lim f)) / 2 ) by ABSVALUE:5;
then A6: ((f . N2) - (lim f)) + (lim f) <= ((K - (lim f)) / 2) + (lim f) by XREAL_1:7;
((K - (lim f)) / 2) + (lim f) < (K - (lim f)) + (lim f) by A3, XREAL_1:8;
then f . N2 < K by A6, XXREAL_0:2;
hence contradiction by A2, XXREAL_0:25; :: thesis: verum