let n be Nat; :: thesis: for x being Real st 0 < x & x < PI / 2 holds
( 0 < sin . x & sin . x < 1 )
let x be Real; :: thesis: ( 0 < x & x < PI / 2 implies ( 0 < sin . x & sin . x < 1 ) )
assume A1: ( 0 < x & x < PI / 2 ) ; :: thesis: ( 0 < sin . x & sin . x < 1 )
reconsider t = sin . x as Real ;
x < PI by A1, XXREAL_0:2, COMPTRIG:5;
then A2: x in ].0,PI.[ by A1, XXREAL_1:4;
A3: x in ].(- (PI / 2)),(PI / 2).[ by A1, XXREAL_1:4;
then A5: x in [.(- (PI / 2)),(PI / 2).] by XXREAL_1:16;
A4: dom sin = REAL by FUNCT_2:def 1;
then A6: x in dom (sin | [.(- (PI / 2)),(PI / 2).]) by XXREAL_1:16, A3;
A7: PI / 2 in dom (sin | [.(- (PI / 2)),(PI / 2).]) by A4, XXREAL_1:1, COMPTRIG:5;
reconsider x1 = x, x2 = PI / 2 as ExtReal ;
( sin . x1 = (sin | [.(- (PI / 2)),(PI / 2).]) . x1 & sin . x2 = (sin | [.(- (PI / 2)),(PI / 2).]) . x2 ) by A5, COMPTRIG:5, XXREAL_1:1, FUNCT_1:49;
hence ( 0 < sin . x & sin . x < 1 ) by A2, A1, A6, A7, COMPTRIG:7, COMPTRIG:23, VALUED_0:def 13, SIN_COS:76; :: thesis: verum