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 ) )

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

end;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

0 <> numerator p
by A2, Th35;
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;( 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

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

now :: thesis: ( numerator q = denominator p & denominator q = numerator p implies ( 0 < p & q = 1 / p ) )

hence
( 0 < p & q = 1 / p iff ( numerator q = denominator p & denominator q = numerator p ) )
by A1; :: thesis: verumassume 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;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