Theorem gausslemma2dlem0e

Description: Auxiliary lemma 5 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}⌋$$
Assertion	gausslemma2dlem0e	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 2<\frac{P}{2}$$

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	2	oveq1i	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 2=⌊\frac{P}{4}⌋\cdot 2$$
4		nnoddn2prm	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \left(P\in \mathbb{N}\wedge \neg 2\parallel P\right)$$
5		nnz	$$⊢P\in \mathbb{N}\to P\in \mathbb{Z}$$
6	5	anim1i	$$⊢\left(P\in \mathbb{N}\wedge \neg 2\parallel P\right)\to \left(P\in \mathbb{Z}\wedge \neg 2\parallel P\right)$$
7		flodddiv4t2lthalf	$$⊢\left(P\in \mathbb{Z}\wedge \neg 2\parallel P\right)\to ⌊\frac{P}{4}⌋\cdot 2<\frac{P}{2}$$
8	1 4 6 7	4syl	$$⊢\phi \to ⌊\frac{P}{4}⌋\cdot 2<\frac{P}{2}$$
9	3 8	eqbrtrid	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 2<\frac{P}{2}$$