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

A1: now

set x = denominator p;
assume that
A2: 0 < p and
A3: q = 1 / p ; :: thesis: ( numerator p = denominator q & denominator p = numerator q )
A4: q = 1 / ((numerator p) / (denominator p)) by A3, Th37
.= (1 * (denominator p)) / (numerator p) by XCMPLX_1:77
.= (denominator p) / (numerator p) ;
reconsider y = numerator p as Element of NAT by A2, INT_1:3;
A5: 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 and
A7: 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
A8: denominator p = m * k and
A9: y = l * k by A7;

now

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

end;

then reconsider z = m as Element of NAT by INT_1:3;
denominator p = z * k by A8;
hence contradiction by A6, A9, Th62; :: thesis: verum

end;

0 <> numerator p by A2, Th77;
hence ( numerator p = denominator q & denominator p = numerator q ) by A4, A5, Th63; :: thesis: verum

end;

now

assume that
A10: numerator q = denominator p and
A11: denominator q = numerator p ; :: thesis: ( 0 < p & q = 1 / p )
thus 0 < p by A11, Th27; :: thesis: q = 1 / p
thus q = (1 * (denominator p)) / (numerator p) by A10, A11, Th37
.= 1 / ((numerator p) / (denominator p)) by XCMPLX_1:77
.= 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