# Metamath Proof Explorer

## Theorem 2lgslem2

Description: Lemma 2 for 2lgs . (Contributed by AV, 20-Jun-2021)

Ref Expression
Hypothesis 2lgslem2.n ${⊢}{N}=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$
Assertion 2lgslem2 ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to {N}\in ℤ$

### Proof

Step Hyp Ref Expression
1 2lgslem2.n ${⊢}{N}=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$
2 simpl ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to {P}\in ℙ$
3 elsng ${⊢}{P}\in ℙ\to \left({P}\in \left\{2\right\}↔{P}=2\right)$
4 z2even ${⊢}2\parallel 2$
5 breq2 ${⊢}{P}=2\to \left(2\parallel {P}↔2\parallel 2\right)$
6 4 5 mpbiri ${⊢}{P}=2\to 2\parallel {P}$
7 3 6 syl6bi ${⊢}{P}\in ℙ\to \left({P}\in \left\{2\right\}\to 2\parallel {P}\right)$
8 7 con3dimp ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to ¬{P}\in \left\{2\right\}$
9 2 8 eldifd ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
10 oddprm ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)\to \frac{{P}-1}{2}\in ℕ$
11 10 nnzd ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)\to \frac{{P}-1}{2}\in ℤ$
12 9 11 syl ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \frac{{P}-1}{2}\in ℤ$
13 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
14 13 zred ${⊢}{P}\in ℙ\to {P}\in ℝ$
15 4re ${⊢}4\in ℝ$
16 15 a1i ${⊢}{P}\in ℙ\to 4\in ℝ$
17 4ne0 ${⊢}4\ne 0$
18 17 a1i ${⊢}{P}\in ℙ\to 4\ne 0$
19 14 16 18 redivcld ${⊢}{P}\in ℙ\to \frac{{P}}{4}\in ℝ$
20 19 flcld ${⊢}{P}\in ℙ\to ⌊\frac{{P}}{4}⌋\in ℤ$
21 20 adantr ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to ⌊\frac{{P}}{4}⌋\in ℤ$
22 12 21 zsubcld ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋\in ℤ$
23 1 22 eqeltrid ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to {N}\in ℤ$