Theorem gausslemma2dlem0b

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

	Ref	Expression
Hypotheses	gausslemma2dlem0a.p	|- ( ph -> P e. ( Prime \ { 2 } ) )
	gausslemma2dlem0b.h	|- H = ( ( P - 1 ) / 2 )
Assertion	gausslemma2dlem0b	|- ( ph -> H e. NN )

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0a.p	|- ( ph -> P e. ( Prime \ { 2 } ) )
2		gausslemma2dlem0b.h	|- H = ( ( P - 1 ) / 2 )
3		eldifi	|- ( P e. ( Prime \ { 2 } ) -> P e. Prime )
4		prmuz2	|- ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
5	3 4	syl	|- ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 2 ) )
6		nnoddn2prm	|- ( P e. ( Prime \ { 2 } ) -> ( P e. NN /\ -. 2 || P ) )
7		nnoddm1d2	|- ( P e. NN -> ( -. 2 || P <-> ( ( P + 1 ) / 2 ) e. NN ) )
8	7	biimpa	|- ( ( P e. NN /\ -. 2 || P ) -> ( ( P + 1 ) / 2 ) e. NN )
9	8	nnnn0d	|- ( ( P e. NN /\ -. 2 || P ) -> ( ( P + 1 ) / 2 ) e. NN0 )
10	6 9	syl	|- ( P e. ( Prime \ { 2 } ) -> ( ( P + 1 ) / 2 ) e. NN0 )
11	5 10	jca	|- ( P e. ( Prime \ { 2 } ) -> ( P e. ( ZZ>= ` 2 ) /\ ( ( P + 1 ) / 2 ) e. NN0 ) )
12	1 11	syl	|- ( ph -> ( P e. ( ZZ>= ` 2 ) /\ ( ( P + 1 ) / 2 ) e. NN0 ) )
13		nno	|- ( ( P e. ( ZZ>= ` 2 ) /\ ( ( P + 1 ) / 2 ) e. NN0 ) -> ( ( P - 1 ) / 2 ) e. NN )
14	12 13	syl	|- ( ph -> ( ( P - 1 ) / 2 ) e. NN )
15	2 14	eqeltrid	|- ( ph -> H e. NN )