ncoprmlnprm

Description: If two positive integers are not coprime, the larger of them is not a prime number. (Contributed by AV, 9-Aug-2020)

		Ref	Expression
	Assertion	ncoprmlnprm	$⊢ (A \in ℕ \land B \in ℕ \land A < B) \to (1 < A \gcd B \to B \notin ℙ)$

Proof

Step	Hyp	Ref	Expression
1		ncoprmgcdgt1b	$⊢ (A \in ℕ \land B \in ℕ) \to (\exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B) \leftrightarrow 1 < A \gcd B)$
2	1	bicomd	$⊢ (A \in ℕ \land B \in ℕ) \to (1 < A \gcd B \leftrightarrow \exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B))$
3	2	3adant3	$⊢ (A \in ℕ \land B \in ℕ \land A < B) \to (1 < A \gcd B \leftrightarrow \exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B))$
4		simp1	$⊢ (A \in ℕ \land B \in ℕ \land A < B) \to A \in ℕ$
5		eluzelz	$⊢ i \in ℤ_{\geq 2} \to i \in ℤ$
6	4 5	anim12ci	$⊢ ((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \to (i \in ℤ \land A \in ℕ)$
7		dvdsle	$⊢ (i \in ℤ \land A \in ℕ) \to (i ∥ A \to i \leq A)$
8	6 7	syl	$⊢ ((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \to (i ∥ A \to i \leq A)$
9		nnre	$⊢ A \in ℕ \to A \in ℝ$
10		nnre	$⊢ B \in ℕ \to B \in ℝ$
11		eluzelre	$⊢ i \in ℤ_{\geq 2} \to i \in ℝ$
12	9 10 11	3anim123i	$⊢ (A \in ℕ \land B \in ℕ \land i \in ℤ_{\geq 2}) \to (A \in ℝ \land B \in ℝ \land i \in ℝ)$
13		3anrot	$⊢ (i \in ℝ \land A \in ℝ \land B \in ℝ) \leftrightarrow (A \in ℝ \land B \in ℝ \land i \in ℝ)$
14	12 13	sylibr	$⊢ (A \in ℕ \land B \in ℕ \land i \in ℤ_{\geq 2}) \to (i \in ℝ \land A \in ℝ \land B \in ℝ)$
15		lelttr	$⊢ (i \in ℝ \land A \in ℝ \land B \in ℝ) \to ((i \leq A \land A < B) \to i < B)$
16	14 15	syl	$⊢ (A \in ℕ \land B \in ℕ \land i \in ℤ_{\geq 2}) \to ((i \leq A \land A < B) \to i < B)$
17	16	expcomd	$⊢ (A \in ℕ \land B \in ℕ \land i \in ℤ_{\geq 2}) \to (A < B \to (i \leq A \to i < B))$
18	17	3exp	$⊢ A \in ℕ \to (B \in ℕ \to (i \in ℤ_{\geq 2} \to (A < B \to (i \leq A \to i < B))))$
19	18	com34	$⊢ A \in ℕ \to (B \in ℕ \to (A < B \to (i \in ℤ_{\geq 2} \to (i \leq A \to i < B))))$
20	19	3imp1	$⊢ ((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \to (i \leq A \to i < B)$
21	20	imp	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land i \leq A) \to i < B$
22		nnz	$⊢ B \in ℕ \to B \in ℤ$
23	22	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land A < B) \to B \in ℤ$
24	23 5	anim12ci	$⊢ ((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \to (i \in ℤ \land B \in ℤ)$
25	24	adantr	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land i \leq A) \to (i \in ℤ \land B \in ℤ)$
26		zltlem1	$⊢ (i \in ℤ \land B \in ℤ) \to (i < B \leftrightarrow i \leq B - 1)$
27	25 26	syl	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land i \leq A) \to (i < B \leftrightarrow i \leq B - 1)$
28	21 27	mpbid	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land i \leq A) \to i \leq B - 1$
29	28	ex	$⊢ ((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \to (i \leq A \to i \leq B - 1)$
30	8 29	syldc	$⊢ i ∥ A \to (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \to i \leq B - 1)$
31	30	adantr	$⊢ (i ∥ A \land i ∥ B) \to (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \to i \leq B - 1)$
32	31	impcom	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \to i \leq B - 1$
33		peano2zm	$⊢ B \in ℤ \to B - 1 \in ℤ$
34	22 33	syl	$⊢ B \in ℕ \to B - 1 \in ℤ$
35	34	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land A < B) \to B - 1 \in ℤ$
36	35	anim1ci	$⊢ ((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \to (i \in ℤ_{\geq 2} \land B - 1 \in ℤ)$
37	36	adantr	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \to (i \in ℤ_{\geq 2} \land B - 1 \in ℤ)$
38		elfz5	$⊢ (i \in ℤ_{\geq 2} \land B - 1 \in ℤ) \to (i \in (2 \dots B - 1) \leftrightarrow i \leq B - 1)$
39	37 38	syl	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \to (i \in (2 \dots B - 1) \leftrightarrow i \leq B - 1)$
40	32 39	mpbird	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \to i \in (2 \dots B - 1)$
41		breq1	$⊢ j = i \to (j ∥ B \leftrightarrow i ∥ B)$
42	41	adantl	$⊢ ((((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \land j = i) \to (j ∥ B \leftrightarrow i ∥ B)$
43		simprr	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \to i ∥ B$
44	40 42 43	rspcedvd	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \to \exists j \in (2 \dots B - 1) j ∥ B$
45		rexnal	$⊢ \exists j \in (2 \dots B - 1) \neg \neg j ∥ B \leftrightarrow \neg \forall j \in (2 \dots B - 1) \neg j ∥ B$
46		notnotb	$⊢ j ∥ B \leftrightarrow \neg \neg j ∥ B$
47	46	bicomi	$⊢ \neg \neg j ∥ B \leftrightarrow j ∥ B$
48	47	rexbii	$⊢ \exists j \in (2 \dots B - 1) \neg \neg j ∥ B \leftrightarrow \exists j \in (2 \dots B - 1) j ∥ B$
49	45 48	bitr3i	$⊢ \neg \forall j \in (2 \dots B - 1) \neg j ∥ B \leftrightarrow \exists j \in (2 \dots B - 1) j ∥ B$
50	44 49	sylibr	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \to \neg \forall j \in (2 \dots B - 1) \neg j ∥ B$
51	50	olcd	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \to (\neg B \in ℤ_{\geq 2} \lor \neg \forall j \in (2 \dots B - 1) \neg j ∥ B)$
52		df-nel	$⊢ B \notin ℙ \leftrightarrow \neg B \in ℙ$
53		ianor	$⊢ \neg (B \in ℤ_{\geq 2} \land \forall j \in (2 \dots B - 1) \neg j ∥ B) \leftrightarrow (\neg B \in ℤ_{\geq 2} \lor \neg \forall j \in (2 \dots B - 1) \neg j ∥ B)$
54		isprm3	$⊢ B \in ℙ \leftrightarrow (B \in ℤ_{\geq 2} \land \forall j \in (2 \dots B - 1) \neg j ∥ B)$
55	53 54	xchnxbir	$⊢ \neg B \in ℙ \leftrightarrow (\neg B \in ℤ_{\geq 2} \lor \neg \forall j \in (2 \dots B - 1) \neg j ∥ B)$
56	52 55	bitri	$⊢ B \notin ℙ \leftrightarrow (\neg B \in ℤ_{\geq 2} \lor \neg \forall j \in (2 \dots B - 1) \neg j ∥ B)$
57	51 56	sylibr	$⊢ (((A \in ℕ \land B \in ℕ \land A < B) \land i \in ℤ_{\geq 2}) \land (i ∥ A \land i ∥ B)) \to B \notin ℙ$
58	57	rexlimdva2	$⊢ (A \in ℕ \land B \in ℕ \land A < B) \to (\exists i \in ℤ_{\geq 2} (i ∥ A \land i ∥ B) \to B \notin ℙ)$
59	3 58	sylbid	$⊢ (A \in ℕ \land B \in ℕ \land A < B) \to (1 < A \gcd B \to B \notin ℙ)$

Metamath Proof Explorer

Theorem ncoprmlnprm

Proof