Theorem gausslemma2dlem0d

Description: Auxiliary lemma 4 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	gausslemma2dlem0d	$$⊢\phi \to M\in {\mathbb{N}}_0$$

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	1	gausslemma2dlem0a	$$⊢\phi \to P\in \mathbb{N}$$
4		nnre	$$⊢P\in \mathbb{N}\to P\in ℝ$$
5		4re	$$⊢4\in ℝ$$
6	5	a1i	$$⊢P\in \mathbb{N}\to 4\in ℝ$$
7		4ne0	$$⊢4\ne 0$$
8	7	a1i	$$⊢P\in \mathbb{N}\to 4\ne 0$$
9	4 6 8	redivcld	$$⊢P\in \mathbb{N}\to \frac{P}{4}\in ℝ$$
10		nnnn0	$$⊢P\in \mathbb{N}\to P\in {\mathbb{N}}_0$$
11	10	nn0ge0d	$$⊢P\in \mathbb{N}\to 0\le P$$
12		4pos	$$⊢0<4$$
13	5 12	pm3.2i	$$⊢\left(4\in ℝ\wedge 0<4\right)$$
14	13	a1i	$$⊢P\in \mathbb{N}\to \left(4\in ℝ\wedge 0<4\right)$$
15		divge0	$$⊢\left(\left(P\in ℝ\wedge 0\le P\right)\wedge \left(4\in ℝ\wedge 0<4\right)\right)\to 0\le \frac{P}{4}$$
16	4 11 14 15	syl21anc	$$⊢P\in \mathbb{N}\to 0\le \frac{P}{4}$$
17	9 16	jca	$$⊢P\in \mathbb{N}\to \left(\frac{P}{4}\in ℝ\wedge 0\le \frac{P}{4}\right)$$
18		flge0nn0	$$⊢\left(\frac{P}{4}\in ℝ\wedge 0\le \frac{P}{4}\right)\to ⌊\frac{P}{4}⌋\in {\mathbb{N}}_0$$
19	3 17 18	3syl	$$⊢\phi \to ⌊\frac{P}{4}⌋\in {\mathbb{N}}_0$$
20	2 19	eqeltrid	$$⊢\phi \to M\in {\mathbb{N}}_0$$