Theorem gausslemma2dlem0h

Description: Auxiliary lemma 8 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}$$
	gausslemma2dlem0.n	$$⊢N=H-M$$
Assertion	gausslemma2dlem0h	$$⊢\phi \to N\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		gausslemma2dlem0.h	$$⊢H=\frac{P-1}{2}$$
4		gausslemma2dlem0.n	$$⊢N=H-M$$
5	1 3	gausslemma2dlem0b	$$⊢\phi \to H\in \mathbb{N}$$
6	5	nnzd	$$⊢\phi \to H\in \mathbb{Z}$$
7	1 2	gausslemma2dlem0d	$$⊢\phi \to M\in {\mathbb{N}}_0$$
8	7	nn0zd	$$⊢\phi \to M\in \mathbb{Z}$$
9	6 8	zsubcld	$$⊢\phi \to H-M\in \mathbb{Z}$$
10	1 2 3	gausslemma2dlem0g	$$⊢\phi \to M\le H$$
11	5	nnred	$$⊢\phi \to H\in ℝ$$
12	7	nn0red	$$⊢\phi \to M\in ℝ$$
13	11 12	subge0d	$$⊢\phi \to \left(0\le H-M\leftrightarrow M\le H\right)$$
14	10 13	mpbird	$$⊢\phi \to 0\le H-M$$
15		elnn0z	$$⊢H-M\in {\mathbb{N}}_0\leftrightarrow \left(H-M\in \mathbb{Z}\wedge 0\le H-M\right)$$
16	9 14 15	sylanbrc	$$⊢\phi \to H-M\in {\mathbb{N}}_0$$
17	4 16	eqeltrid	$$⊢\phi \to N\in {\mathbb{N}}_0$$