let sn be Real; :: thesis: for q being Point of (TOP-REAL 2) st sn < 1 & 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: ( sn < 1 & 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: sn < 1 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:149;
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 A5: p = |[(|.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2))))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]| by A2, A3, Th16;
then A6: p `1 = |.q.| * (- (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))) by EUCLID:52;
A7: ((q `2) / |.q.|) - sn >= 0 by A3, XREAL_1:48;
A8: |.q.| > 0 by A2, Lm1, JGRAPH_2:3;
then A9: |.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 A9, XREAL_1:74;
then ((q `2) ^2) / (|.q.| ^2) < 1 by A9, 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 (- (1 - sn)) / (1 - sn) < (- (((q `2) / |.q.|) - sn)) / (1 - sn) by A4, XREAL_1:74;
then - 1 < (- (((q `2) / |.q.|) - sn)) / (1 - sn) by A4, XCMPLX_1:197;
then ((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2 < 1 ^2 by A4, A7, SQUARE_1:50;
hence ( p `1 < 0 & p `2 >= 0 ) by A5, A8, A4, A6, A7, Lm13, EUCLID:52, XREAL_1:132; :: thesis: verum