begin
begin
deffunc H1( Integer) -> Element of REAL = (2 * PI) * $1;
Lm1:
[.((- (PI / 2)) + H1( 0 )),((PI / 2) + H1( 0 )).] = [.(- (PI / 2)),(PI / 2).]
;
Lm2:
[.((PI / 2) + H1( 0 )),(((3 / 2) * PI) + H1( 0 )).] = [.(PI / 2),((3 / 2) * PI).]
;
Lm3:
[.H1( 0 ),(PI + H1( 0 )).] = [.0,PI.]
;
Lm4:
[.(PI + H1( 0 )),((2 * PI) + H1( 0 )).] = [.PI,(2 * PI).]
;
Lm5:
for r, s being real number st (r ^2) + (s ^2) = 1 holds
( - 1 <= r & r <= 1 )
Lm6:
PI / 2 < PI / 1
by XREAL_1:76;
Lm7:
1 * PI < (3 / 2) * PI
by XREAL_1:68;
Lm8:
0 + H1(1) < (PI / 2) + H1(1)
by XREAL_1:6;
Lm9:
(3 / 2) * PI < 2 * PI
by XREAL_1:68;
Lm10:
1 * PI < 2 * PI
by XREAL_1:68;
Lm11:
now for i being integer number
for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]
let i be
integer number ;
for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]let r be
real number ;
for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]let p1,
p2 be
real number ;
( r in [.(p1 + H1(i)),(p2 + H1(i)).] implies r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] )assume A1:
r in [.(p1 + H1(i)),(p2 + H1(i)).]
;
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]then
r <= p2 + H1(
i)
by XXREAL_1:1;
then A2:
r + (2 * PI) <= (p2 + H1(i)) + (2 * PI)
by XREAL_1:6;
p1 + H1(
i)
<= r
by A1, XXREAL_1:1;
then
(p1 + H1(i)) + (2 * PI) <= r + (2 * PI)
by XREAL_1:6;
hence
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]
by A2, XXREAL_1:1;
verum
end;
Lm12:
now for i being integer number
for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL
let i be
integer number ;
for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REALlet r be
real number ;
for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REALlet p1,
p2 be
real number ;
( r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL implies r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL )assume
r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL
;
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REALthen
r in [.(p1 + H1(i)),(p2 + H1(i)).]
by XBOOLE_0:def 4;
then
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]
by Lm11;
hence
r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL
by XBOOLE_0:def 4;
verum
end;
Lm13:
now for i being integer number
for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]
let i be
integer number ;
for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]let r be
real number ;
for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]let p1,
p2 be
real number ;
( r in [.(p1 + H1(i)),(p2 + H1(i)).] implies r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] )assume A1:
r in [.(p1 + H1(i)),(p2 + H1(i)).]
;
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]then
r <= p2 + H1(
i)
by XXREAL_1:1;
then A2:
r - (2 * PI) <= (p2 + H1(i)) - (2 * PI)
by XREAL_1:9;
p1 + H1(
i)
<= r
by A1, XXREAL_1:1;
then
(p1 + H1(i)) - (2 * PI) <= r - (2 * PI)
by XREAL_1:9;
hence
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]
by A2, XXREAL_1:1;
verum
end;
Lm14:
now for i being integer number
for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL
let i be
integer number ;
for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REALlet r be
real number ;
for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REALlet p1,
p2 be
real number ;
( r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL implies r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL )assume
r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL
;
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REALthen
r in [.(p1 + H1(i)),(p2 + H1(i)).]
by XBOOLE_0:def 4;
then
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]
by Lm13;
hence
r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL
by XBOOLE_0:def 4;
verum
end;
begin
Lm15:
arcsin " = sin | [.(- (PI / 2)),(PI / 2).]
by FUNCT_1:43;
begin
Lm16:
arccos " = cos | [.0,PI.]
by FUNCT_1:43;