Description: Auxiliary lemma 5 for gausslemma2d . (Contributed by AV, 9-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gausslemma2dlem0.p | ||
gausslemma2dlem0.m | |||
Assertion | gausslemma2dlem0e |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gausslemma2dlem0.p | ||
2 | gausslemma2dlem0.m | ||
3 | 2 | oveq1i | |
4 | nnoddn2prm | ||
5 | nnz | ||
6 | 5 | anim1i | |
7 | flodddiv4t2lthalf | ||
8 | 1 4 6 7 | 4syl | |
9 | 3 8 | eqbrtrid |