let i1, i2 be Integer; :: thesis: for n being Nat st n > 0 & i1 mod n = 0 holds

(i1 * i2) mod n = 0

let n be Nat; :: thesis: ( n > 0 & i1 mod n = 0 implies (i1 * i2) mod n = 0 )

assume that

A1: n > 0 and

A2: i1 mod n = 0 ; :: thesis: (i1 * i2) mod n = 0

n divides i1 by A1, A2, INT_1:62;

then n divides i1 * i2 by INT_2:2;

hence (i1 * i2) mod n = 0 by A1, INT_1:62; :: thesis: verum

(i1 * i2) mod n = 0

let n be Nat; :: thesis: ( n > 0 & i1 mod n = 0 implies (i1 * i2) mod n = 0 )

assume that

A1: n > 0 and

A2: i1 mod n = 0 ; :: thesis: (i1 * i2) mod n = 0

n divides i1 by A1, A2, INT_1:62;

then n divides i1 * i2 by INT_2:2;

hence (i1 * i2) mod n = 0 by A1, INT_1:62; :: thesis: verum