let r be Real; :: thesis: ( 0 <= r implies sin . r <= r )
assume 0 <= r ; :: thesis: sin . r <= r
then reconsider A = [.0,r.] as non empty closed_interval Subset of REAL by MEASURE5:def 3, XXREAL_1:1;
A1: dom cos = REAL by FUNCT_2:def 1;
then dom (cos | A) = A by RELAT_1:62;
then cos | A is total by PARTFUN1:def 2;
then reconsider cA = cos || A as Function of A,REAL ;
A2: ( cA | A is bounded & cA is integrable )
proof
cos | A is continuous ;
hence ( cA | A is bounded & cA is integrable ) by INTEGRA5:def 1, INTEGRA5:11, INTEGRA5:10, A1; :: thesis: verum
end;
A3: integral cA = sin . r
proof
thus integral cA = integral (cos,A) by INTEGRA5:def 2
.= integral (cos,0,r) by INTEGRA5:19
.= (sin . r) - (sin . 0) by INTEGRA7:24
.= sin . r by SIN_COS:30 ; :: thesis: verum
end;
set Z0 = #Z 0;
A4: 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 ;
A5: ( ZA | A is bounded & ZA is integrable )
proof
(#Z 0) | A is continuous ;
hence ( ZA | A is bounded & ZA is integrable ) by A4, INTEGRA5:def 1, INTEGRA5:11, INTEGRA5:10; :: thesis: verum
end;
A6: integral ZA = r
proof
set Z1 = #Z 1;
A7: (0 + 1) (#) (#Z 0) = #Z 0 by RFUNCT_1:21;
A8: (#Z 1) . r = r #Z 1 by TAYLOR_1:def 1
.= r by PREPOWER:35 ;
A9: (#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 A7, INTEGRA7:30
.= r by A8, A9 ; :: thesis: verum
end;
for r being Real st r in A holds
cA . r <= ZA . r
proof
let r be Real; :: thesis: ( r in A implies cA . r <= ZA . r )
assume A10: r in A ; :: thesis: cA . r <= ZA . r
then ZA . r = (#Z 0) . r by FUNCT_1:49;
then A11: ZA . r = r #Z 0 by TAYLOR_1:def 1
.= 1 by PREPOWER:34 ;
cos r <= 1 by SIN_COS6:6;
hence cA . r <= ZA . r by A11, A10, FUNCT_1:49; :: thesis: verum
end;
hence sin . r <= r by A2, A3, A5, A6, INTEGRA2:34; :: thesis: verum