Metamath Proof Explorer


Theorem gausslemma2dlem0g

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

Ref Expression
Hypotheses gausslemma2dlem0.p ( 𝜑𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2dlem0.m 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
gausslemma2dlem0.h 𝐻 = ( ( 𝑃 − 1 ) / 2 )
Assertion gausslemma2dlem0g ( 𝜑𝑀𝐻 )

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0.p ( 𝜑𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 gausslemma2dlem0.m 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
3 gausslemma2dlem0.h 𝐻 = ( ( 𝑃 − 1 ) / 2 )
4 1 gausslemma2dlem0a ( 𝜑𝑃 ∈ ℕ )
5 fldiv4lem1div2 ( 𝑃 ∈ ℕ → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
6 4 5 syl ( 𝜑 → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
7 6 2 3 3brtr4g ( 𝜑𝑀𝐻 )