let p, q be Nat; :: thesis: ( p is prime & q is prime & not p,q are_coprime implies p = q )

assume that

A1: p is prime and

A2: q is prime ; :: thesis: ( p,q are_coprime or p = q )

A3: p gcd q divides q by Def2;

assume not p,q are_coprime ; :: thesis: p = q

then A4: p gcd q <> 1 ;

p gcd q divides p by Def2;

then p gcd q = p by A1, A4;

hence p = q by A2, A4, A3; :: thesis: verum

assume that

A1: p is prime and

A2: q is prime ; :: thesis: ( p,q are_coprime or p = q )

A3: p gcd q divides q by Def2;

assume not p,q are_coprime ; :: thesis: p = q

then A4: p gcd q <> 1 ;

p gcd q divides p by Def2;

then p gcd q = p by A1, A4;

hence p = q by A2, A4, A3; :: thesis: verum