ge2nprmge4

Description: A composite integer greater than or equal to 2 is greater than or equal to 4 . (Contributed by AV, 5-Jun-2023)

		Ref	Expression
	Assertion	ge2nprmge4	$⊢ (X \in ℤ_{\geq 2} \land X \notin ℙ) \to X \in ℤ_{\geq 4}$

Proof

Step	Hyp	Ref	Expression
1		eluz2b2	$⊢ X \in ℤ_{\geq 2} \leftrightarrow (X \in ℕ \land 1 < X)$
2		4z	$⊢ 4 \in ℤ$
3	2	a1i	$⊢ ((X \in ℕ \land 1 < X) \land X \notin ℙ) \to 4 \in ℤ$
4		nnz	$⊢ X \in ℕ \to X \in ℤ$
5	4	ad2antrr	$⊢ ((X \in ℕ \land 1 < X) \land X \notin ℙ) \to X \in ℤ$
6		1z	$⊢ 1 \in ℤ$
7		zltp1le	$⊢ (1 \in ℤ \land X \in ℤ) \to (1 < X \leftrightarrow 1 + 1 \leq X)$
8	6 4 7	sylancr	$⊢ X \in ℕ \to (1 < X \leftrightarrow 1 + 1 \leq X)$
9		1p1e2	$⊢ 1 + 1 = 2$
10	9	breq1i	$⊢ 1 + 1 \leq X \leftrightarrow 2 \leq X$
11	8 10	bitrdi	$⊢ X \in ℕ \to (1 < X \leftrightarrow 2 \leq X)$
12		2re	$⊢ 2 \in ℝ$
13		nnre	$⊢ X \in ℕ \to X \in ℝ$
14		leloe	$⊢ (2 \in ℝ \land X \in ℝ) \to (2 \leq X \leftrightarrow (2 < X \lor 2 = X))$
15	12 13 14	sylancr	$⊢ X \in ℕ \to (2 \leq X \leftrightarrow (2 < X \lor 2 = X))$
16		2z	$⊢ 2 \in ℤ$
17		zltp1le	$⊢ (2 \in ℤ \land X \in ℤ) \to (2 < X \leftrightarrow 2 + 1 \leq X)$
18	16 4 17	sylancr	$⊢ X \in ℕ \to (2 < X \leftrightarrow 2 + 1 \leq X)$
19		2p1e3	$⊢ 2 + 1 = 3$
20	19	breq1i	$⊢ 2 + 1 \leq X \leftrightarrow 3 \leq X$
21	18 20	bitrdi	$⊢ X \in ℕ \to (2 < X \leftrightarrow 3 \leq X)$
22		3re	$⊢ 3 \in ℝ$
23		leloe	$⊢ (3 \in ℝ \land X \in ℝ) \to (3 \leq X \leftrightarrow (3 < X \lor 3 = X))$
24	22 13 23	sylancr	$⊢ X \in ℕ \to (3 \leq X \leftrightarrow (3 < X \lor 3 = X))$
25		df-4	$⊢ 4 = 3 + 1$
26		3z	$⊢ 3 \in ℤ$
27		zltp1le	$⊢ (3 \in ℤ \land X \in ℤ) \to (3 < X \leftrightarrow 3 + 1 \leq X)$
28	26 4 27	sylancr	$⊢ X \in ℕ \to (3 < X \leftrightarrow 3 + 1 \leq X)$
29	28	biimpa	$⊢ (X \in ℕ \land 3 < X) \to 3 + 1 \leq X$
30	25 29	eqbrtrid	$⊢ (X \in ℕ \land 3 < X) \to 4 \leq X$
31	30	a1d	$⊢ (X \in ℕ \land 3 < X) \to (X \notin ℙ \to 4 \leq X)$
32	31	ex	$⊢ X \in ℕ \to (3 < X \to (X \notin ℙ \to 4 \leq X))$
33		neleq1	$⊢ X = 3 \to (X \notin ℙ \leftrightarrow 3 \notin ℙ)$
34	33	eqcoms	$⊢ 3 = X \to (X \notin ℙ \leftrightarrow 3 \notin ℙ)$
35		3prm	$⊢ 3 \in ℙ$
36		elnelall	$⊢ 3 \in ℙ \to (3 \notin ℙ \to 4 \leq X)$
37	35 36	mp1i	$⊢ 3 = X \to (3 \notin ℙ \to 4 \leq X)$
38	34 37	sylbid	$⊢ 3 = X \to (X \notin ℙ \to 4 \leq X)$
39	38	a1i	$⊢ X \in ℕ \to (3 = X \to (X \notin ℙ \to 4 \leq X))$
40	32 39	jaod	$⊢ X \in ℕ \to ((3 < X \lor 3 = X) \to (X \notin ℙ \to 4 \leq X))$
41	24 40	sylbid	$⊢ X \in ℕ \to (3 \leq X \to (X \notin ℙ \to 4 \leq X))$
42	21 41	sylbid	$⊢ X \in ℕ \to (2 < X \to (X \notin ℙ \to 4 \leq X))$
43		neleq1	$⊢ X = 2 \to (X \notin ℙ \leftrightarrow 2 \notin ℙ)$
44	43	eqcoms	$⊢ 2 = X \to (X \notin ℙ \leftrightarrow 2 \notin ℙ)$
45		2prm	$⊢ 2 \in ℙ$
46		elnelall	$⊢ 2 \in ℙ \to (2 \notin ℙ \to 4 \leq X)$
47	45 46	mp1i	$⊢ 2 = X \to (2 \notin ℙ \to 4 \leq X)$
48	44 47	sylbid	$⊢ 2 = X \to (X \notin ℙ \to 4 \leq X)$
49	48	a1i	$⊢ X \in ℕ \to (2 = X \to (X \notin ℙ \to 4 \leq X))$
50	42 49	jaod	$⊢ X \in ℕ \to ((2 < X \lor 2 = X) \to (X \notin ℙ \to 4 \leq X))$
51	15 50	sylbid	$⊢ X \in ℕ \to (2 \leq X \to (X \notin ℙ \to 4 \leq X))$
52	11 51	sylbid	$⊢ X \in ℕ \to (1 < X \to (X \notin ℙ \to 4 \leq X))$
53	52	imp	$⊢ (X \in ℕ \land 1 < X) \to (X \notin ℙ \to 4 \leq X)$
54	53	imp	$⊢ ((X \in ℕ \land 1 < X) \land X \notin ℙ) \to 4 \leq X$
55	3 5 54	3jca	$⊢ ((X \in ℕ \land 1 < X) \land X \notin ℙ) \to (4 \in ℤ \land X \in ℤ \land 4 \leq X)$
56	55	ex	$⊢ (X \in ℕ \land 1 < X) \to (X \notin ℙ \to (4 \in ℤ \land X \in ℤ \land 4 \leq X))$
57		eluz2	$⊢ X \in ℤ_{\geq 4} \leftrightarrow (4 \in ℤ \land X \in ℤ \land 4 \leq X)$
58	56 57	syl6ibr	$⊢ (X \in ℕ \land 1 < X) \to (X \notin ℙ \to X \in ℤ_{\geq 4})$
59	1 58	sylbi	$⊢ X \in ℤ_{\geq 2} \to (X \notin ℙ \to X \in ℤ_{\geq 4})$
60	59	imp	$⊢ (X \in ℤ_{\geq 2} \land X \notin ℙ) \to X \in ℤ_{\geq 4}$

Metamath Proof Explorer

Theorem ge2nprmge4

Proof