let m be Nat; for i being Integer st m <> 0 holds
(i div (i gcd m)) gcd (m div (i gcd m)) = 1
let i be Integer; ( 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
; (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 for w being Integer st w divides i div (i gcd m) & w divides m div (i gcd m) holds
w divides 1let w be
Integer;
( 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)
;
w divides 1consider 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;
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;
verum end;
hence
(i div (i gcd m)) gcd (m div (i gcd m)) = 1
by A3, INT_2:def 2; verum