:: Classical Isoperimetric Theorem
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received December 14, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

LmPI: 0 < PI
by LEIBNIZ1:17;

Lm1: for a, b being Real holds ].a,b.[ c= [.a,b.]
by XXREAL_1:25;

LmX: for a being Real ex f being constant Function of NAT,REAL st
for x being Nat holds f . x = a

proof end;

theorem Th1: :: PDLAX:1

for a, b, C being Real
for u being PartFunc of REAL,REAL st a < b & ['a,b'] c= dom u & u is continuous & ( for t being Real st t in ].a,b.[ holds
u . t = C ) holds
for t being Real st t in ['a,b'] holds
u . t = C

proof end;

theorem Th2: :: PDLAX:2

for a, b, c, d being Real
for f being PartFunc of REAL,REAL st a <= b & c <= d & [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.] & f | ['a,b'] is continuous & ( for t being Real st t in [.c,d.] holds
0 <= f . t ) holds
0 <= integral (f,c,d)

proof end;

theorem Th3: :: PDLAX:3

for a, b, c, d being Real
for f, g being PartFunc of REAL,REAL st a <= b & c <= d & [.a,b.] c= dom f & [.a,b.] c= dom g & c in [.a,b.] & d in [.a,b.] & f | ['a,b'] is continuous & g | ['a,b'] is continuous & ( for t being Real st t in [.c,d.] holds
f . t <= g . t ) holds
integral (f,c,d) <= integral (g,c,d)

proof end;

theorem Th4: :: PDLAX:4

for a, b, c, d, e being Real
for f being PartFunc of REAL,REAL st a <= b & c <= d & c in [.a,b.] & d in [.a,b.] & [.a,b.] c= dom f & f | ['a,b'] is continuous & ( for t being Real st t in [.c,d.] holds
e <= f . t ) holds
e * (d - c) <= integral (f,c,d)

proof end;

theorem Th5: :: PDLAX:5

for a, b, c, d, e being Real
for f being PartFunc of REAL,REAL st 0 < e & a <= b & c < d & c in [.a,b.] & d in [.a,b.] & [.a,b.] c= dom f & f | ['a,b'] is continuous & ( for t being Real st t in [.a,b.] holds
0 <= f . t ) & ( for t being Real st t in [.c,d.] holds
e <= f . t ) holds
( 0 < e * (d - c) & e * (d - c) <= integral (f,a,b) )

proof end;

theorem Th6: :: PDLAX:6

for a, b being Real
for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f | ['a,b'] is continuous & ( for t being Real st t in [.a,b.] holds
0 <= f . t ) & ex t0 being Real st
( t0 in ].a,b.[ & 0 < f . t0 ) holds
ex d, c, e being Real st
( 0 < e & c < d & c in [.a,b.] & d in [.a,b.] & 0 < e * (d - c) & e * (d - c) <= integral (f,a,b) )

proof end;

Lm2: for f being Real_Sequence
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

proof end;

theorem Th7: :: PDLAX:7

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & ['a,b'] c= dom f & f | ['a,b'] is continuous holds
ex I being Real_Sequence st
( ( for n being Nat holds I . n = integral (f,(a + (1 / (n + 1))),(b - (1 / (n + 1)))) ) & I is convergent & lim I = integral (f,a,b) )

proof end;

Lm3: for n being Nat holds
( 0 < 1 / (n + 1) & 1 / (n + 1) < PI - (1 / (n + 1)) & PI - (1 / (n + 1)) < PI & [.(1 / (n + 1)),(PI - (1 / (n + 1))).] c= ].0,PI.[ & ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).] )

proof end;

theorem Th8: :: PDLAX:8

for Z being open Subset of REAL holds
( sin is_differentiable_on Z & sin `| Z = cos | Z & cos is_differentiable_on Z & cos `| Z = - (sin | Z) )

proof end;

theorem Th9: :: PDLAX:9

for f being PartFunc of REAL,REAL holds f + f = 2 (#) f

proof end;

Th12: for Z being open Subset of REAL
for r being Real
for f being PartFunc of REAL,REAL st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & (r (#) f) `| Z = r (#) (f `| Z) )
by FDIFF_2:19;

Th13: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 (#) f2 is_differentiable_on Z & (f1 (#) f2) `| Z = ((f1 `| Z) (#) f2) + (f1 (#) (f2 `| Z)) )
by FDIFF_2:20;

theorem Th14: :: PDLAX:10

for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for x being Real st Z is open & x in Z & Z c= dom f holds
( f | Z is_differentiable_in x iff f is_differentiable_in x )

proof end;

theorem :: PDLAX:11

for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for x being Real st Z is open & x in Z & Z c= dom f & f is_differentiable_in x holds
diff (f,x) = diff ((f | Z),x)

proof end;

Th16: for f being PartFunc of REAL,REAL
for Z being Subset of REAL holds
( f | Z is_differentiable_on Z iff f is_differentiable_on Z )
by INTEGRA7:5;

Th17: for f being PartFunc of REAL,REAL
for Z being Subset of REAL st f is_differentiable_on Z holds
(f | Z) `| Z = f `| Z
by FDIFF_2:16;

theorem Th18: :: PDLAX:12

for f being PartFunc of REAL,REAL
for X, Z being Subset of REAL st Z is open & Z c= X & f is_differentiable_on X holds
f `| Z = (f `| X) | Z

proof end;

theorem Th19: :: PDLAX:13

for a, b being Real
for u being PartFunc of REAL,REAL st a < b & u is_differentiable_on ].a,b.[ & dom u = ['a,b'] & u is continuous & ( for t being Real st t in ].a,b.[ holds
(u `| ].a,b.[) . t = 0 ) holds
ex C being Real st
for t being Real st t in ['a,b'] holds
u . t = C

proof end;

Lm5: for a, b being Real holds a * b <= (1 / 2) * ((a ^2) + (b ^2))

proof end;

Lm7: for x, y being PartFunc of REAL,REAL
for t being Real holds (x (#) y) . t <= (1 / 2) * (((x (#) x) . t) + ((y (#) y) . t))

proof end;

Lm10: for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL
for a, b being Real st x is continuous & y is differentiable & y `| Z is continuous & a <= b & ['a,b'] c= Z & Z c= dom x & Z c= dom y holds
integral ((x (#) (y `| Z)),a,b) <= (1 / 2) * (integral (((x (#) x) + ((y `| Z) (#) (y `| Z))),a,b))

proof end;

Lm11: for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL
for a, b being Real st x is differentiable & y is differentiable & x `| Z is continuous & Z c= dom x & Z c= dom y & a <= b & ['a,b'] c= Z & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) holds
( integral ((y (#) (x `| Z)),a,b) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),a,b) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),a,b) )

proof end;

Lm13: for t being Real st t in ].(- PI),0.[ holds
sin . t < 0

proof end;

Lm17: for y being PartFunc of REAL,REAL
for Z being open Subset of REAL st ['0,PI'] c= Z & Z c= dom y & y is differentiable & y `| Z is continuous & y . 0 = 0 & y . PI = 0 holds
ex u being PartFunc of REAL,REAL st
( dom u = ['0,PI'] & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) )

proof end;

Lm18: for y, u being PartFunc of REAL,REAL
for Z being open Subset of REAL st y is differentiable & ['0,PI'] c= Z & Z c= dom y & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) holds
for t being Real st t in ].0,PI.[ holds
(((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (((((u . t) ^2) * (((sin . t) ^2) - ((cos . t) ^2))) - ((((2 * (u . t)) * (diff (u,t))) * (sin . t)) * (cos . t))) - (((diff (u,t)) ^2) * ((sin . t) ^2))) + 1

proof end;

Lm19: for y, u being PartFunc of REAL,REAL
for Z being open Subset of REAL st y is differentiable & ['0,PI'] c= Z & Z c= dom y & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) holds
for t being Real st t in ].0,PI.[ holds
(((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))) . t = (1 - (((diff (u,t)) ^2) * ((sin . t) ^2))) - (diff ((((u (#) u) (#) sin) (#) cos),t))

proof end;

Lm20: for y, u being PartFunc of REAL,REAL
for Z0 being open Subset of REAL st y is differentiable & ['0,PI'] c= Z0 & Z0 c= dom y & y `| Z0 is continuous & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) holds
for n being Nat holds integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),(0 + (1 / (n + 1))),(PI - (1 / (n + 1)))) = ((integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(0 + (1 / (n + 1))),(PI - (1 / (n + 1))))) - ((((u (#) u) (#) sin) (#) cos) . (PI - (1 / (n + 1))))) + ((((u (#) u) (#) sin) (#) cos) . (1 / (n + 1)))

proof end;

Lm21: for y, u being PartFunc of REAL,REAL
for Z0 being open Subset of REAL st y is differentiable & ['0,PI'] c= Z0 & Z0 c= dom y & y `| Z0 is continuous & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) holds
ex F being Real_Sequence st
( ( for n being Nat holds F . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & F is convergent & integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z0) (#) (y `| Z0))),0,PI) = lim F )

proof end;

theorem Th20: :: PDLAX:14

for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL st x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & y `| Z is continuous & x `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 holds
ex u being PartFunc of REAL,REAL ex F being Real_Sequence st
( u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) & ( for n being Nat holds F . n = integral (((AffineMap (0,1)) - ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin)),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & F is convergent & integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI) & integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI) = lim F )

proof end;

Lm23: for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL st x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & y `| Z is continuous & x `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 holds
ex u being PartFunc of REAL,REAL ex G being Real_Sequence st
( u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous & dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * (integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI)) & (y (#) y) + ((x `| Z) (#) (x `| Z)) = ((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z)) & integral (((y (#) y) + ((x `| Z) (#) (x `| Z))),0,PI) = integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI) & (1 / 2) * (integral ((((y (#) y) + (AffineMap (0,1))) - ((y `| Z) (#) (y `| Z))),0,PI)) = ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI )

proof end;

Lm24: for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL
for G being Real_Sequence st integral ((y (#) (x `| Z)),0,PI) <= ((1 / 2) * PI) - ((1 / 2) * (lim G)) & 0 <= lim G & ((1 / 2) * PI) - ((1 / 2) * (lim G)) <= (1 / 2) * PI & integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI holds
lim G = 0

proof end;

Lm25: for g being PartFunc of REAL,REAL
for G being Real_Sequence st g is continuous & dom g = ].0,PI.[ & ( for n being Nat holds
( G . n = integral (g,(1 / (n + 1)),(PI - (1 / (n + 1)))) & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom g & g | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & g | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & g is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) ) ) & ( for t being Real st t in ].0,PI.[ holds
0 <= g . t ) holds
for n, m being Nat st n <= m holds
G . n <= G . m

proof end;

Lm26: for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL
for u being PartFunc of REAL,REAL
for G being Real_Sequence st x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & y `| Z is continuous & x `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 & u is_differentiable_on ].0,PI.[ & u `| ].0,PI.[ is continuous & dom u = ['0,PI'] & u is continuous & y | ['0,PI'] = (u (#) sin) | ['0,PI'] & ( for t being Real st t in ].0,PI.[ holds
diff (y,t) = ((diff (u,t)) * (sin . t)) + ((u . t) * (cos . t)) ) & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is continuous & dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) = ].0,PI.[ & ( for n being Nat holds G . n = integral (((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin),(1 / (n + 1)),(PI - (1 / (n + 1)))) ) & G is convergent & ( for n being Nat holds
( ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] c= dom ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is continuous & ((((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin) | ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] is bounded & (((u `| ].0,PI.[) (#) (u `| ].0,PI.[)) (#) sin) (#) sin is_integrable_on ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] ) ) & ( for n being Nat holds
( 0 <= G . n & ((1 / 2) * PI) - (G . n) <= (1 / 2) * PI ) ) & lim G = 0 holds
for t being Real st t in ].0,PI.[ holds
(u `| ].0,PI.[) . t = 0

proof end;

Lm27: for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL st x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & y `| Z is continuous & x `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 holds
( integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) )

proof end;

Lm28: for x, y being PartFunc of REAL,REAL
for a, b being Real st a < b & [.a,b.] c= dom x & [.a,b.] c= dom y & x is continuous & y is continuous & ( for t being Real st t in ].a,b.[ holds
x . t = y . t ) holds
x | [.a,b.] = y | [.a,b.]

proof end;

Lm29: for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL st x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & y `| Z is continuous & x `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 & ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) holds
integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI

proof end;

theorem :: PDLAX:15

for x, y being PartFunc of REAL,REAL
for Z being open Subset of REAL st x is differentiable & y is differentiable & ['0,PI'] c= Z & Z c= dom x & Z c= dom y & x `| Z is continuous & y `| Z is continuous & ( for t being Real st t in Z holds
(((x `| Z) . t) ^2) + (((y `| Z) . t) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 holds
( integral ((y (#) (x `| Z)),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) implies integral ((y (#) (x `| Z)),0,PI) = (1 / 2) * PI ) ) by Lm27, Lm29;

theorem Th22: :: PDLAX:16

for x, y being PartFunc of REAL,REAL st x is differentiable & y is differentiable & ['0,PI'] c= dom x & ['0,PI'] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
((diff (x,t)) ^2) + ((diff (y,t)) ^2) = 1 ) & y . 0 = 0 & y . PI = 0 holds
( integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * PI & ( not integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * PI or for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( y . t = sin . t & x . t = ((- (cos . t)) + (cos . 0)) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - (sin . t) & x . t = ((cos . t) - (cos . 0)) + (x . 0) ) ) implies integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * PI ) )

proof end;

theorem :: PDLAX:17

for x, y being PartFunc of REAL,REAL
for L being Real st 0 < L & x is differentiable & y is differentiable & [.0,PI.] c= dom x & [.0,PI.] c= dom y & x `| (dom x) is continuous & y `| (dom y) is continuous & ( for t being Real st t in (dom x) /\ (dom y) holds
((diff (x,t)) ^2) + ((diff (y,t)) ^2) = L / PI ) & y . 0 = 0 & y . PI = 0 holds
( integral ((y (#) (x `| (dom x))),0,PI) <= (1 / 2) * L & ( not integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L or for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) & ( ( for t being Real st t in [.0,PI.] holds
( y . t = (sin . t) / (sqrt (PI / L)) & x . t = ((- ((cos . t) / (sqrt (PI / L)))) + ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) or for t being Real st t in [.0,PI.] holds
( y . t = - ((sin . t) / (sqrt (PI / L))) & x . t = (((cos . t) / (sqrt (PI / L))) - ((cos . 0) / (sqrt (PI / L)))) + (x . 0) ) ) implies integral ((y (#) (x `| (dom x))),0,PI) = (1 / 2) * L ) )

proof end;