Theorem gausslemma2dlem0g

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

	Ref	Expression
Hypotheses	gausslemma2dlem0.p	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
	gausslemma2dlem0.m	$$⊢M=⌊\frac{P}{4}⌋$$
	gausslemma2dlem0.h	$$⊢H=\frac{P-1}{2}$$
Assertion	gausslemma2dlem0g	$$⊢\phi \to M\le H$$

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0.p	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
2		gausslemma2dlem0.m	$$⊢M=⌊\frac{P}{4}⌋$$
3		gausslemma2dlem0.h	$$⊢H=\frac{P-1}{2}$$
4	1	gausslemma2dlem0a	$$⊢\phi \to P\in \mathbb{N}$$
5		fldiv4lem1div2	$$⊢P\in \mathbb{N}\to ⌊\frac{P}{4}⌋\le \frac{P-1}{2}$$
6	4 5	syl	$$⊢\phi \to ⌊\frac{P}{4}⌋\le \frac{P-1}{2}$$
7	6 2 3	3brtr4g	$$⊢\phi \to M\le H$$