Step |
Hyp |
Ref |
Expression |
1 |
|
gausslemma2dlem0.p |
|- ( ph -> P e. ( Prime \ { 2 } ) ) |
2 |
|
gausslemma2dlem0.m |
|- M = ( |_ ` ( P / 4 ) ) |
3 |
|
gausslemma2dlem0.h |
|- H = ( ( P - 1 ) / 2 ) |
4 |
|
eldifsn |
|- ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) ) |
5 |
|
prm23ge5 |
|- ( P e. Prime -> ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) |
6 |
|
eqneqall |
|- ( P = 2 -> ( P =/= 2 -> ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) |
7 |
|
orc |
|- ( P = 3 -> ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) |
8 |
7
|
a1d |
|- ( P = 3 -> ( P =/= 2 -> ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) |
9 |
|
olc |
|- ( P e. ( ZZ>= ` 5 ) -> ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) |
10 |
9
|
a1d |
|- ( P e. ( ZZ>= ` 5 ) -> ( P =/= 2 -> ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) |
11 |
6 8 10
|
3jaoi |
|- ( ( P = 2 \/ P = 3 \/ P e. ( ZZ>= ` 5 ) ) -> ( P =/= 2 -> ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) |
12 |
5 11
|
syl |
|- ( P e. Prime -> ( P =/= 2 -> ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) ) |
13 |
12
|
imp |
|- ( ( P e. Prime /\ P =/= 2 ) -> ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) |
14 |
4 13
|
sylbi |
|- ( P e. ( Prime \ { 2 } ) -> ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) ) |
15 |
|
fldiv4p1lem1div2 |
|- ( ( P = 3 \/ P e. ( ZZ>= ` 5 ) ) -> ( ( |_ ` ( P / 4 ) ) + 1 ) <_ ( ( P - 1 ) / 2 ) ) |
16 |
1 14 15
|
3syl |
|- ( ph -> ( ( |_ ` ( P / 4 ) ) + 1 ) <_ ( ( P - 1 ) / 2 ) ) |
17 |
2
|
oveq1i |
|- ( M + 1 ) = ( ( |_ ` ( P / 4 ) ) + 1 ) |
18 |
16 17 3
|
3brtr4g |
|- ( ph -> ( M + 1 ) <_ H ) |