let p be Prime; :: thesis: for n being non zero Nat st n < p holds
n gcd p = 1
let n be non zero Nat; :: thesis: ( n < p implies n gcd p = 1 )
assume A: n < p ; :: thesis: n gcd p = 1
( 1 * n = n & 1 * p = p ) ;
then B: ( 1 divides n & 1 divides p ) by NAT_D:def 3;

now :: thesis: for m being Nat st m divides n & m divides p holds
m divides 1

let m be Nat; :: thesis: ( m divides n & m divides p implies b₁ divides 1 )
assume C: ( m divides n & m divides p ) ; :: thesis: b₁ divides 1

per cases then ( m = 1 or m = p ) by INT_2:def 4;

suppose m = 1 ; :: thesis: b₁ divides 1

hence m divides 1 ; :: thesis: verum

end;

suppose m = p ; :: thesis: b₁ divides 1

hence m divides 1 by A, C, NAT_D:7; :: thesis: verum

end;

end;

end;

hence n gcd p = 1 by B, NAT_D:def 5; :: thesis: verum