Step |
Hyp |
Ref |
Expression |
1 |
|
gausslemma2dlem0.p |
|- ( ph -> P e. ( Prime \ { 2 } ) ) |
2 |
|
gausslemma2dlem0.m |
|- M = ( |_ ` ( P / 4 ) ) |
3 |
2
|
oveq1i |
|- ( M x. 2 ) = ( ( |_ ` ( P / 4 ) ) x. 2 ) |
4 |
|
nnoddn2prm |
|- ( P e. ( Prime \ { 2 } ) -> ( P e. NN /\ -. 2 || P ) ) |
5 |
|
nnz |
|- ( P e. NN -> P e. ZZ ) |
6 |
5
|
anim1i |
|- ( ( P e. NN /\ -. 2 || P ) -> ( P e. ZZ /\ -. 2 || P ) ) |
7 |
|
flodddiv4t2lthalf |
|- ( ( P e. ZZ /\ -. 2 || P ) -> ( ( |_ ` ( P / 4 ) ) x. 2 ) < ( P / 2 ) ) |
8 |
1 4 6 7
|
4syl |
|- ( ph -> ( ( |_ ` ( P / 4 ) ) x. 2 ) < ( P / 2 ) ) |
9 |
3 8
|
eqbrtrid |
|- ( ph -> ( M x. 2 ) < ( P / 2 ) ) |