let m be Nat; :: thesis: for i being Integer st m <> 0 holds
( denominator (i / m) = m div (i gcd m) & numerator (i / m) = i div (i gcd m) )
let i be Integer; :: thesis: ( m <> 0 implies ( denominator (i / m) = m div (i gcd m) & numerator (i / m) = i div (i gcd m) ) )
set p = i / m;
set g = i gcd m;
set d = m div (i gcd m);
assume A1: 0 <> m ; :: thesis: ( denominator (i / m) = m div (i gcd m) & numerator (i / m) = i div (i gcd m) )
then A2: i gcd m <> 0 by INT_2:5;
i gcd m divides m by INT_2:def 2;
then i gcd m <= m by A1, INT_2:27;
then A3: m div (i gcd m) <> 0 by A2, PRE_FF:3;
A4: i / m = (i div (i gcd m)) / (m div (i gcd m)) by Th10;

now :: thesis: for w being Nat holds
( not 1 < w or for i1 being Integer
for m1 being Nat holds
( not i div (i gcd m) = i1 * w or not m div (i gcd m) = m1 * w ) )

given w being Nat such that A5: 1 < w and
A6: ex i1 being Integer ex m1 being Nat st
( i div (i gcd m) = i1 * w & m div (i gcd m) = m1 * w ) ; :: thesis: contradiction
consider i1 being Integer, m1 being Nat such that
A7: i div (i gcd m) = i1 * w and
A8: m div (i gcd m) = m1 * w by A6;
( w divides i div (i gcd m) & w divides m div (i gcd m) ) by A7, A8;
then A9: w divides (i div (i gcd m)) gcd (m div (i gcd m)) by INT_2:def 2;
(i div (i gcd m)) gcd (m div (i gcd m)) = 1 by A1, Th14;
hence contradiction by A5, A9, WSIERP_1:15; :: thesis: verum

end;

hence ( denominator (i / m) = m div (i gcd m) & numerator (i / m) = i div (i gcd m) ) by A3, A4, RAT_1:30; :: thesis: verum