let th1, th2 be Real; ( 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
; 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
; contradiction
now 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
;
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.[
A13:
for
th being
Element of
REAL st
th in [.th1,th2.] holds
th in [.0,1.]
].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;
( th in ].0,1.[ & diff (tan,th) = 0 )thus
(
th in ].0,1.[ &
diff (
tan,
th)
= 0 )
by A10, A17;
verum end; suppose A18:
th2 < th1
;
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.[
A22:
for
th being
Element of
REAL st
th in [.th2,th1.] holds
th in [.0,1.]
].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;
( th in ].0,1.[ & diff (tan,th) = 0 )thus
(
th in ].0,1.[ &
diff (
tan,
th)
= 0 )
by A19, A26;
verum end; end; end;
hence
contradiction
by Lm15; verum