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:151;
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, Th23;
then A6: p `1 = |.q.| * (- (sqrt (1 - (((((q `2 ) / |.q.|) - sn) / (1 - sn)) ^2 )))) by EUCLID:56;
A7: ((q `2 ) / |.q.|) - sn >= 0 by A3, XREAL_1:50;
A8: |.q.| > 0 by A2, Lm1, JGRAPH_2:11;
then A9: |.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 A9, XREAL_1:76;
then ((q `2 ) ^2 ) / (|.q.| ^2 ) < 1 by A9, 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 (- (1 - sn)) / (1 - sn) < (- (((q `2 ) / |.q.|) - sn)) / (1 - sn) by A4, XREAL_1:76;
then - 1 < (- (((q `2 ) / |.q.|) - sn)) / (1 - sn) by A4, XCMPLX_1:198;
then ((- (((q `2 ) / |.q.|) - sn)) / (1 - sn)) ^2 < 1 ^2 by A4, A7, SQUARE_1:120;
hence ( p `1 < 0 & p `2 >= 0 ) by A5, A8, A4, A6, A7, Lm13, EUCLID:56, XREAL_1:134; :: thesis: verum