# Metamath Proof Explorer

## Theorem 2lgslem1

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

Ref Expression
Assertion 2lgslem1 ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left|\left\{{x}\in ℤ|\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right\}\right|=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$

### Proof

Step Hyp Ref Expression
1 2lgslem1a ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left\{{x}\in ℤ|\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right\}=\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}$
2 1 fveq2d ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left|\left\{{x}\in ℤ|\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right\}\right|=\left|\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}\right|$
3 ovex ${⊢}\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\in \mathrm{V}$
4 3 mptex ${⊢}\left({y}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)⟼{y}\cdot 2\right)\in \mathrm{V}$
5 f1oeq1 ${⊢}{f}=\left({y}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)⟼{y}\cdot 2\right)\to \left({f}:\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}↔\left({y}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)⟼{y}\cdot 2\right):\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}\right)$
6 eqid ${⊢}\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)=\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)$
7 eqid ${⊢}\left({y}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)⟼{y}\cdot 2\right)=\left({y}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)⟼{y}\cdot 2\right)$
8 6 7 2lgslem1b ${⊢}\left({y}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)⟼{y}\cdot 2\right):\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}$
9 4 5 8 ceqsexv2d ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}$
10 9 a1i ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}$
11 hasheqf1oi ${⊢}\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\in \mathrm{V}\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\underset{1-1 onto}{⟶}\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}\to \left|\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\right|=\left|\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}\right|\right)$
12 3 10 11 mpsyl ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left|\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\right|=\left|\left\{{x}\in ℤ|\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right\}\right|$
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 oddm1d2 ${⊢}{P}\in ℤ\to \left(¬2\parallel {P}↔\frac{{P}-1}{2}\in ℤ\right)$
23 13 22 syl ${⊢}{P}\in ℙ\to \left(¬2\parallel {P}↔\frac{{P}-1}{2}\in ℤ\right)$
24 23 biimpa ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \frac{{P}-1}{2}\in ℤ$
25 2lgslem1c ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to ⌊\frac{{P}}{4}⌋\le \frac{{P}-1}{2}$
26 eluz2 ${⊢}\frac{{P}-1}{2}\in {ℤ}_{\ge ⌊\frac{{P}}{4}⌋}↔\left(⌊\frac{{P}}{4}⌋\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge ⌊\frac{{P}}{4}⌋\le \frac{{P}-1}{2}\right)$
27 21 24 25 26 syl3anbrc ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \frac{{P}-1}{2}\in {ℤ}_{\ge ⌊\frac{{P}}{4}⌋}$
28 hashfzp1 ${⊢}\frac{{P}-1}{2}\in {ℤ}_{\ge ⌊\frac{{P}}{4}⌋}\to \left|\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\right|=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$
29 27 28 syl ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left|\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\right|=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$
30 2 12 29 3eqtr2d ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \left|\left\{{x}\in ℤ|\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right\}\right|=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$