Theorem ncoprmgcdgt1b

Description: Two positive integers are not coprime, i.e. there is an integer greater than 1 which divides both integers, iff their greatest common divisor is greater than 1. (Contributed by AV, 9-Aug-2020)

	Ref	Expression
Assertion	ncoprmgcdgt1b	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(\exists i\in {\mathbb{Z}}_{\ge 2}\left(i\parallel A\wedge i\parallel B\right)\leftrightarrow 1<A\gcd B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ncoprmgcdne1b	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(\exists i\in {\mathbb{Z}}_{\ge 2}\left(i\parallel A\wedge i\parallel B\right)\leftrightarrow A\gcd B\ne 1\right)$$
2		gcdnncl	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to A\gcd B\in \mathbb{N}$$
3		nngt1ne1	$$⊢A\gcd B\in \mathbb{N}\to \left(1<A\gcd B\leftrightarrow A\gcd B\ne 1\right)$$
4	2 3	syl	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(1<A\gcd B\leftrightarrow A\gcd B\ne 1\right)$$
5	1 4	bitr4d	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(\exists i\in {\mathbb{Z}}_{\ge 2}\left(i\parallel A\wedge i\parallel B\right)\leftrightarrow 1<A\gcd B\right)$$