Description: Auxiliary lemma 7 for gausslemma2d . (Contributed by AV, 9-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gausslemma2dlem0.p | ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) ) | |
gausslemma2dlem0.m | ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) ) | ||
gausslemma2dlem0.h | ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 ) | ||
Assertion | gausslemma2dlem0g | ⊢ ( 𝜑 → 𝑀 ≤ 𝐻 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gausslemma2dlem0.p | ⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) ) | |
2 | gausslemma2dlem0.m | ⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) ) | |
3 | gausslemma2dlem0.h | ⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 ) | |
4 | 1 | gausslemma2dlem0a | ⊢ ( 𝜑 → 𝑃 ∈ ℕ ) |
5 | fldiv4lem1div2 | ⊢ ( 𝑃 ∈ ℕ → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) | |
6 | 4 5 | syl | ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝑃 / 4 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) |
7 | 6 2 3 | 3brtr4g | ⊢ ( 𝜑 → 𝑀 ≤ 𝐻 ) |