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 Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) ) )
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 Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| ) )
hereby :: thesis: ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) or Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| )
assume A2: ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) ; :: thesis: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
now :: thesis: ( ( p `1 <= p `2 & - (p `2) <= p `1 & Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) or ( p `1 >= p `2 & p `1 <= - (p `2) & Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) )
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: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
now :: thesis: ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| )
assume A4: ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) ; :: thesis: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
A5: 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 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:24;
hence ( p `1 = p `2 or p `1 = - (p `2) ) by A3, XXREAL_0:1; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( p `1 = p `2 & Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) or ( p `1 = - (p `2) & Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) )
per cases ( p `1 = p `2 or p `1 = - (p `2) ) by A5;
case A6: p `1 = p `2 ; :: thesis: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
then p `1 <> 0 by A1, EUCLID:53, EUCLID:54;
then ((p `1) / (p `2)) / (p `2) = 1 / (p `1) by A6, XCMPLX_1:60;
hence Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| by A1, A4, A6, Def1; :: thesis: verum
end;
case A7: p `1 = - (p `2) ; :: thesis: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
then A8: p `2 <> 0 by A1, EUCLID:53, EUCLID:54;
A9: ((p `1) / (p `2)) / (p `2) = (- ((p `2) / (p `2))) / (p `2) by A7
.= (- 1) / (p `2) by A8, XCMPLX_1:60
.= 1 / (p `1) by A7, XCMPLX_1:192 ;
- (p `1) = p `2 by A7;
then 1 / (p `2) = - (1 / (p `1)) by XCMPLX_1:188
.= - (((p `2) / (p `1)) / (- (p `1))) by A7, A9, XCMPLX_1:192
.= - (- (((p `2) / (p `1)) / (p `1))) by XCMPLX_1:188
.= ((p `2) / (p `1)) / (p `1) ;
hence Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| by A1, A4, A9, Def1; :: thesis: verum
end;
end;
end;
hence Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ; :: thesis: verum
end;
hence Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| by A1, Def1; :: thesis: verum
end;
case A10: ( p `1 >= p `2 & p `1 <= - (p `2) ) ; :: thesis: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
now :: thesis: ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) implies Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| )
assume A11: ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) ; :: thesis: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
A12: 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 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:24;
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 :: thesis: ( ( p `1 = p `2 & Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) or ( p `1 = - (p `2) & Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) )
per cases ( p `1 = p `2 or p `1 = - (p `2) ) by A12;
case A13: p `1 = p `2 ; :: thesis: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
then p `1 <> 0 by A1, EUCLID:53, EUCLID:54;
then ((p `1) / (p `2)) / (p `2) = 1 / (p `1) by A13, XCMPLX_1:60;
hence Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| by A1, A11, A13, Def1; :: thesis: verum
end;
case A14: p `1 = - (p `2) ; :: thesis: Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]|
then A15: p `2 <> 0 by A1, EUCLID:53, EUCLID:54;
A16: ((p `1) / (p `2)) / (p `2) = (- ((p `2) / (p `2))) / (p `2) by A14
.= (- 1) / (p `2) by A15, XCMPLX_1:60
.= 1 / (p `1) by A14, XCMPLX_1:192 ;
- (p `1) = p `2 by A14;
then 1 / (p `2) = - (((p `1) / (p `2)) / (p `2)) by A16, XCMPLX_1:188
.= - (((p `2) / (p `1)) / (- (p `1))) by A14, XCMPLX_1:191
.= - (- (((p `2) / (p `1)) / (p `1))) by XCMPLX_1:188
.= ((p `2) / (p `1)) / (p `1) ;
hence Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| by A1, A11, A16, Def1; :: thesis: verum
end;
end;
end;
hence Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ; :: thesis: verum
end;
hence Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| by A1, Def1; :: thesis: verum
end;
end;
end;
hence Out_In_Sq . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ; :: thesis: verum
end;
hereby :: thesis: verum
A17: ( - (p `2) > p `1 implies - (- (p `2)) < - (p `1) ) by XREAL_1:24;
A18: ( - (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: Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]|
hence Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| by A1, A18, A17, Def1; :: thesis: verum
end;