let R be commutative domRing-like Ring; :: thesis: for a, b, c being Element of R st c <> 0. R holds
( ( c divides a * b & c divides a implies (a * b) / c = (a / c) * b ) & ( c divides a * b & c divides b implies (a * b) / c = a * (b / c) ) )
let A, B, C be Element of R; :: thesis: ( C <> 0. R implies ( ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) & ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) ) )
assume A1: C <> 0. R ; :: thesis: ( ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) & ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) )
A2: now :: thesis: ( C divides A * B & C divides B & C divides A * B & C divides B implies (A * B) / C = A * (B / C) )
set A2 = B / C;
set A1 = (A * B) / C;
assume ( C divides A * B & C divides B ) ; :: thesis: ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) )
then ( ((A * B) / C) * C = A * B & (B / C) * C = B ) by A1, Def4;
then ((A * B) / C) * C = (A * (B / C)) * C by GROUP_1:def 3;
hence ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) by A1, Th1; :: thesis: verum
end;
now :: thesis: ( C divides A * B & C divides A & C divides A * B & C divides A implies (A * B) / C = (A / C) * B )
set A2 = A / C;
set A1 = (A * B) / C;
assume ( C divides A * B & C divides A ) ; :: thesis: ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B )
then ( ((A * B) / C) * C = A * B & (A / C) * C = A ) by A1, Def4;
then ((A * B) / C) * C = ((A / C) * B) * C by GROUP_1:def 3;
hence ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) by A1, Th1; :: thesis: verum
end;
hence ( ( C divides A * B & C divides A implies (A * B) / C = (A / C) * B ) & ( C divides A * B & C divides B implies (A * B) / C = A * (B / C) ) ) by A2; :: thesis: verum