ncoprmgcdne1b

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 not 1. See prmdvdsncoprmbd for a version where the existential quantifier is restricted to primes. (Contributed by AV, 9-Aug-2020)

		Ref	Expression
	Assertion	ncoprmgcdne1b	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B) \leftrightarrow A \gcd B \neq 1)$

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$⊢ i \in ℤ_{\geq 2} \to i \in ℕ$
2	1	adantr	$⊢ (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B)) \to i \in ℕ$
3		eluz2b3	$⊢ i \in ℤ_{\geq 2} \leftrightarrow (i \in ℕ \land i \neq 1)$
4		neneq	$⊢ i \neq 1 \to \neg i = 1$
5	3 4	simplbiim	$⊢ i \in ℤ_{\geq 2} \to \neg i = 1$
6	5	anim1ci	$⊢ (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B)) \to ((i ∥ A \land i ∥ B) \land \neg i = 1)$
7	2 6	jca	$⊢ (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B)) \to (i \in ℕ \land ((i ∥ A \land i ∥ B) \land \neg i = 1))$
8		neqne	$⊢ \neg i = 1 \to i \neq 1$
9	8	anim1ci	$⊢ (\neg i = 1 \land i \in ℕ) \to (i \in ℕ \land i \neq 1)$
10	9 3	sylibr	$⊢ (\neg i = 1 \land i \in ℕ) \to i \in ℤ_{\geq 2}$
11	10	ex	$⊢ \neg i = 1 \to (i \in ℕ \to i \in ℤ_{\geq 2})$
12	11	adantl	$⊢ ((i ∥ A \land i ∥ B) \land \neg i = 1) \to (i \in ℕ \to i \in ℤ_{\geq 2})$
13	12	impcom	$⊢ (i \in ℕ \land ((i ∥ A \land i ∥ B) \land \neg i = 1)) \to i \in ℤ_{\geq 2}$
14	13	adantl	$⊢ ((A \in ℕ \land B \in ℕ) \land (i \in ℕ \land ((i ∥ A \land i ∥ B) \land \neg i = 1))) \to i \in ℤ_{\geq 2}$
15		simprrl	$⊢ ((A \in ℕ \land B \in ℕ) \land (i \in ℕ \land ((i ∥ A \land i ∥ B) \land \neg i = 1))) \to (i ∥ A \land i ∥ B)$
16	14 15	jca	$⊢ ((A \in ℕ \land B \in ℕ) \land (i \in ℕ \land ((i ∥ A \land i ∥ B) \land \neg i = 1))) \to (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))$
17	16	ex	$⊢ (A \in ℕ \land B \in ℕ) \to ((i \in ℕ \land ((i ∥ A \land i ∥ B) \land \neg i = 1)) \to (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B)))$
18	7 17	impbid2	$⊢ (A \in ℕ \land B \in ℕ) \to ((i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B)) \leftrightarrow (i \in ℕ \land ((i ∥ A \land i ∥ B) \land \neg i = 1)))$
19	18	rexbidv2	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B) \leftrightarrow \exists i \in ℕ ((i ∥ A \land i ∥ B) \land \neg i = 1))$
20		rexanali	$⊢ \exists i \in ℕ ((i ∥ A \land i ∥ B) \land \neg i = 1) \leftrightarrow \neg \forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1)$
21	20	a1i	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists i \in ℕ ((i ∥ A \land i ∥ B) \land \neg i = 1) \leftrightarrow \neg \forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1))$
22		coprmgcdb	$⊢ (A \in ℕ \land B \in ℕ) \to (\forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1) \leftrightarrow A \gcd B = 1)$
23	22	necon3bbid	$⊢ (A \in ℕ \land B \in ℕ) \to (\neg \forall i \in ℕ ((i ∥ A \land i ∥ B) \to i = 1) \leftrightarrow A \gcd B \neq 1)$
24	19 21 23	3bitrd	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B) \leftrightarrow A \gcd B \neq 1)$

Metamath Proof Explorer

Theorem ncoprmgcdne1b

Proof