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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Z )
assume aa: x in A ; :: thesis: x in Z
then reconsider xx = x as Real ;
( n <= xx & xx <= n + 1 ) by aa, Z1, XXREAL_1:1;
hence x in Z by XXREAL_1:235, Z1; :: 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 Z1, XREAL_1:31, XXREAL_2:25;
B2: upper_bound A = n + 1 by Z1, 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, Z1, TAYLOR_1:18, a3, INTEGRA9:61
.= ln . ((n + 1) / n) by Z1, DIFF_4:4, B1, B2 ;
hence integral (((id Z) ^),A) = ln . ((n + 1) / n) ; :: thesis: verum