let p be Point of (TOP-REAL 2); ( p <> 0. (TOP-REAL 2) implies ( ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) implies Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) ) )
A1:
( - (p `2) < p `1 implies - (- (p `2)) > - (p `1) )
by XREAL_1:24;
assume A2:
p <> 0. (TOP-REAL 2)
; ( ( ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) implies Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) )
hereby ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| )
assume A3:
( (
p `1 <= p `2 &
- (p `2) <= p `1 ) or (
p `1 >= p `2 &
p `1 <= - (p `2) ) )
;
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|now ( ( p `1 <= p `2 & - (p `2) <= p `1 & Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) or ( p `1 >= p `2 & p `1 <= - (p `2) & Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )per cases
( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) )
by A3;
case A4:
(
p `1 <= p `2 &
- (p `2) <= p `1 )
;
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|now ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| )assume A5:
( (
p `2 <= p `1 &
- (p `1) <= p `2 ) or (
p `2 >= p `1 &
p `2 <= - (p `1) ) )
;
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|now ( ( p `1 = p `2 & Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) or ( p `1 = - (p `2) & Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )per cases
( p `1 = p `2 or p `1 = - (p `2) )
by A6;
case A7:
p `1 = - (p `2)
;
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|then
(
p `1 <> 0 &
- (p `1) = p `2 )
by A2, EUCLID:53, EUCLID:54;
then A8:
(p `2) / (p `1) = - 1
by XCMPLX_1:197;
p `2 <> 0
by A2, A7, EUCLID:53, EUCLID:54;
then
(p `1) / (p `2) = - 1
by A7, XCMPLX_1:197;
hence
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
by A2, A5, A8, Def1;
verum end; end; end; hence
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
;
verum end; hence
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
by A2, Def1;
verum end; case A9:
(
p `1 >= p `2 &
p `1 <= - (p `2) )
;
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|now ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| )assume A10:
( (
p `2 <= p `1 &
- (p `1) <= p `2 ) or (
p `2 >= p `1 &
p `2 <= - (p `1) ) )
;
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|now ( ( p `1 = p `2 & Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) or ( p `1 = - (p `2) & Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )per cases
( p `1 = p `2 or p `1 = - (p `2) )
by A11;
case A12:
p `1 = - (p `2)
;
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|then
(
p `1 <> 0 &
- (p `1) = p `2 )
by A2, EUCLID:53, EUCLID:54;
then A13:
(p `2) / (p `1) = - 1
by XCMPLX_1:197;
p `2 <> 0
by A2, A12, EUCLID:53, EUCLID:54;
then
(p `1) / (p `2) = - 1
by A12, XCMPLX_1:197;
hence
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
by A2, A10, A13, Def1;
verum end; end; end; hence
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
;
verum end; hence
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
by A2, Def1;
verum end; end; end; hence
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
;
verum
end;
A14:
( - (p `2) > p `1 implies - (- (p `2)) < - (p `1) )
by XREAL_1:24;
assume
( not ( p `1 <= p `2 & - (p `2) <= p `1 ) & not ( p `1 >= p `2 & p `1 <= - (p `2) ) )
; Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]|
hence
Sq_Circ . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]|
by A2, A1, A14, Def1; verum