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