let i be Integer; :: thesis: for p being Prime holds

( i,p are_coprime or p divides i )

let p be Prime; :: thesis: ( i,p are_coprime or p divides i )

( i,p are_coprime or p divides i )

let p be Prime; :: thesis: ( i,p are_coprime or p divides i )

per cases
( i >= 0 or i < 0 )
;

end;

suppose
i >= 0
; :: thesis: ( i,p are_coprime or p divides i )

then reconsider i = i as Element of NAT by INT_1:3;

( i,p are_coprime or i gcd p = p ) by PEPIN:2;

hence ( i,p are_coprime or p divides i ) by NAT_D:def 5; :: thesis: verum

end;( i,p are_coprime or i gcd p = p ) by PEPIN:2;

hence ( i,p are_coprime or p divides i ) by NAT_D:def 5; :: thesis: verum

suppose A1:
i < 0
; :: thesis: ( i,p are_coprime or p divides i )

then reconsider m = - i as Element of NAT by INT_1:3;

A2: ( m,p are_coprime or m gcd p = p ) by PEPIN:2;

end;A2: ( m,p are_coprime or m gcd p = p ) by PEPIN:2;

per cases
( m,p are_coprime or p divides m )
by A2, NAT_D:def 5;

end;

suppose A3:
m,p are_coprime
; :: thesis: ( i,p are_coprime or p divides i )

m = |.i.|
by A1, ABSVALUE:def 1;

then i gcd p = m gcd |.p.| by INT_2:34

.= m gcd p by ABSVALUE:def 1

.= 1 by A3, INT_2:def 3 ;

hence ( i,p are_coprime or p divides i ) by INT_2:def 3; :: thesis: verum

end;then i gcd p = m gcd |.p.| by INT_2:34

.= m gcd p by ABSVALUE:def 1

.= 1 by A3, INT_2:def 3 ;

hence ( i,p are_coprime or p divides i ) by INT_2:def 3; :: thesis: verum

suppose
p divides m
; :: thesis: ( i,p are_coprime or p divides i )

then consider t being Nat such that

A4: m = p * t by NAT_D:def 3;

i = p * (- t) by A4;

hence ( i,p are_coprime or p divides i ) ; :: thesis: verum

end;A4: m = p * t by NAT_D:def 3;

i = p * (- t) by A4;

hence ( i,p are_coprime or p divides i ) ; :: thesis: verum