let A be non empty closed_interval Subset of REAL; :: thesis: for Z being open Subset of REAL
for n being non zero Nat st Z = right_open_halfline 0 & A = [.n,(n + 1).] holds
integral (((id Z) ^),A) < 1 / n
let Z be open Subset of REAL; :: thesis: for n being non zero Nat st Z = right_open_halfline 0 & A = [.n,(n + 1).] holds
integral (((id Z) ^),A) < 1 / n
let n be non zero Nat; :: thesis: ( Z = right_open_halfline 0 & A = [.n,(n + 1).] implies integral (((id Z) ^),A) < 1 / n )
assume aa: ( Z = right_open_halfline 0 & A = [.n,(n + 1).] ) ; :: thesis: integral (((id Z) ^),A) < 1 / n
N1: not 0 in Z by aa, XXREAL_1:4;
A1: A c= Z

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Z )
assume BB: x in A ; :: thesis: x in Z
then reconsider xx = x as Real ;
( n <= xx & xx <= n + 1 ) by BB, aa, XXREAL_1:1;
hence x in Z by aa, XXREAL_1:235; :: thesis: verum

end;

set f = id Z;
a3: dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def 2
.= Z \ {} by Counter0, N1
.= Z ;
B1: lower_bound A = n by aa, XREAL_1:31, XXREAL_2:25;
B2: upper_bound A = n + 1 by aa, XREAL_1:31, XXREAL_2:29;
((id Z) ^) | A is continuous by ContCut, A1, N1;
then integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A)) by A1, aa, TAYLOR_1:18, a3, INTEGRA9:61
.= ln . ((n + 1) / n) by B1, B2, DIFF_4:4 ;
hence integral (((id Z) ^),A) < 1 / n by Diesel2; :: thesis: verum