Metamath Proof Explorer


Theorem gausslemma2dlem0d

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

Ref Expression
Hypotheses gausslemma2dlem0.p ( 𝜑𝑃 ∈ ( ℙ ∖ { 2 } ) )
gausslemma2dlem0.m 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
Assertion gausslemma2dlem0d ( 𝜑𝑀 ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0.p ( 𝜑𝑃 ∈ ( ℙ ∖ { 2 } ) )
2 gausslemma2dlem0.m 𝑀 = ( ⌊ ‘ ( 𝑃 / 4 ) )
3 1 gausslemma2dlem0a ( 𝜑𝑃 ∈ ℕ )
4 nnre ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ )
5 4re 4 ∈ ℝ
6 5 a1i ( 𝑃 ∈ ℕ → 4 ∈ ℝ )
7 4ne0 4 ≠ 0
8 7 a1i ( 𝑃 ∈ ℕ → 4 ≠ 0 )
9 4 6 8 redivcld ( 𝑃 ∈ ℕ → ( 𝑃 / 4 ) ∈ ℝ )
10 nnnn0 ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
11 10 nn0ge0d ( 𝑃 ∈ ℕ → 0 ≤ 𝑃 )
12 4pos 0 < 4
13 5 12 pm3.2i ( 4 ∈ ℝ ∧ 0 < 4 )
14 13 a1i ( 𝑃 ∈ ℕ → ( 4 ∈ ℝ ∧ 0 < 4 ) )
15 divge0 ( ( ( 𝑃 ∈ ℝ ∧ 0 ≤ 𝑃 ) ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → 0 ≤ ( 𝑃 / 4 ) )
16 4 11 14 15 syl21anc ( 𝑃 ∈ ℕ → 0 ≤ ( 𝑃 / 4 ) )
17 9 16 jca ( 𝑃 ∈ ℕ → ( ( 𝑃 / 4 ) ∈ ℝ ∧ 0 ≤ ( 𝑃 / 4 ) ) )
18 flge0nn0 ( ( ( 𝑃 / 4 ) ∈ ℝ ∧ 0 ≤ ( 𝑃 / 4 ) ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ0 )
19 3 17 18 3syl ( 𝜑 → ( ⌊ ‘ ( 𝑃 / 4 ) ) ∈ ℕ0 )
20 2 19 eqeltrid ( 𝜑𝑀 ∈ ℕ0 )