dvdsnprmd

Description: If a number is divisible by an integer greater than 1 and less than the number, the number is not prime. (Contributed by AV, 24-Jul-2021)

	Ref	Expression
Hypotheses	dvdsnprmd.g	$⊢ φ \to 1 < A$
	dvdsnprmd.l	$⊢ φ \to A < N$
	dvdsnprmd.d	$⊢ φ \to A ∥ N$
Assertion	dvdsnprmd	$⊢ φ \to \neg N \in ℙ$

Proof

Step	Hyp	Ref	Expression
1		dvdsnprmd.g	$⊢ φ \to 1 < A$
2		dvdsnprmd.l	$⊢ φ \to A < N$
3		dvdsnprmd.d	$⊢ φ \to A ∥ N$
4		dvdszrcl	$⊢ A ∥ N \to (A \in ℤ \land N \in ℤ)$
5		divides	$⊢ (A \in ℤ \land N \in ℤ) \to (A ∥ N \leftrightarrow \exists k \in ℤ k A = N)$
6	3 4 5	3syl	$⊢ φ \to (A ∥ N \leftrightarrow \exists k \in ℤ k A = N)$
7		2z	$⊢ 2 \in ℤ$
8	7	a1i	$⊢ ((φ \land k \in ℤ) \land k A = N) \to 2 \in ℤ$
9		simplr	$⊢ ((φ \land k \in ℤ) \land k A = N) \to k \in ℤ$
10	2	adantr	$⊢ (φ \land k \in ℤ) \to A < N$
11	10	adantr	$⊢ ((φ \land k \in ℤ) \land k A = N) \to A < N$
12		breq2	$⊢ k A = N \to (A < k A \leftrightarrow A < N)$
13	12	adantl	$⊢ ((φ \land k \in ℤ) \land k A = N) \to (A < k A \leftrightarrow A < N)$
14	11 13	mpbird	$⊢ ((φ \land k \in ℤ) \land k A = N) \to A < k A$
15		zre	$⊢ A \in ℤ \to A \in ℝ$
16	15	3ad2ant1	$⊢ (A \in ℤ \land 1 < A \land k \in ℤ) \to A \in ℝ$
17		zre	$⊢ k \in ℤ \to k \in ℝ$
18	17	3ad2ant3	$⊢ (A \in ℤ \land 1 < A \land k \in ℤ) \to k \in ℝ$
19		0lt1	$⊢ 0 < 1$
20		0red	$⊢ A \in ℤ \to 0 \in ℝ$
21		1red	$⊢ A \in ℤ \to 1 \in ℝ$
22		lttr	$⊢ (0 \in ℝ \land 1 \in ℝ \land A \in ℝ) \to ((0 < 1 \land 1 < A) \to 0 < A)$
23	20 21 15 22	syl3anc	$⊢ A \in ℤ \to ((0 < 1 \land 1 < A) \to 0 < A)$
24	19 23	mpani	$⊢ A \in ℤ \to (1 < A \to 0 < A)$
25	24	imp	$⊢ (A \in ℤ \land 1 < A) \to 0 < A$
26	25	3adant3	$⊢ (A \in ℤ \land 1 < A \land k \in ℤ) \to 0 < A$
27	16 18 26	3jca	$⊢ (A \in ℤ \land 1 < A \land k \in ℤ) \to (A \in ℝ \land k \in ℝ \land 0 < A)$
28	27	3exp	$⊢ A \in ℤ \to (1 < A \to (k \in ℤ \to (A \in ℝ \land k \in ℝ \land 0 < A)))$
29	28	adantr	$⊢ (A \in ℤ \land N \in ℤ) \to (1 < A \to (k \in ℤ \to (A \in ℝ \land k \in ℝ \land 0 < A)))$
30	3 4 29	3syl	$⊢ φ \to (1 < A \to (k \in ℤ \to (A \in ℝ \land k \in ℝ \land 0 < A)))$
31	1 30	mpd	$⊢ φ \to (k \in ℤ \to (A \in ℝ \land k \in ℝ \land 0 < A))$
32	31	imp	$⊢ (φ \land k \in ℤ) \to (A \in ℝ \land k \in ℝ \land 0 < A)$
33	32	adantr	$⊢ ((φ \land k \in ℤ) \land k A = N) \to (A \in ℝ \land k \in ℝ \land 0 < A)$
34		ltmulgt12	$⊢ (A \in ℝ \land k \in ℝ \land 0 < A) \to (1 < k \leftrightarrow A < k A)$
35	33 34	syl	$⊢ ((φ \land k \in ℤ) \land k A = N) \to (1 < k \leftrightarrow A < k A)$
36	14 35	mpbird	$⊢ ((φ \land k \in ℤ) \land k A = N) \to 1 < k$
37		df-2	$⊢ 2 = 1 + 1$
38	37	breq1i	$⊢ 2 \leq k \leftrightarrow 1 + 1 \leq k$
39		1zzd	$⊢ k \in ℤ \to 1 \in ℤ$
40		zltp1le	$⊢ (1 \in ℤ \land k \in ℤ) \to (1 < k \leftrightarrow 1 + 1 \leq k)$
41	39 40	mpancom	$⊢ k \in ℤ \to (1 < k \leftrightarrow 1 + 1 \leq k)$
42	41	bicomd	$⊢ k \in ℤ \to (1 + 1 \leq k \leftrightarrow 1 < k)$
43	42	adantl	$⊢ (φ \land k \in ℤ) \to (1 + 1 \leq k \leftrightarrow 1 < k)$
44	43	adantr	$⊢ ((φ \land k \in ℤ) \land k A = N) \to (1 + 1 \leq k \leftrightarrow 1 < k)$
45	38 44	syl5bb	$⊢ ((φ \land k \in ℤ) \land k A = N) \to (2 \leq k \leftrightarrow 1 < k)$
46	36 45	mpbird	$⊢ ((φ \land k \in ℤ) \land k A = N) \to 2 \leq k$
47		eluz2	$⊢ k \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land k \in ℤ \land 2 \leq k)$
48	8 9 46 47	syl3anbrc	$⊢ ((φ \land k \in ℤ) \land k A = N) \to k \in ℤ_{\geq 2}$
49	7	a1i	$⊢ (A \in ℤ \land 1 < A) \to 2 \in ℤ$
50		simpl	$⊢ (A \in ℤ \land 1 < A) \to A \in ℤ$
51		1zzd	$⊢ A \in ℤ \to 1 \in ℤ$
52		zltp1le	$⊢ (1 \in ℤ \land A \in ℤ) \to (1 < A \leftrightarrow 1 + 1 \leq A)$
53	51 52	mpancom	$⊢ A \in ℤ \to (1 < A \leftrightarrow 1 + 1 \leq A)$
54	53	biimpa	$⊢ (A \in ℤ \land 1 < A) \to 1 + 1 \leq A$
55	37	breq1i	$⊢ 2 \leq A \leftrightarrow 1 + 1 \leq A$
56	54 55	sylibr	$⊢ (A \in ℤ \land 1 < A) \to 2 \leq A$
57	49 50 56	3jca	$⊢ (A \in ℤ \land 1 < A) \to (2 \in ℤ \land A \in ℤ \land 2 \leq A)$
58	57	ex	$⊢ A \in ℤ \to (1 < A \to (2 \in ℤ \land A \in ℤ \land 2 \leq A))$
59	58	adantr	$⊢ (A \in ℤ \land N \in ℤ) \to (1 < A \to (2 \in ℤ \land A \in ℤ \land 2 \leq A))$
60	3 4 59	3syl	$⊢ φ \to (1 < A \to (2 \in ℤ \land A \in ℤ \land 2 \leq A))$
61	1 60	mpd	$⊢ φ \to (2 \in ℤ \land A \in ℤ \land 2 \leq A)$
62		eluz2	$⊢ A \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land A \in ℤ \land 2 \leq A)$
63	61 62	sylibr	$⊢ φ \to A \in ℤ_{\geq 2}$
64	63	adantr	$⊢ (φ \land k \in ℤ) \to A \in ℤ_{\geq 2}$
65	64	adantr	$⊢ ((φ \land k \in ℤ) \land k A = N) \to A \in ℤ_{\geq 2}$
66		nprm	$⊢ (k \in ℤ_{\geq 2} \land A \in ℤ_{\geq 2}) \to \neg k A \in ℙ$
67	48 65 66	syl2anc	$⊢ ((φ \land k \in ℤ) \land k A = N) \to \neg k A \in ℙ$
68		eleq1	$⊢ k A = N \to (k A \in ℙ \leftrightarrow N \in ℙ)$
69	68	notbid	$⊢ k A = N \to (\neg k A \in ℙ \leftrightarrow \neg N \in ℙ)$
70	69	adantl	$⊢ ((φ \land k \in ℤ) \land k A = N) \to (\neg k A \in ℙ \leftrightarrow \neg N \in ℙ)$
71	67 70	mpbid	$⊢ ((φ \land k \in ℤ) \land k A = N) \to \neg N \in ℙ$
72	71	rexlimdva2	$⊢ φ \to (\exists k \in ℤ k A = N \to \neg N \in ℙ)$
73	6 72	sylbid	$⊢ φ \to (A ∥ N \to \neg N \in ℙ)$
74	3 73	mpd	$⊢ φ \to \neg N \in ℙ$

Metamath Proof Explorer

Theorem dvdsnprmd

Proof