let r be Real; :: thesis: ( 0 <= r & r < PI / 2 implies r <= tan . r )
assume A1: ( 0 <= r & r < PI / 2 ) ; :: thesis: r <= tan . r
then reconsider A = [.0,r.] as non empty closed_interval Subset of REAL by MEASURE5:def 3, XXREAL_1:1;
A2: dom cos = REAL by FUNCT_2:def 1;
set Z0 = #Z 0;
A3: dom (#Z 0) = REAL by FUNCT_2:def 1;
then dom ((#Z 0) | A) = A by RELAT_1:62;
then (#Z 0) | A is total by PARTFUN1:def 2;
then reconsider ZA = (#Z 0) || A as Function of A,REAL ;
A4: ( ZA | A is bounded & ZA is integrable )

proof

(#Z 0) | A is continuous ;
hence ( ZA | A is bounded & ZA is integrable ) by INTEGRA5:def 1, INTEGRA5:11, INTEGRA5:10, A3; :: thesis: verum

end;

A5: integral ZA = r

proof

set Z1 = #Z 1;
A6: (0 + 1) (#) (#Z 0) = #Z 0 by RFUNCT_1:21;
A7: (#Z 1) . r = r #Z 1 by TAYLOR_1:def 1
.= r by PREPOWER:35 ;
A8: (#Z 1) . 0 = 0 #Z 1 by TAYLOR_1:def 1
.= 0 by PREPOWER:35 ;
thus integral ZA = integral ((#Z 0),A) by INTEGRA5:def 2
.= integral ((#Z 0),0,r) by INTEGRA5:19
.= ((#Z 1) . r) - ((#Z 1) . 0) by A6, INTEGRA7:30
.= r by A7, A8 ; :: thesis: verum

end;

set T = dom tan;
dom sin = REAL by FUNCT_2:def 1;
then dom tan = REAL /\ ((dom cos) \ (cos " {0})) by RFUNCT_1:def 1;
then A9: dom tan = REAL \ (cos " {0}) by A2, XBOOLE_1:28;
set cc = cos (#) cos;
set ccT = (cos (#) cos) | (dom tan);
set Z0ccT = (#Z 0) / ((cos (#) cos) | (dom tan));
dom (cos (#) cos) = REAL by FUNCT_2:def 1;
then A10: dom ((cos (#) cos) | (dom tan)) = dom tan by RELAT_1:62;
then A11: dom tan = (dom ((cos (#) cos) | (dom tan))) /\ (dom (#Z 0)) by A3, XBOOLE_1:28;
A12: A c= ].(- (PI / 2)),(PI / 2).[ by A1, XXREAL_1:47;
then A13: A c= dom tan by SIN_COS9:1;
A14: ((cos (#) cos) | (dom tan)) " {0} = {}

proof

assume ((cos (#) cos) | (dom tan)) " {0} <> {} ; :: thesis: contradiction
then consider x being object such that
A15: x in ((cos (#) cos) | (dom tan)) " {0} by XBOOLE_0:def 1;
reconsider x = x as Element of REAL by A15;
A16: ( x in dom ((cos (#) cos) | (dom tan)) & ((cos (#) cos) | (dom tan)) . x in {0} ) by A15, FUNCT_1:def 7;
then 0 = ((cos (#) cos) | (dom tan)) . x by TARSKI:def 1
.= (cos (#) cos) . x by A16, FUNCT_1:47
.= (cos . x) * (cos . x) by VALUED_1:5 ;
then cos . x = 0 ;
then cos . x in {0} by TARSKI:def 1;
then x in cos " {0} by FUNCT_1:def 7, A2;
hence contradiction by A9, A10, A16, XBOOLE_0:def 5; :: thesis: verum

end;

then (dom ((cos (#) cos) | (dom tan))) \ (((cos (#) cos) | (dom tan)) " {0}) = dom ((cos (#) cos) | (dom tan)) ;
then A17: dom tan = dom ((#Z 0) / ((cos (#) cos) | (dom tan))) by A11, RFUNCT_1:def 1;
then dom (((#Z 0) / ((cos (#) cos) | (dom tan))) | A) = A by A13, RELAT_1:62;
then ( (((#Z 0) / ((cos (#) cos) | (dom tan))) | A) | A is total & (((#Z 0) / ((cos (#) cos) | (dom tan))) | A) | A = ((#Z 0) / ((cos (#) cos) | (dom tan))) | A ) by PARTFUN1:def 2;
then reconsider Z0ccTA = ((#Z 0) / ((cos (#) cos) | (dom tan))) || A as Function of A,REAL ;
A18: ( ((#Z 0) / ((cos (#) cos) | (dom tan))) | A is continuous & Z0ccTA | A is bounded & Z0ccTA is integrable )

proof

A19: A c= (dom (#Z 0)) /\ (dom ((cos (#) cos) | (dom tan))) by A10, A13, A3, XBOOLE_1:28;
A20: ((cos (#) cos) | (dom tan)) | A is continuous ;
(#Z 0) | A is continuous ;
then ((#Z 0) / ((cos (#) cos) | (dom tan))) | A is continuous by A19, FCONT_1:24, A20, A14;
hence ( ((#Z 0) / ((cos (#) cos) | (dom tan))) | A is continuous & Z0ccTA | A is bounded & Z0ccTA is integrable ) by INTEGRA5:def 1, INTEGRA5:11, INTEGRA5:10, A17, A13; :: thesis: verum

end;

A21: for s being Real st s in dom tan holds
( ((#Z 0) / ((cos (#) cos) | (dom tan))) . s = 1 / ((cos . s) ^2) & cos . s <> 0 )

proof

let s be Real; :: thesis: ( s in dom tan implies ( ((#Z 0) / ((cos (#) cos) | (dom tan))) . s = 1 / ((cos . s) ^2) & cos . s <> 0 ) )
assume A22: s in dom tan ; :: thesis: ( ((#Z 0) / ((cos (#) cos) | (dom tan))) . s = 1 / ((cos . s) ^2) & cos . s <> 0 )
A23: (#Z 0) . s = s #Z 0 by TAYLOR_1:def 1
.= 1 by PREPOWER:34 ;
((cos (#) cos) | (dom tan)) . s = (cos (#) cos) . s by A22, A10, FUNCT_1:47
.= (cos . s) ^2 by VALUED_1:5 ;
hence ((#Z 0) / ((cos (#) cos) | (dom tan))) . s = 1 / ((cos . s) ^2) by A23, RFUNCT_1:def 1, A22, A17; :: thesis: cos . s <> 0
A24: s in REAL by XREAL_0:def 1;
assume cos . s = 0 ; :: thesis: contradiction
then cos . s in {0} by TARSKI:def 1;
then s in cos " {0} by FUNCT_1:def 7, A2, A24;
hence contradiction by A22, A9, XBOOLE_0:def 5; :: thesis: verum

end;

A25: integral Z0ccTA = tan . r

proof

A26: ( upper_bound A = r & lower_bound A = 0 ) by A1, JORDAN5A:19;
thus integral Z0ccTA = integral (((#Z 0) / ((cos (#) cos) | (dom tan))),A) by INTEGRA5:def 2
.= (tan . r) - (tan . 0) by A13, A17, A21, A18, A26, INTEGRA8:59
.= tan . r by SIN_COS9:41 ; :: thesis: verum

end;

for r being Real st r in A holds
ZA . r <= Z0ccTA . r

proof

let r be Real; :: thesis: ( r in A implies ZA . r <= Z0ccTA . r )
assume A27: r in A ; :: thesis: ZA . r <= Z0ccTA . r
then A28: ( Z0ccTA . r = ((#Z 0) / ((cos (#) cos) | (dom tan))) . r & ZA . r = (#Z 0) . r ) by FUNCT_1:49;
then A29: ZA . r = r #Z 0 by TAYLOR_1:def 1
.= 1 by PREPOWER:34 ;
A30: Z0ccTA . r = 1 / ((cos . r) ^2) by A28, A27, A21, A13;
A31: cos r > 0 by A27, A12, COMPTRIG:11;
( cos r <= 1 & cos . r = cos r ) by SIN_COS6:6;
then ( (cos . r) ^2 <= 1 ^2 & (cos . r) ^2 > 0 ) by XREAL_1:66, A31;
then 1 " <= ((cos . r) ^2) " by XREAL_1:85;
hence ZA . r <= Z0ccTA . r by A29, A30; :: thesis: verum

end;

hence r <= tan . r by A4, A5, A18, A25, INTEGRA2:34; :: thesis: verum