Metamath Proof Explorer


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 ) ≤ 𝐻 )