let sn be Real; :: thesis: 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); :: thesis: ( - 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 ; :: thesis: 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:148;
A5: ((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 A6: - 1 < (- (((q `2) / |.q.|) - sn)) / (1 + sn) by A4, XCMPLX_1:197;
|.q.| > 0 by A2, Lm1, JGRAPH_2:3;
then A7: |.q.| ^2 > 0 by SQUARE_1:12;
( |.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 A6, 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 sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2)) > 0 by XCMPLX_1:76;
then A8: - (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 + sn)) ^2))) < - 0 by XREAL_1:24;
let p be Point of (TOP-REAL 2); :: thesis: ( p = (sn -FanMorphW) . q implies ( p `1 < 0 & p `2 < 0 ) )
set qz = p;
assume p = (sn -FanMorphW) . q ; :: thesis: ( 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, Th17;
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:52;
(((q `2) / |.q.|) - sn) / (1 + sn) < 0 by A1, A5, XREAL_1:141, XREAL_1:148;
hence ( p `1 < 0 & p `2 < 0 ) by A2, A9, A8, Lm1, JGRAPH_2:3, XREAL_1:132; :: thesis: verum