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:148;
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, Th83;
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:52;
A6:
|.q.| <> 0
by A2, JGRAPH_2:3, TOPRNS_1:24;
then A7:
|.q.| ^2 > 0
by SQUARE_1:12;
A8:
((q `2) / |.q.|) - sn < 0
by A3, XREAL_1:49;
then
- (((q `2) / |.q.|) - sn) > 0
by XREAL_1:58;
then
(- (1 + sn)) / (1 + sn) < (- (((q `2) / |.q.|) - sn)) / (1 + sn)
by A4, XREAL_1:74;
then A9:
- 1 < (- (((q `2) / |.q.|) - sn)) / (1 + sn)
by A4, XCMPLX_1:197;
( |.q.| ^2 = ((q `1) ^2) + ((q `2) ^2) & 0 + ((q `2) ^2) < ((q `1) ^2) + ((q `2) ^2) )
by A2, JGRAPH_3:1, SQUARE_1:12, XREAL_1:8;
then
((q `2) ^2) / (|.q.| ^2) < (|.q.| ^2) / (|.q.| ^2)
by A7, XREAL_1:74;
then
((q `2) ^2) / (|.q.| ^2) < 1
by A7, XCMPLX_1:60;
then
((q `2) / |.q.|) ^2 < 1
by XCMPLX_1:76;
then
- 1 < (q `2) / |.q.|
by SQUARE_1:52;
then
(- 1) - sn < ((q `2) / |.q.|) - sn
by XREAL_1:9;
then
- (- (1 + sn)) > - (((q `2) / |.q.|) - sn)
by XREAL_1:24;
then
(- (((q `2) / |.q.|) - sn)) / (1 + sn) < 1
by A4, XREAL_1:191;
then
((- (((q `2) / |.q.|) - sn)) / (1 + sn)) ^2 < 1 ^2
by A9, SQUARE_1:50;
then
1 - (((- (((q `2) / |.q.|) - sn)) / (1 + sn)) ^2) > 0
by XREAL_1:50;
then
sqrt (1 - (((- (((q `2) / |.q.|) - sn)) / (1 + sn)) ^2)) > 0
by SQUARE_1:25;
then
sqrt (1 - (((- (((q `2) / |.q.|) - sn)) ^2) / ((1 + sn) ^2))) > 0
by XCMPLX_1:76;
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:76;
(((q `2) / |.q.|) - sn) / (1 + sn) < 0
by A1, A8, XREAL_1:141, XREAL_1:148;
hence
( p `1 > 0 & p `2 < 0 )
by A6, A5, A10, XREAL_1:129, XREAL_1:132; verum