Theorem gausslemma2dlem0f

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

	Ref	Expression
Hypotheses	gausslemma2dlem0.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
	gausslemma2dlem0.m	⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
	gausslemma2dlem0.h	⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
Assertion	gausslemma2dlem0f	⊢ ( 𝜑 → ( 𝑀 + 1 ) ≤ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		gausslemma2dlem0.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2		gausslemma2dlem0.m	⊢ 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
3		gausslemma2dlem0.h	⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
4		eldifsn	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
5		prm23ge5	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) )
6		eqneqall	⊢ ( 𝑃 = 2 → ( 𝑃 ≠ 2 → ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) ) )
7		orc	⊢ ( 𝑃 = 3 → ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) )
8	7	a1d	⊢ ( 𝑃 = 3 → ( 𝑃 ≠ 2 → ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) ) )
9		olc	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) )
10	9	a1d	⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 5 ) → ( 𝑃 ≠ 2 → ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) ) )
11	6 8 10	3jaoi	⊢ ( ( 𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) → ( 𝑃 ≠ 2 → ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) ) )
12	5 11	syl	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ≠ 2 → ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) ) )
13	12	imp	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) → ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) )
14	4 13	sylbi	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) )
15		fldiv4p1lem1div2	⊢ ( ( 𝑃 = 3 ∨ 𝑃 ∈ ( ℤ≥ ‘ 5 ) ) → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
16	1 14 15	3syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
17	2	oveq1i	⊢ ( 𝑀 + 1 ) = ( ( ⌊ ‘ ( 𝑃 / 4 ) ) + 1 )
18	16 17 3	3brtr4g	⊢ ( 𝜑 → ( 𝑀 + 1 ) ≤ 𝐻 )