Theorem gausslemma2dlem0f

Description: Auxiliary lemma 6 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	gausslemma2dlem0f	$$⊢\phi \to M+1\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		eldifsn	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\leftrightarrow \left(P\in \mathbb{P}\wedge P\ne 2\right)$$
5		prm23ge5	$$⊢P\in \mathbb{P}\to \left(P=2\vee P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)$$
6		eqneqall	$$⊢P=2\to \left(P\ne 2\to \left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)\right)$$
7		orc	$$⊢P=3\to \left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)$$
8	7	a1d	$$⊢P=3\to \left(P\ne 2\to \left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)\right)$$
9		olc	$$⊢P\in {\mathbb{Z}}_{\ge 5}\to \left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)$$
10	9	a1d	$$⊢P\in {\mathbb{Z}}_{\ge 5}\to \left(P\ne 2\to \left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)\right)$$
11	6 8 10	3jaoi	$$⊢\left(P=2\vee P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)\to \left(P\ne 2\to \left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)\right)$$
12	5 11	syl	$$⊢P\in \mathbb{P}\to \left(P\ne 2\to \left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)\right)$$
13	12	imp	$$⊢\left(P\in \mathbb{P}\wedge P\ne 2\right)\to \left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)$$
14	4 13	sylbi	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)$$
15		fldiv4p1lem1div2	$$⊢\left(P=3\vee P\in {\mathbb{Z}}_{\ge 5}\right)\to ⌊\frac{P}{4}⌋+1\le \frac{P-1}{2}$$
16	1 14 15	3syl	$$⊢\phi \to ⌊\frac{P}{4}⌋+1\le \frac{P-1}{2}$$
17	2	oveq1i	$$⊢M+1=⌊\frac{P}{4}⌋+1$$
18	16 17 3	3brtr4g	$$⊢\phi \to M+1\le H$$