Metamath Proof Explorer

Theorem gausslemma2dlem0b

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

Ref Expression
Hypotheses gausslemma2dlem0a.p ⊢ φ → P ∈ ℙ ∖ 2
gausslemma2dlem0b.h ⊢ H = P − 1 2
Assertion gausslemma2dlem0b ⊢ φ → H ∈ ℕ

Proof

Step Hyp Ref Expression
1 gausslemma2dlem0a.p ⊢ φ → P ∈ ℙ ∖ 2
2 gausslemma2dlem0b.h ⊢ H = P − 1 2
3 eldifi ⊢ P ∈ ℙ ∖ 2 → P ∈ ℙ
4 prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2
5 3 4 syl ⊢ P ∈ ℙ ∖ 2 → P ∈ ℤ ≥ 2
6 nnoddn2prm ⊢ P ∈ ℙ ∖ 2 → P ∈ ℕ ∧ ¬ 2 ∥ P
7 nnoddm1d2 ⊢ P ∈ ℕ → ¬ 2 ∥ P ↔ P + 1 2 ∈ ℕ
8 7 biimpa ⊢ P ∈ ℕ ∧ ¬ 2 ∥ P → P + 1 2 ∈ ℕ
9 8 nnnn0d ⊢ P ∈ ℕ ∧ ¬ 2 ∥ P → P + 1 2 ∈ ℕ 0
10 6 9 syl ⊢ P ∈ ℙ ∖ 2 → P + 1 2 ∈ ℕ 0
11 5 10 jca ⊢ P ∈ ℙ ∖ 2 → P ∈ ℤ ≥ 2 ∧ P + 1 2 ∈ ℕ 0
12 1 11 syl ⊢ φ → P ∈ ℤ ≥ 2 ∧ P + 1 2 ∈ ℕ 0
13 nno ⊢ P ∈ ℤ ≥ 2 ∧ P + 1 2 ∈ ℕ 0 → P − 1 2 ∈ ℕ
14 12 13 syl ⊢ φ → P − 1 2 ∈ ℕ
15 2 14 eqeltrid ⊢ φ → H ∈ ℕ