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 syl6ibr ⊢X∈ℕ∧1<X→X∉ℙ→X∈ℤ≥4
59 1 58 sylbi ⊢X∈ℤ≥2→X∉ℙ→X∈ℤ≥4
60 59 imp ⊢X∈ℤ≥2∧X∉ℙ→X∈ℤ≥4