let m be Nat; :: thesis:
let i be Integer; :: thesis:
set p = i / m;
set g = i gcd m;
set d = m div (i gcd m);
assume A1: 0 <> m ; :: thesis:
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;

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

end;