Metamath Proof Explorer


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 )