let cn be Real; for q being Point of (TOP-REAL 2) st cn < 1 & q `2 < 0 & (q `1) / |.q.| >= cn holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
( p `2 < 0 & p `1 >= 0 )
let q be Point of (TOP-REAL 2); ( cn < 1 & q `2 < 0 & (q `1) / |.q.| >= cn implies for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
( p `2 < 0 & p `1 >= 0 ) )
assume that
A1:
cn < 1
and
A2:
q `2 < 0
and
A3:
(q `1) / |.q.| >= cn
; for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
( p `2 < 0 & p `1 >= 0 )
A4:
1 - cn > 0
by A1, XREAL_1:149;
let p be Point of (TOP-REAL 2); ( p = (cn -FanMorphS) . q implies ( p `2 < 0 & p `1 >= 0 ) )
set qz = p;
assume
p = (cn -FanMorphS) . q
; ( p `2 < 0 & p `1 >= 0 )
then A5:
p = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 - cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2)))))]|
by A2, A3, Th113;
then A6:
p `2 = |.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 - cn)) ^2))))
by EUCLID:52;
A7:
((q `1) / |.q.|) - cn >= 0
by A3, XREAL_1:48;
A8:
|.q.| <> 0
by A2, JGRAPH_2:3, TOPRNS_1:24;
then A9:
|.q.| ^2 > 0
by SQUARE_1:12;
( |.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) & 0 + ((q `1) ^2) < ((q `1) ^2) + ((q `2) ^2) )
by A2, JGRAPH_3:1, SQUARE_1:12, XREAL_1:8;
then
((q `1) ^2) / (|.q.| ^2) < (|.q.| ^2) / (|.q.| ^2)
by A9, XREAL_1:74;
then
((q `1) ^2) / (|.q.| ^2) < 1
by A9, XCMPLX_1:60;
then
((q `1) / |.q.|) ^2 < 1
by XCMPLX_1:76;
then
1 > (q `1) / |.q.|
by SQUARE_1:52;
then
1 - cn > ((q `1) / |.q.|) - cn
by XREAL_1:9;
then
- (1 - cn) < - (((q `1) / |.q.|) - cn)
by XREAL_1:24;
then
(- (1 - cn)) / (1 - cn) < (- (((q `1) / |.q.|) - cn)) / (1 - cn)
by A4, XREAL_1:74;
then
- 1 < (- (((q `1) / |.q.|) - cn)) / (1 - cn)
by A4, XCMPLX_1:197;
then
((- (((q `1) / |.q.|) - cn)) / (1 - cn)) ^2 < 1 ^2
by A4, A7, SQUARE_1:50;
hence
( p `2 < 0 & p `1 >= 0 )
by A5, A8, A4, A6, A7, Lm13, EUCLID:52, XREAL_1:132; verum