Theorem gausslemma2dlem0a

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

	Ref	Expression
Hypothesis	gausslemma2dlem0a.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
Assertion	gausslemma2dlem0a	⊢ ( 𝜑 → 𝑃 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0a.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2		nnoddn2prm	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) )
3		simpl	⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → 𝑃 ∈ ℕ )
4	1 2 3	3syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )