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 `1 ) = p `2 ;
A9: p `2 <> 0 by A1, A7, EUCLID:57, EUCLID:58;
A10: ((p `1 ) / (p `2 )) / (p `2 ) = (- ((p `2 ) / (p `2 ))) / (p `2 ) by A7
.= (- 1) / (p `2 ) by A9, XCMPLX_1:60
.= 1 / (p `1 ) by A7, XCMPLX_1:193 ;
1 / (p `2 ) = - (1 / (p `1 )) by A8, XCMPLX_1:189
.= - (((p `2 ) / (p `1 )) / (- (p `1 ))) by A7, A10, 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, A10, 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 A11: ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ; :: thesis: Out_In_Sq . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]|
now
assume A12: ( ( 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 ))]|
A13: now
per cases ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) by A12;
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 A11, 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 A11, XXREAL_0:1; :: thesis: verum
end;
end;
end;
now
per cases ( p `1 = p `2 or p `1 = - (p `2 ) ) by A13;
case A14: 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 A14, XCMPLX_1:60;
hence Out_In_Sq . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| by A1, A12, A14, Def1; :: thesis: verum
end;
case A15: p `1 = - (p `2 ) ; :: thesis: Out_In_Sq . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]|
then A16: - (p `1 ) = p `2 ;
A17: p `2 <> 0 by A1, A15, EUCLID:57, EUCLID:58;
A18: ((p `1 ) / (p `2 )) / (p `2 ) = (- ((p `2 ) / (p `2 ))) / (p `2 ) by A15
.= (- 1) / (p `2 ) by A17, XCMPLX_1:60
.= 1 / (p `1 ) by A15, XCMPLX_1:193 ;
then 1 / (p `2 ) = - (((p `1 ) / (p `2 )) / (p `2 )) by A16, XCMPLX_1:189
.= - (((p `2 ) / (p `1 )) / (- (p `1 ))) by A15, 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, A12, A18, 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
assume A19: ( 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 ))]|
A20: ( - (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 Out_In_Sq . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| by A1, A19, A20, Def1; :: thesis: verum
end;