consider j being Integer such that
A1: i = 2 * j by Lm1;
i - 1 = (2 * (j - 1)) + 1 by A1;
hence not i - 1 is even ; :: thesis: verum