Theorem gausslemma2dlem0a

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

	Ref	Expression
Hypothesis	gausslemma2dlem0a.p	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
Assertion	gausslemma2dlem0a	$$⊢\phi \to P\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0a.p	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
2		nnoddn2prm	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \left(P\in \mathbb{N}\wedge \neg 2\parallel P\right)$$
3		simpl	$$⊢\left(P\in \mathbb{N}\wedge \neg 2\parallel P\right)\to P\in \mathbb{N}$$
4	1 2 3	3syl	$$⊢\phi \to P\in \mathbb{N}$$