Theorem gausslemma2dlem0f

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

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

Proof

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 )