Step |
Hyp |
Ref |
Expression |
1 |
|
eldifi |
|- ( P e. ( Prime \ { 2 } ) -> P e. Prime ) |
2 |
|
oddprmgt2 |
|- ( P e. ( Prime \ { 2 } ) -> 2 < P ) |
3 |
|
3z |
|- 3 e. ZZ |
4 |
3
|
a1i |
|- ( ( P e. Prime /\ 2 < P ) -> 3 e. ZZ ) |
5 |
|
prmz |
|- ( P e. Prime -> P e. ZZ ) |
6 |
5
|
adantr |
|- ( ( P e. Prime /\ 2 < P ) -> P e. ZZ ) |
7 |
|
df-3 |
|- 3 = ( 2 + 1 ) |
8 |
|
2z |
|- 2 e. ZZ |
9 |
|
zltp1le |
|- ( ( 2 e. ZZ /\ P e. ZZ ) -> ( 2 < P <-> ( 2 + 1 ) <_ P ) ) |
10 |
8 5 9
|
sylancr |
|- ( P e. Prime -> ( 2 < P <-> ( 2 + 1 ) <_ P ) ) |
11 |
10
|
biimpa |
|- ( ( P e. Prime /\ 2 < P ) -> ( 2 + 1 ) <_ P ) |
12 |
7 11
|
eqbrtrid |
|- ( ( P e. Prime /\ 2 < P ) -> 3 <_ P ) |
13 |
4 6 12
|
3jca |
|- ( ( P e. Prime /\ 2 < P ) -> ( 3 e. ZZ /\ P e. ZZ /\ 3 <_ P ) ) |
14 |
1 2 13
|
syl2anc |
|- ( P e. ( Prime \ { 2 } ) -> ( 3 e. ZZ /\ P e. ZZ /\ 3 <_ P ) ) |
15 |
|
eluz2 |
|- ( P e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ P e. ZZ /\ 3 <_ P ) ) |
16 |
14 15
|
sylibr |
|- ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 3 ) ) |