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	⊢ ( 𝜑 → 𝑀 ≤ 𝐻 )