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 ( ( 𝑋 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∉ ℙ ) → 𝑋 ∈ ( ℤ≥ ‘ 4 ) )

Proof

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