Metamath Proof Explorer


Theorem gausslemma2dlem0a

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

Ref Expression
Hypothesis gausslemma2dlem0a.p
|- ( ph -> P e. ( Prime \ { 2 } ) )
Assertion gausslemma2dlem0a
|- ( ph -> P e. NN )

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0a.p
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 nnoddn2prm
 |-  ( P e. ( Prime \ { 2 } ) -> ( P e. NN /\ -. 2 || P ) )
3 simpl
 |-  ( ( P e. NN /\ -. 2 || P ) -> P e. NN )
4 1 2 3 3syl
 |-  ( ph -> P e. NN )