let cn be Real; for q being Point of (TOP-REAL 2) st cn < 1 & 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); ( cn < 1 & 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:
cn < 1
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:
((q `1 ) / |.q.|) - cn >= 0
by A3, XREAL_1:50;
let p be Point of (TOP-REAL 2); ( p = (cn -FanMorphN ) . q implies ( p `2 > 0 & p `1 >= 0 ) )
set qz = p;
A5:
1 - cn > 0
by A1, XREAL_1:151;
A6:
|.q.| <> 0
by A2, JGRAPH_2:11, TOPRNS_1:25;
then A7:
|.q.| ^2 > 0
by SQUARE_1:74;
( |.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
(- (1 - cn)) / (1 - cn) < (- (((q `1 ) / |.q.|) - cn)) / (1 - cn)
by A5, XREAL_1:76;
then
- 1 < (- (((q `1 ) / |.q.|) - cn)) / (1 - cn)
by A5, XCMPLX_1:198;
then
((- (((q `1 ) / |.q.|) - cn)) / (1 - cn)) ^2 < 1 ^2
by A5, A4, 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 A8:
sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )) > 0
by XCMPLX_1:77;
assume
p = (cn -FanMorphN ) . q
; ( p `2 > 0 & p `1 >= 0 )
then A9:
p = |[(|.q.| * ((((q `1 ) / |.q.|) - cn) / (1 - cn))),(|.q.| * (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 ))))]|
by A2, A3, Th56;
then
p `2 = |.q.| * (sqrt (1 - (((((q `1 ) / |.q.|) - cn) / (1 - cn)) ^2 )))
by EUCLID:56;
hence
( p `2 > 0 & p `1 >= 0 )
by A9, A6, A5, A4, A8, EUCLID:56, XREAL_1:131; verum