let x1, h be Nat; :: thesis: for y1 being Integer st 1 < h & x1 mod h = y1 mod h & y1 = 0 holds
ex m1 being Integer st x1 = h * m1
let y1 be Integer; :: thesis: ( 1 < h & x1 mod h = y1 mod h & y1 = 0 implies ex m1 being Integer st x1 = h * m1 )
assume that
A1: 1 < h and
A2: x1 mod h = y1 mod h and
A3: y1 = 0 ; :: thesis: ex m1 being Integer st x1 = h * m1
A5: x1 mod h = 0 by NAT_D:26, A2, A3;
reconsider x1 = x1 as Integer ;
A6: h divides x1 by A1, A5, INT_1:62;
reconsider h = h as Integer ;
thus ex m1 being Integer st x1 = h * m1 by A6, INT_1:def 3; :: thesis: verum