let y be object ; 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 object 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 3;
reconsider x = x as Real by A1;
A3: y =
(AffineMap ((1 / (2 * PI)),1)) . x
by A1, A2, Lm52, FUNCT_1:49
.=
((1 / (2 * PI)) * x) + 1
by FCONT_1:def 4
.=
(x / (2 * PI)) + 1
by XCMPLX_1:99
;
then reconsider y = y as Real ;
x < PI
by A1, Lm52, XXREAL_1:3;
then
x / (2 * PI) < (1 * PI) / (2 * PI)
by XREAL_1:74;
then
x / (2 * PI) < 1 / 2
by XCMPLX_1:91;
then A4:
(x / (2 * PI)) + 1 < (1 / 2) + 1
by XREAL_1:6;
0 <= x
by A1, Lm52, XXREAL_1:3;
then
0 + 1 <= (x / (2 * PI)) + 1
by XREAL_1:6;
then
1 / 2 < y
by A3, XXREAL_0:2;
hence
y in ].(1 / 2),((1 / 2) + p1).[
by A3, A4, XXREAL_1:4; verum