Metamath Proof Explorer


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 )