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 e. ( ZZ>= ` 2 ) /\ X e/ Prime ) -> X e. ( ZZ>= ` 4 ) )

Proof

Step Hyp Ref Expression
1 eluz2b2 
 |-  ( X e. ( ZZ>= ` 2 ) <-> ( X e. NN /\ 1 < X ) )
2 4z 
 |-  4 e. ZZ
3 2 a1i 
 |-  ( ( ( X e. NN /\ 1 < X ) /\ X e/ Prime ) -> 4 e. ZZ )
4 nnz 
 |-  ( X e. NN -> X e. ZZ )
5 4 ad2antrr 
 |-  ( ( ( X e. NN /\ 1 < X ) /\ X e/ Prime ) -> X e. ZZ )
6 1z 
 |-  1 e. ZZ
7 zltp1le 
 |-  ( ( 1 e. ZZ /\ X e. ZZ ) -> ( 1 < X <-> ( 1 + 1 ) <_ X ) )
8 6 4 7 sylancr 
 |-  ( X e. NN -> ( 1 < X <-> ( 1 + 1 ) <_ X ) )
9 1p1e2 
 |-  ( 1 + 1 ) = 2
10 9 breq1i 
 |-  ( ( 1 + 1 ) <_ X <-> 2 <_ X )
11 8 10 bitrdi 
 |-  ( X e. NN -> ( 1 < X <-> 2 <_ X ) )
12 2re 
 |-  2 e. RR
13 nnre 
 |-  ( X e. NN -> X e. RR )
14 leloe 
 |-  ( ( 2 e. RR /\ X e. RR ) -> ( 2 <_ X <-> ( 2 < X \/ 2 = X ) ) )
15 12 13 14 sylancr 
 |-  ( X e. NN -> ( 2 <_ X <-> ( 2 < X \/ 2 = X ) ) )
16 2z 
 |-  2 e. ZZ
17 zltp1le 
 |-  ( ( 2 e. ZZ /\ X e. ZZ ) -> ( 2 < X <-> ( 2 + 1 ) <_ X ) )
18 16 4 17 sylancr 
 |-  ( X e. NN -> ( 2 < X <-> ( 2 + 1 ) <_ X ) )
19 2p1e3 
 |-  ( 2 + 1 ) = 3
20 19 breq1i 
 |-  ( ( 2 + 1 ) <_ X <-> 3 <_ X )
21 18 20 bitrdi 
 |-  ( X e. NN -> ( 2 < X <-> 3 <_ X ) )
22 3re 
 |-  3 e. RR
23 leloe 
 |-  ( ( 3 e. RR /\ X e. RR ) -> ( 3 <_ X <-> ( 3 < X \/ 3 = X ) ) )
24 22 13 23 sylancr 
 |-  ( X e. NN -> ( 3 <_ X <-> ( 3 < X \/ 3 = X ) ) )
25 df-4 
 |-  4 = ( 3 + 1 )
26 3z 
 |-  3 e. ZZ
27 zltp1le 
 |-  ( ( 3 e. ZZ /\ X e. ZZ ) -> ( 3 < X <-> ( 3 + 1 ) <_ X ) )
28 26 4 27 sylancr 
 |-  ( X e. NN -> ( 3 < X <-> ( 3 + 1 ) <_ X ) )
29 28 biimpa 
 |-  ( ( X e. NN /\ 3 < X ) -> ( 3 + 1 ) <_ X )
30 25 29 eqbrtrid 
 |-  ( ( X e. NN /\ 3 < X ) -> 4 <_ X )
31 30 a1d 
 |-  ( ( X e. NN /\ 3 < X ) -> ( X e/ Prime -> 4 <_ X ) )
32 31 ex 
 |-  ( X e. NN -> ( 3 < X -> ( X e/ Prime -> 4 <_ X ) ) )
33 neleq1 
 |-  ( X = 3 -> ( X e/ Prime <-> 3 e/ Prime ) )
34 33 eqcoms 
 |-  ( 3 = X -> ( X e/ Prime <-> 3 e/ Prime ) )
35 3prm 
 |-  3 e. Prime
36 pm2.24nel 
 |-  ( 3 e. Prime -> ( 3 e/ Prime -> 4 <_ X ) )
37 35 36 mp1i 
 |-  ( 3 = X -> ( 3 e/ Prime -> 4 <_ X ) )
38 34 37 sylbid 
 |-  ( 3 = X -> ( X e/ Prime -> 4 <_ X ) )
39 38 a1i 
 |-  ( X e. NN -> ( 3 = X -> ( X e/ Prime -> 4 <_ X ) ) )
40 32 39 jaod 
 |-  ( X e. NN -> ( ( 3 < X \/ 3 = X ) -> ( X e/ Prime -> 4 <_ X ) ) )
41 24 40 sylbid 
 |-  ( X e. NN -> ( 3 <_ X -> ( X e/ Prime -> 4 <_ X ) ) )
42 21 41 sylbid 
 |-  ( X e. NN -> ( 2 < X -> ( X e/ Prime -> 4 <_ X ) ) )
43 neleq1 
 |-  ( X = 2 -> ( X e/ Prime <-> 2 e/ Prime ) )
44 43 eqcoms 
 |-  ( 2 = X -> ( X e/ Prime <-> 2 e/ Prime ) )
45 2prm 
 |-  2 e. Prime
46 pm2.24nel 
 |-  ( 2 e. Prime -> ( 2 e/ Prime -> 4 <_ X ) )
47 45 46 mp1i 
 |-  ( 2 = X -> ( 2 e/ Prime -> 4 <_ X ) )
48 44 47 sylbid 
 |-  ( 2 = X -> ( X e/ Prime -> 4 <_ X ) )
49 48 a1i 
 |-  ( X e. NN -> ( 2 = X -> ( X e/ Prime -> 4 <_ X ) ) )
50 42 49 jaod 
 |-  ( X e. NN -> ( ( 2 < X \/ 2 = X ) -> ( X e/ Prime -> 4 <_ X ) ) )
51 15 50 sylbid 
 |-  ( X e. NN -> ( 2 <_ X -> ( X e/ Prime -> 4 <_ X ) ) )
52 11 51 sylbid 
 |-  ( X e. NN -> ( 1 < X -> ( X e/ Prime -> 4 <_ X ) ) )
53 52 imp 
 |-  ( ( X e. NN /\ 1 < X ) -> ( X e/ Prime -> 4 <_ X ) )
54 53 imp 
 |-  ( ( ( X e. NN /\ 1 < X ) /\ X e/ Prime ) -> 4 <_ X )
55 3 5 54 3jca 
 |-  ( ( ( X e. NN /\ 1 < X ) /\ X e/ Prime ) -> ( 4 e. ZZ /\ X e. ZZ /\ 4 <_ X ) )
56 55 ex 
 |-  ( ( X e. NN /\ 1 < X ) -> ( X e/ Prime -> ( 4 e. ZZ /\ X e. ZZ /\ 4 <_ X ) ) )
57 eluz2 
 |-  ( X e. ( ZZ>= ` 4 ) <-> ( 4 e. ZZ /\ X e. ZZ /\ 4 <_ X ) )
58 56 57 imbitrrdi 
 |-  ( ( X e. NN /\ 1 < X ) -> ( X e/ Prime -> X e. ( ZZ>= ` 4 ) ) )
59 1 58 sylbi 
 |-  ( X e. ( ZZ>= ` 2 ) -> ( X e/ Prime -> X e. ( ZZ>= ` 4 ) ) )
60 59 imp 
 |-  ( ( X e. ( ZZ>= ` 2 ) /\ X e/ Prime ) -> X e. ( ZZ>= ` 4 ) )