let p, q be Rational; :: thesis: ( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) )

A1: now

assume A2: ( 0 < p & q = 1 / p ) ; :: thesis: ( numerator p = denominator q & denominator p = numerator q )
then A3: 0 < numerator p by Th77;
A4: 0 <> numerator p by A2, Th77;
A5: q = 1 / ((numerator p) / (denominator p)) by A2, Th37
.= (1 * (denominator p)) / (numerator p) by XCMPLX_1:78
.= (denominator p) / (numerator p) ;
set x = denominator p;
reconsider y = numerator p as Element of NAT by A3, INT_1:16;
for k being Element of NAT holds
( not 1 < k or for m being Integer
for l being Element of NAT holds
( not denominator p = m * k or not y = l * k ) )

proof

assume ex k being Element of NAT st
( 1 < k & ex m being Integer ex l being Element of NAT st
( denominator p = m * k & y = l * k ) ) ; :: thesis: contradiction
then consider k being Element of NAT such that
A6: ( 1 < k & ex m being Integer ex l being Element of NAT st
( denominator p = m * k & y = l * k ) ) ;
consider m being Integer, l being Element of NAT such that
A7: ( denominator p = m * k & y = l * k ) by A6;

now

assume not 0 <= m ; :: thesis: contradiction
then m * k < 0 * m by A6, XREAL_1:71;
hence contradiction by A7; :: thesis: verum

end;

then reconsider z = m as Element of NAT by INT_1:16;
reconsider v = l as Integer ;
( 1 < k & numerator p = v * k & denominator p = z * k ) by A6, A7;
hence contradiction by Th62; :: thesis: verum

end;

hence ( numerator p = denominator q & denominator p = numerator q ) by A4, A5, Th63; :: thesis: verum

end;

now

assume A8: ( numerator q = denominator p & denominator q = numerator p ) ; :: thesis: ( 0 < p & q = 1 / p )
then 0 < numerator p by Th27;
hence 0 < p ; :: thesis: q = 1 / p
thus q = (1 * (denominator p)) / (numerator p) by A8, Th37
.= 1 / ((numerator p) / (denominator p)) by XCMPLX_1:78
.= 1 / p by Th37 ; :: thesis: verum

end;

hence ( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) ) by A1; :: thesis: verum