:: SINCOS10 semantic presentation begin Lm1: [.0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ proof A1: 0 in ].(- (PI / 2)),(PI / 2).[ ; A2: {0} c= ].(- (PI / 2)),(PI / 2).[ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {0} or x in ].(- (PI / 2)),(PI / 2).[ ) assume x in {0} ; ::_thesis: x in ].(- (PI / 2)),(PI / 2).[ hence x in ].(- (PI / 2)),(PI / 2).[ by A1, TARSKI:def_1; ::_thesis: verum end; ].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then ].0,(PI / 2).[ \/ {0} c= ].(- (PI / 2)),(PI / 2).[ by A2, XBOOLE_1:8; hence [.0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:131; ::_thesis: verum end; theorem Th1: :: SINCOS10:1 [.0,(PI / 2).[ c= dom sec proof [.0,(PI / 2).[ /\ (cos " {0}) = {} proof assume [.0,(PI / 2).[ /\ (cos " {0}) <> {} ; ::_thesis: contradiction then consider rr being set such that A1: rr in [.0,(PI / 2).[ /\ (cos " {0}) by XBOOLE_0:def_1; rr in cos " {0} by A1, XBOOLE_0:def_4; then A2: cos . rr in {0} by FUNCT_1:def_7; rr in [.0,(PI / 2).[ by A1, XBOOLE_0:def_4; then cos . rr <> 0 by Lm1, COMPTRIG:11; hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; then ( [.0,(PI / 2).[ \ (cos " {0}) c= (dom cos) \ (cos " {0}) & [.0,(PI / 2).[ misses cos " {0} ) by SIN_COS:24, XBOOLE_0:def_7, XBOOLE_1:33; then [.0,(PI / 2).[ c= (dom cos) \ (cos " {0}) by XBOOLE_1:83; hence [.0,(PI / 2).[ c= dom sec by RFUNCT_1:def_2; ::_thesis: verum end; Lm2: ].(PI / 2),PI.] c= ].(PI / 2),((3 / 2) * PI).[ proof A1: PI / 2 < PI / 1 by XREAL_1:76; A2: PI < (3 / 2) * PI by XREAL_1:155; then A3: PI in ].(PI / 2),((3 / 2) * PI).[ by A1; A4: {PI} c= ].(PI / 2),((3 / 2) * PI).[ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {PI} or x in ].(PI / 2),((3 / 2) * PI).[ ) assume x in {PI} ; ::_thesis: x in ].(PI / 2),((3 / 2) * PI).[ hence x in ].(PI / 2),((3 / 2) * PI).[ by A3, TARSKI:def_1; ::_thesis: verum end; ].(PI / 2),PI.[ c= ].(PI / 2),((3 / 2) * PI).[ by A2, XXREAL_1:46; then ].(PI / 2),PI.[ \/ {PI} c= ].(PI / 2),((3 / 2) * PI).[ by A4, XBOOLE_1:8; hence ].(PI / 2),PI.] c= ].(PI / 2),((3 / 2) * PI).[ by A1, XXREAL_1:132; ::_thesis: verum end; theorem Th2: :: SINCOS10:2 ].(PI / 2),PI.] c= dom sec proof ].(PI / 2),PI.] /\ (cos " {0}) = {} proof assume ].(PI / 2),PI.] /\ (cos " {0}) <> {} ; ::_thesis: contradiction then consider rr being set such that A1: rr in ].(PI / 2),PI.] /\ (cos " {0}) by XBOOLE_0:def_1; rr in cos " {0} by A1, XBOOLE_0:def_4; then A2: cos . rr in {0} by FUNCT_1:def_7; rr in ].(PI / 2),PI.] by A1, XBOOLE_0:def_4; then cos . rr <> 0 by Lm2, COMPTRIG:13; hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; then ( ].(PI / 2),PI.] \ (cos " {0}) c= (dom cos) \ (cos " {0}) & ].(PI / 2),PI.] misses cos " {0} ) by SIN_COS:24, XBOOLE_0:def_7, XBOOLE_1:33; then ].(PI / 2),PI.] c= (dom cos) \ (cos " {0}) by XBOOLE_1:83; hence ].(PI / 2),PI.] c= dom sec by RFUNCT_1:def_2; ::_thesis: verum end; Lm3: [.(- (PI / 2)),0.[ c= ].(- PI),0.[ proof PI / 2 < PI / 1 by XREAL_1:76; then A1: - PI < - (PI / 2) by XREAL_1:24; then A2: - (PI / 2) in ].(- PI),0.[ ; A3: {(- (PI / 2))} c= ].(- PI),0.[ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(- (PI / 2))} or x in ].(- PI),0.[ ) assume x in {(- (PI / 2))} ; ::_thesis: x in ].(- PI),0.[ hence x in ].(- PI),0.[ by A2, TARSKI:def_1; ::_thesis: verum end; ].(- (PI / 2)),0.[ c= ].(- PI),0.[ by A1, XXREAL_1:46; then ].(- (PI / 2)),0.[ \/ {(- (PI / 2))} c= ].(- PI),0.[ by A3, XBOOLE_1:8; hence [.(- (PI / 2)),0.[ c= ].(- PI),0.[ by XXREAL_1:131; ::_thesis: verum end; theorem Th3: :: SINCOS10:3 [.(- (PI / 2)),0.[ c= dom cosec proof [.(- (PI / 2)),0.[ /\ (sin " {0}) = {} proof assume [.(- (PI / 2)),0.[ /\ (sin " {0}) <> {} ; ::_thesis: contradiction then consider rr being set such that A1: rr in [.(- (PI / 2)),0.[ /\ (sin " {0}) by XBOOLE_0:def_1; A2: rr in sin " {0} by A1, XBOOLE_0:def_4; A3: rr in [.(- (PI / 2)),0.[ by A1, XBOOLE_0:def_4; reconsider rr = rr as real number by A1; rr < 0 by A3, Lm3, XXREAL_1:4; then A4: rr + (2 * PI) < 0 + (2 * PI) by XREAL_1:8; - PI < rr by A3, Lm3, XXREAL_1:4; then (- PI) + (2 * PI) < rr + (2 * PI) by XREAL_1:8; then rr + (2 * PI) in ].PI,(2 * PI).[ by A4; then sin . (rr + (2 * PI)) < 0 by COMPTRIG:9; then A5: sin . rr <> 0 by SIN_COS:78; sin . rr in {0} by A2, FUNCT_1:def_7; hence contradiction by A5, TARSKI:def_1; ::_thesis: verum end; then ( [.(- (PI / 2)),0.[ \ (sin " {0}) c= (dom sin) \ (sin " {0}) & [.(- (PI / 2)),0.[ misses sin " {0} ) by SIN_COS:24, XBOOLE_0:def_7, XBOOLE_1:33; then [.(- (PI / 2)),0.[ c= (dom sin) \ (sin " {0}) by XBOOLE_1:83; hence [.(- (PI / 2)),0.[ c= dom cosec by RFUNCT_1:def_2; ::_thesis: verum end; Lm4: ].0,(PI / 2).] c= ].0,PI.[ proof A1: PI / 2 < PI / 1 by XREAL_1:76; then A2: PI / 2 in ].0,PI.[ ; A3: {(PI / 2)} c= ].0,PI.[ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(PI / 2)} or x in ].0,PI.[ ) assume x in {(PI / 2)} ; ::_thesis: x in ].0,PI.[ hence x in ].0,PI.[ by A2, TARSKI:def_1; ::_thesis: verum end; ].0,(PI / 2).[ c= ].0,PI.[ by A1, XXREAL_1:46; then ].0,(PI / 2).[ \/ {(PI / 2)} c= ].0,PI.[ by A3, XBOOLE_1:8; hence ].0,(PI / 2).] c= ].0,PI.[ by XXREAL_1:132; ::_thesis: verum end; theorem Th4: :: SINCOS10:4 ].0,(PI / 2).] c= dom cosec proof ].0,(PI / 2).] /\ (sin " {0}) = {} proof assume ].0,(PI / 2).] /\ (sin " {0}) <> {} ; ::_thesis: contradiction then consider rr being set such that A1: rr in ].0,(PI / 2).] /\ (sin " {0}) by XBOOLE_0:def_1; rr in sin " {0} by A1, XBOOLE_0:def_4; then A2: sin . rr in {0} by FUNCT_1:def_7; rr in ].0,(PI / 2).] by A1, XBOOLE_0:def_4; then sin . rr <> 0 by Lm4, COMPTRIG:7; hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; then ( ].0,(PI / 2).] \ (sin " {0}) c= (dom sin) \ (sin " {0}) & ].0,(PI / 2).] misses sin " {0} ) by SIN_COS:24, XBOOLE_0:def_7, XBOOLE_1:33; then ].0,(PI / 2).] c= (dom sin) \ (sin " {0}) by XBOOLE_1:83; hence ].0,(PI / 2).] c= dom cosec by RFUNCT_1:def_2; ::_thesis: verum end; theorem Th5: :: SINCOS10:5 ( sec is_differentiable_on ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds diff (sec,x) = (sin . x) / ((cos . x) ^2) ) ) proof set Z = ].0,(PI / 2).[; [.0,(PI / 2).[ = ].0,(PI / 2).[ \/ {0} by XXREAL_1:131; then ].0,(PI / 2).[ c= [.0,(PI / 2).[ by XBOOLE_1:7; then A1: ].0,(PI / 2).[ c= dom sec by Th1, XBOOLE_1:1; then A2: sec is_differentiable_on ].0,(PI / 2).[ by FDIFF_9:4; for x being Real st x in ].0,(PI / 2).[ holds diff (sec,x) = (sin . x) / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in ].0,(PI / 2).[ implies diff (sec,x) = (sin . x) / ((cos . x) ^2) ) assume A3: x in ].0,(PI / 2).[ ; ::_thesis: diff (sec,x) = (sin . x) / ((cos . x) ^2) then diff (sec,x) = (sec `| ].0,(PI / 2).[) . x by A2, FDIFF_1:def_7 .= (sin . x) / ((cos . x) ^2) by A1, A3, FDIFF_9:4 ; hence diff (sec,x) = (sin . x) / ((cos . x) ^2) ; ::_thesis: verum end; hence ( sec is_differentiable_on ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds diff (sec,x) = (sin . x) / ((cos . x) ^2) ) ) by A1, FDIFF_9:4; ::_thesis: verum end; theorem Th6: :: SINCOS10:6 ( sec is_differentiable_on ].(PI / 2),PI.[ & ( for x being Real st x in ].(PI / 2),PI.[ holds diff (sec,x) = (sin . x) / ((cos . x) ^2) ) ) proof set Z = ].(PI / 2),PI.[; PI / 2 < PI / 1 by XREAL_1:76; then ].(PI / 2),PI.] = ].(PI / 2),PI.[ \/ {PI} by XXREAL_1:132; then ].(PI / 2),PI.[ c= ].(PI / 2),PI.] by XBOOLE_1:7; then A1: ].(PI / 2),PI.[ c= dom sec by Th2, XBOOLE_1:1; then A2: sec is_differentiable_on ].(PI / 2),PI.[ by FDIFF_9:4; for x being Real st x in ].(PI / 2),PI.[ holds diff (sec,x) = (sin . x) / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in ].(PI / 2),PI.[ implies diff (sec,x) = (sin . x) / ((cos . x) ^2) ) assume A3: x in ].(PI / 2),PI.[ ; ::_thesis: diff (sec,x) = (sin . x) / ((cos . x) ^2) then diff (sec,x) = (sec `| ].(PI / 2),PI.[) . x by A2, FDIFF_1:def_7 .= (sin . x) / ((cos . x) ^2) by A1, A3, FDIFF_9:4 ; hence diff (sec,x) = (sin . x) / ((cos . x) ^2) ; ::_thesis: verum end; hence ( sec is_differentiable_on ].(PI / 2),PI.[ & ( for x being Real st x in ].(PI / 2),PI.[ holds diff (sec,x) = (sin . x) / ((cos . x) ^2) ) ) by A1, FDIFF_9:4; ::_thesis: verum end; theorem Th7: :: SINCOS10:7 ( cosec is_differentiable_on ].(- (PI / 2)),0.[ & ( for x being Real st x in ].(- (PI / 2)),0.[ holds diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) ) proof set Z = ].(- (PI / 2)),0.[; [.(- (PI / 2)),0.[ = ].(- (PI / 2)),0.[ \/ {(- (PI / 2))} by XXREAL_1:131; then ].(- (PI / 2)),0.[ c= [.(- (PI / 2)),0.[ by XBOOLE_1:7; then A1: ].(- (PI / 2)),0.[ c= dom cosec by Th3, XBOOLE_1:1; then A2: cosec is_differentiable_on ].(- (PI / 2)),0.[ by FDIFF_9:5; for x being Real st x in ].(- (PI / 2)),0.[ holds diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in ].(- (PI / 2)),0.[ implies diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) assume A3: x in ].(- (PI / 2)),0.[ ; ::_thesis: diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) then diff (cosec,x) = (cosec `| ].(- (PI / 2)),0.[) . x by A2, FDIFF_1:def_7 .= - ((cos . x) / ((sin . x) ^2)) by A1, A3, FDIFF_9:5 ; hence diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( cosec is_differentiable_on ].(- (PI / 2)),0.[ & ( for x being Real st x in ].(- (PI / 2)),0.[ holds diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) ) by A1, FDIFF_9:5; ::_thesis: verum end; theorem Th8: :: SINCOS10:8 ( cosec is_differentiable_on ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) ) proof set Z = ].0,(PI / 2).[; ].0,(PI / 2).] = ].0,(PI / 2).[ \/ {(PI / 2)} by XXREAL_1:132; then ].0,(PI / 2).[ c= ].0,(PI / 2).] by XBOOLE_1:7; then A1: ].0,(PI / 2).[ c= dom cosec by Th4, XBOOLE_1:1; then A2: cosec is_differentiable_on ].0,(PI / 2).[ by FDIFF_9:5; for x being Real st x in ].0,(PI / 2).[ holds diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in ].0,(PI / 2).[ implies diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) assume A3: x in ].0,(PI / 2).[ ; ::_thesis: diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) then diff (cosec,x) = (cosec `| ].0,(PI / 2).[) . x by A2, FDIFF_1:def_7 .= - ((cos . x) / ((sin . x) ^2)) by A1, A3, FDIFF_9:5 ; hence diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( cosec is_differentiable_on ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) ) by A1, FDIFF_9:5; ::_thesis: verum end; theorem :: SINCOS10:9 sec | ].0,(PI / 2).[ is continuous by Th5, FDIFF_1:25; theorem :: SINCOS10:10 sec | ].(PI / 2),PI.[ is continuous by Th6, FDIFF_1:25; theorem :: SINCOS10:11 cosec | ].(- (PI / 2)),0.[ is continuous by Th7, FDIFF_1:25; theorem :: SINCOS10:12 cosec | ].0,(PI / 2).[ is continuous by Th8, FDIFF_1:25; Lm5: ( 0 in [.0,(PI / 2).[ & PI / 4 in [.0,(PI / 2).[ ) proof PI / 4 < PI / 2 by XREAL_1:76; hence ( 0 in [.0,(PI / 2).[ & PI / 4 in [.0,(PI / 2).[ ) ; ::_thesis: verum end; Lm6: ( (3 / 4) * PI in ].(PI / 2),PI.] & PI in ].(PI / 2),PI.] ) proof PI / 4 < PI / 2 by XREAL_1:76; then ( (PI / 4) + (PI / 2) > 0 + (PI / 2) & (PI / 4) + (PI / 2) < (PI / 2) + (PI / 2) ) by XREAL_1:8; hence ( (3 / 4) * PI in ].(PI / 2),PI.] & PI in ].(PI / 2),PI.] ) by COMPTRIG:5; ::_thesis: verum end; Lm7: ( - (PI / 2) in [.(- (PI / 2)),0.[ & - (PI / 4) in [.(- (PI / 2)),0.[ ) proof PI / 4 < PI / 2 by XREAL_1:76; then - (PI / 4) > - (PI / 2) by XREAL_1:24; hence ( - (PI / 2) in [.(- (PI / 2)),0.[ & - (PI / 4) in [.(- (PI / 2)),0.[ ) ; ::_thesis: verum end; Lm8: ( PI / 4 in ].0,(PI / 2).] & PI / 2 in ].0,(PI / 2).] ) proof PI / 4 < PI / 2 by XREAL_1:76; hence ( PI / 4 in ].0,(PI / 2).] & PI / 2 in ].0,(PI / 2).] ) ; ::_thesis: verum end; Lm9: ].0,(PI / 2).[ c= [.0,(PI / 2).[ by XXREAL_1:22; then Lm10: ].0,(PI / 2).[ c= dom sec by Th1, XBOOLE_1:1; Lm11: ].(PI / 2),PI.[ c= ].(PI / 2),PI.] by XXREAL_1:21; then Lm12: ].(PI / 2),PI.[ c= dom sec by Th2, XBOOLE_1:1; Lm13: [.0,(PI / 4).] c= [.0,(PI / 2).[ by Lm5, XXREAL_2:def_12; Lm14: [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def_12; Lm15: ].(- (PI / 2)),0.[ c= [.(- (PI / 2)),0.[ by XXREAL_1:22; then Lm16: ].(- (PI / 2)),0.[ c= dom cosec by Th3, XBOOLE_1:1; Lm17: ].0,(PI / 2).[ c= ].0,(PI / 2).] by XXREAL_1:21; then Lm18: ].0,(PI / 2).[ c= dom cosec by Th4, XBOOLE_1:1; Lm19: [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def_12; Lm20: [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def_12; ].0,(PI / 2).[ = dom (sec | ].0,(PI / 2).[) by Lm9, Th1, RELAT_1:62, XBOOLE_1:1; then Lm21: ].0,(PI / 2).[ c= dom ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) by RELAT_1:74, XXREAL_1:22; ].(PI / 2),PI.[ = dom (sec | ].(PI / 2),PI.[) by Lm11, Th2, RELAT_1:62, XBOOLE_1:1; then Lm22: ].(PI / 2),PI.[ c= dom ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) by RELAT_1:74, XXREAL_1:21; ].(- (PI / 2)),0.[ = dom (cosec | ].(- (PI / 2)),0.[) by Lm15, Th3, RELAT_1:62, XBOOLE_1:1; then Lm23: ].(- (PI / 2)),0.[ c= dom ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) by RELAT_1:74, XXREAL_1:22; ].0,(PI / 2).[ = dom (cosec | ].0,(PI / 2).[) by Lm17, Th4, RELAT_1:62, XBOOLE_1:1; then Lm24: ].0,(PI / 2).[ c= dom ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) by RELAT_1:74, XXREAL_1:21; theorem Th13: :: SINCOS10:13 sec | ].0,(PI / 2).[ is increasing proof for x being Real st x in ].0,(PI / 2).[ holds diff (sec,x) > 0 proof let x be Real; ::_thesis: ( x in ].0,(PI / 2).[ implies diff (sec,x) > 0 ) assume A1: x in ].0,(PI / 2).[ ; ::_thesis: diff (sec,x) > 0 ].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then A2: cos . x > 0 by A1, COMPTRIG:11; PI / 2 < PI / 1 by XREAL_1:76; then ].0,(PI / 2).[ c= ].0,PI.[ by XXREAL_1:46; then sin . x > 0 by A1, COMPTRIG:7; then (sin . x) / ((cos . x) ^2) > 0 / ((cos . x) ^2) by A2; hence diff (sec,x) > 0 by A1, Th5; ::_thesis: verum end; hence sec | ].0,(PI / 2).[ is increasing by Lm9, Th1, Th5, ROLLE:9, XBOOLE_1:1; ::_thesis: verum end; theorem Th14: :: SINCOS10:14 sec | ].(PI / 2),PI.[ is increasing proof for x being Real st x in ].(PI / 2),PI.[ holds diff (sec,x) > 0 proof let x be Real; ::_thesis: ( x in ].(PI / 2),PI.[ implies diff (sec,x) > 0 ) assume A1: x in ].(PI / 2),PI.[ ; ::_thesis: diff (sec,x) > 0 PI <= (3 / 2) * PI by XREAL_1:151; then ].(PI / 2),PI.[ c= ].(PI / 2),((3 / 2) * PI).[ by XXREAL_1:46; then A2: cos . x < 0 by A1, COMPTRIG:13; ].(PI / 2),PI.[ c= ].0,PI.[ by XXREAL_1:46; then sin . x > 0 by A1, COMPTRIG:7; then (sin . x) / ((cos . x) ^2) > 0 / ((cos . x) ^2) by A2; hence diff (sec,x) > 0 by A1, Th6; ::_thesis: verum end; hence sec | ].(PI / 2),PI.[ is increasing by Lm11, Th2, Th6, ROLLE:9, XBOOLE_1:1; ::_thesis: verum end; theorem Th15: :: SINCOS10:15 cosec | ].(- (PI / 2)),0.[ is decreasing proof for x being Real st x in ].(- (PI / 2)),0.[ holds diff (cosec,x) < 0 proof let x be Real; ::_thesis: ( x in ].(- (PI / 2)),0.[ implies diff (cosec,x) < 0 ) assume A1: x in ].(- (PI / 2)),0.[ ; ::_thesis: diff (cosec,x) < 0 then x < 0 by XXREAL_1:4; then A2: x + (2 * PI) < 0 + (2 * PI) by XREAL_1:8; ].(- (PI / 2)),0.[ \/ {(- (PI / 2))} = [.(- (PI / 2)),0.[ by XXREAL_1:131; then ].(- (PI / 2)),0.[ c= [.(- (PI / 2)),0.[ by XBOOLE_1:7; then ].(- (PI / 2)),0.[ c= ].(- PI),0.[ by Lm3, XBOOLE_1:1; then - PI < x by A1, XXREAL_1:4; then (- PI) + (2 * PI) < x + (2 * PI) by XREAL_1:8; then x + (2 * PI) in ].PI,(2 * PI).[ by A2; then sin . (x + (2 * PI)) < 0 by COMPTRIG:9; then A3: sin . x < 0 by SIN_COS:78; ].(- (PI / 2)),0.[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then cos . x > 0 by A1, COMPTRIG:11; then - ((cos . x) / ((sin . x) ^2)) < - 0 by A3; hence diff (cosec,x) < 0 by A1, Th7; ::_thesis: verum end; hence cosec | ].(- (PI / 2)),0.[ is decreasing by Lm15, Th3, Th7, ROLLE:10, XBOOLE_1:1; ::_thesis: verum end; theorem Th16: :: SINCOS10:16 cosec | ].0,(PI / 2).[ is decreasing proof for x being Real st x in ].0,(PI / 2).[ holds diff (cosec,x) < 0 proof let x be Real; ::_thesis: ( x in ].0,(PI / 2).[ implies diff (cosec,x) < 0 ) assume A1: x in ].0,(PI / 2).[ ; ::_thesis: diff (cosec,x) < 0 ].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then A2: cos . x > 0 by A1, COMPTRIG:11; ].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46; then sin . x > 0 by A1, COMPTRIG:7; then - ((cos . x) / ((sin . x) ^2)) < - 0 by A2; hence diff (cosec,x) < 0 by A1, Th8; ::_thesis: verum end; hence cosec | ].0,(PI / 2).[ is decreasing by Lm17, Th4, Th8, ROLLE:10, XBOOLE_1:1; ::_thesis: verum end; theorem Th17: :: SINCOS10:17 sec | [.0,(PI / 2).[ is increasing proof now__::_thesis:_for_r1,_r2_being_Real_st_r1_in_[.0,(PI_/_2).[_/\_(dom_sec)_&_r2_in_[.0,(PI_/_2).[_/\_(dom_sec)_&_r1_<_r2_holds_ sec_._r2_>_sec_._r1 let r1, r2 be Real; ::_thesis: ( r1 in [.0,(PI / 2).[ /\ (dom sec) & r2 in [.0,(PI / 2).[ /\ (dom sec) & r1 < r2 implies sec . r2 > sec . r1 ) assume that A1: r1 in [.0,(PI / 2).[ /\ (dom sec) and A2: r2 in [.0,(PI / 2).[ /\ (dom sec) and A3: r1 < r2 ; ::_thesis: sec . r2 > sec . r1 A4: r1 in dom sec by A1, XBOOLE_0:def_4; A5: r1 in [.0,(PI / 2).[ by A1, XBOOLE_0:def_4; then A6: r1 < PI / 2 by XXREAL_1:3; A7: r2 in dom sec by A2, XBOOLE_0:def_4; A8: r2 in [.0,(PI / 2).[ by A2, XBOOLE_0:def_4; then A9: r2 < PI / 2 by XXREAL_1:3; now__::_thesis:_sec_._r2_>_sec_._r1 percases ( 0 = r1 or 0 < r1 ) by A5, XXREAL_1:3; supposeA10: 0 = r1 ; ::_thesis: sec . r2 > sec . r1 ( r2 < PI / 2 & PI / 2 < 2 * PI ) by A8, Lm1, XREAL_1:68, XXREAL_1:4; then r2 < 2 * PI by XXREAL_0:2; then cos r2 < 1 by A3, A10, SIN_COS6:34; then A11: cos . r2 < 1 by SIN_COS:def_19; ( (- (PI / 2)) + ((2 * PI) * 0) < r2 & r2 < (PI / 2) + ((2 * PI) * 0) ) by A8, Lm1, XXREAL_1:4; then cos r2 > 0 by SIN_COS6:13; then cos . r2 > 0 by SIN_COS:def_19; then A12: 1 / 1 < 1 / (cos . r2) by A11, XREAL_1:76; sec . r1 = 1 / 1 by A4, A10, RFUNCT_1:def_2, SIN_COS:30 .= 1 ; hence sec . r2 > sec . r1 by A7, A12, RFUNCT_1:def_2; ::_thesis: verum end; supposeA13: 0 < r1 ; ::_thesis: sec . r2 > sec . r1 then r1 in ].0,(PI / 2).[ by A6; then A14: r1 in ].0,(PI / 2).[ /\ (dom sec) by A4, XBOOLE_0:def_4; r2 in ].0,(PI / 2).[ by A3, A9, A13; then r2 in ].0,(PI / 2).[ /\ (dom sec) by A7, XBOOLE_0:def_4; hence sec . r2 > sec . r1 by A3, A14, Th13, RFUNCT_2:20; ::_thesis: verum end; end; end; hence sec . r2 > sec . r1 ; ::_thesis: verum end; hence sec | [.0,(PI / 2).[ is increasing by RFUNCT_2:20; ::_thesis: verum end; theorem Th18: :: SINCOS10:18 sec | ].(PI / 2),PI.] is increasing proof now__::_thesis:_for_r1,_r2_being_Real_st_r1_in_].(PI_/_2),PI.]_/\_(dom_sec)_&_r2_in_].(PI_/_2),PI.]_/\_(dom_sec)_&_r1_<_r2_holds_ sec_._r2_>_sec_._r1 let r1, r2 be Real; ::_thesis: ( r1 in ].(PI / 2),PI.] /\ (dom sec) & r2 in ].(PI / 2),PI.] /\ (dom sec) & r1 < r2 implies sec . r2 > sec . r1 ) assume that A1: r1 in ].(PI / 2),PI.] /\ (dom sec) and A2: r2 in ].(PI / 2),PI.] /\ (dom sec) and A3: r1 < r2 ; ::_thesis: sec . r2 > sec . r1 A4: r1 in dom sec by A1, XBOOLE_0:def_4; A5: r2 in dom sec by A2, XBOOLE_0:def_4; A6: r1 in ].(PI / 2),PI.] by A1, XBOOLE_0:def_4; then A7: PI / 2 < r1 by XXREAL_1:2; A8: r2 in ].(PI / 2),PI.] by A2, XBOOLE_0:def_4; then A9: r2 <= PI by XXREAL_1:2; A10: PI / 2 < r2 by A8, XXREAL_1:2; now__::_thesis:_sec_._r2_>_sec_._r1 percases ( r2 < PI or r2 = PI ) by A9, XXREAL_0:1; supposeA11: r2 < PI ; ::_thesis: sec . r2 > sec . r1 then r1 < PI by A3, XXREAL_0:2; then r1 in ].(PI / 2),PI.[ by A7; then A12: r1 in ].(PI / 2),PI.[ /\ (dom sec) by A4, XBOOLE_0:def_4; r2 in ].(PI / 2),PI.[ by A10, A11; then r2 in ].(PI / 2),PI.[ /\ (dom sec) by A5, XBOOLE_0:def_4; hence sec . r2 > sec . r1 by A3, A12, Th14, RFUNCT_2:20; ::_thesis: verum end; supposeA13: r2 = PI ; ::_thesis: sec . r1 < sec . r2 PI * 1 < PI * (3 / 2) by XREAL_1:68; then A14: r1 < ((3 / 2) * PI) + ((2 * PI) * 0) by A3, A13, XXREAL_0:2; (PI / 2) + ((2 * PI) * 0) < r1 by A6, XXREAL_1:2; then cos r1 < 0 by A14, SIN_COS6:14; then A15: cos . r1 < 0 by SIN_COS:def_19; r1 < PI by A3, A9, XXREAL_0:2; then cos r1 > - 1 by A7, SIN_COS6:35; then cos . r1 > - 1 by SIN_COS:def_19; then A16: (cos . r1) " < (- 1) " by A15, XREAL_1:87; sec . r2 = 1 / (- 1) by A5, A13, RFUNCT_1:def_2, SIN_COS:76 .= - 1 ; hence sec . r1 < sec . r2 by A4, A16, RFUNCT_1:def_2; ::_thesis: verum end; end; end; hence sec . r2 > sec . r1 ; ::_thesis: verum end; hence sec | ].(PI / 2),PI.] is increasing by RFUNCT_2:20; ::_thesis: verum end; theorem Th19: :: SINCOS10:19 cosec | [.(- (PI / 2)),0.[ is decreasing proof now__::_thesis:_for_r1,_r2_being_Real_st_r1_in_[.(-_(PI_/_2)),0.[_/\_(dom_cosec)_&_r2_in_[.(-_(PI_/_2)),0.[_/\_(dom_cosec)_&_r1_<_r2_holds_ cosec_._r2_<_cosec_._r1 let r1, r2 be Real; ::_thesis: ( r1 in [.(- (PI / 2)),0.[ /\ (dom cosec) & r2 in [.(- (PI / 2)),0.[ /\ (dom cosec) & r1 < r2 implies cosec . r2 < cosec . r1 ) assume that A1: r1 in [.(- (PI / 2)),0.[ /\ (dom cosec) and A2: r2 in [.(- (PI / 2)),0.[ /\ (dom cosec) and A3: r1 < r2 ; ::_thesis: cosec . r2 < cosec . r1 A4: r1 in dom cosec by A1, XBOOLE_0:def_4; A5: r1 in [.(- (PI / 2)),0.[ by A1, XBOOLE_0:def_4; then A6: r1 < 0 by XXREAL_1:3; A7: r2 in dom cosec by A2, XBOOLE_0:def_4; A8: r2 in [.(- (PI / 2)),0.[ by A2, XBOOLE_0:def_4; then A9: r2 < 0 by XXREAL_1:3; A10: - (PI / 2) <= r1 by A5, XXREAL_1:3; now__::_thesis:_cosec_._r2_<_cosec_._r1 percases ( - (PI / 2) = r1 or - (PI / 2) < r1 ) by A10, XXREAL_0:1; supposeA11: - (PI / 2) = r1 ; ::_thesis: cosec . r2 < cosec . r1 - (PI / 2) > - PI by COMPTRIG:5, XREAL_1:24; then A12: ].(- (PI / 2)),0.[ c= ].(- PI),0.[ by XXREAL_1:46; r2 in ].(- (PI / 2)),0.[ by A3, A9, A11; then - PI < r2 by A12, XXREAL_1:4; then A13: (- PI) + (2 * PI) < r2 + (2 * PI) by XREAL_1:8; r2 + (2 * PI) < 0 + (2 * PI) by A9, XREAL_1:8; then r2 + (2 * PI) in ].PI,(2 * PI).[ by A13; then sin . (r2 + (2 * PI)) < 0 by COMPTRIG:9; then A14: sin . r2 < 0 by SIN_COS:78; A15: r2 < (2 * PI) + ((2 * PI) * (- 1)) by A8, XXREAL_1:3; ((3 / 2) * PI) + ((2 * PI) * (- 1)) < r2 by A3, A11; then sin r2 > - 1 by A15, SIN_COS6:39; then sin . r2 > - 1 by SIN_COS:def_17; then A16: (sin . r2) " < (- 1) " by A14, XREAL_1:87; cosec . r1 = 1 / (sin . (- (PI / 2))) by A4, A11, RFUNCT_1:def_2 .= 1 / (- 1) by SIN_COS:30, SIN_COS:76 .= - 1 ; hence cosec . r2 < cosec . r1 by A7, A16, RFUNCT_1:def_2; ::_thesis: verum end; supposeA17: - (PI / 2) < r1 ; ::_thesis: cosec . r2 < cosec . r1 then - (PI / 2) < r2 by A3, XXREAL_0:2; then r2 in ].(- (PI / 2)),0.[ by A9; then A18: r2 in ].(- (PI / 2)),0.[ /\ (dom cosec) by A7, XBOOLE_0:def_4; r1 in ].(- (PI / 2)),0.[ by A6, A17; then r1 in ].(- (PI / 2)),0.[ /\ (dom cosec) by A4, XBOOLE_0:def_4; hence cosec . r2 < cosec . r1 by A3, A18, Th15, RFUNCT_2:21; ::_thesis: verum end; end; end; hence cosec . r2 < cosec . r1 ; ::_thesis: verum end; hence cosec | [.(- (PI / 2)),0.[ is decreasing by RFUNCT_2:21; ::_thesis: verum end; theorem Th20: :: SINCOS10:20 cosec | ].0,(PI / 2).] is decreasing proof now__::_thesis:_for_r1,_r2_being_Real_st_r1_in_].0,(PI_/_2).]_/\_(dom_cosec)_&_r2_in_].0,(PI_/_2).]_/\_(dom_cosec)_&_r1_<_r2_holds_ cosec_._r2_<_cosec_._r1 let r1, r2 be Real; ::_thesis: ( r1 in ].0,(PI / 2).] /\ (dom cosec) & r2 in ].0,(PI / 2).] /\ (dom cosec) & r1 < r2 implies cosec . r2 < cosec . r1 ) assume that A1: r1 in ].0,(PI / 2).] /\ (dom cosec) and A2: r2 in ].0,(PI / 2).] /\ (dom cosec) and A3: r1 < r2 ; ::_thesis: cosec . r2 < cosec . r1 A4: r1 in dom cosec by A1, XBOOLE_0:def_4; A5: r2 in ].0,(PI / 2).] by A2, XBOOLE_0:def_4; then A6: r2 <= PI / 2 by XXREAL_1:2; A7: r2 in dom cosec by A2, XBOOLE_0:def_4; A8: r1 in ].0,(PI / 2).] by A1, XBOOLE_0:def_4; then A9: 0 < r1 by XXREAL_1:2; A10: 0 < r2 by A5, XXREAL_1:2; now__::_thesis:_cosec_._r2_<_cosec_._r1 percases ( r2 < PI / 2 or r2 = PI / 2 ) by A6, XXREAL_0:1; supposeA11: r2 < PI / 2 ; ::_thesis: cosec . r2 < cosec . r1 then r1 < PI / 2 by A3, XXREAL_0:2; then r1 in ].0,(PI / 2).[ by A9; then A12: r1 in ].0,(PI / 2).[ /\ (dom cosec) by A4, XBOOLE_0:def_4; r2 in ].0,(PI / 2).[ by A10, A11; then r2 in ].0,(PI / 2).[ /\ (dom cosec) by A7, XBOOLE_0:def_4; hence cosec . r2 < cosec . r1 by A3, A12, Th16, RFUNCT_2:21; ::_thesis: verum end; supposeA13: r2 = PI / 2 ; ::_thesis: cosec . r2 < cosec . r1 then sin r1 < 1 by A3, A9, SIN_COS6:30; then A14: sin . r1 < 1 by SIN_COS:def_17; sin . r1 > 0 by A8, Lm4, COMPTRIG:7; then A15: 1 / 1 < 1 / (sin . r1) by A14, XREAL_1:76; cosec . r2 = 1 / 1 by A7, A13, RFUNCT_1:def_2, SIN_COS:76 .= 1 ; hence cosec . r2 < cosec . r1 by A4, A15, RFUNCT_1:def_2; ::_thesis: verum end; end; end; hence cosec . r2 < cosec . r1 ; ::_thesis: verum end; hence cosec | ].0,(PI / 2).] is decreasing by RFUNCT_2:21; ::_thesis: verum end; theorem :: SINCOS10:21 sec | [.0,(PI / 2).[ is one-to-one by Th17, FCONT_3:8; theorem :: SINCOS10:22 sec | ].(PI / 2),PI.] is one-to-one by Th18, FCONT_3:8; theorem :: SINCOS10:23 cosec | [.(- (PI / 2)),0.[ is one-to-one by Th19, FCONT_3:8; theorem :: SINCOS10:24 cosec | ].0,(PI / 2).] is one-to-one by Th20, FCONT_3:8; registration clusterK77(sec,[.0,(PI / 2).[) -> one-to-one ; coherence sec | [.0,(PI / 2).[ is one-to-one by Th17, FCONT_3:8; clusterK77(sec,].(PI / 2),PI.]) -> one-to-one ; coherence sec | ].(PI / 2),PI.] is one-to-one by Th18, FCONT_3:8; clusterK77(cosec,[.(- (PI / 2)),0.[) -> one-to-one ; coherence cosec | [.(- (PI / 2)),0.[ is one-to-one by Th19, FCONT_3:8; clusterK77(cosec,].0,(PI / 2).]) -> one-to-one ; coherence cosec | ].0,(PI / 2).] is one-to-one by Th20, FCONT_3:8; end; definition func arcsec1 -> PartFunc of REAL,REAL equals :: SINCOS10:def 1 (sec | [.0,(PI / 2).[) " ; coherence (sec | [.0,(PI / 2).[) " is PartFunc of REAL,REAL ; func arcsec2 -> PartFunc of REAL,REAL equals :: SINCOS10:def 2 (sec | ].(PI / 2),PI.]) " ; coherence (sec | ].(PI / 2),PI.]) " is PartFunc of REAL,REAL ; func arccosec1 -> PartFunc of REAL,REAL equals :: SINCOS10:def 3 (cosec | [.(- (PI / 2)),0.[) " ; coherence (cosec | [.(- (PI / 2)),0.[) " is PartFunc of REAL,REAL ; func arccosec2 -> PartFunc of REAL,REAL equals :: SINCOS10:def 4 (cosec | ].0,(PI / 2).]) " ; coherence (cosec | ].0,(PI / 2).]) " is PartFunc of REAL,REAL ; end; :: deftheorem defines arcsec1 SINCOS10:def_1_:_ arcsec1 = (sec | [.0,(PI / 2).[) " ; :: deftheorem defines arcsec2 SINCOS10:def_2_:_ arcsec2 = (sec | ].(PI / 2),PI.]) " ; :: deftheorem defines arccosec1 SINCOS10:def_3_:_ arccosec1 = (cosec | [.(- (PI / 2)),0.[) " ; :: deftheorem defines arccosec2 SINCOS10:def_4_:_ arccosec2 = (cosec | ].0,(PI / 2).]) " ; definition let r be Real; func arcsec1 r -> set equals :: SINCOS10:def 5 arcsec1 . r; coherence arcsec1 . r is set ; func arcsec2 r -> set equals :: SINCOS10:def 6 arcsec2 . r; coherence arcsec2 . r is set ; func arccosec1 r -> set equals :: SINCOS10:def 7 arccosec1 . r; coherence arccosec1 . r is set ; func arccosec2 r -> set equals :: SINCOS10:def 8 arccosec2 . r; coherence arccosec2 . r is set ; end; :: deftheorem defines arcsec1 SINCOS10:def_5_:_ for r being Real holds arcsec1 r = arcsec1 . r; :: deftheorem defines arcsec2 SINCOS10:def_6_:_ for r being Real holds arcsec2 r = arcsec2 . r; :: deftheorem defines arccosec1 SINCOS10:def_7_:_ for r being Real holds arccosec1 r = arccosec1 . r; :: deftheorem defines arccosec2 SINCOS10:def_8_:_ for r being Real holds arccosec2 r = arccosec2 . r; definition let r be Real; :: original: arcsec1 redefine func arcsec1 r -> Real; coherence arcsec1 r is Real ; :: original: arcsec2 redefine func arcsec2 r -> Real; coherence arcsec2 r is Real ; :: original: arccosec1 redefine func arccosec1 r -> Real; coherence arccosec1 r is Real ; :: original: arccosec2 redefine func arccosec2 r -> Real; coherence arccosec2 r is Real ; end; Lm25: arcsec1 " = sec | [.0,(PI / 2).[ by FUNCT_1:43; Lm26: arcsec2 " = sec | ].(PI / 2),PI.] by FUNCT_1:43; Lm27: arccosec1 " = cosec | [.(- (PI / 2)),0.[ by FUNCT_1:43; Lm28: arccosec2 " = cosec | ].0,(PI / 2).] by FUNCT_1:43; theorem Th25: :: SINCOS10:25 rng arcsec1 = [.0,(PI / 2).[ proof dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ by Th1, RELAT_1:62; hence rng arcsec1 = [.0,(PI / 2).[ by FUNCT_1:33; ::_thesis: verum end; theorem Th26: :: SINCOS10:26 rng arcsec2 = ].(PI / 2),PI.] proof dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] by Th2, RELAT_1:62; hence rng arcsec2 = ].(PI / 2),PI.] by FUNCT_1:33; ::_thesis: verum end; theorem Th27: :: SINCOS10:27 rng arccosec1 = [.(- (PI / 2)),0.[ proof dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[ by Th3, RELAT_1:62; hence rng arccosec1 = [.(- (PI / 2)),0.[ by FUNCT_1:33; ::_thesis: verum end; theorem Th28: :: SINCOS10:28 rng arccosec2 = ].0,(PI / 2).] proof dom (cosec | ].0,(PI / 2).]) = ].0,(PI / 2).] by Th4, RELAT_1:62; hence rng arccosec2 = ].0,(PI / 2).] by FUNCT_1:33; ::_thesis: verum end; registration cluster arcsec1 -> one-to-one ; coherence arcsec1 is one-to-one ; cluster arcsec2 -> one-to-one ; coherence arcsec2 is one-to-one ; cluster arccosec1 -> one-to-one ; coherence arccosec1 is one-to-one ; cluster arccosec2 -> one-to-one ; coherence arccosec2 is one-to-one ; end; theorem Th29: :: SINCOS10:29 ( sin . (PI / 4) = 1 / (sqrt 2) & cos . (PI / 4) = 1 / (sqrt 2) ) proof A1: (sqrt (1 / 2)) ^2 = 1 / 2 by SQUARE_1:def_2; 1 = ((sin . (PI / 4)) ^2) + ((sin . (PI / 4)) ^2) by SIN_COS:28, SIN_COS:73 .= 2 * ((sin . (PI / 4)) ^2) ; then A2: ( sin . (PI / 4) = sqrt (1 / 2) or sin . (PI / 4) = - (sqrt (1 / 2)) ) by A1, SQUARE_1:40; PI / 4 < PI / 1 by XREAL_1:76; then A3: PI / 4 in ].0,PI.[ ; sqrt (1 / 2) > 0 by SQUARE_1:25; hence ( sin . (PI / 4) = 1 / (sqrt 2) & cos . (PI / 4) = 1 / (sqrt 2) ) by A2, A3, COMPTRIG:7, SIN_COS:73, SQUARE_1:32; ::_thesis: verum end; theorem Th30: :: SINCOS10:30 ( sin . (- (PI / 4)) = - (1 / (sqrt 2)) & cos . (- (PI / 4)) = 1 / (sqrt 2) & sin . ((3 / 4) * PI) = 1 / (sqrt 2) & cos . ((3 / 4) * PI) = - (1 / (sqrt 2)) ) proof A1: cos . (- (PI / 4)) = 1 / (sqrt 2) by Th29, SIN_COS:30; A2: cos . ((3 / 4) * PI) = cos . (PI + (- (PI / 4))) .= - (1 / (sqrt 2)) by A1, SIN_COS:78 ; A3: sin . (- (PI / 4)) = - (1 / (sqrt 2)) by Th29, SIN_COS:30; sin . ((3 / 4) * PI) = sin . (PI + (- (PI / 4))) .= - (- (1 / (sqrt 2))) by A3, SIN_COS:78 .= 1 / (sqrt 2) ; hence ( sin . (- (PI / 4)) = - (1 / (sqrt 2)) & cos . (- (PI / 4)) = 1 / (sqrt 2) & sin . ((3 / 4) * PI) = 1 / (sqrt 2) & cos . ((3 / 4) * PI) = - (1 / (sqrt 2)) ) by A2, Th29, SIN_COS:30; ::_thesis: verum end; theorem Th31: :: SINCOS10:31 ( sec . 0 = 1 & sec . (PI / 4) = sqrt 2 & sec . ((3 / 4) * PI) = - (sqrt 2) & sec . PI = - 1 ) proof A1: sec . PI = 1 / (- 1) by Lm6, Th2, RFUNCT_1:def_2, SIN_COS:76 .= - 1 ; A2: sec . ((3 / 4) * PI) = 1 / (- (1 / (sqrt 2))) by Lm6, Th2, Th30, RFUNCT_1:def_2 .= - (1 / (1 / (sqrt 2))) by XCMPLX_1:188 .= - (sqrt 2) ; A3: sec . 0 = 1 / 1 by Lm5, Th1, RFUNCT_1:def_2, SIN_COS:30 .= 1 ; sec . (PI / 4) = 1 / (1 / (sqrt 2)) by Lm5, Th1, Th29, RFUNCT_1:def_2 .= sqrt 2 ; hence ( sec . 0 = 1 & sec . (PI / 4) = sqrt 2 & sec . ((3 / 4) * PI) = - (sqrt 2) & sec . PI = - 1 ) by A3, A2, A1; ::_thesis: verum end; theorem Th32: :: SINCOS10:32 ( cosec . (- (PI / 2)) = - 1 & cosec . (- (PI / 4)) = - (sqrt 2) & cosec . (PI / 4) = sqrt 2 & cosec . (PI / 2) = 1 ) proof A1: cosec . (PI / 2) = 1 / 1 by Lm8, Th4, RFUNCT_1:def_2, SIN_COS:76 .= 1 ; A2: cosec . (PI / 4) = 1 / (1 / (sqrt 2)) by Lm8, Th4, Th29, RFUNCT_1:def_2 .= sqrt 2 ; A3: cosec . (- (PI / 2)) = 1 / (sin . (- (PI / 2))) by Lm7, Th3, RFUNCT_1:def_2 .= 1 / (- 1) by SIN_COS:30, SIN_COS:76 .= - 1 ; cosec . (- (PI / 4)) = 1 / (- (1 / (sqrt 2))) by Lm7, Th3, Th30, RFUNCT_1:def_2 .= - (1 / (1 / (sqrt 2))) by XCMPLX_1:188 .= - (sqrt 2) ; hence ( cosec . (- (PI / 2)) = - 1 & cosec . (- (PI / 4)) = - (sqrt 2) & cosec . (PI / 4) = sqrt 2 & cosec . (PI / 2) = 1 ) by A3, A2, A1; ::_thesis: verum end; theorem Th33: :: SINCOS10:33 for x being set st x in [.0,(PI / 4).] holds sec . x in [.1,(sqrt 2).] proof let x be set ; ::_thesis: ( x in [.0,(PI / 4).] implies sec . x in [.1,(sqrt 2).] ) assume x in [.0,(PI / 4).] ; ::_thesis: sec . x in [.1,(sqrt 2).] then x in ].0,(PI / 4).[ \/ {0,(PI / 4)} by XXREAL_1:128; then A1: ( x in ].0,(PI / 4).[ or x in {0,(PI / 4)} ) by XBOOLE_0:def_3; percases ( x in ].0,(PI / 4).[ or x = 0 or x = PI / 4 ) by A1, TARSKI:def_2; supposeA2: x in ].0,(PI / 4).[ ; ::_thesis: sec . x in [.1,(sqrt 2).] PI / 4 < PI / 2 by XREAL_1:76; then ( 0 in [.0,(PI / 2).[ & PI / 4 in [.0,(PI / 2).[ ) ; then A3: [.0,(PI / 4).] c= [.0,(PI / 2).[ by XXREAL_2:def_12; then A4: sec | [.0,(PI / 4).] is increasing by Th17, RFUNCT_2:28; A5: ex s being Real st ( s = x & 0 < s & s < PI / 4 ) by A2; A6: ].0,(PI / 4).[ c= [.0,(PI / 4).] by XXREAL_1:25; A7: [.0,(PI / 4).] /\ (dom sec) = [.0,(PI / 4).] by A3, Th1, XBOOLE_1:1, XBOOLE_1:28; ( 0 in [.0,(PI / 4).] & ex s being Real st ( s = x & 0 < s & s < PI / 4 ) ) by A2; then A8: 1 < sec . x by A2, A4, A7, A6, Th31, RFUNCT_2:20; PI / 4 in [.0,(PI / 4).] /\ (dom sec) by A7; then sec . x < sqrt 2 by A2, A4, A7, A6, A5, Th31, RFUNCT_2:20; hence sec . x in [.1,(sqrt 2).] by A8; ::_thesis: verum end; suppose x = 0 ; ::_thesis: sec . x in [.1,(sqrt 2).] hence sec . x in [.1,(sqrt 2).] by Th31, SQUARE_1:19; ::_thesis: verum end; suppose x = PI / 4 ; ::_thesis: sec . x in [.1,(sqrt 2).] hence sec . x in [.1,(sqrt 2).] by Th31, SQUARE_1:19; ::_thesis: verum end; end; end; theorem Th34: :: SINCOS10:34 for x being set st x in [.((3 / 4) * PI),PI.] holds sec . x in [.(- (sqrt 2)),(- 1).] proof let x be set ; ::_thesis: ( x in [.((3 / 4) * PI),PI.] implies sec . x in [.(- (sqrt 2)),(- 1).] ) A1: PI / 4 < PI / 2 by XREAL_1:76; then A2: (PI / 4) + (PI / 2) < (PI / 2) + (PI / 2) by XREAL_1:8; assume x in [.((3 / 4) * PI),PI.] ; ::_thesis: sec . x in [.(- (sqrt 2)),(- 1).] then x in ].((3 / 4) * PI),PI.[ \/ {((3 / 4) * PI),PI} by A2, XXREAL_1:128; then A3: ( x in ].((3 / 4) * PI),PI.[ or x in {((3 / 4) * PI),PI} ) by XBOOLE_0:def_3; percases ( x in ].((3 / 4) * PI),PI.[ or x = (3 / 4) * PI or x = PI ) by A3, TARSKI:def_2; supposeA4: x in ].((3 / 4) * PI),PI.[ ; ::_thesis: sec . x in [.(- (sqrt 2)),(- 1).] (PI / 4) + (PI / 4) < (PI / 2) + (PI / 4) by A1, XREAL_1:8; then A5: (3 / 4) * PI in ].(PI / 2),PI.] by A2; PI in ].(PI / 2),PI.] by COMPTRIG:5; then A6: [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by A5, XXREAL_2:def_12; then A7: sec | [.((3 / 4) * PI),PI.] is increasing by Th18, RFUNCT_2:28; A8: ex s being Real st ( s = x & (3 / 4) * PI < s & s < PI ) by A4; A9: ex s being Real st ( s = x & (3 / 4) * PI < s & s < PI ) by A4; A10: ].((3 / 4) * PI),PI.[ c= [.((3 / 4) * PI),PI.] by XXREAL_1:25; A11: [.((3 / 4) * PI),PI.] /\ (dom sec) = [.((3 / 4) * PI),PI.] by A6, Th2, XBOOLE_1:1, XBOOLE_1:28; then PI in [.((3 / 4) * PI),PI.] /\ (dom sec) by A2; then A12: sec . x < - 1 by A4, A7, A11, A10, A9, Th31, RFUNCT_2:20; (3 / 4) * PI in [.((3 / 4) * PI),PI.] by A2; then - (sqrt 2) < sec . x by A4, A7, A11, A10, A8, Th31, RFUNCT_2:20; hence sec . x in [.(- (sqrt 2)),(- 1).] by A12; ::_thesis: verum end; supposeA13: x = (3 / 4) * PI ; ::_thesis: sec . x in [.(- (sqrt 2)),(- 1).] - (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24; hence sec . x in [.(- (sqrt 2)),(- 1).] by A13, Th31; ::_thesis: verum end; supposeA14: x = PI ; ::_thesis: sec . x in [.(- (sqrt 2)),(- 1).] - (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24; hence sec . x in [.(- (sqrt 2)),(- 1).] by A14, Th31; ::_thesis: verum end; end; end; theorem Th35: :: SINCOS10:35 for x being set st x in [.(- (PI / 2)),(- (PI / 4)).] holds cosec . x in [.(- (sqrt 2)),(- 1).] proof let x be set ; ::_thesis: ( x in [.(- (PI / 2)),(- (PI / 4)).] implies cosec . x in [.(- (sqrt 2)),(- 1).] ) PI / 4 < PI / 2 by XREAL_1:76; then A1: - (PI / 2) < - (PI / 4) by XREAL_1:24; assume x in [.(- (PI / 2)),(- (PI / 4)).] ; ::_thesis: cosec . x in [.(- (sqrt 2)),(- 1).] then x in ].(- (PI / 2)),(- (PI / 4)).[ \/ {(- (PI / 2)),(- (PI / 4))} by A1, XXREAL_1:128; then A2: ( x in ].(- (PI / 2)),(- (PI / 4)).[ or x in {(- (PI / 2)),(- (PI / 4))} ) by XBOOLE_0:def_3; percases ( x in ].(- (PI / 2)),(- (PI / 4)).[ or x = - (PI / 2) or x = - (PI / 4) ) by A2, TARSKI:def_2; supposeA3: x in ].(- (PI / 2)),(- (PI / 4)).[ ; ::_thesis: cosec . x in [.(- (sqrt 2)),(- 1).] then A4: ex s being Real st ( s = x & - (PI / 2) < s & s < - (PI / 4) ) ; A5: ex s being Real st ( s = x & - (PI / 2) < s & s < - (PI / 4) ) by A3; A6: ].(- (PI / 2)),(- (PI / 4)).[ c= [.(- (PI / 2)),(- (PI / 4)).] by XXREAL_1:25; ( - (PI / 2) in [.(- (PI / 2)),0.[ & - (PI / 4) in [.(- (PI / 2)),0.[ ) by A1; then A7: [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by XXREAL_2:def_12; then A8: cosec | [.(- (PI / 2)),(- (PI / 4)).] is decreasing by Th19, RFUNCT_2:29; A9: [.(- (PI / 2)),(- (PI / 4)).] /\ (dom cosec) = [.(- (PI / 2)),(- (PI / 4)).] by A7, Th3, XBOOLE_1:1, XBOOLE_1:28; then - (PI / 4) in [.(- (PI / 2)),(- (PI / 4)).] /\ (dom cosec) by A1; then A10: cosec . x > - (sqrt 2) by A3, A8, A9, A6, A5, Th32, RFUNCT_2:21; - (PI / 2) in [.(- (PI / 2)),(- (PI / 4)).] by A1; then - 1 > cosec . x by A3, A8, A9, A6, A4, Th32, RFUNCT_2:21; hence cosec . x in [.(- (sqrt 2)),(- 1).] by A10; ::_thesis: verum end; supposeA11: x = - (PI / 2) ; ::_thesis: cosec . x in [.(- (sqrt 2)),(- 1).] - (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24; hence cosec . x in [.(- (sqrt 2)),(- 1).] by A11, Th32; ::_thesis: verum end; supposeA12: x = - (PI / 4) ; ::_thesis: cosec . x in [.(- (sqrt 2)),(- 1).] - (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24; hence cosec . x in [.(- (sqrt 2)),(- 1).] by A12, Th32; ::_thesis: verum end; end; end; theorem Th36: :: SINCOS10:36 for x being set st x in [.(PI / 4),(PI / 2).] holds cosec . x in [.1,(sqrt 2).] proof let x be set ; ::_thesis: ( x in [.(PI / 4),(PI / 2).] implies cosec . x in [.1,(sqrt 2).] ) A1: PI / 4 < PI / 2 by XREAL_1:76; assume x in [.(PI / 4),(PI / 2).] ; ::_thesis: cosec . x in [.1,(sqrt 2).] then x in ].(PI / 4),(PI / 2).[ \/ {(PI / 4),(PI / 2)} by A1, XXREAL_1:128; then A2: ( x in ].(PI / 4),(PI / 2).[ or x in {(PI / 4),(PI / 2)} ) by XBOOLE_0:def_3; percases ( x in ].(PI / 4),(PI / 2).[ or x = PI / 4 or x = PI / 2 ) by A2, TARSKI:def_2; supposeA3: x in ].(PI / 4),(PI / 2).[ ; ::_thesis: cosec . x in [.1,(sqrt 2).] then A4: ex s being Real st ( s = x & PI / 4 < s & s < PI / 2 ) ; A5: ex s being Real st ( s = x & PI / 4 < s & s < PI / 2 ) by A3; A6: ].(PI / 4),(PI / 2).[ c= [.(PI / 4),(PI / 2).] by XXREAL_1:25; ( PI / 4 in ].0,(PI / 2).] & PI / 2 in ].0,(PI / 2).] ) by A1; then A7: [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by XXREAL_2:def_12; then A8: cosec | [.(PI / 4),(PI / 2).] is decreasing by Th20, RFUNCT_2:29; A9: [.(PI / 4),(PI / 2).] /\ (dom cosec) = [.(PI / 4),(PI / 2).] by A7, Th4, XBOOLE_1:1, XBOOLE_1:28; then PI / 2 in [.(PI / 4),(PI / 2).] /\ (dom cosec) by A1; then A10: cosec . x > 1 by A3, A8, A9, A6, A5, Th32, RFUNCT_2:21; PI / 4 in [.(PI / 4),(PI / 2).] by A1; then sqrt 2 > cosec . x by A3, A8, A9, A6, A4, Th32, RFUNCT_2:21; hence cosec . x in [.1,(sqrt 2).] by A10; ::_thesis: verum end; suppose x = PI / 4 ; ::_thesis: cosec . x in [.1,(sqrt 2).] hence cosec . x in [.1,(sqrt 2).] by Th32, SQUARE_1:19; ::_thesis: verum end; suppose x = PI / 2 ; ::_thesis: cosec . x in [.1,(sqrt 2).] hence cosec . x in [.1,(sqrt 2).] by Th32, SQUARE_1:19; ::_thesis: verum end; end; end; Lm29: dom (sec | [.0,(PI / 4).]) = [.0,(PI / 4).] proof [.0,(PI / 4).] c= [.0,(PI / 2).[ by Lm5, XXREAL_2:def_12; hence dom (sec | [.0,(PI / 4).]) = [.0,(PI / 4).] by Th1, RELAT_1:62, XBOOLE_1:1; ::_thesis: verum end; Lm30: dom (sec | [.((3 / 4) * PI),PI.]) = [.((3 / 4) * PI),PI.] proof [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def_12; hence dom (sec | [.((3 / 4) * PI),PI.]) = [.((3 / 4) * PI),PI.] by Th2, RELAT_1:62, XBOOLE_1:1; ::_thesis: verum end; Lm31: dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (PI / 2)),(- (PI / 4)).] proof [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def_12; hence dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (PI / 2)),(- (PI / 4)).] by Th3, RELAT_1:62, XBOOLE_1:1; ::_thesis: verum end; Lm32: dom (cosec | [.(PI / 4),(PI / 2).]) = [.(PI / 4),(PI / 2).] proof [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def_12; hence dom (cosec | [.(PI / 4),(PI / 2).]) = [.(PI / 4),(PI / 2).] by Th4, RELAT_1:62, XBOOLE_1:1; ::_thesis: verum end; Lm33: ( dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ & ( for th being real number st th in [.0,(PI / 2).[ holds (sec | [.0,(PI / 2).[) . th = sec . th ) ) proof dom (sec | [.0,(PI / 2).[) = (dom sec) /\ [.0,(PI / 2).[ by RELAT_1:61; then dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ by Th1, XBOOLE_1:28; hence ( dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ & ( for th being real number st th in [.0,(PI / 2).[ holds (sec | [.0,(PI / 2).[) . th = sec . th ) ) by FUNCT_1:47; ::_thesis: verum end; Lm34: ( dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] & ( for th being real number st th in ].(PI / 2),PI.] holds (sec | ].(PI / 2),PI.]) . th = sec . th ) ) proof dom (sec | ].(PI / 2),PI.]) = (dom sec) /\ ].(PI / 2),PI.] by RELAT_1:61; then dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] by Th2, XBOOLE_1:28; hence ( dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] & ( for th being real number st th in ].(PI / 2),PI.] holds (sec | ].(PI / 2),PI.]) . th = sec . th ) ) by FUNCT_1:47; ::_thesis: verum end; Lm35: ( dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[ & ( for th being real number st th in [.(- (PI / 2)),0.[ holds (cosec | [.(- (PI / 2)),0.[) . th = cosec . th ) ) proof dom (cosec | [.(- (PI / 2)),0.[) = (dom cosec) /\ [.(- (PI / 2)),0.[ by RELAT_1:61; then dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[ by Th3, XBOOLE_1:28; hence ( dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[ & ( for th being real number st th in [.(- (PI / 2)),0.[ holds (cosec | [.(- (PI / 2)),0.[) . th = cosec . th ) ) by FUNCT_1:47; ::_thesis: verum end; Lm36: ( dom (cosec | ].0,(PI / 2).]) = ].0,(PI / 2).] & ( for th being real number st th in ].0,(PI / 2).] holds (cosec | ].0,(PI / 2).]) . th = cosec . th ) ) proof dom (cosec | ].0,(PI / 2).]) = (dom cosec) /\ ].0,(PI / 2).] by RELAT_1:61; then dom (cosec | ].0,(PI / 2).]) = ].0,(PI / 2).] by Th4, XBOOLE_1:28; hence ( dom (cosec | ].0,(PI / 2).]) = ].0,(PI / 2).] & ( for th being real number st th in ].0,(PI / 2).] holds (cosec | ].0,(PI / 2).]) . th = cosec . th ) ) by FUNCT_1:47; ::_thesis: verum end; theorem Th37: :: SINCOS10:37 sec | [.0,(PI / 2).[ is continuous proof for th being real number st th in dom (sec | [.0,(PI / 2).[) holds sec | [.0,(PI / 2).[ is_continuous_in th proof let th be real number ; ::_thesis: ( th in dom (sec | [.0,(PI / 2).[) implies sec | [.0,(PI / 2).[ is_continuous_in th ) A1: cos is_differentiable_in th by SIN_COS:63; assume A2: th in dom (sec | [.0,(PI / 2).[) ; ::_thesis: sec | [.0,(PI / 2).[ is_continuous_in th then th in [.0,(PI / 2).[ by RELAT_1:57; then cos . th <> 0 by Lm1, COMPTRIG:11; then A3: sec is_continuous_in th by A1, FCONT_1:10, FDIFF_1:24; now__::_thesis:_for_rseq_being_Real_Sequence_st_rng_rseq_c=_dom_(sec_|_[.0,(PI_/_2).[)_&_rseq_is_convergent_&_lim_rseq_=_th_holds_ (_(sec_|_[.0,(PI_/_2).[)_/*_rseq_is_convergent_&_(sec_|_[.0,(PI_/_2).[)_._th_=_lim_((sec_|_[.0,(PI_/_2).[)_/*_rseq)_) let rseq be Real_Sequence; ::_thesis: ( rng rseq c= dom (sec | [.0,(PI / 2).[) & rseq is convergent & lim rseq = th implies ( (sec | [.0,(PI / 2).[) /* rseq is convergent & (sec | [.0,(PI / 2).[) . th = lim ((sec | [.0,(PI / 2).[) /* rseq) ) ) assume that A4: rng rseq c= dom (sec | [.0,(PI / 2).[) and A5: ( rseq is convergent & lim rseq = th ) ; ::_thesis: ( (sec | [.0,(PI / 2).[) /* rseq is convergent & (sec | [.0,(PI / 2).[) . th = lim ((sec | [.0,(PI / 2).[) /* rseq) ) A6: dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ by Th1, RELAT_1:62; now__::_thesis:_for_n_being_Element_of_NAT_holds_((sec_|_[.0,(PI_/_2).[)_/*_rseq)_._n_=_(sec_/*_rseq)_._n let n be Element of NAT ; ::_thesis: ((sec | [.0,(PI / 2).[) /* rseq) . n = (sec /* rseq) . n dom rseq = NAT by SEQ_1:1; then rseq . n in rng rseq by FUNCT_1:def_3; then A7: (sec | [.0,(PI / 2).[) . (rseq . n) = sec . (rseq . n) by A4, A6, FUNCT_1:49; (sec | [.0,(PI / 2).[) . (rseq . n) = ((sec | [.0,(PI / 2).[) /* rseq) . n by A4, FUNCT_2:108; hence ((sec | [.0,(PI / 2).[) /* rseq) . n = (sec /* rseq) . n by A4, A6, A7, Th1, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; then A8: (sec | [.0,(PI / 2).[) /* rseq = sec /* rseq by FUNCT_2:63; A9: rng rseq c= dom sec by A4, A6, Th1, XBOOLE_1:1; then sec . th = lim (sec /* rseq) by A3, A5, FCONT_1:def_1; hence ( (sec | [.0,(PI / 2).[) /* rseq is convergent & (sec | [.0,(PI / 2).[) . th = lim ((sec | [.0,(PI / 2).[) /* rseq) ) by A2, A3, A5, A9, A8, Lm33, FCONT_1:def_1; ::_thesis: verum end; hence sec | [.0,(PI / 2).[ is_continuous_in th by FCONT_1:def_1; ::_thesis: verum end; hence sec | [.0,(PI / 2).[ is continuous by FCONT_1:def_2; ::_thesis: verum end; theorem Th38: :: SINCOS10:38 sec | ].(PI / 2),PI.] is continuous proof for th being real number st th in dom (sec | ].(PI / 2),PI.]) holds sec | ].(PI / 2),PI.] is_continuous_in th proof let th be real number ; ::_thesis: ( th in dom (sec | ].(PI / 2),PI.]) implies sec | ].(PI / 2),PI.] is_continuous_in th ) A1: cos is_differentiable_in th by SIN_COS:63; assume A2: th in dom (sec | ].(PI / 2),PI.]) ; ::_thesis: sec | ].(PI / 2),PI.] is_continuous_in th then th in ].(PI / 2),PI.] by RELAT_1:57; then cos . th <> 0 by Lm2, COMPTRIG:13; then A3: sec is_continuous_in th by A1, FCONT_1:10, FDIFF_1:24; now__::_thesis:_for_rseq_being_Real_Sequence_st_rng_rseq_c=_dom_(sec_|_].(PI_/_2),PI.])_&_rseq_is_convergent_&_lim_rseq_=_th_holds_ (_(sec_|_].(PI_/_2),PI.])_/*_rseq_is_convergent_&_(sec_|_].(PI_/_2),PI.])_._th_=_lim_((sec_|_].(PI_/_2),PI.])_/*_rseq)_) let rseq be Real_Sequence; ::_thesis: ( rng rseq c= dom (sec | ].(PI / 2),PI.]) & rseq is convergent & lim rseq = th implies ( (sec | ].(PI / 2),PI.]) /* rseq is convergent & (sec | ].(PI / 2),PI.]) . th = lim ((sec | ].(PI / 2),PI.]) /* rseq) ) ) assume that A4: rng rseq c= dom (sec | ].(PI / 2),PI.]) and A5: ( rseq is convergent & lim rseq = th ) ; ::_thesis: ( (sec | ].(PI / 2),PI.]) /* rseq is convergent & (sec | ].(PI / 2),PI.]) . th = lim ((sec | ].(PI / 2),PI.]) /* rseq) ) A6: dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] by Th2, RELAT_1:62; now__::_thesis:_for_n_being_Element_of_NAT_holds_((sec_|_].(PI_/_2),PI.])_/*_rseq)_._n_=_(sec_/*_rseq)_._n let n be Element of NAT ; ::_thesis: ((sec | ].(PI / 2),PI.]) /* rseq) . n = (sec /* rseq) . n dom rseq = NAT by SEQ_1:1; then rseq . n in rng rseq by FUNCT_1:def_3; then A7: (sec | ].(PI / 2),PI.]) . (rseq . n) = sec . (rseq . n) by A4, A6, FUNCT_1:49; (sec | ].(PI / 2),PI.]) . (rseq . n) = ((sec | ].(PI / 2),PI.]) /* rseq) . n by A4, FUNCT_2:108; hence ((sec | ].(PI / 2),PI.]) /* rseq) . n = (sec /* rseq) . n by A4, A6, A7, Th2, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; then A8: (sec | ].(PI / 2),PI.]) /* rseq = sec /* rseq by FUNCT_2:63; A9: rng rseq c= dom sec by A4, A6, Th2, XBOOLE_1:1; then sec . th = lim (sec /* rseq) by A3, A5, FCONT_1:def_1; hence ( (sec | ].(PI / 2),PI.]) /* rseq is convergent & (sec | ].(PI / 2),PI.]) . th = lim ((sec | ].(PI / 2),PI.]) /* rseq) ) by A2, A3, A5, A9, A8, Lm34, FCONT_1:def_1; ::_thesis: verum end; hence sec | ].(PI / 2),PI.] is_continuous_in th by FCONT_1:def_1; ::_thesis: verum end; hence sec | ].(PI / 2),PI.] is continuous by FCONT_1:def_2; ::_thesis: verum end; theorem Th39: :: SINCOS10:39 cosec | [.(- (PI / 2)),0.[ is continuous proof for th being real number st th in dom (cosec | [.(- (PI / 2)),0.[) holds cosec | [.(- (PI / 2)),0.[ is_continuous_in th proof let th be real number ; ::_thesis: ( th in dom (cosec | [.(- (PI / 2)),0.[) implies cosec | [.(- (PI / 2)),0.[ is_continuous_in th ) assume A1: th in dom (cosec | [.(- (PI / 2)),0.[) ; ::_thesis: cosec | [.(- (PI / 2)),0.[ is_continuous_in th then A2: th in [.(- (PI / 2)),0.[ by RELAT_1:57; then th < 0 by Lm3, XXREAL_1:4; then A3: th + (2 * PI) < 0 + (2 * PI) by XREAL_1:8; - PI < th by A2, Lm3, XXREAL_1:4; then (- PI) + (2 * PI) < th + (2 * PI) by XREAL_1:8; then th + (2 * PI) in ].PI,(2 * PI).[ by A3; then sin . (th + (2 * PI)) <> 0 by COMPTRIG:9; then A4: sin . th <> 0 by SIN_COS:78; sin is_differentiable_in th by SIN_COS:64; then A5: cosec is_continuous_in th by A4, FCONT_1:10, FDIFF_1:24; now__::_thesis:_for_rseq_being_Real_Sequence_st_rng_rseq_c=_dom_(cosec_|_[.(-_(PI_/_2)),0.[)_&_rseq_is_convergent_&_lim_rseq_=_th_holds_ (_(cosec_|_[.(-_(PI_/_2)),0.[)_/*_rseq_is_convergent_&_(cosec_|_[.(-_(PI_/_2)),0.[)_._th_=_lim_((cosec_|_[.(-_(PI_/_2)),0.[)_/*_rseq)_) let rseq be Real_Sequence; ::_thesis: ( rng rseq c= dom (cosec | [.(- (PI / 2)),0.[) & rseq is convergent & lim rseq = th implies ( (cosec | [.(- (PI / 2)),0.[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0.[) . th = lim ((cosec | [.(- (PI / 2)),0.[) /* rseq) ) ) assume that A6: rng rseq c= dom (cosec | [.(- (PI / 2)),0.[) and A7: ( rseq is convergent & lim rseq = th ) ; ::_thesis: ( (cosec | [.(- (PI / 2)),0.[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0.[) . th = lim ((cosec | [.(- (PI / 2)),0.[) /* rseq) ) A8: dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[ by Th3, RELAT_1:62; now__::_thesis:_for_n_being_Element_of_NAT_holds_((cosec_|_[.(-_(PI_/_2)),0.[)_/*_rseq)_._n_=_(cosec_/*_rseq)_._n let n be Element of NAT ; ::_thesis: ((cosec | [.(- (PI / 2)),0.[) /* rseq) . n = (cosec /* rseq) . n dom rseq = NAT by SEQ_1:1; then rseq . n in rng rseq by FUNCT_1:def_3; then A9: (cosec | [.(- (PI / 2)),0.[) . (rseq . n) = cosec . (rseq . n) by A6, A8, FUNCT_1:49; (cosec | [.(- (PI / 2)),0.[) . (rseq . n) = ((cosec | [.(- (PI / 2)),0.[) /* rseq) . n by A6, FUNCT_2:108; hence ((cosec | [.(- (PI / 2)),0.[) /* rseq) . n = (cosec /* rseq) . n by A6, A8, A9, Th3, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; then A10: (cosec | [.(- (PI / 2)),0.[) /* rseq = cosec /* rseq by FUNCT_2:63; A11: rng rseq c= dom cosec by A6, A8, Th3, XBOOLE_1:1; then cosec . th = lim (cosec /* rseq) by A5, A7, FCONT_1:def_1; hence ( (cosec | [.(- (PI / 2)),0.[) /* rseq is convergent & (cosec | [.(- (PI / 2)),0.[) . th = lim ((cosec | [.(- (PI / 2)),0.[) /* rseq) ) by A1, A5, A7, A11, A10, Lm35, FCONT_1:def_1; ::_thesis: verum end; hence cosec | [.(- (PI / 2)),0.[ is_continuous_in th by FCONT_1:def_1; ::_thesis: verum end; hence cosec | [.(- (PI / 2)),0.[ is continuous by FCONT_1:def_2; ::_thesis: verum end; theorem Th40: :: SINCOS10:40 cosec | ].0,(PI / 2).] is continuous proof for th being real number st th in dom (cosec | ].0,(PI / 2).]) holds cosec | ].0,(PI / 2).] is_continuous_in th proof let th be real number ; ::_thesis: ( th in dom (cosec | ].0,(PI / 2).]) implies cosec | ].0,(PI / 2).] is_continuous_in th ) A1: sin is_differentiable_in th by SIN_COS:64; assume A2: th in dom (cosec | ].0,(PI / 2).]) ; ::_thesis: cosec | ].0,(PI / 2).] is_continuous_in th then th in ].0,(PI / 2).] by RELAT_1:57; then sin . th <> 0 by Lm4, COMPTRIG:7; then A3: cosec is_continuous_in th by A1, FCONT_1:10, FDIFF_1:24; now__::_thesis:_for_rseq_being_Real_Sequence_st_rng_rseq_c=_dom_(cosec_|_].0,(PI_/_2).])_&_rseq_is_convergent_&_lim_rseq_=_th_holds_ (_(cosec_|_].0,(PI_/_2).])_/*_rseq_is_convergent_&_(cosec_|_].0,(PI_/_2).])_._th_=_lim_((cosec_|_].0,(PI_/_2).])_/*_rseq)_) let rseq be Real_Sequence; ::_thesis: ( rng rseq c= dom (cosec | ].0,(PI / 2).]) & rseq is convergent & lim rseq = th implies ( (cosec | ].0,(PI / 2).]) /* rseq is convergent & (cosec | ].0,(PI / 2).]) . th = lim ((cosec | ].0,(PI / 2).]) /* rseq) ) ) assume that A4: rng rseq c= dom (cosec | ].0,(PI / 2).]) and A5: ( rseq is convergent & lim rseq = th ) ; ::_thesis: ( (cosec | ].0,(PI / 2).]) /* rseq is convergent & (cosec | ].0,(PI / 2).]) . th = lim ((cosec | ].0,(PI / 2).]) /* rseq) ) A6: dom (cosec | ].0,(PI / 2).]) = ].0,(PI / 2).] by Th4, RELAT_1:62; now__::_thesis:_for_n_being_Element_of_NAT_holds_((cosec_|_].0,(PI_/_2).])_/*_rseq)_._n_=_(cosec_/*_rseq)_._n let n be Element of NAT ; ::_thesis: ((cosec | ].0,(PI / 2).]) /* rseq) . n = (cosec /* rseq) . n dom rseq = NAT by SEQ_1:1; then rseq . n in rng rseq by FUNCT_1:def_3; then A7: (cosec | ].0,(PI / 2).]) . (rseq . n) = cosec . (rseq . n) by A4, A6, FUNCT_1:49; (cosec | ].0,(PI / 2).]) . (rseq . n) = ((cosec | ].0,(PI / 2).]) /* rseq) . n by A4, FUNCT_2:108; hence ((cosec | ].0,(PI / 2).]) /* rseq) . n = (cosec /* rseq) . n by A4, A6, A7, Th4, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; then A8: (cosec | ].0,(PI / 2).]) /* rseq = cosec /* rseq by FUNCT_2:63; A9: rng rseq c= dom cosec by A4, A6, Th4, XBOOLE_1:1; then cosec . th = lim (cosec /* rseq) by A3, A5, FCONT_1:def_1; hence ( (cosec | ].0,(PI / 2).]) /* rseq is convergent & (cosec | ].0,(PI / 2).]) . th = lim ((cosec | ].0,(PI / 2).]) /* rseq) ) by A2, A3, A5, A9, A8, Lm36, FCONT_1:def_1; ::_thesis: verum end; hence cosec | ].0,(PI / 2).] is_continuous_in th by FCONT_1:def_1; ::_thesis: verum end; hence cosec | ].0,(PI / 2).] is continuous by FCONT_1:def_2; ::_thesis: verum end; theorem Th41: :: SINCOS10:41 rng (sec | [.0,(PI / 4).]) = [.1,(sqrt 2).] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.1,(sqrt_2).]_implies_ex_x_being_set_st_ (_x_in_dom_(sec_|_[.0,(PI_/_4).])_&_y_=_(sec_|_[.0,(PI_/_4).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(sec_|_[.0,(PI_/_4).])_&_y_=_(sec_|_[.0,(PI_/_4).])_._x_)_implies_y_in_[.1,(sqrt_2).]_)_) let y be set ; ::_thesis: ( ( y in [.1,(sqrt 2).] implies ex x being set st ( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) ) & ( ex x being set st ( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) implies y in [.1,(sqrt 2).] ) ) thus ( y in [.1,(sqrt 2).] implies ex x being set st ( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) implies y in [.1,(sqrt 2).] ) proof assume A1: y in [.1,(sqrt 2).] ; ::_thesis: ex x being set st ( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) then reconsider y1 = y as Real ; [.0,(PI / 4).] c= [.0,(PI / 2).[ by Lm5, XXREAL_2:def_12; then A2: sec | [.0,(PI / 4).] is continuous by Th37, FCONT_1:16; y1 in [.(sec . 0),(sec . (PI / 4)).] \/ [.(sec . (PI / 4)),(sec . 0).] by A1, Th31, XBOOLE_0:def_3; then consider x being Real such that A3: ( x in [.0,(PI / 4).] & y1 = sec . x ) by A2, Lm13, Th1, FCONT_2:15, XBOOLE_1:1; take x ; ::_thesis: ( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) thus ( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) by A3, Lm29, FUNCT_1:49; ::_thesis: verum end; thus ( ex x being set st ( x in dom (sec | [.0,(PI / 4).]) & y = (sec | [.0,(PI / 4).]) . x ) implies y in [.1,(sqrt 2).] ) ::_thesis: verum proof given x being set such that A4: x in dom (sec | [.0,(PI / 4).]) and A5: y = (sec | [.0,(PI / 4).]) . x ; ::_thesis: y in [.1,(sqrt 2).] reconsider x1 = x as Real by A4; y = sec . x1 by A4, A5, Lm29, FUNCT_1:49; hence y in [.1,(sqrt 2).] by A4, Lm29, Th33; ::_thesis: verum end; end; hence rng (sec | [.0,(PI / 4).]) = [.1,(sqrt 2).] by FUNCT_1:def_3; ::_thesis: verum end; theorem Th42: :: SINCOS10:42 rng (sec | [.((3 / 4) * PI),PI.]) = [.(- (sqrt 2)),(- 1).] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(-_(sqrt_2)),(-_1).]_implies_ex_x_being_set_st_ (_x_in_dom_(sec_|_[.((3_/_4)_*_PI),PI.])_&_y_=_(sec_|_[.((3_/_4)_*_PI),PI.])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(sec_|_[.((3_/_4)_*_PI),PI.])_&_y_=_(sec_|_[.((3_/_4)_*_PI),PI.])_._x_)_implies_y_in_[.(-_(sqrt_2)),(-_1).]_)_) let y be set ; ::_thesis: ( ( y in [.(- (sqrt 2)),(- 1).] implies ex x being set st ( x in dom (sec | [.((3 / 4) * PI),PI.]) & y = (sec | [.((3 / 4) * PI),PI.]) . x ) ) & ( ex x being set st ( x in dom (sec | [.((3 / 4) * PI),PI.]) & y = (sec | [.((3 / 4) * PI),PI.]) . x ) implies y in [.(- (sqrt 2)),(- 1).] ) ) thus ( y in [.(- (sqrt 2)),(- 1).] implies ex x being set st ( x in dom (sec | [.((3 / 4) * PI),PI.]) & y = (sec | [.((3 / 4) * PI),PI.]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (sec | [.((3 / 4) * PI),PI.]) & y = (sec | [.((3 / 4) * PI),PI.]) . x ) implies y in [.(- (sqrt 2)),(- 1).] ) proof [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def_12; then A1: sec | [.((3 / 4) * PI),PI.] is continuous by Th38, FCONT_1:16; assume A2: y in [.(- (sqrt 2)),(- 1).] ; ::_thesis: ex x being set st ( x in dom (sec | [.((3 / 4) * PI),PI.]) & y = (sec | [.((3 / 4) * PI),PI.]) . x ) then reconsider y1 = y as Real ; A3: (3 / 4) * PI <= PI by Lm6, XXREAL_1:2; y1 in [.(sec . ((3 / 4) * PI)),(sec . PI).] \/ [.(sec . PI),(sec . ((3 / 4) * PI)).] by A2, Th31, XBOOLE_0:def_3; then consider x being Real such that A4: ( x in [.((3 / 4) * PI),PI.] & y1 = sec . x ) by A3, A1, Lm14, Th2, FCONT_2:15, XBOOLE_1:1; take x ; ::_thesis: ( x in dom (sec | [.((3 / 4) * PI),PI.]) & y = (sec | [.((3 / 4) * PI),PI.]) . x ) thus ( x in dom (sec | [.((3 / 4) * PI),PI.]) & y = (sec | [.((3 / 4) * PI),PI.]) . x ) by A4, Lm30, FUNCT_1:49; ::_thesis: verum end; thus ( ex x being set st ( x in dom (sec | [.((3 / 4) * PI),PI.]) & y = (sec | [.((3 / 4) * PI),PI.]) . x ) implies y in [.(- (sqrt 2)),(- 1).] ) ::_thesis: verum proof given x being set such that A5: x in dom (sec | [.((3 / 4) * PI),PI.]) and A6: y = (sec | [.((3 / 4) * PI),PI.]) . x ; ::_thesis: y in [.(- (sqrt 2)),(- 1).] reconsider x1 = x as Real by A5; y = sec . x1 by A5, A6, Lm30, FUNCT_1:49; hence y in [.(- (sqrt 2)),(- 1).] by A5, Lm30, Th34; ::_thesis: verum end; end; hence rng (sec | [.((3 / 4) * PI),PI.]) = [.(- (sqrt 2)),(- 1).] by FUNCT_1:def_3; ::_thesis: verum end; theorem Th43: :: SINCOS10:43 rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (sqrt 2)),(- 1).] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(-_(sqrt_2)),(-_1).]_implies_ex_x_being_set_st_ (_x_in_dom_(cosec_|_[.(-_(PI_/_2)),(-_(PI_/_4)).])_&_y_=_(cosec_|_[.(-_(PI_/_2)),(-_(PI_/_4)).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(cosec_|_[.(-_(PI_/_2)),(-_(PI_/_4)).])_&_y_=_(cosec_|_[.(-_(PI_/_2)),(-_(PI_/_4)).])_._x_)_implies_y_in_[.(-_(sqrt_2)),(-_1).]_)_) let y be set ; ::_thesis: ( ( y in [.(- (sqrt 2)),(- 1).] implies ex x being set st ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) ) & ( ex x being set st ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) implies y in [.(- (sqrt 2)),(- 1).] ) ) thus ( y in [.(- (sqrt 2)),(- 1).] implies ex x being set st ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) implies y in [.(- (sqrt 2)),(- 1).] ) proof [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def_12; then A1: cosec | [.(- (PI / 2)),(- (PI / 4)).] is continuous by Th39, FCONT_1:16; assume A2: y in [.(- (sqrt 2)),(- 1).] ; ::_thesis: ex x being set st ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) then reconsider y1 = y as Real ; A3: - (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3; y1 in [.(cosec . (- (PI / 4))),(cosec . (- (PI / 2))).] \/ [.(cosec . (- (PI / 2))),(cosec . (- (PI / 4))).] by A2, Th32, XBOOLE_0:def_3; then consider x being Real such that A4: ( x in [.(- (PI / 2)),(- (PI / 4)).] & y1 = cosec . x ) by A3, A1, Lm19, Th3, FCONT_2:15, XBOOLE_1:1; take x ; ::_thesis: ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) thus ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) by A4, Lm31, FUNCT_1:49; ::_thesis: verum end; thus ( ex x being set st ( x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) & y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ) implies y in [.(- (sqrt 2)),(- 1).] ) ::_thesis: verum proof given x being set such that A5: x in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) and A6: y = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . x ; ::_thesis: y in [.(- (sqrt 2)),(- 1).] reconsider x1 = x as Real by A5; y = cosec . x1 by A5, A6, Lm31, FUNCT_1:49; hence y in [.(- (sqrt 2)),(- 1).] by A5, Lm31, Th35; ::_thesis: verum end; end; hence rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (sqrt 2)),(- 1).] by FUNCT_1:def_3; ::_thesis: verum end; theorem Th44: :: SINCOS10:44 rng (cosec | [.(PI / 4),(PI / 2).]) = [.1,(sqrt 2).] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.1,(sqrt_2).]_implies_ex_x_being_set_st_ (_x_in_dom_(cosec_|_[.(PI_/_4),(PI_/_2).])_&_y_=_(cosec_|_[.(PI_/_4),(PI_/_2).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(cosec_|_[.(PI_/_4),(PI_/_2).])_&_y_=_(cosec_|_[.(PI_/_4),(PI_/_2).])_._x_)_implies_y_in_[.1,(sqrt_2).]_)_) let y be set ; ::_thesis: ( ( y in [.1,(sqrt 2).] implies ex x being set st ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) ) & ( ex x being set st ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) implies y in [.1,(sqrt 2).] ) ) thus ( y in [.1,(sqrt 2).] implies ex x being set st ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) implies y in [.1,(sqrt 2).] ) proof [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def_12; then A1: cosec | [.(PI / 4),(PI / 2).] is continuous by Th40, FCONT_1:16; assume A2: y in [.1,(sqrt 2).] ; ::_thesis: ex x being set st ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) then reconsider y1 = y as Real ; A3: PI / 4 <= PI / 2 by Lm8, XXREAL_1:2; y1 in [.(cosec . (PI / 2)),(cosec . (PI / 4)).] \/ [.(cosec . (PI / 4)),(cosec . (PI / 2)).] by A2, Th32, XBOOLE_0:def_3; then consider x being Real such that A4: ( x in [.(PI / 4),(PI / 2).] & y1 = cosec . x ) by A3, A1, Lm20, Th4, FCONT_2:15, XBOOLE_1:1; take x ; ::_thesis: ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) thus ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) by A4, Lm32, FUNCT_1:49; ::_thesis: verum end; thus ( ex x being set st ( x in dom (cosec | [.(PI / 4),(PI / 2).]) & y = (cosec | [.(PI / 4),(PI / 2).]) . x ) implies y in [.1,(sqrt 2).] ) ::_thesis: verum proof given x being set such that A5: x in dom (cosec | [.(PI / 4),(PI / 2).]) and A6: y = (cosec | [.(PI / 4),(PI / 2).]) . x ; ::_thesis: y in [.1,(sqrt 2).] reconsider x1 = x as Real by A5; y = cosec . x1 by A5, A6, Lm32, FUNCT_1:49; hence y in [.1,(sqrt 2).] by A5, Lm32, Th36; ::_thesis: verum end; end; hence rng (cosec | [.(PI / 4),(PI / 2).]) = [.1,(sqrt 2).] by FUNCT_1:def_3; ::_thesis: verum end; theorem Th45: :: SINCOS10:45 [.1,(sqrt 2).] c= dom arcsec1 proof A1: [.0,(PI / 4).] c= [.0,(PI / 2).[ by Lm5, XXREAL_2:def_12; rng (sec | [.0,(PI / 4).]) c= rng (sec | [.0,(PI / 2).[) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (sec | [.0,(PI / 4).]) or y in rng (sec | [.0,(PI / 2).[) ) assume y in rng (sec | [.0,(PI / 4).]) ; ::_thesis: y in rng (sec | [.0,(PI / 2).[) then y in sec .: [.0,(PI / 4).] by RELAT_1:115; then ex x being set st ( x in dom sec & x in [.0,(PI / 4).] & y = sec . x ) by FUNCT_1:def_6; then y in sec .: [.0,(PI / 2).[ by A1, FUNCT_1:def_6; hence y in rng (sec | [.0,(PI / 2).[) by RELAT_1:115; ::_thesis: verum end; hence [.1,(sqrt 2).] c= dom arcsec1 by Th41, FUNCT_1:33; ::_thesis: verum end; theorem Th46: :: SINCOS10:46 [.(- (sqrt 2)),(- 1).] c= dom arcsec2 proof A1: [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def_12; rng (sec | [.((3 / 4) * PI),PI.]) c= rng (sec | ].(PI / 2),PI.]) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (sec | [.((3 / 4) * PI),PI.]) or y in rng (sec | ].(PI / 2),PI.]) ) assume y in rng (sec | [.((3 / 4) * PI),PI.]) ; ::_thesis: y in rng (sec | ].(PI / 2),PI.]) then y in sec .: [.((3 / 4) * PI),PI.] by RELAT_1:115; then ex x being set st ( x in dom sec & x in [.((3 / 4) * PI),PI.] & y = sec . x ) by FUNCT_1:def_6; then y in sec .: ].(PI / 2),PI.] by A1, FUNCT_1:def_6; hence y in rng (sec | ].(PI / 2),PI.]) by RELAT_1:115; ::_thesis: verum end; hence [.(- (sqrt 2)),(- 1).] c= dom arcsec2 by Th42, FUNCT_1:33; ::_thesis: verum end; theorem Th47: :: SINCOS10:47 [.(- (sqrt 2)),(- 1).] c= dom arccosec1 proof A1: [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def_12; rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) c= rng (cosec | [.(- (PI / 2)),0.[) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) or y in rng (cosec | [.(- (PI / 2)),0.[) ) assume y in rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) ; ::_thesis: y in rng (cosec | [.(- (PI / 2)),0.[) then y in cosec .: [.(- (PI / 2)),(- (PI / 4)).] by RELAT_1:115; then ex x being set st ( x in dom cosec & x in [.(- (PI / 2)),(- (PI / 4)).] & y = cosec . x ) by FUNCT_1:def_6; then y in cosec .: [.(- (PI / 2)),0.[ by A1, FUNCT_1:def_6; hence y in rng (cosec | [.(- (PI / 2)),0.[) by RELAT_1:115; ::_thesis: verum end; hence [.(- (sqrt 2)),(- 1).] c= dom arccosec1 by Th43, FUNCT_1:33; ::_thesis: verum end; theorem Th48: :: SINCOS10:48 [.1,(sqrt 2).] c= dom arccosec2 proof A1: [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def_12; rng (cosec | [.(PI / 4),(PI / 2).]) c= rng (cosec | ].0,(PI / 2).]) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (cosec | [.(PI / 4),(PI / 2).]) or y in rng (cosec | ].0,(PI / 2).]) ) assume y in rng (cosec | [.(PI / 4),(PI / 2).]) ; ::_thesis: y in rng (cosec | ].0,(PI / 2).]) then y in cosec .: [.(PI / 4),(PI / 2).] by RELAT_1:115; then ex x being set st ( x in dom cosec & x in [.(PI / 4),(PI / 2).] & y = cosec . x ) by FUNCT_1:def_6; then y in cosec .: ].0,(PI / 2).] by A1, FUNCT_1:def_6; hence y in rng (cosec | ].0,(PI / 2).]) by RELAT_1:115; ::_thesis: verum end; hence [.1,(sqrt 2).] c= dom arccosec2 by Th44, FUNCT_1:33; ::_thesis: verum end; Lm37: (sec | [.0,(PI / 4).]) | [.0,(PI / 4).] is increasing proof [.0,(PI / 4).] c= [.0,(PI / 2).[ by Lm5, XXREAL_2:def_12; then sec | [.0,(PI / 4).] is increasing by Th17, RFUNCT_2:28; hence (sec | [.0,(PI / 4).]) | [.0,(PI / 4).] is increasing ; ::_thesis: verum end; Lm38: (sec | [.((3 / 4) * PI),PI.]) | [.((3 / 4) * PI),PI.] is increasing proof [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def_12; then sec | [.((3 / 4) * PI),PI.] is increasing by Th18, RFUNCT_2:28; hence (sec | [.((3 / 4) * PI),PI.]) | [.((3 / 4) * PI),PI.] is increasing ; ::_thesis: verum end; Lm39: (cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).] is decreasing proof [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def_12; then cosec | [.(- (PI / 2)),(- (PI / 4)).] is decreasing by Th19, RFUNCT_2:29; hence (cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).] is decreasing ; ::_thesis: verum end; Lm40: (cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] is decreasing proof [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def_12; then cosec | [.(PI / 4),(PI / 2).] is decreasing by Th20, RFUNCT_2:29; hence (cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] is decreasing ; ::_thesis: verum end; Lm41: sec | [.0,(PI / 4).] is one-to-one proof [.0,(PI / 4).] c= [.0,(PI / 2).[ by Lm5, XXREAL_2:def_12; then (sec | [.0,(PI / 2).[) | [.0,(PI / 4).] = sec | [.0,(PI / 4).] by RELAT_1:74; hence sec | [.0,(PI / 4).] is one-to-one ; ::_thesis: verum end; Lm42: sec | [.((3 / 4) * PI),PI.] is one-to-one proof [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def_12; then (sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.] = sec | [.((3 / 4) * PI),PI.] by RELAT_1:74; hence sec | [.((3 / 4) * PI),PI.] is one-to-one ; ::_thesis: verum end; Lm43: cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one proof [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def_12; then (cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).] = cosec | [.(- (PI / 2)),(- (PI / 4)).] by RELAT_1:74; hence cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one ; ::_thesis: verum end; Lm44: cosec | [.(PI / 4),(PI / 2).] is one-to-one proof [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def_12; then (cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).] = cosec | [.(PI / 4),(PI / 2).] by RELAT_1:74; hence cosec | [.(PI / 4),(PI / 2).] is one-to-one ; ::_thesis: verum end; registration clusterK77(sec,[.0,(PI / 4).]) -> one-to-one ; coherence sec | [.0,(PI / 4).] is one-to-one by Lm41; clusterK77(sec,[.((3 / 4) * PI),PI.]) -> one-to-one ; coherence sec | [.((3 / 4) * PI),PI.] is one-to-one by Lm42; clusterK77(cosec,[.(- (PI / 2)),(- (PI / 4)).]) -> one-to-one ; coherence cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one by Lm43; clusterK77(cosec,[.(PI / 4),(PI / 2).]) -> one-to-one ; coherence cosec | [.(PI / 4),(PI / 2).] is one-to-one by Lm44; end; theorem Th49: :: SINCOS10:49 arcsec1 | [.1,(sqrt 2).] = (sec | [.0,(PI / 4).]) " proof set h = sec | [.0,(PI / 2).[; A1: [.0,(PI / 4).] c= [.0,(PI / 2).[ by Lm5, XXREAL_2:def_12; then (sec | [.0,(PI / 4).]) " = ((sec | [.0,(PI / 2).[) | [.0,(PI / 4).]) " by RELAT_1:74 .= ((sec | [.0,(PI / 2).[) ") | ((sec | [.0,(PI / 2).[) .: [.0,(PI / 4).]) by RFUNCT_2:17 .= ((sec | [.0,(PI / 2).[) ") | (rng ((sec | [.0,(PI / 2).[) | [.0,(PI / 4).])) by RELAT_1:115 .= ((sec | [.0,(PI / 2).[) ") | [.1,(sqrt 2).] by A1, Th41, RELAT_1:74 ; hence arcsec1 | [.1,(sqrt 2).] = (sec | [.0,(PI / 4).]) " ; ::_thesis: verum end; theorem Th50: :: SINCOS10:50 arcsec2 | [.(- (sqrt 2)),(- 1).] = (sec | [.((3 / 4) * PI),PI.]) " proof set h = sec | ].(PI / 2),PI.]; A1: [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def_12; then (sec | [.((3 / 4) * PI),PI.]) " = ((sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.]) " by RELAT_1:74 .= ((sec | ].(PI / 2),PI.]) ") | ((sec | ].(PI / 2),PI.]) .: [.((3 / 4) * PI),PI.]) by RFUNCT_2:17 .= ((sec | ].(PI / 2),PI.]) ") | (rng ((sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.])) by RELAT_1:115 .= ((sec | ].(PI / 2),PI.]) ") | [.(- (sqrt 2)),(- 1).] by A1, Th42, RELAT_1:74 ; hence arcsec2 | [.(- (sqrt 2)),(- 1).] = (sec | [.((3 / 4) * PI),PI.]) " ; ::_thesis: verum end; theorem Th51: :: SINCOS10:51 arccosec1 | [.(- (sqrt 2)),(- 1).] = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) " proof set h = cosec | [.(- (PI / 2)),0.[; A1: [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def_12; then (cosec | [.(- (PI / 2)),(- (PI / 4)).]) " = ((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).]) " by RELAT_1:74 .= ((cosec | [.(- (PI / 2)),0.[) ") | ((cosec | [.(- (PI / 2)),0.[) .: [.(- (PI / 2)),(- (PI / 4)).]) by RFUNCT_2:17 .= ((cosec | [.(- (PI / 2)),0.[) ") | (rng ((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).])) by RELAT_1:115 .= ((cosec | [.(- (PI / 2)),0.[) ") | [.(- (sqrt 2)),(- 1).] by A1, Th43, RELAT_1:74 ; hence arccosec1 | [.(- (sqrt 2)),(- 1).] = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) " ; ::_thesis: verum end; theorem Th52: :: SINCOS10:52 arccosec2 | [.1,(sqrt 2).] = (cosec | [.(PI / 4),(PI / 2).]) " proof set h = cosec | ].0,(PI / 2).]; A1: [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def_12; then (cosec | [.(PI / 4),(PI / 2).]) " = ((cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).]) " by RELAT_1:74 .= ((cosec | ].0,(PI / 2).]) ") | ((cosec | ].0,(PI / 2).]) .: [.(PI / 4),(PI / 2).]) by RFUNCT_2:17 .= ((cosec | ].0,(PI / 2).]) ") | (rng ((cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).])) by RELAT_1:115 .= ((cosec | ].0,(PI / 2).]) ") | [.1,(sqrt 2).] by A1, Th44, RELAT_1:74 ; hence arccosec2 | [.1,(sqrt 2).] = (cosec | [.(PI / 4),(PI / 2).]) " ; ::_thesis: verum end; theorem :: SINCOS10:53 (sec | [.0,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th41, Th49, FUNCT_1:39; theorem :: SINCOS10:54 (sec | [.((3 / 4) * PI),PI.]) * (arcsec2 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th42, Th50, FUNCT_1:39; theorem :: SINCOS10:55 (cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (arccosec1 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th43, Th51, FUNCT_1:39; theorem :: SINCOS10:56 (cosec | [.(PI / 4),(PI / 2).]) * (arccosec2 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th44, Th52, FUNCT_1:39; theorem :: SINCOS10:57 (sec | [.0,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th41, Th49, FUNCT_1:39; theorem :: SINCOS10:58 (sec | [.((3 / 4) * PI),PI.]) * (arcsec2 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th42, Th50, FUNCT_1:39; theorem :: SINCOS10:59 (cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (arccosec1 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th43, Th51, FUNCT_1:39; theorem :: SINCOS10:60 (cosec | [.(PI / 4),(PI / 2).]) * (arccosec2 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th44, Th52, FUNCT_1:39; theorem :: SINCOS10:61 arcsec1 * (sec | [.0,(PI / 2).[) = id [.0,(PI / 2).[ by Lm25, Th25, FUNCT_1:39; theorem :: SINCOS10:62 arcsec2 * (sec | ].(PI / 2),PI.]) = id ].(PI / 2),PI.] by Lm26, Th26, FUNCT_1:39; theorem :: SINCOS10:63 arccosec1 * (cosec | [.(- (PI / 2)),0.[) = id [.(- (PI / 2)),0.[ by Lm27, Th27, FUNCT_1:39; theorem :: SINCOS10:64 arccosec2 * (cosec | ].0,(PI / 2).]) = id ].0,(PI / 2).] by Lm28, Th28, FUNCT_1:39; theorem Th65: :: SINCOS10:65 arcsec1 * (sec | [.0,(PI / 2).[) = id [.0,(PI / 2).[ by Lm25, Th25, FUNCT_1:39; theorem Th66: :: SINCOS10:66 arcsec2 * (sec | ].(PI / 2),PI.]) = id ].(PI / 2),PI.] by Lm26, Th26, FUNCT_1:39; theorem Th67: :: SINCOS10:67 arccosec1 * (cosec | [.(- (PI / 2)),0.[) = id [.(- (PI / 2)),0.[ by Lm27, Th27, FUNCT_1:39; theorem Th68: :: SINCOS10:68 arccosec2 * (cosec | ].0,(PI / 2).]) = id ].0,(PI / 2).] by Lm28, Th28, FUNCT_1:39; theorem Th69: :: SINCOS10:69 for r being Real st 0 <= r & r < PI / 2 holds arcsec1 (sec . r) = r proof let r be Real; ::_thesis: ( 0 <= r & r < PI / 2 implies arcsec1 (sec . r) = r ) A1: dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ by Th1, RELAT_1:62; assume ( 0 <= r & r < PI / 2 ) ; ::_thesis: arcsec1 (sec . r) = r then A2: r in [.0,(PI / 2).[ ; then arcsec1 (sec . r) = arcsec1 . ((sec | [.0,(PI / 2).[) . r) by FUNCT_1:49 .= (id [.0,(PI / 2).[) . r by A2, A1, Th65, FUNCT_1:13 .= r by A2, FUNCT_1:18 ; hence arcsec1 (sec . r) = r ; ::_thesis: verum end; theorem Th70: :: SINCOS10:70 for r being Real st PI / 2 < r & r <= PI holds arcsec2 (sec . r) = r proof let r be Real; ::_thesis: ( PI / 2 < r & r <= PI implies arcsec2 (sec . r) = r ) A1: dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] by Th2, RELAT_1:62; assume ( PI / 2 < r & r <= PI ) ; ::_thesis: arcsec2 (sec . r) = r then A2: r in ].(PI / 2),PI.] ; then arcsec2 (sec . r) = arcsec2 . ((sec | ].(PI / 2),PI.]) . r) by FUNCT_1:49 .= (id ].(PI / 2),PI.]) . r by A2, A1, Th66, FUNCT_1:13 .= r by A2, FUNCT_1:18 ; hence arcsec2 (sec . r) = r ; ::_thesis: verum end; theorem Th71: :: SINCOS10:71 for r being Real st - (PI / 2) <= r & r < 0 holds arccosec1 (cosec . r) = r proof let r be Real; ::_thesis: ( - (PI / 2) <= r & r < 0 implies arccosec1 (cosec . r) = r ) A1: dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[ by Th3, RELAT_1:62; assume ( - (PI / 2) <= r & r < 0 ) ; ::_thesis: arccosec1 (cosec . r) = r then A2: r in [.(- (PI / 2)),0.[ ; then arccosec1 (cosec . r) = arccosec1 . ((cosec | [.(- (PI / 2)),0.[) . r) by FUNCT_1:49 .= (id [.(- (PI / 2)),0.[) . r by A2, A1, Th67, FUNCT_1:13 .= r by A2, FUNCT_1:18 ; hence arccosec1 (cosec . r) = r ; ::_thesis: verum end; theorem Th72: :: SINCOS10:72 for r being Real st 0 < r & r <= PI / 2 holds arccosec2 (cosec . r) = r proof let r be Real; ::_thesis: ( 0 < r & r <= PI / 2 implies arccosec2 (cosec . r) = r ) A1: dom (cosec | ].0,(PI / 2).]) = ].0,(PI / 2).] by Th4, RELAT_1:62; assume ( 0 < r & r <= PI / 2 ) ; ::_thesis: arccosec2 (cosec . r) = r then A2: r in ].0,(PI / 2).] ; then arccosec2 (cosec . r) = arccosec2 . ((cosec | ].0,(PI / 2).]) . r) by FUNCT_1:49 .= (id ].0,(PI / 2).]) . r by A2, A1, Th68, FUNCT_1:13 .= r by A2, FUNCT_1:18 ; hence arccosec2 (cosec . r) = r ; ::_thesis: verum end; theorem Th73: :: SINCOS10:73 ( arcsec1 . 1 = 0 & arcsec1 . (sqrt 2) = PI / 4 ) proof A1: arcsec1 . 1 = arcsec1 1 .= 0 by Th31, Th69 ; A2: PI / 4 < PI / 2 by Lm5, XXREAL_1:3; arcsec1 . (sqrt 2) = arcsec1 (sqrt 2) .= PI / 4 by A2, Th31, Th69 ; hence ( arcsec1 . 1 = 0 & arcsec1 . (sqrt 2) = PI / 4 ) by A1; ::_thesis: verum end; theorem Th74: :: SINCOS10:74 ( arcsec2 . (- (sqrt 2)) = (3 / 4) * PI & arcsec2 . (- 1) = PI ) proof A1: PI / 2 < PI by Lm6, XXREAL_1:2; A2: arcsec2 . (- 1) = arcsec2 (- 1) .= PI by A1, Th31, Th70 ; A3: ( PI / 2 < (3 / 4) * PI & (3 / 4) * PI <= PI ) by Lm6, XXREAL_1:2; arcsec2 . (- (sqrt 2)) = arcsec2 (- (sqrt 2)) .= (3 / 4) * PI by A3, Th31, Th70 ; hence ( arcsec2 . (- (sqrt 2)) = (3 / 4) * PI & arcsec2 . (- 1) = PI ) by A2; ::_thesis: verum end; theorem Th75: :: SINCOS10:75 ( arccosec1 . (- 1) = - (PI / 2) & arccosec1 . (- (sqrt 2)) = - (PI / 4) ) proof A1: arccosec1 . (- 1) = arccosec1 (- 1) .= - (PI / 2) by Th32, Th71 ; A2: - (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3; arccosec1 . (- (sqrt 2)) = arccosec1 (- (sqrt 2)) .= - (PI / 4) by A2, Th32, Th71 ; hence ( arccosec1 . (- 1) = - (PI / 2) & arccosec1 . (- (sqrt 2)) = - (PI / 4) ) by A1; ::_thesis: verum end; theorem Th76: :: SINCOS10:76 ( arccosec2 . (sqrt 2) = PI / 4 & arccosec2 . 1 = PI / 2 ) proof A1: arccosec2 . 1 = arccosec2 1 .= PI / 2 by Th32, Th72 ; A2: PI / 4 <= PI / 2 by Lm8, XXREAL_1:2; arccosec2 . (sqrt 2) = arccosec2 (sqrt 2) .= PI / 4 by A2, Th32, Th72 ; hence ( arccosec2 . (sqrt 2) = PI / 4 & arccosec2 . 1 = PI / 2 ) by A1; ::_thesis: verum end; theorem Th77: :: SINCOS10:77 arcsec1 | (sec .: [.0,(PI / 2).[) is increasing proof set f = sec | [.0,(PI / 2).[; A1: (sec | [.0,(PI / 2).[) .: [.0,(PI / 2).[ = rng ((sec | [.0,(PI / 2).[) | [.0,(PI / 2).[) by RELAT_1:115 .= rng (sec | [.0,(PI / 2).[) by RELAT_1:73 .= sec .: [.0,(PI / 2).[ by RELAT_1:115 ; (sec | [.0,(PI / 2).[) | [.0,(PI / 2).[ = sec | [.0,(PI / 2).[ by RELAT_1:73; hence arcsec1 | (sec .: [.0,(PI / 2).[) is increasing by A1, Th17, FCONT_3:9; ::_thesis: verum end; theorem Th78: :: SINCOS10:78 arcsec2 | (sec .: ].(PI / 2),PI.]) is increasing proof set f = sec | ].(PI / 2),PI.]; A1: (sec | ].(PI / 2),PI.]) .: ].(PI / 2),PI.] = rng ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.]) by RELAT_1:115 .= rng (sec | ].(PI / 2),PI.]) by RELAT_1:73 .= sec .: ].(PI / 2),PI.] by RELAT_1:115 ; (sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.] = sec | ].(PI / 2),PI.] by RELAT_1:73; hence arcsec2 | (sec .: ].(PI / 2),PI.]) is increasing by A1, Th18, FCONT_3:9; ::_thesis: verum end; theorem Th79: :: SINCOS10:79 arccosec1 | (cosec .: [.(- (PI / 2)),0.[) is decreasing proof set f = cosec | [.(- (PI / 2)),0.[; A1: (cosec | [.(- (PI / 2)),0.[) .: [.(- (PI / 2)),0.[ = rng ((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),0.[) by RELAT_1:115 .= rng (cosec | [.(- (PI / 2)),0.[) by RELAT_1:73 .= cosec .: [.(- (PI / 2)),0.[ by RELAT_1:115 ; (cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),0.[ = cosec | [.(- (PI / 2)),0.[ by RELAT_1:73; hence arccosec1 | (cosec .: [.(- (PI / 2)),0.[) is decreasing by A1, Th19, FCONT_3:10; ::_thesis: verum end; theorem Th80: :: SINCOS10:80 arccosec2 | (cosec .: ].0,(PI / 2).]) is decreasing proof set f = cosec | ].0,(PI / 2).]; A1: (cosec | ].0,(PI / 2).]) .: ].0,(PI / 2).] = rng ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).]) by RELAT_1:115 .= rng (cosec | ].0,(PI / 2).]) by RELAT_1:73 .= cosec .: ].0,(PI / 2).] by RELAT_1:115 ; (cosec | ].0,(PI / 2).]) | ].0,(PI / 2).] = cosec | ].0,(PI / 2).] by RELAT_1:73; hence arccosec2 | (cosec .: ].0,(PI / 2).]) is decreasing by A1, Th20, FCONT_3:10; ::_thesis: verum end; theorem Th81: :: SINCOS10:81 arcsec1 | [.1,(sqrt 2).] is increasing proof ( [.1,(sqrt 2).] = sec .: [.0,(PI / 4).] & [.0,(PI / 4).] c= [.0,(PI / 2).[ ) by Lm5, Th41, RELAT_1:115, XXREAL_2:def_12; hence arcsec1 | [.1,(sqrt 2).] is increasing by Th77, RELAT_1:123, RFUNCT_2:28; ::_thesis: verum end; theorem Th82: :: SINCOS10:82 arcsec2 | [.(- (sqrt 2)),(- 1).] is increasing proof ( [.(- (sqrt 2)),(- 1).] = sec .: [.((3 / 4) * PI),PI.] & [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] ) by Lm6, Th42, RELAT_1:115, XXREAL_2:def_12; hence arcsec2 | [.(- (sqrt 2)),(- 1).] is increasing by Th78, RELAT_1:123, RFUNCT_2:28; ::_thesis: verum end; theorem Th83: :: SINCOS10:83 arccosec1 | [.(- (sqrt 2)),(- 1).] is decreasing proof ( [.(- (sqrt 2)),(- 1).] = cosec .: [.(- (PI / 2)),(- (PI / 4)).] & [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ ) by Lm7, Th43, RELAT_1:115, XXREAL_2:def_12; hence arccosec1 | [.(- (sqrt 2)),(- 1).] is decreasing by Th79, RELAT_1:123, RFUNCT_2:29; ::_thesis: verum end; theorem Th84: :: SINCOS10:84 arccosec2 | [.1,(sqrt 2).] is decreasing proof ( [.1,(sqrt 2).] = cosec .: [.(PI / 4),(PI / 2).] & [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] ) by Lm8, Th44, RELAT_1:115, XXREAL_2:def_12; hence arccosec2 | [.1,(sqrt 2).] is decreasing by Th80, RELAT_1:123, RFUNCT_2:29; ::_thesis: verum end; theorem Th85: :: SINCOS10:85 for x being set st x in [.1,(sqrt 2).] holds arcsec1 . x in [.0,(PI / 4).] proof let x be set ; ::_thesis: ( x in [.1,(sqrt 2).] implies arcsec1 . x in [.0,(PI / 4).] ) assume x in [.1,(sqrt 2).] ; ::_thesis: arcsec1 . x in [.0,(PI / 4).] then x in ].1,(sqrt 2).[ \/ {1,(sqrt 2)} by SQUARE_1:19, XXREAL_1:128; then A1: ( x in ].1,(sqrt 2).[ or x in {1,(sqrt 2)} ) by XBOOLE_0:def_3; percases ( x in ].1,(sqrt 2).[ or x = 1 or x = sqrt 2 ) by A1, TARSKI:def_2; supposeA2: x in ].1,(sqrt 2).[ ; ::_thesis: arcsec1 . x in [.0,(PI / 4).] then A3: ( ].1,(sqrt 2).[ c= [.1,(sqrt 2).] & ex s being Real st ( s = x & 1 < s & s < sqrt 2 ) ) by XXREAL_1:25; A4: [.1,(sqrt 2).] /\ (dom arcsec1) = [.1,(sqrt 2).] by Th45, XBOOLE_1:28; then sqrt 2 in [.1,(sqrt 2).] /\ (dom arcsec1) by SQUARE_1:19; then A5: arcsec1 . x < PI / 4 by A2, A4, A3, Th73, Th81, RFUNCT_2:20; 1 in [.1,(sqrt 2).] by SQUARE_1:19; then 0 < arcsec1 . x by A2, A4, A3, Th73, Th81, RFUNCT_2:20; hence arcsec1 . x in [.0,(PI / 4).] by A5; ::_thesis: verum end; suppose x = 1 ; ::_thesis: arcsec1 . x in [.0,(PI / 4).] hence arcsec1 . x in [.0,(PI / 4).] by Th73; ::_thesis: verum end; suppose x = sqrt 2 ; ::_thesis: arcsec1 . x in [.0,(PI / 4).] hence arcsec1 . x in [.0,(PI / 4).] by Th73; ::_thesis: verum end; end; end; theorem Th86: :: SINCOS10:86 for x being set st x in [.(- (sqrt 2)),(- 1).] holds arcsec2 . x in [.((3 / 4) * PI),PI.] proof let x be set ; ::_thesis: ( x in [.(- (sqrt 2)),(- 1).] implies arcsec2 . x in [.((3 / 4) * PI),PI.] ) A1: - (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24; assume x in [.(- (sqrt 2)),(- 1).] ; ::_thesis: arcsec2 . x in [.((3 / 4) * PI),PI.] then x in ].(- (sqrt 2)),(- 1).[ \/ {(- (sqrt 2)),(- 1)} by A1, XXREAL_1:128; then A2: ( x in ].(- (sqrt 2)),(- 1).[ or x in {(- (sqrt 2)),(- 1)} ) by XBOOLE_0:def_3; percases ( x in ].(- (sqrt 2)),(- 1).[ or x = - (sqrt 2) or x = - 1 ) by A2, TARSKI:def_2; supposeA3: x in ].(- (sqrt 2)),(- 1).[ ; ::_thesis: arcsec2 . x in [.((3 / 4) * PI),PI.] then A4: ( ].(- (sqrt 2)),(- 1).[ c= [.(- (sqrt 2)),(- 1).] & ex s being Real st ( s = x & - (sqrt 2) < s & s < - 1 ) ) by XXREAL_1:25; A5: [.(- (sqrt 2)),(- 1).] /\ (dom arcsec2) = [.(- (sqrt 2)),(- 1).] by Th46, XBOOLE_1:28; then - 1 in [.(- (sqrt 2)),(- 1).] /\ (dom arcsec2) by A1; then A6: arcsec2 . x < PI by A3, A5, A4, Th74, Th82, RFUNCT_2:20; - (sqrt 2) in [.(- (sqrt 2)),(- 1).] by A1; then (3 / 4) * PI < arcsec2 . x by A3, A5, A4, Th74, Th82, RFUNCT_2:20; hence arcsec2 . x in [.((3 / 4) * PI),PI.] by A6; ::_thesis: verum end; supposeA7: x = - (sqrt 2) ; ::_thesis: arcsec2 . x in [.((3 / 4) * PI),PI.] (3 / 4) * PI <= PI by Lm6, XXREAL_1:2; hence arcsec2 . x in [.((3 / 4) * PI),PI.] by A7, Th74; ::_thesis: verum end; supposeA8: x = - 1 ; ::_thesis: arcsec2 . x in [.((3 / 4) * PI),PI.] (3 / 4) * PI <= PI by Lm6, XXREAL_1:2; hence arcsec2 . x in [.((3 / 4) * PI),PI.] by A8, Th74; ::_thesis: verum end; end; end; theorem Th87: :: SINCOS10:87 for x being set st x in [.(- (sqrt 2)),(- 1).] holds arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] proof let x be set ; ::_thesis: ( x in [.(- (sqrt 2)),(- 1).] implies arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] ) A1: - (sqrt 2) < - 1 by SQUARE_1:19, XREAL_1:24; assume x in [.(- (sqrt 2)),(- 1).] ; ::_thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] then x in ].(- (sqrt 2)),(- 1).[ \/ {(- (sqrt 2)),(- 1)} by A1, XXREAL_1:128; then A2: ( x in ].(- (sqrt 2)),(- 1).[ or x in {(- (sqrt 2)),(- 1)} ) by XBOOLE_0:def_3; percases ( x in ].(- (sqrt 2)),(- 1).[ or x = - (sqrt 2) or x = - 1 ) by A2, TARSKI:def_2; supposeA3: x in ].(- (sqrt 2)),(- 1).[ ; ::_thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] then A4: ( ].(- (sqrt 2)),(- 1).[ c= [.(- (sqrt 2)),(- 1).] & ex s being Real st ( s = x & - (sqrt 2) < s & s < - 1 ) ) by XXREAL_1:25; A5: [.(- (sqrt 2)),(- 1).] /\ (dom arccosec1) = [.(- (sqrt 2)),(- 1).] by Th47, XBOOLE_1:28; then - 1 in [.(- (sqrt 2)),(- 1).] /\ (dom arccosec1) by A1; then A6: arccosec1 . x > - (PI / 2) by A3, A5, A4, Th75, Th83, RFUNCT_2:21; - (sqrt 2) in [.(- (sqrt 2)),(- 1).] by A1; then - (PI / 4) > arccosec1 . x by A3, A5, A4, Th75, Th83, RFUNCT_2:21; hence arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] by A6; ::_thesis: verum end; supposeA7: x = - (sqrt 2) ; ::_thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] - (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3; hence arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] by A7, Th75; ::_thesis: verum end; supposeA8: x = - 1 ; ::_thesis: arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] - (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3; hence arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] by A8, Th75; ::_thesis: verum end; end; end; theorem Th88: :: SINCOS10:88 for x being set st x in [.1,(sqrt 2).] holds arccosec2 . x in [.(PI / 4),(PI / 2).] proof let x be set ; ::_thesis: ( x in [.1,(sqrt 2).] implies arccosec2 . x in [.(PI / 4),(PI / 2).] ) assume x in [.1,(sqrt 2).] ; ::_thesis: arccosec2 . x in [.(PI / 4),(PI / 2).] then x in ].1,(sqrt 2).[ \/ {1,(sqrt 2)} by SQUARE_1:19, XXREAL_1:128; then A1: ( x in ].1,(sqrt 2).[ or x in {1,(sqrt 2)} ) by XBOOLE_0:def_3; percases ( x in ].1,(sqrt 2).[ or x = 1 or x = sqrt 2 ) by A1, TARSKI:def_2; supposeA2: x in ].1,(sqrt 2).[ ; ::_thesis: arccosec2 . x in [.(PI / 4),(PI / 2).] then A3: ( ].1,(sqrt 2).[ c= [.1,(sqrt 2).] & ex s being Real st ( s = x & 1 < s & s < sqrt 2 ) ) by XXREAL_1:25; A4: [.1,(sqrt 2).] /\ (dom arccosec2) = [.1,(sqrt 2).] by Th48, XBOOLE_1:28; then sqrt 2 in [.1,(sqrt 2).] /\ (dom arccosec2) by SQUARE_1:19; then A5: arccosec2 . x > PI / 4 by A2, A4, A3, Th76, Th84, RFUNCT_2:21; 1 in [.1,(sqrt 2).] by SQUARE_1:19; then PI / 2 > arccosec2 . x by A2, A4, A3, Th76, Th84, RFUNCT_2:21; hence arccosec2 . x in [.(PI / 4),(PI / 2).] by A5; ::_thesis: verum end; supposeA6: x = 1 ; ::_thesis: arccosec2 . x in [.(PI / 4),(PI / 2).] PI / 4 <= PI / 2 by Lm8, XXREAL_1:2; hence arccosec2 . x in [.(PI / 4),(PI / 2).] by A6, Th76; ::_thesis: verum end; supposeA7: x = sqrt 2 ; ::_thesis: arccosec2 . x in [.(PI / 4),(PI / 2).] PI / 4 <= PI / 2 by Lm8, XXREAL_1:2; hence arccosec2 . x in [.(PI / 4),(PI / 2).] by A7, Th76; ::_thesis: verum end; end; end; theorem Th89: :: SINCOS10:89 for r being Real st 1 <= r & r <= sqrt 2 holds sec . (arcsec1 r) = r proof let r be Real; ::_thesis: ( 1 <= r & r <= sqrt 2 implies sec . (arcsec1 r) = r ) assume ( 1 <= r & r <= sqrt 2 ) ; ::_thesis: sec . (arcsec1 r) = r then A1: r in [.1,(sqrt 2).] ; then A2: r in dom (arcsec1 | [.1,(sqrt 2).]) by Th45, RELAT_1:62; sec . (arcsec1 r) = (sec | [.0,(PI / 4).]) . (arcsec1 . r) by A1, Th85, FUNCT_1:49 .= (sec | [.0,(PI / 4).]) . ((arcsec1 | [.1,(sqrt 2).]) . r) by A1, FUNCT_1:49 .= ((sec | [.0,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).])) . r by A2, FUNCT_1:13 .= (id [.1,(sqrt 2).]) . r by Th41, Th49, FUNCT_1:39 .= r by A1, FUNCT_1:18 ; hence sec . (arcsec1 r) = r ; ::_thesis: verum end; theorem Th90: :: SINCOS10:90 for r being Real st - (sqrt 2) <= r & r <= - 1 holds sec . (arcsec2 r) = r proof let r be Real; ::_thesis: ( - (sqrt 2) <= r & r <= - 1 implies sec . (arcsec2 r) = r ) assume ( - (sqrt 2) <= r & r <= - 1 ) ; ::_thesis: sec . (arcsec2 r) = r then A1: r in [.(- (sqrt 2)),(- 1).] ; then A2: r in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) by Th46, RELAT_1:62; sec . (arcsec2 r) = (sec | [.((3 / 4) * PI),PI.]) . (arcsec2 . r) by A1, Th86, FUNCT_1:49 .= (sec | [.((3 / 4) * PI),PI.]) . ((arcsec2 | [.(- (sqrt 2)),(- 1).]) . r) by A1, FUNCT_1:49 .= ((sec | [.((3 / 4) * PI),PI.]) * (arcsec2 | [.(- (sqrt 2)),(- 1).])) . r by A2, FUNCT_1:13 .= (id [.(- (sqrt 2)),(- 1).]) . r by Th42, Th50, FUNCT_1:39 .= r by A1, FUNCT_1:18 ; hence sec . (arcsec2 r) = r ; ::_thesis: verum end; theorem Th91: :: SINCOS10:91 for r being Real st - (sqrt 2) <= r & r <= - 1 holds cosec . (arccosec1 r) = r proof let r be Real; ::_thesis: ( - (sqrt 2) <= r & r <= - 1 implies cosec . (arccosec1 r) = r ) assume ( - (sqrt 2) <= r & r <= - 1 ) ; ::_thesis: cosec . (arccosec1 r) = r then A1: r in [.(- (sqrt 2)),(- 1).] ; then A2: r in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) by Th47, RELAT_1:62; cosec . (arccosec1 r) = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . (arccosec1 . r) by A1, Th87, FUNCT_1:49 .= (cosec | [.(- (PI / 2)),(- (PI / 4)).]) . ((arccosec1 | [.(- (sqrt 2)),(- 1).]) . r) by A1, FUNCT_1:49 .= ((cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (arccosec1 | [.(- (sqrt 2)),(- 1).])) . r by A2, FUNCT_1:13 .= (id [.(- (sqrt 2)),(- 1).]) . r by Th43, Th51, FUNCT_1:39 .= r by A1, FUNCT_1:18 ; hence cosec . (arccosec1 r) = r ; ::_thesis: verum end; theorem Th92: :: SINCOS10:92 for r being Real st 1 <= r & r <= sqrt 2 holds cosec . (arccosec2 r) = r proof let r be Real; ::_thesis: ( 1 <= r & r <= sqrt 2 implies cosec . (arccosec2 r) = r ) assume ( 1 <= r & r <= sqrt 2 ) ; ::_thesis: cosec . (arccosec2 r) = r then A1: r in [.1,(sqrt 2).] ; then A2: r in dom (arccosec2 | [.1,(sqrt 2).]) by Th48, RELAT_1:62; cosec . (arccosec2 r) = (cosec | [.(PI / 4),(PI / 2).]) . (arccosec2 . r) by A1, Th88, FUNCT_1:49 .= (cosec | [.(PI / 4),(PI / 2).]) . ((arccosec2 | [.1,(sqrt 2).]) . r) by A1, FUNCT_1:49 .= ((cosec | [.(PI / 4),(PI / 2).]) * (arccosec2 | [.1,(sqrt 2).])) . r by A2, FUNCT_1:13 .= (id [.1,(sqrt 2).]) . r by Th44, Th52, FUNCT_1:39 .= r by A1, FUNCT_1:18 ; hence cosec . (arccosec2 r) = r ; ::_thesis: verum end; theorem Th93: :: SINCOS10:93 arcsec1 | [.1,(sqrt 2).] is continuous proof set f = sec | [.0,(PI / 4).]; ( (sec | [.0,(PI / 4).]) | [.0,(PI / 4).] = sec | [.0,(PI / 4).] & (((sec | [.0,(PI / 4).]) | [.0,(PI / 4).]) ") | ((sec | [.0,(PI / 4).]) .: [.0,(PI / 4).]) is continuous ) by Lm29, Lm37, FCONT_1:47, RELAT_1:72; then (arcsec1 | [.1,(sqrt 2).]) | [.1,(sqrt 2).] is continuous by Th41, Th49, RELAT_1:115; hence arcsec1 | [.1,(sqrt 2).] is continuous by FCONT_1:15; ::_thesis: verum end; theorem Th94: :: SINCOS10:94 arcsec2 | [.(- (sqrt 2)),(- 1).] is continuous proof set f = sec | [.((3 / 4) * PI),PI.]; (3 / 4) * PI <= PI by Lm6, XXREAL_1:2; then ( (sec | [.((3 / 4) * PI),PI.]) | [.((3 / 4) * PI),PI.] = sec | [.((3 / 4) * PI),PI.] & (((sec | [.((3 / 4) * PI),PI.]) | [.((3 / 4) * PI),PI.]) ") | ((sec | [.((3 / 4) * PI),PI.]) .: [.((3 / 4) * PI),PI.]) is continuous ) by Lm30, Lm38, FCONT_1:47, RELAT_1:72; then (arcsec2 | [.(- (sqrt 2)),(- 1).]) | [.(- (sqrt 2)),(- 1).] is continuous by Th42, Th50, RELAT_1:115; hence arcsec2 | [.(- (sqrt 2)),(- 1).] is continuous by FCONT_1:15; ::_thesis: verum end; theorem Th95: :: SINCOS10:95 arccosec1 | [.(- (sqrt 2)),(- 1).] is continuous proof set f = cosec | [.(- (PI / 2)),(- (PI / 4)).]; - (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3; then ( (cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).] = cosec | [.(- (PI / 2)),(- (PI / 4)).] & (((cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).]) ") | ((cosec | [.(- (PI / 2)),(- (PI / 4)).]) .: [.(- (PI / 2)),(- (PI / 4)).]) is continuous ) by Lm31, Lm39, FCONT_1:47, RELAT_1:72; then (arccosec1 | [.(- (sqrt 2)),(- 1).]) | [.(- (sqrt 2)),(- 1).] is continuous by Th43, Th51, RELAT_1:115; hence arccosec1 | [.(- (sqrt 2)),(- 1).] is continuous by FCONT_1:15; ::_thesis: verum end; theorem Th96: :: SINCOS10:96 arccosec2 | [.1,(sqrt 2).] is continuous proof set f = cosec | [.(PI / 4),(PI / 2).]; PI / 4 <= PI / 2 by Lm8, XXREAL_1:2; then ( (cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] = cosec | [.(PI / 4),(PI / 2).] & (((cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).]) ") | ((cosec | [.(PI / 4),(PI / 2).]) .: [.(PI / 4),(PI / 2).]) is continuous ) by Lm32, Lm40, FCONT_1:47, RELAT_1:72; then (arccosec2 | [.1,(sqrt 2).]) | [.1,(sqrt 2).] is continuous by Th44, Th52, RELAT_1:115; hence arccosec2 | [.1,(sqrt 2).] is continuous by FCONT_1:15; ::_thesis: verum end; theorem Th97: :: SINCOS10:97 rng (arcsec1 | [.1,(sqrt 2).]) = [.0,(PI / 4).] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.0,(PI_/_4).]_implies_ex_x_being_set_st_ (_x_in_dom_(arcsec1_|_[.1,(sqrt_2).])_&_y_=_(arcsec1_|_[.1,(sqrt_2).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(arcsec1_|_[.1,(sqrt_2).])_&_y_=_(arcsec1_|_[.1,(sqrt_2).])_._x_)_implies_y_in_[.0,(PI_/_4).]_)_) let y be set ; ::_thesis: ( ( y in [.0,(PI / 4).] implies ex x being set st ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) ) & ( ex x being set st ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) implies y in [.0,(PI / 4).] ) ) thus ( y in [.0,(PI / 4).] implies ex x being set st ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) implies y in [.0,(PI / 4).] ) proof assume A1: y in [.0,(PI / 4).] ; ::_thesis: ex x being set st ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) then reconsider y1 = y as Real ; y1 in [.(arcsec1 . 1),(arcsec1 . (sqrt 2)).] \/ [.(arcsec1 . (sqrt 2)),(arcsec1 . 1).] by A1, Th73, XBOOLE_0:def_3; then consider x being Real such that A2: ( x in [.1,(sqrt 2).] & y1 = arcsec1 . x ) by Th45, Th93, FCONT_2:15, SQUARE_1:19; take x ; ::_thesis: ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) thus ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) by A2, Th45, FUNCT_1:49, RELAT_1:62; ::_thesis: verum end; thus ( ex x being set st ( x in dom (arcsec1 | [.1,(sqrt 2).]) & y = (arcsec1 | [.1,(sqrt 2).]) . x ) implies y in [.0,(PI / 4).] ) ::_thesis: verum proof given x being set such that A3: x in dom (arcsec1 | [.1,(sqrt 2).]) and A4: y = (arcsec1 | [.1,(sqrt 2).]) . x ; ::_thesis: y in [.0,(PI / 4).] A5: dom (arcsec1 | [.1,(sqrt 2).]) = [.1,(sqrt 2).] by Th45, RELAT_1:62; then y = arcsec1 . x by A3, A4, FUNCT_1:49; hence y in [.0,(PI / 4).] by A3, A5, Th85; ::_thesis: verum end; end; hence rng (arcsec1 | [.1,(sqrt 2).]) = [.0,(PI / 4).] by FUNCT_1:def_3; ::_thesis: verum end; theorem Th98: :: SINCOS10:98 rng (arcsec2 | [.(- (sqrt 2)),(- 1).]) = [.((3 / 4) * PI),PI.] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.((3_/_4)_*_PI),PI.]_implies_ex_x_being_set_st_ (_x_in_dom_(arcsec2_|_[.(-_(sqrt_2)),(-_1).])_&_y_=_(arcsec2_|_[.(-_(sqrt_2)),(-_1).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(arcsec2_|_[.(-_(sqrt_2)),(-_1).])_&_y_=_(arcsec2_|_[.(-_(sqrt_2)),(-_1).])_._x_)_implies_y_in_[.((3_/_4)_*_PI),PI.]_)_) let y be set ; ::_thesis: ( ( y in [.((3 / 4) * PI),PI.] implies ex x being set st ( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) ) & ( ex x being set st ( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.((3 / 4) * PI),PI.] ) ) thus ( y in [.((3 / 4) * PI),PI.] implies ex x being set st ( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.((3 / 4) * PI),PI.] ) proof assume A1: y in [.((3 / 4) * PI),PI.] ; ::_thesis: ex x being set st ( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) then reconsider y1 = y as Real ; ( - (sqrt 2) < - 1 & y1 in [.(arcsec2 . (- (sqrt 2))),(arcsec2 . (- 1)).] \/ [.(arcsec2 . (- 1)),(arcsec2 . (- (sqrt 2))).] ) by A1, Th74, SQUARE_1:19, XBOOLE_0:def_3, XREAL_1:24; then consider x being Real such that A2: ( x in [.(- (sqrt 2)),(- 1).] & y1 = arcsec2 . x ) by Th46, Th94, FCONT_2:15; take x ; ::_thesis: ( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) thus ( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) by A2, Th46, FUNCT_1:49, RELAT_1:62; ::_thesis: verum end; thus ( ex x being set st ( x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) & y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.((3 / 4) * PI),PI.] ) ::_thesis: verum proof given x being set such that A3: x in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) and A4: y = (arcsec2 | [.(- (sqrt 2)),(- 1).]) . x ; ::_thesis: y in [.((3 / 4) * PI),PI.] A5: dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) = [.(- (sqrt 2)),(- 1).] by Th46, RELAT_1:62; then y = arcsec2 . x by A3, A4, FUNCT_1:49; hence y in [.((3 / 4) * PI),PI.] by A3, A5, Th86; ::_thesis: verum end; end; hence rng (arcsec2 | [.(- (sqrt 2)),(- 1).]) = [.((3 / 4) * PI),PI.] by FUNCT_1:def_3; ::_thesis: verum end; theorem Th99: :: SINCOS10:99 rng (arccosec1 | [.(- (sqrt 2)),(- 1).]) = [.(- (PI / 2)),(- (PI / 4)).] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(-_(PI_/_2)),(-_(PI_/_4)).]_implies_ex_x_being_set_st_ (_x_in_dom_(arccosec1_|_[.(-_(sqrt_2)),(-_1).])_&_y_=_(arccosec1_|_[.(-_(sqrt_2)),(-_1).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(arccosec1_|_[.(-_(sqrt_2)),(-_1).])_&_y_=_(arccosec1_|_[.(-_(sqrt_2)),(-_1).])_._x_)_implies_y_in_[.(-_(PI_/_2)),(-_(PI_/_4)).]_)_) let y be set ; ::_thesis: ( ( y in [.(- (PI / 2)),(- (PI / 4)).] implies ex x being set st ( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) ) & ( ex x being set st ( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.(- (PI / 2)),(- (PI / 4)).] ) ) thus ( y in [.(- (PI / 2)),(- (PI / 4)).] implies ex x being set st ( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.(- (PI / 2)),(- (PI / 4)).] ) proof assume A1: y in [.(- (PI / 2)),(- (PI / 4)).] ; ::_thesis: ex x being set st ( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) then reconsider y1 = y as Real ; ( - (sqrt 2) < - 1 & y1 in [.(arccosec1 . (- 1)),(arccosec1 . (- (sqrt 2))).] \/ [.(arccosec1 . (- (sqrt 2))),(arccosec1 . (- 1)).] ) by A1, Th75, SQUARE_1:19, XBOOLE_0:def_3, XREAL_1:24; then consider x being Real such that A2: ( x in [.(- (sqrt 2)),(- 1).] & y1 = arccosec1 . x ) by Th47, Th95, FCONT_2:15; take x ; ::_thesis: ( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) thus ( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) by A2, Th47, FUNCT_1:49, RELAT_1:62; ::_thesis: verum end; thus ( ex x being set st ( x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) & y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ) implies y in [.(- (PI / 2)),(- (PI / 4)).] ) ::_thesis: verum proof given x being set such that A3: x in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) and A4: y = (arccosec1 | [.(- (sqrt 2)),(- 1).]) . x ; ::_thesis: y in [.(- (PI / 2)),(- (PI / 4)).] A5: dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) = [.(- (sqrt 2)),(- 1).] by Th47, RELAT_1:62; then y = arccosec1 . x by A3, A4, FUNCT_1:49; hence y in [.(- (PI / 2)),(- (PI / 4)).] by A3, A5, Th87; ::_thesis: verum end; end; hence rng (arccosec1 | [.(- (sqrt 2)),(- 1).]) = [.(- (PI / 2)),(- (PI / 4)).] by FUNCT_1:def_3; ::_thesis: verum end; theorem Th100: :: SINCOS10:100 rng (arccosec2 | [.1,(sqrt 2).]) = [.(PI / 4),(PI / 2).] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(PI_/_4),(PI_/_2).]_implies_ex_x_being_set_st_ (_x_in_dom_(arccosec2_|_[.1,(sqrt_2).])_&_y_=_(arccosec2_|_[.1,(sqrt_2).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(arccosec2_|_[.1,(sqrt_2).])_&_y_=_(arccosec2_|_[.1,(sqrt_2).])_._x_)_implies_y_in_[.(PI_/_4),(PI_/_2).]_)_) let y be set ; ::_thesis: ( ( y in [.(PI / 4),(PI / 2).] implies ex x being set st ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) ) & ( ex x being set st ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) implies y in [.(PI / 4),(PI / 2).] ) ) thus ( y in [.(PI / 4),(PI / 2).] implies ex x being set st ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) implies y in [.(PI / 4),(PI / 2).] ) proof assume A1: y in [.(PI / 4),(PI / 2).] ; ::_thesis: ex x being set st ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) then reconsider y1 = y as Real ; y1 in [.(arccosec2 . (sqrt 2)),(arccosec2 . 1).] \/ [.(arccosec2 . 1),(arccosec2 . (sqrt 2)).] by A1, Th76, XBOOLE_0:def_3; then consider x being Real such that A2: ( x in [.1,(sqrt 2).] & y1 = arccosec2 . x ) by Th48, Th96, FCONT_2:15, SQUARE_1:19; take x ; ::_thesis: ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) thus ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) by A2, Th48, FUNCT_1:49, RELAT_1:62; ::_thesis: verum end; thus ( ex x being set st ( x in dom (arccosec2 | [.1,(sqrt 2).]) & y = (arccosec2 | [.1,(sqrt 2).]) . x ) implies y in [.(PI / 4),(PI / 2).] ) ::_thesis: verum proof given x being set such that A3: x in dom (arccosec2 | [.1,(sqrt 2).]) and A4: y = (arccosec2 | [.1,(sqrt 2).]) . x ; ::_thesis: y in [.(PI / 4),(PI / 2).] A5: dom (arccosec2 | [.1,(sqrt 2).]) = [.1,(sqrt 2).] by Th48, RELAT_1:62; then y = arccosec2 . x by A3, A4, FUNCT_1:49; hence y in [.(PI / 4),(PI / 2).] by A3, A5, Th88; ::_thesis: verum end; end; hence rng (arccosec2 | [.1,(sqrt 2).]) = [.(PI / 4),(PI / 2).] by FUNCT_1:def_3; ::_thesis: verum end; theorem :: SINCOS10:101 for r being Real holds ( ( 1 <= r & r <= sqrt 2 & arcsec1 r = 0 implies r = 1 ) & ( 1 <= r & r <= sqrt 2 & arcsec1 r = PI / 4 implies r = sqrt 2 ) ) by Th31, Th89; theorem :: SINCOS10:102 for r being Real holds ( ( - (sqrt 2) <= r & r <= - 1 & arcsec2 r = (3 / 4) * PI implies r = - (sqrt 2) ) & ( - (sqrt 2) <= r & r <= - 1 & arcsec2 r = PI implies r = - 1 ) ) by Th31, Th90; theorem :: SINCOS10:103 for r being Real holds ( ( - (sqrt 2) <= r & r <= - 1 & arccosec1 r = - (PI / 2) implies r = - 1 ) & ( - (sqrt 2) <= r & r <= - 1 & arccosec1 r = - (PI / 4) implies r = - (sqrt 2) ) ) by Th32, Th91; theorem :: SINCOS10:104 for r being Real holds ( ( 1 <= r & r <= sqrt 2 & arccosec2 r = PI / 4 implies r = sqrt 2 ) & ( 1 <= r & r <= sqrt 2 & arccosec2 r = PI / 2 implies r = 1 ) ) by Th32, Th92; theorem Th105: :: SINCOS10:105 for r being Real st 1 <= r & r <= sqrt 2 holds ( 0 <= arcsec1 r & arcsec1 r <= PI / 4 ) proof let r be Real; ::_thesis: ( 1 <= r & r <= sqrt 2 implies ( 0 <= arcsec1 r & arcsec1 r <= PI / 4 ) ) assume ( 1 <= r & r <= sqrt 2 ) ; ::_thesis: ( 0 <= arcsec1 r & arcsec1 r <= PI / 4 ) then A1: r in [.1,(sqrt 2).] ; then r in dom (arcsec1 | [.1,(sqrt 2).]) by Th45, RELAT_1:62; then (arcsec1 | [.1,(sqrt 2).]) . r in rng (arcsec1 | [.1,(sqrt 2).]) by FUNCT_1:def_3; then arcsec1 r in rng (arcsec1 | [.1,(sqrt 2).]) by A1, FUNCT_1:49; hence ( 0 <= arcsec1 r & arcsec1 r <= PI / 4 ) by Th97, XXREAL_1:1; ::_thesis: verum end; theorem Th106: :: SINCOS10:106 for r being Real st - (sqrt 2) <= r & r <= - 1 holds ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI ) proof let r be Real; ::_thesis: ( - (sqrt 2) <= r & r <= - 1 implies ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI ) ) assume ( - (sqrt 2) <= r & r <= - 1 ) ; ::_thesis: ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI ) then A1: r in [.(- (sqrt 2)),(- 1).] ; then r in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) by Th46, RELAT_1:62; then (arcsec2 | [.(- (sqrt 2)),(- 1).]) . r in rng (arcsec2 | [.(- (sqrt 2)),(- 1).]) by FUNCT_1:def_3; then arcsec2 r in rng (arcsec2 | [.(- (sqrt 2)),(- 1).]) by A1, FUNCT_1:49; hence ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI ) by Th98, XXREAL_1:1; ::_thesis: verum end; theorem Th107: :: SINCOS10:107 for r being Real st - (sqrt 2) <= r & r <= - 1 holds ( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) ) proof let r be Real; ::_thesis: ( - (sqrt 2) <= r & r <= - 1 implies ( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) ) ) assume ( - (sqrt 2) <= r & r <= - 1 ) ; ::_thesis: ( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) ) then A1: r in [.(- (sqrt 2)),(- 1).] ; then r in dom (arccosec1 | [.(- (sqrt 2)),(- 1).]) by Th47, RELAT_1:62; then (arccosec1 | [.(- (sqrt 2)),(- 1).]) . r in rng (arccosec1 | [.(- (sqrt 2)),(- 1).]) by FUNCT_1:def_3; then arccosec1 r in rng (arccosec1 | [.(- (sqrt 2)),(- 1).]) by A1, FUNCT_1:49; hence ( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) ) by Th99, XXREAL_1:1; ::_thesis: verum end; theorem Th108: :: SINCOS10:108 for r being Real st 1 <= r & r <= sqrt 2 holds ( PI / 4 <= arccosec2 r & arccosec2 r <= PI / 2 ) proof let r be Real; ::_thesis: ( 1 <= r & r <= sqrt 2 implies ( PI / 4 <= arccosec2 r & arccosec2 r <= PI / 2 ) ) assume ( 1 <= r & r <= sqrt 2 ) ; ::_thesis: ( PI / 4 <= arccosec2 r & arccosec2 r <= PI / 2 ) then A1: r in [.1,(sqrt 2).] ; then r in dom (arccosec2 | [.1,(sqrt 2).]) by Th48, RELAT_1:62; then (arccosec2 | [.1,(sqrt 2).]) . r in rng (arccosec2 | [.1,(sqrt 2).]) by FUNCT_1:def_3; then arccosec2 r in rng (arccosec2 | [.1,(sqrt 2).]) by A1, FUNCT_1:49; hence ( PI / 4 <= arccosec2 r & arccosec2 r <= PI / 2 ) by Th100, XXREAL_1:1; ::_thesis: verum end; theorem Th109: :: SINCOS10:109 for r being Real st 1 < r & r < sqrt 2 holds ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) proof let r be Real; ::_thesis: ( 1 < r & r < sqrt 2 implies ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) ) assume A1: ( 1 < r & r < sqrt 2 ) ; ::_thesis: ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) then arcsec1 r <= PI / 4 by Th105; then ( ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) or 0 = arcsec1 r or arcsec1 r = PI / 4 ) by A1, Th105, XXREAL_0:1; hence ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) by A1, Th31, Th89; ::_thesis: verum end; theorem Th110: :: SINCOS10:110 for r being Real st - (sqrt 2) < r & r < - 1 holds ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) proof let r be Real; ::_thesis: ( - (sqrt 2) < r & r < - 1 implies ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) ) assume A1: ( - (sqrt 2) < r & r < - 1 ) ; ::_thesis: ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) then ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI ) by Th106; then ( ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) or (3 / 4) * PI = arcsec2 r or arcsec2 r = PI ) by XXREAL_0:1; hence ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) by A1, Th31, Th90; ::_thesis: verum end; theorem Th111: :: SINCOS10:111 for r being Real st - (sqrt 2) < r & r < - 1 holds ( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) ) proof let r be Real; ::_thesis: ( - (sqrt 2) < r & r < - 1 implies ( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) ) ) assume A1: ( - (sqrt 2) < r & r < - 1 ) ; ::_thesis: ( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) ) then ( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) ) by Th107; then ( ( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) ) or - (PI / 2) = arccosec1 r or arccosec1 r = - (PI / 4) ) by XXREAL_0:1; hence ( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) ) by A1, Th32, Th91; ::_thesis: verum end; theorem Th112: :: SINCOS10:112 for r being Real st 1 < r & r < sqrt 2 holds ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) proof let r be Real; ::_thesis: ( 1 < r & r < sqrt 2 implies ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) ) assume A1: ( 1 < r & r < sqrt 2 ) ; ::_thesis: ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) then ( PI / 4 <= arccosec2 r & arccosec2 r <= PI / 2 ) by Th108; then ( ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) or PI / 4 = arccosec2 r or arccosec2 r = PI / 2 ) by XXREAL_0:1; hence ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) by A1, Th32, Th92; ::_thesis: verum end; theorem Th113: :: SINCOS10:113 for r being Real st 1 <= r & r <= sqrt 2 holds ( sin . (arcsec1 r) = (sqrt ((r ^2) - 1)) / r & cos . (arcsec1 r) = 1 / r ) proof let r be Real; ::_thesis: ( 1 <= r & r <= sqrt 2 implies ( sin . (arcsec1 r) = (sqrt ((r ^2) - 1)) / r & cos . (arcsec1 r) = 1 / r ) ) set x = arcsec1 r; assume that A1: 1 <= r and A2: r <= sqrt 2 ; ::_thesis: ( sin . (arcsec1 r) = (sqrt ((r ^2) - 1)) / r & cos . (arcsec1 r) = 1 / r ) r in [.1,(sqrt 2).] by A1, A2; then A3: arcsec1 r in dom (sec | [.0,(PI / 4).]) by Lm29, Th85; PI / 4 < PI / 1 by XREAL_1:76; then ( 0 in [.0,PI.] & PI / 4 in [.0,PI.] ) ; then [.0,(PI / 4).] c= [.0,PI.] by XXREAL_2:def_12; then A4: sin . (arcsec1 r) >= 0 by A3, Lm29, COMPTRIG:8; A5: dom (sec | [.0,(PI / 4).]) c= dom sec by RELAT_1:60; A6: r = (cos ^) . (arcsec1 r) by A1, A2, Th89 .= 1 / (cos . (arcsec1 r)) by A3, A5, RFUNCT_1:def_2 ; r ^2 >= 1 ^2 by A1, SQUARE_1:15; then A7: (r ^2) - 1 >= 0 by XREAL_1:48; ((sin . (arcsec1 r)) ^2) + ((cos . (arcsec1 r)) ^2) = 1 by SIN_COS:28; then (sin . (arcsec1 r)) ^2 = 1 - ((cos . (arcsec1 r)) ^2) .= 1 - ((1 / r) * (1 / r)) by A6 .= 1 - (1 / (r ^2)) by XCMPLX_1:102 .= ((r ^2) / (r ^2)) - (1 / (r ^2)) by A1, XCMPLX_1:60 .= ((r ^2) - 1) / (r ^2) ; then sin . (arcsec1 r) = sqrt (((r ^2) - 1) / (r ^2)) by A4, SQUARE_1:def_2 .= (sqrt ((r ^2) - 1)) / (sqrt (r ^2)) by A1, A7, SQUARE_1:30 .= (sqrt ((r ^2) - 1)) / r by A1, SQUARE_1:22 ; hence ( sin . (arcsec1 r) = (sqrt ((r ^2) - 1)) / r & cos . (arcsec1 r) = 1 / r ) by A6; ::_thesis: verum end; theorem Th114: :: SINCOS10:114 for r being Real st - (sqrt 2) <= r & r <= - 1 holds ( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r ) proof let r be Real; ::_thesis: ( - (sqrt 2) <= r & r <= - 1 implies ( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r ) ) (3 / 4) * PI <= PI by Lm6, XXREAL_1:2; then A1: (3 / 4) * PI in [.0,PI.] ; A2: dom (sec | [.((3 / 4) * PI),PI.]) c= dom sec by RELAT_1:60; set x = arcsec2 r; assume that A3: - (sqrt 2) <= r and A4: r <= - 1 ; ::_thesis: ( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r ) r in [.(- (sqrt 2)),(- 1).] by A3, A4; then A5: arcsec2 r in dom (sec | [.((3 / 4) * PI),PI.]) by Lm30, Th86; A6: r = (cos ^) . (arcsec2 r) by A3, A4, Th90 .= 1 / (cos . (arcsec2 r)) by A5, A2, RFUNCT_1:def_2 ; PI in [.0,PI.] ; then [.((3 / 4) * PI),PI.] c= [.0,PI.] by A1, XXREAL_2:def_12; then A7: sin . (arcsec2 r) >= 0 by A5, Lm30, COMPTRIG:8; - r >= - (- 1) by A4, XREAL_1:24; then (- r) ^2 >= 1 ^2 by SQUARE_1:15; then A8: (r ^2) - 1 >= 0 by XREAL_1:48; ((sin . (arcsec2 r)) ^2) + ((cos . (arcsec2 r)) ^2) = 1 by SIN_COS:28; then (sin . (arcsec2 r)) ^2 = 1 - ((cos . (arcsec2 r)) ^2) .= 1 - ((1 / r) * (1 / r)) by A6 .= 1 - (1 / (r ^2)) by XCMPLX_1:102 .= ((r ^2) / (r ^2)) - (1 / (r ^2)) by A4, XCMPLX_1:60 .= ((r ^2) - 1) / (r ^2) ; then sin . (arcsec2 r) = sqrt (((r ^2) - 1) / (r ^2)) by A7, SQUARE_1:def_2 .= (sqrt ((r ^2) - 1)) / (sqrt (r ^2)) by A4, A8, SQUARE_1:30 .= (sqrt ((r ^2) - 1)) / (- r) by A4, SQUARE_1:23 .= - ((sqrt ((r ^2) - 1)) / r) by XCMPLX_1:188 ; hence ( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r ) by A6; ::_thesis: verum end; theorem Th115: :: SINCOS10:115 for r being Real st - (sqrt 2) <= r & r <= - 1 holds ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2) - 1)) / r) ) proof let r be Real; ::_thesis: ( - (sqrt 2) <= r & r <= - 1 implies ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2) - 1)) / r) ) ) set x = arccosec1 r; assume that A1: - (sqrt 2) <= r and A2: r <= - 1 ; ::_thesis: ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2) - 1)) / r) ) r in [.(- (sqrt 2)),(- 1).] by A1, A2; then A3: arccosec1 r in dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) by Lm31, Th87; - (PI / 4) >= - (PI / 2) by Lm7, XXREAL_1:3; then ( - (PI / 2) in [.(- (PI / 2)),(PI / 2).] & - (PI / 4) in [.(- (PI / 2)),(PI / 2).] ) ; then [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),(PI / 2).] by XXREAL_2:def_12; then A4: cos . (arccosec1 r) >= 0 by A3, Lm31, COMPTRIG:12; A5: dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) c= dom cosec by RELAT_1:60; A6: r = (sin ^) . (arccosec1 r) by A1, A2, Th91 .= 1 / (sin . (arccosec1 r)) by A3, A5, RFUNCT_1:def_2 ; - r >= - (- 1) by A2, XREAL_1:24; then (- r) ^2 >= 1 ^2 by SQUARE_1:15; then A7: (r ^2) - 1 >= 0 by XREAL_1:48; ((sin . (arccosec1 r)) ^2) + ((cos . (arccosec1 r)) ^2) = 1 by SIN_COS:28; then (cos . (arccosec1 r)) ^2 = 1 - ((sin . (arccosec1 r)) ^2) .= 1 - ((1 / r) * (1 / r)) by A6 .= 1 - (1 / (r ^2)) by XCMPLX_1:102 .= ((r ^2) / (r ^2)) - (1 / (r ^2)) by A2, XCMPLX_1:60 .= ((r ^2) - 1) / (r ^2) ; then cos . (arccosec1 r) = sqrt (((r ^2) - 1) / (r ^2)) by A4, SQUARE_1:def_2 .= (sqrt ((r ^2) - 1)) / (sqrt (r ^2)) by A2, A7, SQUARE_1:30 .= (sqrt ((r ^2) - 1)) / (- r) by A2, SQUARE_1:23 .= - ((sqrt ((r ^2) - 1)) / r) by XCMPLX_1:188 ; hence ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2) - 1)) / r) ) by A6; ::_thesis: verum end; theorem Th116: :: SINCOS10:116 for r being Real st 1 <= r & r <= sqrt 2 holds ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r ) proof let r be Real; ::_thesis: ( 1 <= r & r <= sqrt 2 implies ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r ) ) PI / 4 <= PI / 2 by Lm8, XXREAL_1:2; then A1: PI / 4 in [.(- (PI / 2)),(PI / 2).] ; A2: dom (cosec | [.(PI / 4),(PI / 2).]) c= dom cosec by RELAT_1:60; set x = arccosec2 r; assume that A3: 1 <= r and A4: r <= sqrt 2 ; ::_thesis: ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r ) r in [.1,(sqrt 2).] by A3, A4; then A5: arccosec2 r in dom (cosec | [.(PI / 4),(PI / 2).]) by Lm32, Th88; A6: r = (sin ^) . (arccosec2 r) by A3, A4, Th92 .= 1 / (sin . (arccosec2 r)) by A5, A2, RFUNCT_1:def_2 ; PI / 2 in [.(- (PI / 2)),(PI / 2).] ; then [.(PI / 4),(PI / 2).] c= [.(- (PI / 2)),(PI / 2).] by A1, XXREAL_2:def_12; then A7: cos . (arccosec2 r) >= 0 by A5, Lm32, COMPTRIG:12; r ^2 >= 1 ^2 by A3, SQUARE_1:15; then A8: (r ^2) - 1 >= 0 by XREAL_1:48; ((sin . (arccosec2 r)) ^2) + ((cos . (arccosec2 r)) ^2) = 1 by SIN_COS:28; then (cos . (arccosec2 r)) ^2 = 1 - ((sin . (arccosec2 r)) ^2) .= 1 - ((1 / r) * (1 / r)) by A6 .= 1 - (1 / (r ^2)) by XCMPLX_1:102 .= ((r ^2) / (r ^2)) - (1 / (r ^2)) by A3, XCMPLX_1:60 .= ((r ^2) - 1) / (r ^2) ; then cos . (arccosec2 r) = sqrt (((r ^2) - 1) / (r ^2)) by A7, SQUARE_1:def_2 .= (sqrt ((r ^2) - 1)) / (sqrt (r ^2)) by A3, A8, SQUARE_1:30 .= (sqrt ((r ^2) - 1)) / r by A3, SQUARE_1:22 ; hence ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r ) by A6; ::_thesis: verum end; theorem :: SINCOS10:117 for r being Real st 1 < r & r < sqrt 2 holds cosec . (arcsec1 r) = r / (sqrt ((r ^2) - 1)) proof let r be Real; ::_thesis: ( 1 < r & r < sqrt 2 implies cosec . (arcsec1 r) = r / (sqrt ((r ^2) - 1)) ) set x = arcsec1 r; ].0,(PI / 2).] = ].0,(PI / 2).[ \/ {(PI / 2)} by XXREAL_1:132; then A1: ].0,(PI / 2).[ c= ].0,(PI / 2).] by XBOOLE_1:7; PI / 4 < PI / 2 by XREAL_1:76; then ].0,(PI / 4).[ c= ].0,(PI / 2).[ by XXREAL_1:46; then ].0,(PI / 4).[ c= ].0,(PI / 2).] by A1, XBOOLE_1:1; then A2: ].0,(PI / 4).[ c= dom cosec by Th4, XBOOLE_1:1; assume A3: ( 1 < r & r < sqrt 2 ) ; ::_thesis: cosec . (arcsec1 r) = r / (sqrt ((r ^2) - 1)) then ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) by Th109; then arcsec1 r in ].0,(PI / 4).[ ; then cosec . (arcsec1 r) = 1 / (sin . (arcsec1 r)) by A2, RFUNCT_1:def_2 .= 1 / ((sqrt ((r ^2) - 1)) / r) by A3, Th113 .= r / (sqrt ((r ^2) - 1)) by XCMPLX_1:57 ; hence cosec . (arcsec1 r) = r / (sqrt ((r ^2) - 1)) ; ::_thesis: verum end; theorem :: SINCOS10:118 for r being Real st - (sqrt 2) < r & r < - 1 holds cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1))) proof let r be Real; ::_thesis: ( - (sqrt 2) < r & r < - 1 implies cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1))) ) set x = arcsec2 r; A1: ].((3 / 4) * PI),PI.[ c= dom cosec proof ].((3 / 4) * PI),PI.[ /\ (sin " {0}) = {} proof assume ].((3 / 4) * PI),PI.[ /\ (sin " {0}) <> {} ; ::_thesis: contradiction then consider rr being set such that A2: rr in ].((3 / 4) * PI),PI.[ /\ (sin " {0}) by XBOOLE_0:def_1; rr in sin " {0} by A2, XBOOLE_0:def_4; then A3: sin . rr in {0} by FUNCT_1:def_7; A4: ].((3 / 4) * PI),PI.[ c= ].0,PI.[ by XXREAL_1:46; rr in ].((3 / 4) * PI),PI.[ by A2, XBOOLE_0:def_4; then sin . rr <> 0 by A4, COMPTRIG:7; hence contradiction by A3, TARSKI:def_1; ::_thesis: verum end; then ( ].((3 / 4) * PI),PI.[ \ (sin " {0}) c= (dom sin) \ (sin " {0}) & ].((3 / 4) * PI),PI.[ misses sin " {0} ) by SIN_COS:24, XBOOLE_0:def_7, XBOOLE_1:33; then ].((3 / 4) * PI),PI.[ c= (dom sin) \ (sin " {0}) by XBOOLE_1:83; hence ].((3 / 4) * PI),PI.[ c= dom cosec by RFUNCT_1:def_2; ::_thesis: verum end; assume A5: ( - (sqrt 2) < r & r < - 1 ) ; ::_thesis: cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1))) then ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) by Th110; then arcsec2 r in ].((3 / 4) * PI),PI.[ ; then cosec . (arcsec2 r) = 1 / (sin . (arcsec2 r)) by A1, RFUNCT_1:def_2 .= 1 / (- ((sqrt ((r ^2) - 1)) / r)) by A5, Th114 .= - (1 / ((sqrt ((r ^2) - 1)) / r)) by XCMPLX_1:188 .= - (r / (sqrt ((r ^2) - 1))) by XCMPLX_1:57 ; hence cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1))) ; ::_thesis: verum end; theorem :: SINCOS10:119 for r being Real st - (sqrt 2) < r & r < - 1 holds sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1))) proof let r be Real; ::_thesis: ( - (sqrt 2) < r & r < - 1 implies sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1))) ) set x = arccosec1 r; A1: ].(- (PI / 2)),(- (PI / 4)).[ c= dom sec proof ].(- (PI / 2)),(- (PI / 4)).[ /\ (cos " {0}) = {} proof assume ].(- (PI / 2)),(- (PI / 4)).[ /\ (cos " {0}) <> {} ; ::_thesis: contradiction then consider rr being set such that A2: rr in ].(- (PI / 2)),(- (PI / 4)).[ /\ (cos " {0}) by XBOOLE_0:def_1; rr in cos " {0} by A2, XBOOLE_0:def_4; then A3: cos . rr in {0} by FUNCT_1:def_7; A4: ].(- (PI / 2)),(- (PI / 4)).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; rr in ].(- (PI / 2)),(- (PI / 4)).[ by A2, XBOOLE_0:def_4; then cos . rr <> 0 by A4, COMPTRIG:11; hence contradiction by A3, TARSKI:def_1; ::_thesis: verum end; then ( ].(- (PI / 2)),(- (PI / 4)).[ \ (cos " {0}) c= (dom cos) \ (cos " {0}) & ].(- (PI / 2)),(- (PI / 4)).[ misses cos " {0} ) by SIN_COS:24, XBOOLE_0:def_7, XBOOLE_1:33; then ].(- (PI / 2)),(- (PI / 4)).[ c= (dom cos) \ (cos " {0}) by XBOOLE_1:83; hence ].(- (PI / 2)),(- (PI / 4)).[ c= dom sec by RFUNCT_1:def_2; ::_thesis: verum end; assume A5: ( - (sqrt 2) < r & r < - 1 ) ; ::_thesis: sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1))) then ( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) ) by Th111; then arccosec1 r in ].(- (PI / 2)),(- (PI / 4)).[ ; then sec . (arccosec1 r) = 1 / (cos . (arccosec1 r)) by A1, RFUNCT_1:def_2 .= 1 / (- ((sqrt ((r ^2) - 1)) / r)) by A5, Th115 .= - (1 / ((sqrt ((r ^2) - 1)) / r)) by XCMPLX_1:188 .= - (r / (sqrt ((r ^2) - 1))) by XCMPLX_1:57 ; hence sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1))) ; ::_thesis: verum end; theorem :: SINCOS10:120 for r being Real st 1 < r & r < sqrt 2 holds sec . (arccosec2 r) = r / (sqrt ((r ^2) - 1)) proof let r be Real; ::_thesis: ( 1 < r & r < sqrt 2 implies sec . (arccosec2 r) = r / (sqrt ((r ^2) - 1)) ) set x = arccosec2 r; [.0,(PI / 2).[ = ].0,(PI / 2).[ \/ {0} by XXREAL_1:131; then ( ].(PI / 4),(PI / 2).[ c= ].0,(PI / 2).[ & ].0,(PI / 2).[ c= [.0,(PI / 2).[ ) by XBOOLE_1:7, XXREAL_1:46; then ].(PI / 4),(PI / 2).[ c= [.0,(PI / 2).[ by XBOOLE_1:1; then A1: ].(PI / 4),(PI / 2).[ c= dom sec by Th1, XBOOLE_1:1; assume A2: ( 1 < r & r < sqrt 2 ) ; ::_thesis: sec . (arccosec2 r) = r / (sqrt ((r ^2) - 1)) then ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) by Th112; then arccosec2 r in ].(PI / 4),(PI / 2).[ ; then sec . (arccosec2 r) = 1 / (cos . (arccosec2 r)) by A1, RFUNCT_1:def_2 .= 1 / ((sqrt ((r ^2) - 1)) / r) by A2, Th116 .= r / (sqrt ((r ^2) - 1)) by XCMPLX_1:57 ; hence sec . (arccosec2 r) = r / (sqrt ((r ^2) - 1)) ; ::_thesis: verum end; theorem Th121: :: SINCOS10:121 arcsec1 is_differentiable_on sec .: ].0,(PI / 2).[ proof set X = sec .: ].0,(PI / 2).[; set g1 = arcsec1 | (sec .: ].0,(PI / 2).[); set f = sec | [.0,(PI / 2).[; set g = (sec | [.0,(PI / 2).[) | ].0,(PI / 2).[; A1: (sec | [.0,(PI / 2).[) | ].0,(PI / 2).[ = sec | ].0,(PI / 2).[ by RELAT_1:74, XXREAL_1:22; A2: dom ((((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[) ") = rng (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[) by FUNCT_1:33 .= rng (sec | ].0,(PI / 2).[) by A1, RELAT_1:72 .= sec .: ].0,(PI / 2).[ by RELAT_1:115 ; A3: (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[) " = ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) " by RELAT_1:72 .= arcsec1 | ((sec | [.0,(PI / 2).[) .: ].0,(PI / 2).[) by RFUNCT_2:17 .= arcsec1 | (rng ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[)) by RELAT_1:115 .= arcsec1 | (rng (sec | ].0,(PI / 2).[)) by RELAT_1:74, XXREAL_1:22 .= arcsec1 | (sec .: ].0,(PI / 2).[) by RELAT_1:115 ; A4: (sec | [.0,(PI / 2).[) | ].0,(PI / 2).[ is_differentiable_on ].0,(PI / 2).[ by A1, Th5, FDIFF_2:16; now__::_thesis:_for_x0_being_Real_st_x0_in_].0,(PI_/_2).[_holds_ diff_(((sec_|_[.0,(PI_/_2).[)_|_].0,(PI_/_2).[),x0)_>_0 A5: for x0 being Real st x0 in ].0,(PI / 2).[ holds (sin . x0) / ((cos . x0) ^2) > 0 proof let x0 be Real; ::_thesis: ( x0 in ].0,(PI / 2).[ implies (sin . x0) / ((cos . x0) ^2) > 0 ) assume A6: x0 in ].0,(PI / 2).[ ; ::_thesis: (sin . x0) / ((cos . x0) ^2) > 0 ].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then A7: cos . x0 > 0 by A6, COMPTRIG:11; ].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46; then sin . x0 > 0 by A6, COMPTRIG:7; hence (sin . x0) / ((cos . x0) ^2) > 0 by A7; ::_thesis: verum end; let x0 be Real; ::_thesis: ( x0 in ].0,(PI / 2).[ implies diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x0) > 0 ) assume A8: x0 in ].0,(PI / 2).[ ; ::_thesis: diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x0) > 0 diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x0) = (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x0 by A4, A8, FDIFF_1:def_7 .= ((sec | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x0 by RELAT_1:74, XXREAL_1:22 .= (sec `| ].0,(PI / 2).[) . x0 by Th5, FDIFF_2:16 .= diff (sec,x0) by A8, Th5, FDIFF_1:def_7 .= (sin . x0) / ((cos . x0) ^2) by A8, Th5 ; hence diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x0) > 0 by A8, A5; ::_thesis: verum end; then A9: arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_on sec .: ].0,(PI / 2).[ by A2, A4, A3, Lm21, FDIFF_2:48; A10: for x being Real st x in sec .: ].0,(PI / 2).[ holds arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_in x proof let x be Real; ::_thesis: ( x in sec .: ].0,(PI / 2).[ implies arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_in x ) assume x in sec .: ].0,(PI / 2).[ ; ::_thesis: arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_in x then (arcsec1 | (sec .: ].0,(PI / 2).[)) | (sec .: ].0,(PI / 2).[) is_differentiable_in x by A9, FDIFF_1:def_6; hence arcsec1 | (sec .: ].0,(PI / 2).[) is_differentiable_in x by RELAT_1:72; ::_thesis: verum end; sec .: ].0,(PI / 2).[ c= dom arcsec1 by A2, A3, RELAT_1:60; hence arcsec1 is_differentiable_on sec .: ].0,(PI / 2).[ by A10, FDIFF_1:def_6; ::_thesis: verum end; theorem Th122: :: SINCOS10:122 arcsec2 is_differentiable_on sec .: ].(PI / 2),PI.[ proof set X = sec .: ].(PI / 2),PI.[; set g1 = arcsec2 | (sec .: ].(PI / 2),PI.[); set f = sec | ].(PI / 2),PI.]; set g = (sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[; A1: (sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[ = sec | ].(PI / 2),PI.[ by RELAT_1:74, XXREAL_1:21; A2: dom ((((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) | ].(PI / 2),PI.[) ") = rng (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) | ].(PI / 2),PI.[) by FUNCT_1:33 .= rng (sec | ].(PI / 2),PI.[) by A1, RELAT_1:72 .= sec .: ].(PI / 2),PI.[ by RELAT_1:115 ; A3: (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) | ].(PI / 2),PI.[) " = ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) " by RELAT_1:72 .= arcsec2 | ((sec | ].(PI / 2),PI.]) .: ].(PI / 2),PI.[) by RFUNCT_2:17 .= arcsec2 | (rng ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[)) by RELAT_1:115 .= arcsec2 | (rng (sec | ].(PI / 2),PI.[)) by RELAT_1:74, XXREAL_1:21 .= arcsec2 | (sec .: ].(PI / 2),PI.[) by RELAT_1:115 ; A4: (sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[ is_differentiable_on ].(PI / 2),PI.[ by A1, Th6, FDIFF_2:16; now__::_thesis:_for_x0_being_Real_st_x0_in_].(PI_/_2),PI.[_holds_ diff_(((sec_|_].(PI_/_2),PI.])_|_].(PI_/_2),PI.[),x0)_>_0 A5: for x0 being Real st x0 in ].(PI / 2),PI.[ holds (sin . x0) / ((cos . x0) ^2) > 0 proof let x0 be Real; ::_thesis: ( x0 in ].(PI / 2),PI.[ implies (sin . x0) / ((cos . x0) ^2) > 0 ) assume A6: x0 in ].(PI / 2),PI.[ ; ::_thesis: (sin . x0) / ((cos . x0) ^2) > 0 ].(PI / 2),PI.[ c= ].(PI / 2),((3 / 2) * PI).[ by COMPTRIG:5, XXREAL_1:46; then A7: cos . x0 < 0 by A6, COMPTRIG:13; ].(PI / 2),PI.[ c= ].0,PI.[ by XXREAL_1:46; then sin . x0 > 0 by A6, COMPTRIG:7; hence (sin . x0) / ((cos . x0) ^2) > 0 by A7; ::_thesis: verum end; let x0 be Real; ::_thesis: ( x0 in ].(PI / 2),PI.[ implies diff (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[),x0) > 0 ) assume A8: x0 in ].(PI / 2),PI.[ ; ::_thesis: diff (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[),x0) > 0 diff (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[),x0) = (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) `| ].(PI / 2),PI.[) . x0 by A4, A8, FDIFF_1:def_7 .= ((sec | ].(PI / 2),PI.[) `| ].(PI / 2),PI.[) . x0 by RELAT_1:74, XXREAL_1:21 .= (sec `| ].(PI / 2),PI.[) . x0 by Th6, FDIFF_2:16 .= diff (sec,x0) by A8, Th6, FDIFF_1:def_7 .= (sin . x0) / ((cos . x0) ^2) by A8, Th6 ; hence diff (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[),x0) > 0 by A8, A5; ::_thesis: verum end; then A9: arcsec2 | (sec .: ].(PI / 2),PI.[) is_differentiable_on sec .: ].(PI / 2),PI.[ by A2, A4, A3, Lm22, FDIFF_2:48; A10: for x being Real st x in sec .: ].(PI / 2),PI.[ holds arcsec2 | (sec .: ].(PI / 2),PI.[) is_differentiable_in x proof let x be Real; ::_thesis: ( x in sec .: ].(PI / 2),PI.[ implies arcsec2 | (sec .: ].(PI / 2),PI.[) is_differentiable_in x ) assume x in sec .: ].(PI / 2),PI.[ ; ::_thesis: arcsec2 | (sec .: ].(PI / 2),PI.[) is_differentiable_in x then (arcsec2 | (sec .: ].(PI / 2),PI.[)) | (sec .: ].(PI / 2),PI.[) is_differentiable_in x by A9, FDIFF_1:def_6; hence arcsec2 | (sec .: ].(PI / 2),PI.[) is_differentiable_in x by RELAT_1:72; ::_thesis: verum end; sec .: ].(PI / 2),PI.[ c= dom arcsec2 by A2, A3, RELAT_1:60; hence arcsec2 is_differentiable_on sec .: ].(PI / 2),PI.[ by A10, FDIFF_1:def_6; ::_thesis: verum end; theorem Th123: :: SINCOS10:123 arccosec1 is_differentiable_on cosec .: ].(- (PI / 2)),0.[ proof set X = cosec .: ].(- (PI / 2)),0.[; set g1 = arccosec1 | (cosec .: ].(- (PI / 2)),0.[); set f = cosec | [.(- (PI / 2)),0.[; set g = (cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[; A1: (cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[ = cosec | ].(- (PI / 2)),0.[ by RELAT_1:74, XXREAL_1:22; A2: dom ((((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) ") = rng (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) by FUNCT_1:33 .= rng (cosec | ].(- (PI / 2)),0.[) by A1, RELAT_1:72 .= cosec .: ].(- (PI / 2)),0.[ by RELAT_1:115 ; A3: (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) " = ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) " by RELAT_1:72 .= arccosec1 | ((cosec | [.(- (PI / 2)),0.[) .: ].(- (PI / 2)),0.[) by RFUNCT_2:17 .= arccosec1 | (rng ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[)) by RELAT_1:115 .= arccosec1 | (rng (cosec | ].(- (PI / 2)),0.[)) by RELAT_1:74, XXREAL_1:22 .= arccosec1 | (cosec .: ].(- (PI / 2)),0.[) by RELAT_1:115 ; A4: (cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[ is_differentiable_on ].(- (PI / 2)),0.[ by A1, Th7, FDIFF_2:16; now__::_thesis:_for_x0_being_Real_st_x0_in_].(-_(PI_/_2)),0.[_holds_ diff_(((cosec_|_[.(-_(PI_/_2)),0.[)_|_].(-_(PI_/_2)),0.[),x0)_<_0 A5: for x0 being Real st x0 in ].(- (PI / 2)),0.[ holds - ((cos . x0) / ((sin . x0) ^2)) < 0 proof let x0 be Real; ::_thesis: ( x0 in ].(- (PI / 2)),0.[ implies - ((cos . x0) / ((sin . x0) ^2)) < 0 ) assume A6: x0 in ].(- (PI / 2)),0.[ ; ::_thesis: - ((cos . x0) / ((sin . x0) ^2)) < 0 then x0 < 0 by XXREAL_1:4; then A7: x0 + (2 * PI) < 0 + (2 * PI) by XREAL_1:8; ].(- (PI / 2)),0.[ \/ {(- (PI / 2))} = [.(- (PI / 2)),0.[ by XXREAL_1:131; then ].(- (PI / 2)),0.[ c= [.(- (PI / 2)),0.[ by XBOOLE_1:7; then ].(- (PI / 2)),0.[ c= ].(- PI),0.[ by Lm3, XBOOLE_1:1; then - PI < x0 by A6, XXREAL_1:4; then (- PI) + (2 * PI) < x0 + (2 * PI) by XREAL_1:8; then x0 + (2 * PI) in ].PI,(2 * PI).[ by A7; then sin . (x0 + (2 * PI)) < 0 by COMPTRIG:9; then A8: sin . x0 < 0 by SIN_COS:78; ].(- (PI / 2)),0.[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then cos . x0 > 0 by A6, COMPTRIG:11; hence - ((cos . x0) / ((sin . x0) ^2)) < 0 by A8; ::_thesis: verum end; let x0 be Real; ::_thesis: ( x0 in ].(- (PI / 2)),0.[ implies diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x0) < 0 ) assume A9: x0 in ].(- (PI / 2)),0.[ ; ::_thesis: diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x0) < 0 diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x0) = (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) `| ].(- (PI / 2)),0.[) . x0 by A4, A9, FDIFF_1:def_7 .= ((cosec | ].(- (PI / 2)),0.[) `| ].(- (PI / 2)),0.[) . x0 by RELAT_1:74, XXREAL_1:22 .= (cosec `| ].(- (PI / 2)),0.[) . x0 by Th7, FDIFF_2:16 .= diff (cosec,x0) by A9, Th7, FDIFF_1:def_7 .= - ((cos . x0) / ((sin . x0) ^2)) by A9, Th7 ; hence diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x0) < 0 by A9, A5; ::_thesis: verum end; then A10: arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_on cosec .: ].(- (PI / 2)),0.[ by A2, A4, A3, Lm23, FDIFF_2:48; A11: for x being Real st x in cosec .: ].(- (PI / 2)),0.[ holds arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x proof let x be Real; ::_thesis: ( x in cosec .: ].(- (PI / 2)),0.[ implies arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x ) assume x in cosec .: ].(- (PI / 2)),0.[ ; ::_thesis: arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x then (arccosec1 | (cosec .: ].(- (PI / 2)),0.[)) | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x by A10, FDIFF_1:def_6; hence arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is_differentiable_in x by RELAT_1:72; ::_thesis: verum end; cosec .: ].(- (PI / 2)),0.[ c= dom arccosec1 by A2, A3, RELAT_1:60; hence arccosec1 is_differentiable_on cosec .: ].(- (PI / 2)),0.[ by A11, FDIFF_1:def_6; ::_thesis: verum end; theorem Th124: :: SINCOS10:124 arccosec2 is_differentiable_on cosec .: ].0,(PI / 2).[ proof set X = cosec .: ].0,(PI / 2).[; set g1 = arccosec2 | (cosec .: ].0,(PI / 2).[); set f = cosec | ].0,(PI / 2).]; set g = (cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[; A1: (cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[ = cosec | ].0,(PI / 2).[ by RELAT_1:74, XXREAL_1:21; A2: dom ((((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) | ].0,(PI / 2).[) ") = rng (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) | ].0,(PI / 2).[) by FUNCT_1:33 .= rng (cosec | ].0,(PI / 2).[) by A1, RELAT_1:72 .= cosec .: ].0,(PI / 2).[ by RELAT_1:115 ; A3: (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) | ].0,(PI / 2).[) " = ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) " by RELAT_1:72 .= arccosec2 | ((cosec | ].0,(PI / 2).]) .: ].0,(PI / 2).[) by RFUNCT_2:17 .= arccosec2 | (rng ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[)) by RELAT_1:115 .= arccosec2 | (rng (cosec | ].0,(PI / 2).[)) by RELAT_1:74, XXREAL_1:21 .= arccosec2 | (cosec .: ].0,(PI / 2).[) by RELAT_1:115 ; A4: (cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[ is_differentiable_on ].0,(PI / 2).[ by A1, Th8, FDIFF_2:16; now__::_thesis:_for_x0_being_Real_st_x0_in_].0,(PI_/_2).[_holds_ diff_(((cosec_|_].0,(PI_/_2).])_|_].0,(PI_/_2).[),x0)_<_0 A5: for x0 being Real st x0 in ].0,(PI / 2).[ holds - ((cos . x0) / ((sin . x0) ^2)) < 0 proof let x0 be Real; ::_thesis: ( x0 in ].0,(PI / 2).[ implies - ((cos . x0) / ((sin . x0) ^2)) < 0 ) assume A6: x0 in ].0,(PI / 2).[ ; ::_thesis: - ((cos . x0) / ((sin . x0) ^2)) < 0 ].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then A7: cos . x0 > 0 by A6, COMPTRIG:11; ].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46; then sin . x0 > 0 by A6, COMPTRIG:7; hence - ((cos . x0) / ((sin . x0) ^2)) < 0 by A7; ::_thesis: verum end; let x0 be Real; ::_thesis: ( x0 in ].0,(PI / 2).[ implies diff (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),x0) < 0 ) assume A8: x0 in ].0,(PI / 2).[ ; ::_thesis: diff (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),x0) < 0 diff (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),x0) = (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x0 by A4, A8, FDIFF_1:def_7 .= ((cosec | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x0 by RELAT_1:74, XXREAL_1:21 .= (cosec `| ].0,(PI / 2).[) . x0 by Th8, FDIFF_2:16 .= diff (cosec,x0) by A8, Th8, FDIFF_1:def_7 .= - ((cos . x0) / ((sin . x0) ^2)) by A8, Th8 ; hence diff (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),x0) < 0 by A8, A5; ::_thesis: verum end; then A9: arccosec2 | (cosec .: ].0,(PI / 2).[) is_differentiable_on cosec .: ].0,(PI / 2).[ by A2, A4, A3, Lm24, FDIFF_2:48; A10: for x being Real st x in cosec .: ].0,(PI / 2).[ holds arccosec2 | (cosec .: ].0,(PI / 2).[) is_differentiable_in x proof let x be Real; ::_thesis: ( x in cosec .: ].0,(PI / 2).[ implies arccosec2 | (cosec .: ].0,(PI / 2).[) is_differentiable_in x ) assume x in cosec .: ].0,(PI / 2).[ ; ::_thesis: arccosec2 | (cosec .: ].0,(PI / 2).[) is_differentiable_in x then (arccosec2 | (cosec .: ].0,(PI / 2).[)) | (cosec .: ].0,(PI / 2).[) is_differentiable_in x by A9, FDIFF_1:def_6; hence arccosec2 | (cosec .: ].0,(PI / 2).[) is_differentiable_in x by RELAT_1:72; ::_thesis: verum end; cosec .: ].0,(PI / 2).[ c= dom arccosec2 by A2, A3, RELAT_1:60; hence arccosec2 is_differentiable_on cosec .: ].0,(PI / 2).[ by A10, FDIFF_1:def_6; ::_thesis: verum end; theorem :: SINCOS10:125 sec .: ].0,(PI / 2).[ is open proof for x0 being Real st x0 in ].0,(PI / 2).[ holds diff (sec,x0) > 0 proof let x0 be Real; ::_thesis: ( x0 in ].0,(PI / 2).[ implies diff (sec,x0) > 0 ) assume A1: x0 in ].0,(PI / 2).[ ; ::_thesis: diff (sec,x0) > 0 ].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then A2: cos . x0 > 0 by A1, COMPTRIG:11; ].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46; then sin . x0 > 0 by A1, COMPTRIG:7; then (sin . x0) / ((cos . x0) ^2) > 0 / ((cos . x0) ^2) by A2; hence diff (sec,x0) > 0 by A1, Th5; ::_thesis: verum end; then rng (sec | ].0,(PI / 2).[) is open by Lm10, Th5, FDIFF_2:41; hence sec .: ].0,(PI / 2).[ is open by RELAT_1:115; ::_thesis: verum end; theorem :: SINCOS10:126 sec .: ].(PI / 2),PI.[ is open proof for x0 being Real st x0 in ].(PI / 2),PI.[ holds diff (sec,x0) > 0 proof let x0 be Real; ::_thesis: ( x0 in ].(PI / 2),PI.[ implies diff (sec,x0) > 0 ) assume A1: x0 in ].(PI / 2),PI.[ ; ::_thesis: diff (sec,x0) > 0 ].(PI / 2),PI.[ c= ].(PI / 2),((3 / 2) * PI).[ by COMPTRIG:5, XXREAL_1:46; then A2: cos . x0 < 0 by A1, COMPTRIG:13; ].(PI / 2),PI.[ c= ].0,PI.[ by XXREAL_1:46; then sin . x0 > 0 by A1, COMPTRIG:7; then (sin . x0) / ((cos . x0) ^2) > 0 / ((cos . x0) ^2) by A2; hence diff (sec,x0) > 0 by A1, Th6; ::_thesis: verum end; then rng (sec | ].(PI / 2),PI.[) is open by Lm12, Th6, FDIFF_2:41; hence sec .: ].(PI / 2),PI.[ is open by RELAT_1:115; ::_thesis: verum end; theorem :: SINCOS10:127 cosec .: ].(- (PI / 2)),0.[ is open proof for x0 being Real st x0 in ].(- (PI / 2)),0.[ holds diff (cosec,x0) < 0 proof let x0 be Real; ::_thesis: ( x0 in ].(- (PI / 2)),0.[ implies diff (cosec,x0) < 0 ) assume A1: x0 in ].(- (PI / 2)),0.[ ; ::_thesis: diff (cosec,x0) < 0 then x0 < 0 by XXREAL_1:4; then A2: x0 + (2 * PI) < 0 + (2 * PI) by XREAL_1:8; ].(- (PI / 2)),0.[ \/ {(- (PI / 2))} = [.(- (PI / 2)),0.[ by XXREAL_1:131; then ].(- (PI / 2)),0.[ c= [.(- (PI / 2)),0.[ by XBOOLE_1:7; then ].(- (PI / 2)),0.[ c= ].(- PI),0.[ by Lm3, XBOOLE_1:1; then - PI < x0 by A1, XXREAL_1:4; then (- PI) + (2 * PI) < x0 + (2 * PI) by XREAL_1:8; then x0 + (2 * PI) in ].PI,(2 * PI).[ by A2; then sin . (x0 + (2 * PI)) < 0 by COMPTRIG:9; then A3: sin . x0 < 0 by SIN_COS:78; ].(- (PI / 2)),0.[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then cos . x0 > 0 by A1, COMPTRIG:11; then - ((cos . x0) / ((sin . x0) ^2)) < - 0 by A3; hence diff (cosec,x0) < 0 by A1, Th7; ::_thesis: verum end; then rng (cosec | ].(- (PI / 2)),0.[) is open by Lm16, Th7, FDIFF_2:41; hence cosec .: ].(- (PI / 2)),0.[ is open by RELAT_1:115; ::_thesis: verum end; theorem :: SINCOS10:128 cosec .: ].0,(PI / 2).[ is open proof for x0 being Real st x0 in ].0,(PI / 2).[ holds diff (cosec,x0) < 0 proof let x0 be Real; ::_thesis: ( x0 in ].0,(PI / 2).[ implies diff (cosec,x0) < 0 ) assume A1: x0 in ].0,(PI / 2).[ ; ::_thesis: diff (cosec,x0) < 0 ].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46; then A2: cos . x0 > 0 by A1, COMPTRIG:11; ].0,(PI / 2).[ c= ].0,PI.[ by COMPTRIG:5, XXREAL_1:46; then sin . x0 > 0 by A1, COMPTRIG:7; then - ((cos . x0) / ((sin . x0) ^2)) < - 0 by A2; hence diff (cosec,x0) < 0 by A1, Th8; ::_thesis: verum end; then rng (cosec | ].0,(PI / 2).[) is open by Lm18, Th8, FDIFF_2:41; hence cosec .: ].0,(PI / 2).[ is open by RELAT_1:115; ::_thesis: verum end; theorem :: SINCOS10:129 arcsec1 | (sec .: ].0,(PI / 2).[) is continuous by Th121, FDIFF_1:25; theorem :: SINCOS10:130 arcsec2 | (sec .: ].(PI / 2),PI.[) is continuous by Th122, FDIFF_1:25; theorem :: SINCOS10:131 arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is continuous by Th123, FDIFF_1:25; theorem :: SINCOS10:132 arccosec2 | (cosec .: ].0,(PI / 2).[) is continuous by Th124, FDIFF_1:25;