Theorem gausslemma2dlem0b

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

	Ref	Expression
Hypotheses	gausslemma2dlem0a.p	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
	gausslemma2dlem0b.h	$$⊢H=\frac{P-1}{2}$$
Assertion	gausslemma2dlem0b	$$⊢\phi \to H\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0a.p	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
2		gausslemma2dlem0b.h	$$⊢H=\frac{P-1}{2}$$
3		eldifi	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to P\in \mathbb{P}$$
4		prmuz2	$$⊢P\in \mathbb{P}\to P\in {\mathbb{Z}}_{\ge 2}$$
5	3 4	syl	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to P\in {\mathbb{Z}}_{\ge 2}$$
6		nnoddn2prm	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \left(P\in \mathbb{N}\wedge \neg 2\parallel P\right)$$
7		nnoddm1d2	$$⊢P\in \mathbb{N}\to \left(\neg 2\parallel P\leftrightarrow \frac{P+1}{2}\in \mathbb{N}\right)$$
8	7	biimpa	$$⊢\left(P\in \mathbb{N}\wedge \neg 2\parallel P\right)\to \frac{P+1}{2}\in \mathbb{N}$$
9	8	nnnn0d	$$⊢\left(P\in \mathbb{N}\wedge \neg 2\parallel P\right)\to \frac{P+1}{2}\in {\mathbb{N}}_0$$
10	6 9	syl	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \frac{P+1}{2}\in {\mathbb{N}}_0$$
11	5 10	jca	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \left(P\in {\mathbb{Z}}_{\ge 2}\wedge \frac{P+1}{2}\in {\mathbb{N}}_0\right)$$
12	1 11	syl	$$⊢\phi \to \left(P\in {\mathbb{Z}}_{\ge 2}\wedge \frac{P+1}{2}\in {\mathbb{N}}_0\right)$$
13		nno	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \frac{P+1}{2}\in {\mathbb{N}}_0\right)\to \frac{P-1}{2}\in \mathbb{N}$$
14	12 13	syl	$$⊢\phi \to \frac{P-1}{2}\in \mathbb{N}$$
15	2 14	eqeltrid	$$⊢\phi \to H\in \mathbb{N}$$