let cn be Real; for q being Point of (TOP-REAL 2) st - 1 < cn & 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); ( - 1 < cn & 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:
- 1 < cn
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:148;
A5:
((q `1) / |.q.|) - cn < 0
by A3, XREAL_1:49;
then
- (((q `1) / |.q.|) - cn) > 0
by XREAL_1:58;
then
(- (1 + cn)) / (1 + cn) < (- (((q `1) / |.q.|) - cn)) / (1 + cn)
by A4, XREAL_1:74;
then A6:
- 1 < (- (((q `1) / |.q.|) - cn)) / (1 + cn)
by A4, XCMPLX_1:197;
A7:
|.q.| <> 0
by A2, JGRAPH_2:3, TOPRNS_1:24;
then A8:
|.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 A8, XREAL_1:74;
then
((q `1) ^2) / (|.q.| ^2) < 1
by A8, 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
(- (((q `1) / |.q.|) - cn)) / (1 + cn) < 1
by A4, XREAL_1:191;
then
((- (((q `1) / |.q.|) - cn)) / (1 + cn)) ^2 < 1 ^2
by A6, SQUARE_1:50;
then
1 - (((- (((q `1) / |.q.|) - cn)) / (1 + cn)) ^2) > 0
by XREAL_1:50;
then
sqrt (1 - (((- (((q `1) / |.q.|) - cn)) / (1 + cn)) ^2)) > 0
by SQUARE_1:25;
then
sqrt (1 - (((- (((q `1) / |.q.|) - cn)) ^2) / ((1 + cn) ^2))) > 0
by XCMPLX_1:76;
then
sqrt (1 - (((((q `1) / |.q.|) - cn) ^2) / ((1 + cn) ^2))) > 0
;
then
- (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))) > 0
by XCMPLX_1:76;
then A9:
- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2))) < 0
;
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
p = |[(|.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn))),(|.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))))]|
by A2, A3, Th114;
then A10:
( p `2 = |.q.| * (- (sqrt (1 - (((((q `1) / |.q.|) - cn) / (1 + cn)) ^2)))) & p `1 = |.q.| * ((((q `1) / |.q.|) - cn) / (1 + cn)) )
by EUCLID:52;
(((q `1) / |.q.|) - cn) / (1 + cn) < 0
by A1, A5, XREAL_1:141, XREAL_1:148;
hence
( p `2 < 0 & p `1 < 0 )
by A7, A10, A9, XREAL_1:132; verum