let cn be Real; for q being Point of (TOP-REAL 2) st - 1 < cn & q `2 > 0 & (q `1 ) / |.q.| < cn holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN ) . q holds
( p `2 > 0 & p `1 < 0 )
let q be Point of (TOP-REAL 2); ( - 1 < cn & q `2 > 0 & (q `1 ) / |.q.| < cn implies for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN ) . q holds
( p `2 > 0 & p `1 < 0 ) )
assume that
A1:
- 1 < cn
and
A2:
q `2 > 0
and
A3:
(q `1 ) / |.q.| < cn
; for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN ) . q holds
( p `2 > 0 & p `1 < 0 )
A4:
1 + cn > 0
by A1, XREAL_1:150;
let p be Point of (TOP-REAL 2); ( p = (cn -FanMorphN ) . q implies ( p `2 > 0 & p `1 < 0 ) )
set qz = p;
assume
p = (cn -FanMorphN ) . q
; ( p `2 > 0 & p `1 < 0 )
then
p = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn))),(|.q.| * (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ))))]|
by A2, A3, Th57;
then A5:
( p `2 = |.q.| * (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 ))) & p `1 = |.q.| * ((((q `1 ) / |.q.|) - cn) / (1 + cn)) )
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 `1 ) / |.q.|) - cn < 0
by A3, XREAL_1:51;
then
- (((q `1 ) / |.q.|) - cn) > 0
by XREAL_1:60;
then
(- (1 + cn)) / (1 + cn) < (- (((q `1 ) / |.q.|) - cn)) / (1 + cn)
by A4, XREAL_1:76;
then A9:
- 1 < (- (((q `1 ) / |.q.|) - cn)) / (1 + cn)
by A4, XCMPLX_1:198;
( |.q.| ^2 = ((q `1 ) ^2 ) + ((q `2 ) ^2 ) & 0 + ((q `1 ) ^2 ) < ((q `1 ) ^2 ) + ((q `2 ) ^2 ) )
by A2, JGRAPH_3:10, SQUARE_1:74, XREAL_1:10;
then
((q `1 ) ^2 ) / (|.q.| ^2 ) < (|.q.| ^2 ) / (|.q.| ^2 )
by A7, XREAL_1:76;
then
((q `1 ) ^2 ) / (|.q.| ^2 ) < 1
by A7, XCMPLX_1:60;
then
((q `1 ) / |.q.|) ^2 < 1
by XCMPLX_1:77;
then
- 1 < (q `1 ) / |.q.|
by SQUARE_1:122;
then
(- 1) - cn < ((q `1 ) / |.q.|) - cn
by XREAL_1:11;
then
- (- (1 + cn)) > - (((q `1 ) / |.q.|) - cn)
by XREAL_1:26;
then
(- (((q `1 ) / |.q.|) - cn)) / (1 + cn) < 1
by A4, XREAL_1:193;
then
((- (((q `1 ) / |.q.|) - cn)) / (1 + cn)) ^2 < 1 ^2
by A9, SQUARE_1:120;
then
1 - (((- (((q `1 ) / |.q.|) - cn)) / (1 + cn)) ^2 ) > 0
by XREAL_1:52;
then
sqrt (1 - (((- (((q `1 ) / |.q.|) - cn)) / (1 + cn)) ^2 )) > 0
by SQUARE_1:93;
then
sqrt (1 - (((- (((q `1 ) / |.q.|) - cn)) ^2 ) / ((1 + cn) ^2 ))) > 0
by XCMPLX_1:77;
then
sqrt (1 - (((((q `1 ) / |.q.|) - cn) ^2 ) / ((1 + cn) ^2 ))) > 0
;
then A10:
sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 + cn)) ^2 )) > 0
by XCMPLX_1:77;
(((q `1 ) / |.q.|) - cn) / (1 + cn) < 0
by A1, A8, XREAL_1:143, XREAL_1:150;
hence
( p `2 > 0 & p `1 < 0 )
by A6, A5, A10, XREAL_1:131, XREAL_1:134; verum