let y be set ; TARSKI:def 3 ( not y in rng ((AffineMap (- (1 / (2 * PI ))),1) | (R^1 E)) or y in ].(1 / 2),((1 / 2) + p1).[ )
assume
y in rng ((AffineMap (- (1 / (2 * PI ))),1) | (R^1 E))
; y in ].(1 / 2),((1 / 2) + p1).[
then consider x being set such that
A1:
x in dom ((AffineMap (- (1 / (2 * PI ))),1) | (R^1 E))
and
A2:
((AffineMap (- (1 / (2 * PI ))),1) | (R^1 E)) . x = y
by FUNCT_1:def 5;
reconsider x = x as Real by A1;
A3: y =
(AffineMap (- (1 / (2 * PI ))),1) . x
by A1, A2, Lm49, FUNCT_1:72
.=
((- (1 / (2 * PI ))) * x) + 1
by JORDAN16:def 3
.=
(- ((1 / (2 * PI )) * x)) + 1
.=
(- (x / (2 * PI ))) + 1
by XCMPLX_1:100
;
then reconsider y = y as Real ;
x < PI
by A1, Lm49, XXREAL_1:3;
then
x / (2 * PI ) < (1 * PI ) / (2 * PI )
by XREAL_1:76;
then
x / (2 * PI ) < 1 / 2
by XCMPLX_1:92;
then
- (x / (2 * PI )) > - (1 / 2)
by XREAL_1:26;
then A4:
(- (x / (2 * PI ))) + 1 > (- (1 / 2)) + 1
by XREAL_1:8;
0 <= x
by A1, Lm49, XXREAL_1:3;
then
0 + 1 >= (- (x / (2 * PI ))) + 1
by XREAL_1:8;
then
y < 3 / 2
by A3, XXREAL_0:2;
hence
y in ].(1 / 2),((1 / 2) + p1).[
by A3, A4, XXREAL_1:4; verum