Theorem gausslemma2dlem0h

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

	Ref	Expression
Hypotheses	gausslemma2dlem0.p	|- ( ph -> P e. ( Prime \ { 2 } ) )
	gausslemma2dlem0.m	|- M = ( |_ ` ( P / 4 ) )
	gausslemma2dlem0.h	|- H = ( ( P - 1 ) / 2 )
	gausslemma2dlem0.n	|- N = ( H - M )
Assertion	gausslemma2dlem0h	|- ( ph -> N e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0.p	|- ( ph -> P e. ( Prime \ { 2 } ) )
2		gausslemma2dlem0.m	|- M = ( |_ ` ( P / 4 ) )
3		gausslemma2dlem0.h	|- H = ( ( P - 1 ) / 2 )
4		gausslemma2dlem0.n	|- N = ( H - M )
5	1 3	gausslemma2dlem0b	|- ( ph -> H e. NN )
6	5	nnzd	|- ( ph -> H e. ZZ )
7	1 2	gausslemma2dlem0d	|- ( ph -> M e. NN0 )
8	7	nn0zd	|- ( ph -> M e. ZZ )
9	6 8	zsubcld	|- ( ph -> ( H - M ) e. ZZ )
10	1 2 3	gausslemma2dlem0g	|- ( ph -> M <_ H )
11	5	nnred	|- ( ph -> H e. RR )
12	7	nn0red	|- ( ph -> M e. RR )
13	11 12	subge0d	|- ( ph -> ( 0 <_ ( H - M ) <-> M <_ H ) )
14	10 13	mpbird	|- ( ph -> 0 <_ ( H - M ) )
15		elnn0z	|- ( ( H - M ) e. NN0 <-> ( ( H - M ) e. ZZ /\ 0 <_ ( H - M ) ) )
16	9 14 15	sylanbrc	|- ( ph -> ( H - M ) e. NN0 )
17	4 16	eqeltrid	|- ( ph -> N e. NN0 )