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))))]| ) ) )
A1: ( - (p `2) < p `1 implies - (- (p `2)) > - (p `1) ) by XREAL_1:24;
assume A2: 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 A3: ( ( 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 :: thesis: ( ( 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 ) ; :: thesis: (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
now :: thesis: ( ( ( 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) ) ) ; :: thesis: (Sq_Circ ") . p = |[((p `1) * (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) * (sqrt (1 + (((p `1) / (p `2)) ^2))))]|
A6: now :: thesis: ( ( p `2 <= p `1 & - (p `1) <= p `2 & ( p `1 = p `2 or p `1 = - (p `2) ) ) or ( p `2 >= p `1 & p `2 <= - (p `1) & ( p `1 = p `2 or p `1 = - (p `2) ) ) )
per cases ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) by A5;
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 A4, 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:24;
hence ( p `1 = p `2 or p `1 = - (p `2) ) by A4, XXREAL_0:1; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( 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 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 A2, A5, Th28; :: thesis: verum
end;
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))))]|
then ( p `1 <> 0 & - (p `1) = p `2 ) by A2, EUCLID:53, EUCLID:54;
then ( (p `1) / (p `2) = - 1 & (p `2) / (p `1) = - 1 ) by XCMPLX_1:197, 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 A2, A5, Th28; :: 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 Th28; :: thesis: verum
end;
case A7: ( 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 :: thesis: ( ( ( 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 A8: ( ( 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))))]|
A9: now :: thesis: ( ( p `2 <= p `1 & - (p `1) <= p `2 & ( p `1 = p `2 or p `1 = - (p `2) ) ) or ( p `2 >= p `1 & p `2 <= - (p `1) & ( p `1 = p `2 or p `1 = - (p `2) ) ) )
per cases ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) by A8;
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:24;
hence ( p `1 = p `2 or p `1 = - (p `2) ) by A7, 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 A7, XXREAL_0:1; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( 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 A9;
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 A2, A8, Th28; :: thesis: verum
end;
case A10: 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 ( p `1 <> 0 & - (p `1) = p `2 ) by A2, EUCLID:53, EUCLID:54;
then A11: (p `2) / (p `1) = - 1 by XCMPLX_1:197;
p `2 <> 0 by A2, A10, EUCLID:53, EUCLID:54;
then (p `1) / (p `2) = - 1 by A10, 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, A8, A11, Th28; :: 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 Th28; :: 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;
A12: ( - (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) ) ) ; :: thesis: (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, A12, Th28; :: thesis: verum