let sn be Real; for q being Point of (TOP-REAL 2) st - 1 < sn & q `1 < 0 & (q `2 ) / |.q.| < sn holds
for p being Point of (TOP-REAL 2) st p = (sn -FanMorphW ) . q holds
( p `1 < 0 & p `2 < 0 )
let q be Point of (TOP-REAL 2); ( - 1 < sn & q `1 < 0 & (q `2 ) / |.q.| < sn implies for p being Point of (TOP-REAL 2) st p = (sn -FanMorphW ) . q holds
( p `1 < 0 & p `2 < 0 ) )
assume that
A1:
- 1 < sn
and
A2:
q `1 < 0
and
A3:
(q `2 ) / |.q.| < sn
; for p being Point of (TOP-REAL 2) st p = (sn -FanMorphW ) . q holds
( p `1 < 0 & p `2 < 0 )
A4:
1 + sn > 0
by A1, XREAL_1:150;
A5:
((q `2 ) / |.q.|) - sn < 0
by A3, XREAL_1:51;
then
- (((q `2 ) / |.q.|) - sn) > 0
by XREAL_1:60;
then
(- (1 + sn)) / (1 + sn) < (- (((q `2 ) / |.q.|) - sn)) / (1 + sn)
by A4, XREAL_1:76;
then A6:
- 1 < (- (((q `2 ) / |.q.|) - sn)) / (1 + sn)
by A4, XCMPLX_1:198;
|.q.| > 0
by A2, Lm1, JGRAPH_2:11;
then A7:
|.q.| ^2 > 0
by SQUARE_1:74;
( |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) & 0 + ((q `2 ) ^2 ) < ((q `1 ) ^2 ) + ((q `2 ) ^2 ) )
by A2, JGRAPH_3:10, SQUARE_1:74, XREAL_1:10;
then
((q `2 ) ^2 ) / (|.q.| ^2 ) < (|.q.| ^2 ) / (|.q.| ^2 )
by A7, XREAL_1:76;
then
((q `2 ) ^2 ) / (|.q.| ^2 ) < 1
by A7, XCMPLX_1:60;
then
((q `2 ) / |.q.|) ^2 < 1
by XCMPLX_1:77;
then
- 1 < (q `2 ) / |.q.|
by SQUARE_1:122;
then
(- 1) - sn < ((q `2 ) / |.q.|) - sn
by XREAL_1:11;
then
- (- (1 + sn)) > - (((q `2 ) / |.q.|) - sn)
by XREAL_1:26;
then
(- (((q `2 ) / |.q.|) - sn)) / (1 + sn) < 1
by A4, XREAL_1:193;
then
((- (((q `2 ) / |.q.|) - sn)) / (1 + sn)) ^2 < 1 ^2
by A6, SQUARE_1:120;
then
1 - (((- (((q `2 ) / |.q.|) - sn)) / (1 + sn)) ^2 ) > 0
by XREAL_1:52;
then
sqrt (1 - (((- (((q `2 ) / |.q.|) - sn)) / (1 + sn)) ^2 )) > 0
by SQUARE_1:93;
then
sqrt (1 - (((- (((q `2 ) / |.q.|) - sn)) ^2 ) / ((1 + sn) ^2 ))) > 0
by XCMPLX_1:77;
then
sqrt (1 - (((((q `2 ) / |.q.|) - sn) ^2 ) / ((1 + sn) ^2 ))) > 0
;
then
sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )) > 0
by XCMPLX_1:77;
then A8:
- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))) < - 0
by XREAL_1:26;
let p be Point of (TOP-REAL 2); ( p = (sn -FanMorphW ) . q implies ( p `1 < 0 & p `2 < 0 ) )
set qz = p;
assume
p = (sn -FanMorphW ) . q
; ( p `1 < 0 & p `2 < 0 )
then
p = |[(|.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))))),(|.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)))]|
by A2, A3, Th24;
then A9:
( p `1 = |.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )))) & p `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)) )
by EUCLID:56;
(((q `2 ) / |.q.|) - sn) / (1 + sn) < 0
by A1, A5, XREAL_1:143, XREAL_1:150;
hence
( p `1 < 0 & p `2 < 0 )
by A2, A9, A8, Lm1, JGRAPH_2:11, XREAL_1:134; verum