let sn be Real; 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 -FanMorphE) . q holds
( p `1 > 0 & p `2 >= 0 )
let q be Point of (TOP-REAL 2); ( sn < 1 & q `1 > 0 & (q `2) / |.q.| >= sn implies for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds
( p `1 > 0 & p `2 >= 0 ) )
assume that
A1:
sn < 1
and
A2:
q `1 > 0
and
A3:
(q `2) / |.q.| >= sn
; for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds
( p `1 > 0 & p `2 >= 0 )
A4:
((q `2) / |.q.|) - sn >= 0
by A3, XREAL_1:48;
let p be Point of (TOP-REAL 2); ( p = (sn -FanMorphE) . q implies ( p `1 > 0 & p `2 >= 0 ) )
set qz = p;
A5:
1 - sn > 0
by A1, XREAL_1:149;
A6:
|.q.| <> 0
by A2, JGRAPH_2:3, TOPRNS_1:24;
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
(- (1 - sn)) / (1 - sn) < (- (((q `2) / |.q.|) - sn)) / (1 - sn)
by A5, XREAL_1:74;
then
- 1 < (- (((q `2) / |.q.|) - sn)) / (1 - sn)
by A5, XCMPLX_1:197;
then
((- (((q `2) / |.q.|) - sn)) / (1 - sn)) ^2 < 1 ^2
by A5, A4, 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 A8:
sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)) > 0
by XCMPLX_1:76;
assume
p = (sn -FanMorphE) . q
; ( p `1 > 0 & p `2 >= 0 )
then A9:
p = |[(|.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))),(|.q.| * ((((q `2) / |.q.|) - sn) / (1 - sn)))]|
by A2, A3, Th82;
then
p `1 = |.q.| * (sqrt (1 - (((((q `2) / |.q.|) - sn) / (1 - sn)) ^2)))
by EUCLID:52;
hence
( p `1 > 0 & p `2 >= 0 )
by A9, A6, A5, A4, A8, EUCLID:52, XREAL_1:129; verum