let th1, th2 be Real; :: thesis: ( th1 in ].0,1.[ & th2 in ].0,1.[ & tan . th1 = tan . th2 implies th1 = th2 )
assume that
A1: th1 in ].0,1.[ and
A2: th2 in ].0,1.[ and
A3: tan . th1 = tan . th2 ; :: thesis: th1 = th2
A4: 0 < th1 by A1, XXREAL_1:4;
A5: th1 < 1 by A1, XXREAL_1:4;
A6: 0 < th2 by A2, XXREAL_1:4;
A7: th2 < 1 by A2, XXREAL_1:4;
assume A8: th1 <> th2 ; :: thesis: contradiction
now :: thesis: ex th being Real st
( th in ].0,1.[ & diff (tan,th) = 0 )
per cases ( th1 < th2 or th2 < th1 ) by A8, XXREAL_0:1;
suppose A9: th1 < th2 ; :: thesis: ex th being Real st
( th in ].0,1.[ & diff (tan,th) = 0 )
A10: for th being Element of REAL st th in ].th1,th2.[ holds
th in ].0,1.[
proof
let th be Element of REAL ; :: thesis: ( th in ].th1,th2.[ implies th in ].0,1.[ )
assume A11: th in ].th1,th2.[ ; :: thesis: th in ].0,1.[
then A12: th1 < th by XXREAL_1:4;
th < th2 by A11, XXREAL_1:4;
then th < 1 by A7, XXREAL_0:2;
hence th in ].0,1.[ by A4, A12, XXREAL_1:4; :: thesis: verum
end;
A13: for th being Element of REAL st th in [.th1,th2.] holds
th in [.0,1.]
proof
let th be Element of REAL ; :: thesis: ( th in [.th1,th2.] implies th in [.0,1.] )
assume A14: th in [.th1,th2.] ; :: thesis: th in [.0,1.]
then A15: th1 <= th by XXREAL_1:1;
th <= th2 by A14, XXREAL_1:1;
then th <= 1 by A7, XXREAL_0:2;
hence th in [.0,1.] by A4, A15, XXREAL_1:1; :: thesis: verum
end;
].th1,th2.[ c= ].0,1.[ by A10, SUBSET_1:2;
then A16: tan is_differentiable_on ].th1,th2.[ by Lm15, FDIFF_1:26;
( [.th1,th2.] c= [.0,1.] & tan | [.th1,th2.] is continuous ) by A13, Th70, FCONT_1:16, SUBSET_1:2;
then consider r being Real such that
A17: ( r in ].th1,th2.[ & diff (tan,r) = 0 ) by A3, A9, A16, Th69, ROLLE:1, XBOOLE_1:1;
take th = r; :: thesis: ( th in ].0,1.[ & diff (tan,th) = 0 )
thus ( th in ].0,1.[ & diff (tan,th) = 0 ) by A10, A17; :: thesis: verum
end;
suppose A18: th2 < th1 ; :: thesis: ex th being Real st
( th in ].0,1.[ & diff (tan,th) = 0 )
A19: for th being Element of REAL st th in ].th2,th1.[ holds
th in ].0,1.[
proof
let th be Element of REAL ; :: thesis: ( th in ].th2,th1.[ implies th in ].0,1.[ )
assume A20: th in ].th2,th1.[ ; :: thesis: th in ].0,1.[
then A21: th2 < th by XXREAL_1:4;
th < th1 by A20, XXREAL_1:4;
then th < 1 by A5, XXREAL_0:2;
hence th in ].0,1.[ by A6, A21, XXREAL_1:4; :: thesis: verum
end;
A22: for th being Element of REAL st th in [.th2,th1.] holds
th in [.0,1.]
proof
let th be Element of REAL ; :: thesis: ( th in [.th2,th1.] implies th in [.0,1.] )
assume A23: th in [.th2,th1.] ; :: thesis: th in [.0,1.]
then A24: th2 <= th by XXREAL_1:1;
th <= th1 by A23, XXREAL_1:1;
then th <= 1 by A5, XXREAL_0:2;
hence th in [.0,1.] by A6, A24, XXREAL_1:1; :: thesis: verum
end;
].th2,th1.[ c= ].0,1.[ by A19, SUBSET_1:2;
then A25: tan is_differentiable_on ].th2,th1.[ by Lm15, FDIFF_1:26;
( [.th2,th1.] c= [.0,1.] & tan | [.th2,th1.] is continuous ) by A22, Th70, FCONT_1:16, SUBSET_1:2;
then consider r being Real such that
A26: ( r in ].th2,th1.[ & diff (tan,r) = 0 ) by A3, A18, A25, Th69, ROLLE:1, XBOOLE_1:1;
take th = r; :: thesis: ( th in ].0,1.[ & diff (tan,th) = 0 )
thus ( th in ].0,1.[ & diff (tan,th) = 0 ) by A19, A26; :: thesis: verum
end;
end;
end;
hence contradiction by Lm15; :: thesis: verum