Theorem nnoddn2prm

Description: A prime not equal to 2 is an odd positive integer. (Contributed by AV, 28-Jun-2021)

	Ref	Expression
Assertion	nnoddn2prm	|- ( N e. ( Prime \ { 2 } ) -> ( N e. NN /\ -. 2 || N ) )

Proof

Step	Hyp	Ref	Expression
1		eldifi	|- ( N e. ( Prime \ { 2 } ) -> N e. Prime )
2		prmnn	|- ( N e. Prime -> N e. NN )
3	1 2	syl	|- ( N e. ( Prime \ { 2 } ) -> N e. NN )
4		oddprm	|- ( N e. ( Prime \ { 2 } ) -> ( ( N - 1 ) / 2 ) e. NN )
5		nnz	|- ( ( ( N - 1 ) / 2 ) e. NN -> ( ( N - 1 ) / 2 ) e. ZZ )
6		nnz	|- ( N e. NN -> N e. ZZ )
7		oddm1d2	|- ( N e. ZZ -> ( -. 2 || N <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
8	6 7	syl	|- ( N e. NN -> ( -. 2 || N <-> ( ( N - 1 ) / 2 ) e. ZZ ) )
9	5 8	syl5ibrcom	|- ( ( ( N - 1 ) / 2 ) e. NN -> ( N e. NN -> -. 2 || N ) )
10	4 9	syl	|- ( N e. ( Prime \ { 2 } ) -> ( N e. NN -> -. 2 || N ) )
11	3 10	jcai	|- ( N e. ( Prime \ { 2 } ) -> ( N e. NN /\ -. 2 || N ) )