let a, b, c, n be Nat; ( ( a <> 0 or b <> 0 ) & c <> 0 & a,b,c are_mutually_coprime & a divides n & b divides n & c divides n implies (a * b) * c divides n )
assume that
A1:
( ( a <> 0 or b <> 0 ) & c <> 0 )
and
A2:
a,b,c are_mutually_coprime
and
A3:
( a divides n & b divides n )
; ( not c divides n or (a * b) * c divides n )
a * b divides n
by A2, A3, PEPIN:4;
hence
( not c divides n or (a * b) * c divides n )
by A1, A2, PEPIN:4, EULER_1:14; verum