Metamath Proof Explorer

Theorem gausslemma2dlem0d

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

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

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0.p 
 |-  ( ph -> P e. ( Prime \ { 2 } ) )
2 gausslemma2dlem0.m 
 |-  M = ( |_ ` ( P / 4 ) )
3 1 gausslemma2dlem0a 
 |-  ( ph -> P e. NN )
4 nnre 
 |-  ( P e. NN -> P e. RR )
5 4re 
 |-  4 e. RR
6 5 a1i 
 |-  ( P e. NN -> 4 e. RR )
7 4ne0 
 |-  4 =/= 0
8 7 a1i 
 |-  ( P e. NN -> 4 =/= 0 )
9 4 6 8 redivcld 
 |-  ( P e. NN -> ( P / 4 ) e. RR )
10 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
11 10 nn0ge0d 
 |-  ( P e. NN -> 0 <_ P )
12 4pos 
 |-  0 < 4
13 5 12 pm3.2i 
 |-  ( 4 e. RR /\ 0 < 4 )
14 13 a1i 
 |-  ( P e. NN -> ( 4 e. RR /\ 0 < 4 ) )
15 divge0 
 |-  ( ( ( P e. RR /\ 0 <_ P ) /\ ( 4 e. RR /\ 0 < 4 ) ) -> 0 <_ ( P / 4 ) )
16 4 11 14 15 syl21anc 
 |-  ( P e. NN -> 0 <_ ( P / 4 ) )
17 9 16 jca 
 |-  ( P e. NN -> ( ( P / 4 ) e. RR /\ 0 <_ ( P / 4 ) ) )
18 flge0nn0 
 |-  ( ( ( P / 4 ) e. RR /\ 0 <_ ( P / 4 ) ) -> ( |_ ` ( P / 4 ) ) e. NN0 )
19 3 17 18 3syl 
 |-  ( ph -> ( |_ ` ( P / 4 ) ) e. NN0 )
20 2 19 eqeltrid 
 |-  ( ph -> M e. NN0 )