let a be Nat; :: thesis: for b being non trivial Nat
for c being non zero Nat st a mod (b * c) = 1 holds
a mod b = 1
let b be non trivial Nat; :: thesis: for c being non zero Nat st a mod (b * c) = 1 holds
a mod b = 1
let c be non zero Nat; :: thesis: ( a mod (b * c) = 1 implies a mod b = 1 )
reconsider k = b - 1 as non zero Nat ;

per cases ( c is trivial or not c is trivial ) ;

suppose c is trivial ; :: thesis: ( a mod (b * c) = 1 implies a mod b = 1 )

then c = 1 by NAT_2:def 1;
hence ( a mod (b * c) = 1 implies a mod b = 1 ) ; :: thesis: verum

end;

suppose not c is trivial ; :: thesis: ( a mod (b * c) = 1 implies a mod b = 1 )

then reconsider l = c - 1 as non zero Nat ;
assume a mod (b * c) = 1 ; :: thesis: a mod b = 1
then a mod (b * c) = 1 mod (b * c) ;
then A2: b * c divides a - 1 by INT_4:23;
b divides b * c ;
then b divides a - 1 by A2, INT_2:9;
then a mod b = 1 mod (1 + k) by INT_4:23;
hence a mod b = 1 ; :: thesis: verum

end;

end;