let p, q be Rational; :: thesis: ( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) )
A1: now :: thesis: ( 0 < p & q = 1 / p implies ( numerator p = denominator q & denominator p = numerator q ) )
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, Th12
.= (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 Nat holds
( not 1 < k or for m being Integer
for w being Nat holds
( not denominator p = m * k or not y = w * k ) )
proof
assume ex k being Nat st
( 1 < k & ex m being Integer ex w being Nat st
( denominator p = m * k & y = w * k ) ) ; :: thesis: contradiction
then consider k being Nat such that
A6: 1 < k and
A7: ex m being Integer ex w being Nat st
( denominator p = m * k & y = w * k ) ;
consider m being Integer, w being Nat such that
A8: denominator p = m * k and
A9: y = w * k by A7;
0 <= m by A8;
then reconsider z = m as Element of NAT by INT_1:3;
denominator p = z * k by A8;
hence contradiction by A6, A9, Th26; :: thesis: verum
end;
0 <> numerator p by A2, Th35;
hence ( numerator p = denominator q & denominator p = numerator q ) by A4, A5, Th27; :: thesis: verum
end;
now :: thesis: ( numerator q = denominator p & denominator q = numerator p implies ( 0 < p & q = 1 / p ) )
assume that
A10: numerator q = denominator p and
A11: denominator q = numerator p ; :: thesis: ( 0 < p & q = 1 / p )
thus 0 < p by A11; :: thesis: q = 1 / p
thus q = (1 * (denominator p)) / (numerator p) by A10, A11, Th12
.= 1 / ((numerator p) / (denominator p)) by XCMPLX_1:77
.= 1 / p by Th12 ; :: thesis: verum
end;
hence ( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) ) by A1; :: thesis: verum