let p be Point of (TOP-REAL 2); :: thesis: ( 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 ))))]| ) ) )
assume A1: p <> 0. (TOP-REAL 2) ; :: thesis: ( ( ( ( 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 :: thesis: ( ( 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 A2: ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
now
per cases ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) by A2;
case A3: ( p `1 <= p `2 & - (p `2 ) <= p `1 ) ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
now
assume A4: ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
A5: now
per cases ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) by A4;
case ( p `2 <= p `1 & - (p `1 ) <= p `2 ) ; :: thesis: ( p `1 = p `2 or p `1 = - (p `2 ) )
hence ( p `1 = p `2 or p `1 = - (p `2 ) ) by A3, XXREAL_0:1; :: thesis: verum
end;
case ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ; :: thesis: ( p `1 = p `2 or p `1 = - (p `2 ) )
then - (p `2 ) >= - (- (p `1 )) by XREAL_1:26;
hence ( p `1 = p `2 or p `1 = - (p `2 ) ) by A3, XXREAL_0:1; :: thesis: verum
end;
end;
end;
now
per cases ( p `1 = p `2 or p `1 = - (p `2 ) ) by A5;
case p `1 = p `2 ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
hence (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| by A1, A4, Th38; :: thesis: verum
end;
case A6: p `1 = - (p `2 ) ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
then A7: p `1 <> 0 by A1, EUCLID:57, EUCLID:58;
A8: - (p `1 ) = p `2 by A6;
then A9: (p `1 ) / (p `2 ) = - 1 by A7, XCMPLX_1:199;
(p `2 ) / (p `1 ) = - 1 by A7, A8, XCMPLX_1:198;
hence (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| by A1, A4, A9, Th38; :: thesis: 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 ))))]| ; :: thesis: 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 A1, Th38; :: thesis: verum
end;
case A10: ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
now
assume A11: ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
A12: now
per cases ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) by A11;
case ( p `2 <= p `1 & - (p `1 ) <= p `2 ) ; :: thesis: ( p `1 = p `2 or p `1 = - (p `2 ) )
then - (- (p `1 )) >= - (p `2 ) by XREAL_1:26;
hence ( p `1 = p `2 or p `1 = - (p `2 ) ) by A10, XXREAL_0:1; :: thesis: verum
end;
case ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ; :: thesis: ( p `1 = p `2 or p `1 = - (p `2 ) )
hence ( p `1 = p `2 or p `1 = - (p `2 ) ) by A10, XXREAL_0:1; :: thesis: verum
end;
end;
end;
now
per cases ( p `1 = p `2 or p `1 = - (p `2 ) ) by A12;
case p `1 = p `2 ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
hence (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| by A1, A11, Th38; :: thesis: verum
end;
case A13: p `1 = - (p `2 ) ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]|
then A14: p `1 <> 0 by A1, EUCLID:57, EUCLID:58;
A15: - (p `1 ) = p `2 by A13;
p `2 <> 0 by A1, A13, EUCLID:57, EUCLID:58;
then A16: (p `1 ) / (p `2 ) = - 1 by A13, XCMPLX_1:198;
(p `2 ) / (p `1 ) = - 1 by A14, A15, XCMPLX_1:198;
hence (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| by A1, A11, A16, Th38; :: thesis: 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 ))))]| ; :: thesis: 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 A1, Th38; :: thesis: 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 ))))]| ; :: thesis: verum
end;
assume A17: ( not ( p `1 <= p `2 & - (p `2 ) <= p `1 ) & not ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) ; :: thesis: (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]|
A18: ( - (p `2 ) < p `1 implies - (- (p `2 )) > - (p `1 ) ) by XREAL_1:26;
( - (p `2 ) > p `1 implies - (- (p `2 )) < - (p `1 ) ) by XREAL_1:26;
hence (Sq_Circ " ) . p = |[((p `1 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) * (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| by A1, A17, A18, Th38; :: thesis: verum