Metamath Proof Explorer

Theorem 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 ∈ ℤ ≥ 2 ∧ X ∉ ℙ → X ∈ ℤ ≥ 4

Proof

Step Hyp Ref Expression
1 eluz2b2 ⊢ X ∈ ℤ ≥ 2 ↔ X ∈ ℕ ∧ 1 < X
2 4z ⊢ 4 ∈ ℤ
3 2 a1i ⊢ X ∈ ℕ ∧ 1 < X ∧ X ∉ ℙ → 4 ∈ ℤ
4 nnz ⊢ X ∈ ℕ → X ∈ ℤ
5 4 ad2antrr ⊢ X ∈ ℕ ∧ 1 < X ∧ X ∉ ℙ → X ∈ ℤ
6 1z ⊢ 1 ∈ ℤ
7 zltp1le ⊢ 1 ∈ ℤ ∧ X ∈ ℤ → 1 < X ↔ 1 + 1 ≤ X
8 6 4 7 sylancr ⊢ X ∈ ℕ → 1 < X ↔ 1 + 1 ≤ X
9 1p1e2 ⊢ 1 + 1 = 2
10 9 breq1i ⊢ 1 + 1 ≤ X ↔ 2 ≤ X
11 8 10 bitrdi ⊢ X ∈ ℕ → 1 < X ↔ 2 ≤ X
12 2re ⊢ 2 ∈ ℝ
13 nnre ⊢ X ∈ ℕ → X ∈ ℝ
14 leloe ⊢ 2 ∈ ℝ ∧ X ∈ ℝ → 2 ≤ X ↔ 2 < X ∨ 2 = X
15 12 13 14 sylancr ⊢ X ∈ ℕ → 2 ≤ X ↔ 2 < X ∨ 2 = X
16 2z ⊢ 2 ∈ ℤ
17 zltp1le ⊢ 2 ∈ ℤ ∧ X ∈ ℤ → 2 < X ↔ 2 + 1 ≤ X
18 16 4 17 sylancr ⊢ X ∈ ℕ → 2 < X ↔ 2 + 1 ≤ X
19 2p1e3 ⊢ 2 + 1 = 3
20 19 breq1i ⊢ 2 + 1 ≤ X ↔ 3 ≤ X
21 18 20 bitrdi ⊢ X ∈ ℕ → 2 < X ↔ 3 ≤ X
22 3re ⊢ 3 ∈ ℝ
23 leloe ⊢ 3 ∈ ℝ ∧ X ∈ ℝ → 3 ≤ X ↔ 3 < X ∨ 3 = X
24 22 13 23 sylancr ⊢ X ∈ ℕ → 3 ≤ X ↔ 3 < X ∨ 3 = X
25 df-4 ⊢ 4 = 3 + 1
26 3z ⊢ 3 ∈ ℤ
27 zltp1le ⊢ 3 ∈ ℤ ∧ X ∈ ℤ → 3 < X ↔ 3 + 1 ≤ X
28 26 4 27 sylancr ⊢ X ∈ ℕ → 3 < X ↔ 3 + 1 ≤ X
29 28 biimpa ⊢ X ∈ ℕ ∧ 3 < X → 3 + 1 ≤ X
30 25 29 eqbrtrid ⊢ X ∈ ℕ ∧ 3 < X → 4 ≤ X
31 30 a1d ⊢ X ∈ ℕ ∧ 3 < X → X ∉ ℙ → 4 ≤ X
32 31 ex ⊢ X ∈ ℕ → 3 < X → X ∉ ℙ → 4 ≤ X
33 neleq1 ⊢ X = 3 → X ∉ ℙ ↔ 3 ∉ ℙ
34 33 eqcoms ⊢ 3 = X → X ∉ ℙ ↔ 3 ∉ ℙ
35 3prm ⊢ 3 ∈ ℙ
36 pm2.24nel ⊢ 3 ∈ ℙ → 3 ∉ ℙ → 4 ≤ X
37 35 36 mp1i ⊢ 3 = X → 3 ∉ ℙ → 4 ≤ X
38 34 37 sylbid ⊢ 3 = X → X ∉ ℙ → 4 ≤ X
39 38 a1i ⊢ X ∈ ℕ → 3 = X → X ∉ ℙ → 4 ≤ X
40 32 39 jaod ⊢ X ∈ ℕ → 3 < X ∨ 3 = X → X ∉ ℙ → 4 ≤ X
41 24 40 sylbid ⊢ X ∈ ℕ → 3 ≤ X → X ∉ ℙ → 4 ≤ X
42 21 41 sylbid ⊢ X ∈ ℕ → 2 < X → X ∉ ℙ → 4 ≤ X
43 neleq1 ⊢ X = 2 → X ∉ ℙ ↔ 2 ∉ ℙ
44 43 eqcoms ⊢ 2 = X → X ∉ ℙ ↔ 2 ∉ ℙ
45 2prm ⊢ 2 ∈ ℙ
46 pm2.24nel ⊢ 2 ∈ ℙ → 2 ∉ ℙ → 4 ≤ X
47 45 46 mp1i ⊢ 2 = X → 2 ∉ ℙ → 4 ≤ X
48 44 47 sylbid ⊢ 2 = X → X ∉ ℙ → 4 ≤ X
49 48 a1i ⊢ X ∈ ℕ → 2 = X → X ∉ ℙ → 4 ≤ X
50 42 49 jaod ⊢ X ∈ ℕ → 2 < X ∨ 2 = X → X ∉ ℙ → 4 ≤ X
51 15 50 sylbid ⊢ X ∈ ℕ → 2 ≤ X → X ∉ ℙ → 4 ≤ X
52 11 51 sylbid ⊢ X ∈ ℕ → 1 < X → X ∉ ℙ → 4 ≤ X
53 52 imp ⊢ X ∈ ℕ ∧ 1 < X → X ∉ ℙ → 4 ≤ X
54 53 imp ⊢ X ∈ ℕ ∧ 1 < X ∧ X ∉ ℙ → 4 ≤ X
55 3 5 54 3jca ⊢ X ∈ ℕ ∧ 1 < X ∧ X ∉ ℙ → 4 ∈ ℤ ∧ X ∈ ℤ ∧ 4 ≤ X
56 55 ex ⊢ X ∈ ℕ ∧ 1 < X → X ∉ ℙ → 4 ∈ ℤ ∧ X ∈ ℤ ∧ 4 ≤ X
57 eluz2 ⊢ X ∈ ℤ ≥ 4 ↔ 4 ∈ ℤ ∧ X ∈ ℤ ∧ 4 ≤ X
58 56 57 imbitrrdi ⊢ X ∈ ℕ ∧ 1 < X → X ∉ ℙ → X ∈ ℤ ≥ 4
59 1 58 sylbi ⊢ X ∈ ℤ ≥ 2 → X ∉ ℙ → X ∈ ℤ ≥ 4
60 59 imp ⊢ X ∈ ℤ ≥ 2 ∧ X ∉ ℙ → X ∈ ℤ ≥ 4