Theorem gausslemma2dlem0e

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

	Ref	Expression
Hypotheses	gausslemma2dlem0.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
	gausslemma2dlem0.m	⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
Assertion	gausslemma2dlem0e	⊢ ( 𝜑 → ( 𝑀 · 2 ) < ( 𝑃 / 2 ) )

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2		gausslemma2dlem0.m	⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
3	2	oveq1i	⊢ ( 𝑀 · 2 ) = ( ( ⌊ ‘ ( 𝑃 / 4 ) ) · 2 )
4		nnoddn2prm	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) )
5		nnz	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℤ )
6	5	anim1i	⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
7	1 4 6	3syl	⊢ ( 𝜑 → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
8		flodddiv4t2lthalf	⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) · 2 ) < ( 𝑃 / 2 ) )
9	7 8	syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) · 2 ) < ( 𝑃 / 2 ) )
10	3 9	eqbrtrid	⊢ ( 𝜑 → ( 𝑀 · 2 ) < ( 𝑃 / 2 ) )