let g, m be Nat; :: thesis: for i being Integer st g divides i & g divides m holds
i / m = (i div g) / (m div g)
let i be Integer; :: thesis: ( g divides i & g divides m implies i / m = (i div g) / (m div g) )
assume that
A1: g divides i and
A2: g divides m ; :: thesis: i / m = (i div g) / (m div g)
per cases ( g = 0 or m = 0 or ( g <> 0 & m <> 0 ) ) ;
suppose A3: g = 0 ; :: thesis: i / m = (i div g) / (m div g)
0 gcd 0 = 0 by INT_2:5;
then 0 div (0 gcd 0) = 0 by INT_1:48;
hence i / m = (i div g) / (m div g) by A1, A3; :: thesis: verum
end;
suppose A4: m = 0 ; :: thesis: i / m = (i div g) / (m div g)
0 div g = 0 by NAT_2:2;
then ( i / 0 = 0 & (i div g) / (0 div g) = 0 ) by XCMPLX_1:49;
hence i / m = (i div g) / (m div g) by A4; :: thesis: verum
end;
suppose that A5: g <> 0 and
A6: m <> 0 ; :: thesis: i / m = (i div g) / (m div g)
g <= m by A2, A6, INT_2:27;
then A7: m div g <> 0 by A5, NAT_2:13;
( i mod g = 0 & m mod g = 0 ) by A1, A2, A5, INT_1:62;
then ( m div g = m / g & i div g = i / g ) by A5, PEPIN:63;
then i * (m div g) = m * (i div g) ;
hence i / m = (i div g) / (m div g) by A6, A7, XCMPLX_1:94; :: thesis: verum
end;
end;