let m be Nat; :: thesis: for i being Integer st m <> 0 holds
(i div (i gcd m)) gcd (m div (i gcd m)) = 1
let i be Integer; :: thesis: ( m <> 0 implies (i div (i gcd m)) gcd (m div (i gcd m)) = 1 )
set g = i gcd m;
set a = i div (i gcd m);
set b = m div (i gcd m);
assume A1: m <> 0 ; :: thesis: (i div (i gcd m)) gcd (m div (i gcd m)) = 1
then A2: i gcd m <> 0 by INT_2:5;
A3: ( 1 divides i div (i gcd m) & 1 divides m div (i gcd m) ) by INT_2:12;

now :: thesis: for w being Integer st w divides i div (i gcd m) & w divides m div (i gcd m) holds
w divides 1

let w be Integer; :: thesis: ( w divides i div (i gcd m) & w divides m div (i gcd m) implies w divides 1 )
assume that
A4: w divides i div (i gcd m) and
A5: w divides m div (i gcd m) ; :: thesis: w divides 1
consider i1 being Integer such that
A6: i div (i gcd m) = i1 * w by A4;
consider i2 being Integer such that
A7: m div (i gcd m) = i2 * w by A5;
A8: i gcd m divides i by INT_2:def 2;
A9: i gcd m divides m by INT_2:def 2;

A10: now :: thesis: not w = 0

assume A11: w = 0 ; :: thesis: contradiction
i gcd m <= m by A1, A9, INT_2:27;
hence contradiction by A2, A5, A11, NAT_2:13; :: thesis: verum

end;

A12: ((i / (i gcd m)) / w) * w = i / (i gcd m) by A10, XCMPLX_1:87;
A13: ((m / (i gcd m)) / w) * w = m / (i gcd m) by A10, XCMPLX_1:87;
(i / (i gcd m)) / w = (i1 * w) / w by A6, A8, Th6
.= i1 by A10, XCMPLX_1:89 ;
then (((i / (i gcd m)) / w) * w) * (i gcd m) = (i1 * w) * (i gcd m) ;
then i = i1 * ((i gcd m) * w) by A12, A2, XCMPLX_1:87;
then A14: (i gcd m) * w divides i ;
(m / (i gcd m)) / w = (i2 * w) / w by A7, A9, Th6
.= i2 by A10, XCMPLX_1:89 ;
then (((m / (i gcd m)) / w) * w) * (i gcd m) = (i2 * w) * (i gcd m) ;
then m = i2 * ((i gcd m) * w) by A13, A2, XCMPLX_1:87;
then (i gcd m) * w divides m ;
then (i gcd m) * w divides i gcd m by A14, INT_2:def 2;
then ( w = 1 or w = - 1 ) by A2, Th11;
hence w divides 1 by INT_2:14; :: thesis: verum

end;

hence (i div (i gcd m)) gcd (m div (i gcd m)) = 1 by A3, INT_2:def 2; :: thesis: verum