let A be non empty closed_interval Subset of REAL; 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; 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; ( 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).] )
; integral (((id Z) ^),A) < 1 / n
N1:
not 0 in Z
by aa, XXREAL_1:4;
A1:
A c= Z
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; verum