let a, n be Nat; :: thesis: for b being non zero Nat holds a lcm (((n * a) + 1) * b) = ((n * a) + 1) * (a lcm b)
let b be non zero Nat; :: thesis: a lcm (((n * a) + 1) * b) = ((n * a) + 1) * (a lcm b)
a lcm ((a * (n * b)) + b) = ((((a * n) * b) / b) + 1) * (a lcm b) by LCM2;
hence a lcm (((n * a) + 1) * b) = ((n * a) + 1) * (a lcm b) by XCMPLX_1:89; :: thesis: verum