Theorem gausslemma2dlem0e

Description: Auxiliary lemma 5 for gausslemma2d . (Contributed by AV, 9-Jul-2021)

	Ref	Expression
Hypotheses	gausslemma2dlem0.p	|- ( ph -> P e. ( Prime \ { 2 } ) )
	gausslemma2dlem0.m	|- M = ( |_ ` ( P / 4 ) )
Assertion	gausslemma2dlem0e	|- ( ph -> ( M x. 2 ) < ( P / 2 ) )

Proof

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	1 4 6	3syl	|- ( ph -> ( P e. ZZ /\ -. 2 || P ) )
8		flodddiv4t2lthalf	|- ( ( P e. ZZ /\ -. 2 || P ) -> ( ( |_ ` ( P / 4 ) ) x. 2 ) < ( P / 2 ) )
9	7 8	syl	|- ( ph -> ( ( |_ ` ( P / 4 ) ) x. 2 ) < ( P / 2 ) )
10	3 9	eqbrtrid	|- ( ph -> ( M x. 2 ) < ( P / 2 ) )