let a, n be Nat; :: thesis: for b being non zero Nat holds a lcm ((a * n) + b) = (((a * n) / b) + 1) * (a lcm b)
let b be non zero Nat; :: thesis: a lcm ((a * n) + b) = (((a * n) / b) + 1) * (a lcm b)
per cases ( a is zero or not a is zero ) ;
suppose a is zero ; :: thesis: a lcm ((a * n) + b) = (((a * n) / b) + 1) * (a lcm b)
hence a lcm ((a * n) + b) = (((a * n) / b) + 1) * (a lcm b) ; :: thesis: verum
end;
suppose not a is zero ; :: thesis: a lcm ((a * n) + b) = (((a * n) / b) + 1) * (a lcm b)
then reconsider a = a, b = b as non zero Nat ;
B2: a * ((a * n) + b) = (a lcm ((a * n) + b)) * (a gcd ((a * n) + b)) by NAT_D:29
.= (a lcm ((a * n) + b)) * (a gcd b) by NEWTON02:5 ;
((a * a) * n) + (a * b) = (a gcd b) * ((((a * a) * n) / (a gcd b)) + ((a * b) / (a gcd b))) by XCMPLX_1:114;
then a lcm ((a * n) + b) = (((a * a) * n) / (a gcd b)) + ((a * b) / (a gcd b)) by B2, XCMPLX_1:5
.= (((a * n) * a) / (a gcd b)) + (((a lcm b) * (a gcd b)) / (a gcd b)) by NAT_D:29
.= (((a * n) * a) / (a gcd b)) + (a lcm b) by XCMPLX_1:89
.= ((a * n) * (a / (a gcd b))) + (a lcm b) by XCMPLX_1:74
.= ((a * n) * ((a lcm b) / b)) + (a lcm b) by GL
.= (((a * n) / b) * (a lcm b)) + (1 * (a lcm b)) by XCMPLX_1:75 ;
hence a lcm ((a * n) + b) = (((a * n) / b) + 1) * (a lcm b) ; :: thesis: verum
end;
end;