prmdvdsncoprmbd

Description: Two positive integers are not coprime iff a prime divides both integers. Deduction version of ncoprmgcdne1b with the existential quantifier over the primes instead of integers greater than or equal to 2. (Contributed by SN, 24-Aug-2024)

	Ref	Expression
Hypotheses	prmdvdsncoprmbd.a	$⊢ φ \to A \in ℕ$
	prmdvdsncoprmbd.b	$⊢ φ \to B \in ℕ$
Assertion	prmdvdsncoprmbd	$⊢ φ \to (\exists p \in ℙ (p ∥ A \land p ∥ B) \leftrightarrow A \gcd B \neq 1)$

Proof

Step	Hyp	Ref	Expression
1		prmdvdsncoprmbd.a	$⊢ φ \to A \in ℕ$
2		prmdvdsncoprmbd.b	$⊢ φ \to B \in ℕ$
3		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
4	3	a1i	$⊢ φ \to (p \in ℙ \to p \in ℤ_{\geq 2})$
5	4	anim1d	$⊢ φ \to ((p \in ℙ \land (p ∥ A \land p ∥ B)) \to (p \in ℤ_{\geq 2} \land (p ∥ A \land p ∥ B)))$
6	5	reximdv2	$⊢ φ \to (\exists p \in ℙ (p ∥ A \land p ∥ B) \to \exists p \in ℤ_{\geq 2} (p ∥ A \land p ∥ B))$
7		breq1	$⊢ p = i \to (p ∥ A \leftrightarrow i ∥ A)$
8		breq1	$⊢ p = i \to (p ∥ B \leftrightarrow i ∥ B)$
9	7 8	anbi12d	$⊢ p = i \to ((p ∥ A \land p ∥ B) \leftrightarrow (i ∥ A \land i ∥ B))$
10	9	cbvrexvw	$⊢ \exists p \in ℤ_{\geq 2} (p ∥ A \land p ∥ B) \leftrightarrow \exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B)$
11	6 10	syl6ib	$⊢ φ \to (\exists p \in ℙ (p ∥ A \land p ∥ B) \to \exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B))$
12		exprmfct	$⊢ i \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ i$
13	12	ad2antrl	$⊢ (φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \to \exists p \in ℙ p ∥ i$
14		prmnn	$⊢ p \in ℙ \to p \in ℕ$
15	14	ad2antlr	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to p \in ℕ$
16	15	nnzd	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to p \in ℤ$
17		eluzelz	$⊢ i \in ℤ_{\geq 2} \to i \in ℤ$
18	17	ad2antrr	$⊢ ((i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B)) \land p ∥ i) \to i \in ℤ$
19	18	ad4ant24	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to i \in ℤ$
20	1	ad3antrrr	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to A \in ℕ$
21	20	nnzd	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to A \in ℤ$
22		simpr	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to p ∥ i$
23		simprrl	$⊢ (φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \to i ∥ A$
24	23	ad2antrr	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to i ∥ A$
25	16 19 21 22 24	dvdstrd	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to p ∥ A$
26	2	ad3antrrr	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to B \in ℕ$
27	26	nnzd	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to B \in ℤ$
28		simprrr	$⊢ (φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \to i ∥ B$
29	28	ad2antrr	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to i ∥ B$
30	16 19 27 22 29	dvdstrd	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to p ∥ B$
31	25 30	jca	$⊢ (((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \land p ∥ i) \to (p ∥ A \land p ∥ B)$
32	31	ex	$⊢ ((φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \land p \in ℙ) \to (p ∥ i \to (p ∥ A \land p ∥ B))$
33	32	reximdva	$⊢ (φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \to (\exists p \in ℙ p ∥ i \to \exists p \in ℙ (p ∥ A \land p ∥ B))$
34	13 33	mpd	$⊢ (φ \land (i \in ℤ_{\geq 2} \land (i ∥ A \land i ∥ B))) \to \exists p \in ℙ (p ∥ A \land p ∥ B)$
35	34	rexlimdvaa	$⊢ φ \to (\exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B) \to \exists p \in ℙ (p ∥ A \land p ∥ B))$
36	11 35	impbid	$⊢ φ \to (\exists p \in ℙ (p ∥ A \land p ∥ B) \leftrightarrow \exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B))$
37		ncoprmgcdne1b	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B) \leftrightarrow A \gcd B \neq 1)$
38	1 2 37	syl2anc	$⊢ φ \to (\exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B) \leftrightarrow A \gcd B \neq 1)$
39	36 38	bitrd	$⊢ φ \to (\exists p \in ℙ (p ∥ A \land p ∥ B) \leftrightarrow A \gcd B \neq 1)$

Metamath Proof Explorer

Theorem prmdvdsncoprmbd

Proof