:: Integrability Formulas -- Part {I}
:: by Bo Li and Na Ma
::
:: Received November 7, 2009
:: Copyright (c) 2009 Association of Mizar Users

begin

X: - 1 is Real
by XREAL_0:def 1;

theorem Th1: :: INTEGR12:1

for f1, f2 being PartFunc of REAL ,REAL
for Z being open Subset of REAL st Z c= dom ((f1 + f2) ^ ) & ( for x being Real st x in Z holds
f1 . x = 1 ) & f2 = #Z 2 holds
( (f1 + f2) ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) ^ ) `| Z) . x = - ((2 * x) / ((1 + (x |^ 2)) ^2 )) ) )

proof end;

theorem :: INTEGR12:2

for A being closed-interval Subset of REAL
for f, g1, g2, f2 being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & f = ((g1 + g2) ^ ) / f2 & f2 = arccot & Z c= ].(- 1),1.[ & g2 = #Z 2 & ( for x being Real st x in Z holds
( g1 . x = 1 & f2 . x > 0 ) ) & Z = dom f holds
integral f,A = ((- (ln * arccot )) . (sup A)) - ((- (ln * arccot )) . (inf A))

proof end;

theorem :: INTEGR12:3

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( exp_R . x < 1 & f1 . x = 1 ) ) & Z c= dom (arctan * exp_R ) & Z = dom f & f = exp_R / (f1 + (exp_R ^2 )) holds
integral f,A = ((arctan * exp_R ) . (sup A)) - ((arctan * exp_R ) . (inf A))

proof end;

theorem :: INTEGR12:4

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( exp_R . x < 1 & f1 . x = 1 ) ) & Z c= dom (arccot * exp_R ) & Z = dom f & f = (- exp_R ) / (f1 + (exp_R ^2 )) holds
integral f,A = ((arccot * exp_R ) . (sup A)) - ((arccot * exp_R ) . (inf A))

proof end;

theorem :: INTEGR12:5

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = (exp_R (#) (sin / cos )) + (exp_R / (cos ^2 )) holds
integral f,A = ((exp_R (#) tan ) . (sup A)) - ((exp_R (#) tan ) . (inf A))

proof end;

theorem :: INTEGR12:6

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = (exp_R (#) (cos / sin )) - (exp_R / (sin ^2 )) holds
integral f,A = ((exp_R (#) cot ) . (sup A)) - ((exp_R (#) cot ) . (inf A))

proof end;

theorem :: INTEGR12:7

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = (exp_R (#) arctan ) + (exp_R / (f1 + (#Z 2))) holds
integral f,A = ((exp_R (#) arctan ) . (sup A)) - ((exp_R (#) arctan ) . (inf A))

proof end;

theorem :: INTEGR12:8

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = (exp_R (#) arccot ) - (exp_R / (f1 + (#Z 2))) holds
integral f,A = ((exp_R (#) arccot ) . (sup A)) - ((exp_R (#) arccot ) . (inf A))

proof end;

theorem :: INTEGR12:9

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = (exp_R * sin ) (#) cos holds
integral f,A = ((exp_R * sin ) . (sup A)) - ((exp_R * sin ) . (inf A))

proof end;

theorem :: INTEGR12:10

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = (exp_R * cos ) (#) sin holds
integral f,A = ((- (exp_R * cos )) . (sup A)) - ((- (exp_R * cos )) . (inf A))

proof end;

theorem :: INTEGR12:11

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & Z = dom f & f = (cos * ln ) (#) ((id Z) ^ ) holds
integral f,A = ((sin * ln ) . (sup A)) - ((sin * ln ) . (inf A))

proof end;

Lm1: right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;

theorem :: INTEGR12:12

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & Z = dom f & f = (sin * ln ) (#) ((id Z) ^ ) holds
integral f,A = ((- (cos * ln )) . (sup A)) - ((- (cos * ln )) . (inf A))

proof end;

theorem :: INTEGR12:13

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = exp_R (#) (cos * exp_R ) holds
integral f,A = ((sin * exp_R ) . (sup A)) - ((sin * exp_R ) . (inf A))

proof end;

theorem :: INTEGR12:14

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z = dom f & f = exp_R (#) (sin * exp_R ) holds
integral f,A = ((- (cos * exp_R )) . (sup A)) - ((- (cos * exp_R )) . (inf A))

proof end;

theorem :: INTEGR12:15

for r being Real
for A being closed-interval Subset of REAL
for f1, f2, g, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (ln * (f1 + f2)) & r <> 0 & ( for x being Real st x in Z holds
( g . x = x / r & g . x > - 1 & g . x < 1 & f1 . x = 1 ) ) & f2 = (#Z 2) * g & Z = dom f & f = arctan * g holds
integral f,A = ((((id Z) (#) (arctan * g)) - ((r / 2) (#) (ln * (f1 + f2)))) . (sup A)) - ((((id Z) (#) (arctan * g)) - ((r / 2) (#) (ln * (f1 + f2)))) . (inf A))

proof end;

theorem :: INTEGR12:16

for r being Real
for A being closed-interval Subset of REAL
for f1, f2, g, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (ln * (f1 + f2)) & r <> 0 & ( for x being Real st x in Z holds
( g . x = x / r & g . x > - 1 & g . x < 1 & f1 . x = 1 ) ) & f2 = (#Z 2) * g & Z = dom f & f = arccot * g holds
integral f,A = ((((id Z) (#) (arccot * g)) + ((r / 2) (#) (ln * (f1 + f2)))) . (sup A)) - ((((id Z) (#) (arccot * g)) + ((r / 2) (#) (ln * (f1 + f2)))) . (inf A))

proof end;

theorem :: INTEGR12:17

for r being Real
for A being closed-interval Subset of REAL
for f, f1, g being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & f = (arctan * f1) + ((id Z) / (r (#) (g + (f1 ^2 )))) & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / r & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous holds
integral f,A = (((id Z) (#) (arctan * f1)) . (sup A)) - (((id Z) (#) (arctan * f1)) . (inf A))

proof end;

theorem :: INTEGR12:18

for r being Real
for A being closed-interval Subset of REAL
for f, f1, g being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & f = (arccot * f1) - ((id Z) / (r (#) (g + (f1 ^2 )))) & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / r & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous holds
integral f,A = (((id Z) (#) (arccot * f1)) . (sup A)) - (((id Z) (#) (arccot * f1)) . (inf A))

proof end;

theorem :: INTEGR12:19

for n being Element of NAT
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom f & Z c= dom ((#Z n) * arcsin ) & 1 < n & f = (n (#) ((#Z (n - 1)) * arcsin )) / ((#R (1 / 2)) * (f1 - (#Z 2))) holds
integral f,A = (((#Z n) * arcsin ) . (sup A)) - (((#Z n) * arcsin ) . (inf A))

proof end;

theorem :: INTEGR12:20

for n being Element of NAT
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= dom ((#Z n) * arccos ) & Z = dom f & 1 < n & f = (n (#) ((#Z (n - 1)) * arccos )) / ((#R (1 / 2)) * (f1 - (#Z 2))) holds
integral f,A = ((- ((#Z n) * arccos )) . (sup A)) - ((- ((#Z n) * arccos )) . (inf A))

proof end;

theorem :: INTEGR12:21

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = arcsin + ((id Z) / ((#R (1 / 2)) * (f1 - (#Z 2)))) holds
integral f,A = (((id Z) (#) arcsin ) . (sup A)) - (((id Z) (#) arcsin ) . (inf A))

proof end;

theorem :: INTEGR12:22

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = arccos - ((id Z) / ((#R (1 / 2)) * (f1 - (#Z 2)))) holds
integral f,A = (((id Z) (#) arccos ) . (sup A)) - (((id Z) (#) arccos ) . (inf A))

proof end;

theorem :: INTEGR12:23

for a, b being Real
for A being closed-interval Subset of REAL
for f1, f2, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = (a * x) + b & f2 . x = 1 ) ) & Z = dom f & f = (a (#) arcsin ) + (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) holds
integral f,A = ((f1 (#) arcsin ) . (sup A)) - ((f1 (#) arcsin ) . (inf A))

proof end;

theorem :: INTEGR12:24

for a, b being Real
for A being closed-interval Subset of REAL
for f1, f2, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = (a * x) + b & f2 . x = 1 ) ) & Z = dom f & f = (a (#) arccos ) - (f1 / ((#R (1 / 2)) * (f2 - (#Z 2)))) holds
integral f,A = ((f1 (#) arccos ) . (sup A)) - ((f1 (#) arccos ) . (inf A))

proof end;

theorem :: INTEGR12:25

for a being Real
for A being closed-interval Subset of REAL
for g, f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous & f = (arcsin * f1) + ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) holds
integral f,A = (((id Z) (#) (arcsin * f1)) . (sup A)) - (((id Z) (#) (arcsin * f1)) . (inf A))

proof end;

theorem :: INTEGR12:26

for a being Real
for A being closed-interval Subset of REAL
for g, f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( g . x = 1 & f1 . x = x / a & f1 . x > - 1 & f1 . x < 1 ) ) & Z = dom f & f | A is continuous & f = (arccos * f1) - ((id Z) / (a (#) ((#R (1 / 2)) * (g - (f1 ^2 ))))) holds
integral f,A = (((id Z) (#) (arccos * f1)) . (sup A)) - (((id Z) (#) (arccos * f1)) . (inf A))

proof end;

theorem :: INTEGR12:27

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & f = (n (#) ((#Z (n - 1)) * sin )) / ((#Z (n + 1)) * cos ) & 1 <= n & Z c= dom ((#Z n) * tan ) & Z = dom f holds
integral f,A = (((#Z n) * tan ) . (sup A)) - (((#Z n) * tan ) . (inf A))

proof end;

theorem :: INTEGR12:28

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & f = (n (#) ((#Z (n - 1)) * cos )) / ((#Z (n + 1)) * sin ) & 1 <= n & Z c= dom ((#Z n) * cot ) & Z = dom f holds
integral f,A = ((- ((#Z n) * cot )) . (sup A)) - ((- ((#Z n) * cot )) . (inf A))

proof end;

theorem :: INTEGR12:29

for a being Real
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (tan * f1) & f = ((sin * f1) ^2 ) / ((cos * f1) ^2 ) & ( for x being Real st x in Z holds
( f1 . x = a * x & a <> 0 ) ) & Z = dom f holds
integral f,A = ((((1 / a) (#) (tan * f1)) - (id Z)) . (sup A)) - ((((1 / a) (#) (tan * f1)) - (id Z)) . (inf A))

proof end;

theorem :: INTEGR12:30

for a being Real
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= dom (cot * f1) & f = ((cos * f1) ^2 ) / ((sin * f1) ^2 ) & ( for x being Real st x in Z holds
( f1 . x = a * x & a <> 0 ) ) & Z = dom f holds
integral f,A = ((((- (1 / a)) (#) (cot * f1)) - (id Z)) . (sup A)) - ((((- (1 / a)) (#) (cot * f1)) - (id Z)) . (inf A))

proof end;

theorem :: INTEGR12:31

for a, b being Real
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = (a * x) + b ) & Z = dom f & f = (a (#) (sin / cos )) + (f1 / (cos ^2 )) holds
integral f,A = ((f1 (#) tan ) . (sup A)) - ((f1 (#) tan ) . (inf A))

proof end;

theorem :: INTEGR12:32

for a, b being Real
for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = (a * x) + b ) & Z = dom f & f = (a (#) (cos / sin )) - (f1 / (sin ^2 )) holds
integral f,A = ((f1 (#) cot ) . (sup A)) - ((f1 (#) cot ) . (inf A))

proof end;

theorem :: INTEGR12:33

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f . x = ((sin . x) ^2 ) / ((cos . x) ^2 ) ) & Z c= dom (tan - (id Z)) & Z = dom f & f | A is continuous holds
integral f,A = ((tan - (id Z)) . (sup A)) - ((tan - (id Z)) . (inf A))

proof end;

theorem :: INTEGR12:34

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f . x = ((cos . x) ^2 ) / ((sin . x) ^2 ) ) & Z c= dom ((- cot ) - (id Z)) & Z = dom f & f | A is continuous holds
integral f,A = (((- cot ) - (id Z)) . (sup A)) - (((- cot ) - (id Z)) . (inf A))

proof end;

theorem :: INTEGR12:35

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = 1 / (x * (1 + ((ln . x) ^2 ))) & ln . x > - 1 & ln . x < 1 ) ) & Z c= dom (arctan * ln ) & Z = dom f & f | A is continuous holds
integral f,A = ((arctan * ln ) . (sup A)) - ((arctan * ln ) . (inf A))

proof end;

theorem :: INTEGR12:36

for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = - (1 / (x * (1 + ((ln . x) ^2 )))) & ln . x > - 1 & ln . x < 1 ) ) & Z c= dom (arccot * ln ) & Z = dom f & f | A is continuous holds
integral f,A = ((arccot * ln ) . (sup A)) - ((arccot * ln ) . (inf A))

proof end;

theorem :: INTEGR12:37

for a, b being Real
for A being closed-interval Subset of REAL
for f, f1 being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a / (sqrt (1 - (((a * x) + b) ^2 ))) & f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 ) ) & Z c= dom (arcsin * f1) & Z = dom f & f | A is continuous holds
integral f,A = ((arcsin * f1) . (sup A)) - ((arcsin * f1) . (inf A))

proof end;

theorem :: INTEGR12:38

for a, b being Real
for A being closed-interval Subset of REAL
for f, f1 being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = a / (sqrt (1 - (((a * x) + b) ^2 ))) & f1 . x = (a * x) + b & f1 . x > - 1 & f1 . x < 1 ) ) & Z c= dom (arccos * f1) & Z = dom f & f | A is continuous holds
integral f,A = ((- (arccos * f1)) . (sup A)) - ((- (arccos * f1)) . (inf A))

proof end;

theorem :: INTEGR12:39

for A being closed-interval Subset of REAL
for f1, g, f2, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & f1 = g - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = x * ((1 - (x #Z 2)) #R (- (1 / 2))) & g . x = 1 & f1 . x > 0 ) ) & Z c= dom ((#R (1 / 2)) * f1) & Z = dom f & f | A is continuous holds
integral f,A = ((- ((#R (1 / 2)) * f1)) . (sup A)) - ((- ((#R (1 / 2)) * f1)) . (inf A))

proof end;

theorem :: INTEGR12:40

for a being Real
for A being closed-interval Subset of REAL
for g, f1, f2, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & g = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = x * (((a ^2 ) - (x #Z 2)) #R (- (1 / 2))) & f1 . x = a ^2 & g . x > 0 ) ) & Z c= dom ((#R (1 / 2)) * g) & Z = dom f & f | A is continuous holds
integral f,A = ((- ((#R (1 / 2)) * g)) . (sup A)) - ((- ((#R (1 / 2)) * g)) . (inf A))

proof end;

theorem :: INTEGR12:41

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & n > 0 & ( for x being Real st x in Z holds
( f . x = (cos . x) / ((sin . x) #Z (n + 1)) & sin . x <> 0 ) ) & Z c= dom ((#Z n) * (sin ^ )) & Z = dom f & f | A is continuous holds
integral f,A = (((- (1 / n)) (#) ((#Z n) * (sin ^ ))) . (sup A)) - (((- (1 / n)) (#) ((#Z n) * (sin ^ ))) . (inf A))

proof end;

theorem :: INTEGR12:42

for n being Element of NAT
for A being closed-interval Subset of REAL
for f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & n > 0 & ( for x being Real st x in Z holds
( f . x = (sin . x) / ((cos . x) #Z (n + 1)) & cos . x <> 0 ) ) & Z c= dom ((#Z n) * (cos ^ )) & Z = dom f & f | A is continuous holds
integral f,A = (((1 / n) (#) ((#Z n) * (cos ^ ))) . (sup A)) - (((1 / n) (#) ((#Z n) * (cos ^ ))) . (inf A))

proof end;

theorem :: INTEGR12:43

for A being closed-interval Subset of REAL
for f, g1, g2, f2 being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & f = ((g1 + g2) ^ ) / f2 & f2 = arccot & Z c= ].(- 1),1.[ & g2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = 1 / ((1 + (x ^2 )) * (arccot . x)) & g1 . x = 1 & f2 . x > 0 ) ) & Z = dom f holds
integral f,A = ((- (ln * arccot )) . (sup A)) - ((- (ln * arccot )) . (inf A))

proof end;

theorem :: INTEGR12:44

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( arcsin . x > 0 & f1 . x = 1 ) ) & Z c= dom (ln * arcsin ) & Z = dom f & f = (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arcsin ) ^ holds
integral f,A = ((ln * arcsin ) . (sup A)) - ((ln * arcsin ) . (inf A))

proof end;

theorem :: INTEGR12:45

for A being closed-interval Subset of REAL
for f1, f being PartFunc of REAL ,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = 1 & arccos . x > 0 ) ) & Z c= dom (ln * arccos ) & Z = dom f & f = (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos ) ^ holds
integral f,A = ((- (ln * arccos )) . (sup A)) - ((- (ln * arccos )) . (inf A))

proof end;