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 -FanMorphE ) . 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 -FanMorphE ) . 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 -FanMorphE ) . q holds
( p `1 > 0 & p `2 < 0 )
A4:
1 + sn > 0
by A1, XREAL_1:150;
let p be Point of (TOP-REAL 2); ( p = (sn -FanMorphE ) . q implies ( p `1 > 0 & p `2 < 0 ) )
set qz = p;
assume
p = (sn -FanMorphE ) . 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, Th90;
then A5:
( p `1 = |.q.| * (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 ))) & p `2 = |.q.| * ((((q `2 ) / |.q.|) - sn) / (1 + sn)) )
by EUCLID:56;
A6:
|.q.| <> 0
by A2, JGRAPH_2:11, TOPRNS_1:25;
then A7:
|.q.| ^2 > 0
by SQUARE_1:74;
A8:
((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 A9:
- 1 < (- (((q `2 ) / |.q.|) - sn)) / (1 + sn)
by A4, XCMPLX_1:198;
( |.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 A9, 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 A10:
sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 + sn)) ^2 )) > 0
by XCMPLX_1:77;
(((q `2 ) / |.q.|) - sn) / (1 + sn) < 0
by A1, A8, XREAL_1:143, XREAL_1:150;
hence
( p `1 > 0 & p `2 < 0 )
by A6, A5, A10, XREAL_1:131, XREAL_1:134; verum