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
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
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
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 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:57, EUCLID:58;
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:57, EUCLID:58;
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:193 ;
- (p `1 ) = p `2 by A7;
then 1 / (p `2 ) = - (1 / (p `1 )) by XCMPLX_1:189
.= - (((p `2 ) / (p `1 )) / (- (p `1 ))) by A7, A9, XCMPLX_1:193
.= - (- (((p `2 ) / (p `1 )) / (p `1 ))) by XCMPLX_1:189
.= ((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
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
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 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:57, EUCLID:58;
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:57, EUCLID:58;
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:193 ;
- (p `1 ) = p `2 by A14;
then 1 / (p `2 ) = - (((p `1 ) / (p `2 )) / (p `2 )) by A16, XCMPLX_1:189
.= - (((p `2 ) / (p `1 )) / (- (p `1 ))) by A14, XCMPLX_1:192
.= - (- (((p `2 ) / (p `1 )) / (p `1 ))) by XCMPLX_1:189
.= ((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:26;
A18: ( - (p `2 ) < p `1 implies - (- (p `2 )) > - (p `1 ) ) by XREAL_1:26;
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;