# Metamath Proof Explorer

## Theorem 2lgslem1a

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

Ref Expression
Assertion 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\}$

### Proof

Step Hyp Ref Expression
1 prmnn ${⊢}{P}\in ℙ\to {P}\in ℕ$
2 1 nnnn0d ${⊢}{P}\in ℙ\to {P}\in {ℕ}_{0}$
3 2 ad2antrr ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to {P}\in {ℕ}_{0}$
4 4nn ${⊢}4\in ℕ$
5 3 4 jctir ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to \left({P}\in {ℕ}_{0}\wedge 4\in ℕ\right)$
6 fldivnn0 ${⊢}\left({P}\in {ℕ}_{0}\wedge 4\in ℕ\right)\to ⌊\frac{{P}}{4}⌋\in {ℕ}_{0}$
7 nn0p1nn ${⊢}⌊\frac{{P}}{4}⌋\in {ℕ}_{0}\to ⌊\frac{{P}}{4}⌋+1\in ℕ$
8 5 6 7 3syl ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to ⌊\frac{{P}}{4}⌋+1\in ℕ$
9 elnnuz ${⊢}⌊\frac{{P}}{4}⌋+1\in ℕ↔⌊\frac{{P}}{4}⌋+1\in {ℤ}_{\ge 1}$
10 8 9 sylib ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to ⌊\frac{{P}}{4}⌋+1\in {ℤ}_{\ge 1}$
11 fzss1 ${⊢}⌊\frac{{P}}{4}⌋+1\in {ℤ}_{\ge 1}\to \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\subseteq \left(1\dots \frac{{P}-1}{2}\right)$
12 rexss ${⊢}\left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\subseteq \left(1\dots \frac{{P}-1}{2}\right)\to \left(\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2↔\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\wedge {x}={i}\cdot 2\right)\right)$
13 10 11 12 3syl ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to \left(\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2↔\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\wedge {x}={i}\cdot 2\right)\right)$
14 ancom ${⊢}\left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\wedge {x}={i}\cdot 2\right)↔\left({x}={i}\cdot 2\wedge {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\right)$
15 2 4 jctir ${⊢}{P}\in ℙ\to \left({P}\in {ℕ}_{0}\wedge 4\in ℕ\right)$
16 15 6 syl ${⊢}{P}\in ℙ\to ⌊\frac{{P}}{4}⌋\in {ℕ}_{0}$
17 16 nn0zd ${⊢}{P}\in ℙ\to ⌊\frac{{P}}{4}⌋\in ℤ$
18 17 ad2antrr ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to ⌊\frac{{P}}{4}⌋\in ℤ$
19 elfzelz ${⊢}{i}\in \left(1\dots \frac{{P}-1}{2}\right)\to {i}\in ℤ$
20 zltp1le ${⊢}\left(⌊\frac{{P}}{4}⌋\in ℤ\wedge {i}\in ℤ\right)\to \left(⌊\frac{{P}}{4}⌋<{i}↔⌊\frac{{P}}{4}⌋+1\le {i}\right)$
21 18 19 20 syl2an ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(⌊\frac{{P}}{4}⌋<{i}↔⌊\frac{{P}}{4}⌋+1\le {i}\right)$
22 21 bicomd ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(⌊\frac{{P}}{4}⌋+1\le {i}↔⌊\frac{{P}}{4}⌋<{i}\right)$
23 22 anbi1d ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(\left(⌊\frac{{P}}{4}⌋+1\le {i}\wedge {i}\le \frac{{P}-1}{2}\right)↔\left(⌊\frac{{P}}{4}⌋<{i}\wedge {i}\le \frac{{P}-1}{2}\right)\right)$
24 19 adantl ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {i}\in ℤ$
25 17 peano2zd ${⊢}{P}\in ℙ\to ⌊\frac{{P}}{4}⌋+1\in ℤ$
26 25 adantr ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to ⌊\frac{{P}}{4}⌋+1\in ℤ$
27 26 ad2antrr ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to ⌊\frac{{P}}{4}⌋+1\in ℤ$
28 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
29 oddm1d2 ${⊢}{P}\in ℤ\to \left(¬2\parallel {P}↔\frac{{P}-1}{2}\in ℤ\right)$
30 28 29 syl ${⊢}{P}\in ℙ\to \left(¬2\parallel {P}↔\frac{{P}-1}{2}\in ℤ\right)$
31 30 biimpa ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \frac{{P}-1}{2}\in ℤ$
32 31 ad2antrr ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \frac{{P}-1}{2}\in ℤ$
33 elfz ${⊢}\left({i}\in ℤ\wedge ⌊\frac{{P}}{4}⌋+1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\right)\to \left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)↔\left(⌊\frac{{P}}{4}⌋+1\le {i}\wedge {i}\le \frac{{P}-1}{2}\right)\right)$
34 24 27 32 33 syl3anc ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)↔\left(⌊\frac{{P}}{4}⌋+1\le {i}\wedge {i}\le \frac{{P}-1}{2}\right)\right)$
35 elfzle2 ${⊢}{i}\in \left(1\dots \frac{{P}-1}{2}\right)\to {i}\le \frac{{P}-1}{2}$
36 35 adantl ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {i}\le \frac{{P}-1}{2}$
37 36 biantrud ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(⌊\frac{{P}}{4}⌋<{i}↔\left(⌊\frac{{P}}{4}⌋<{i}\wedge {i}\le \frac{{P}-1}{2}\right)\right)$
38 23 34 37 3bitr4d ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)↔⌊\frac{{P}}{4}⌋<{i}\right)$
39 28 ad2antrr ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to {P}\in ℤ$
40 2lgslem1a2 ${⊢}\left({P}\in ℤ\wedge {i}\in ℤ\right)\to \left(⌊\frac{{P}}{4}⌋<{i}↔\frac{{P}}{2}<{i}\cdot 2\right)$
41 39 19 40 syl2an ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(⌊\frac{{P}}{4}⌋<{i}↔\frac{{P}}{2}<{i}\cdot 2\right)$
42 38 41 bitrd ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)↔\frac{{P}}{2}<{i}\cdot 2\right)$
43 2lgslem1a1 ${⊢}\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to \forall {k}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{k}\cdot 2={k}\cdot 2\mathrm{mod}{P}$
44 1 43 sylan ${⊢}\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\to \forall {k}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{k}\cdot 2={k}\cdot 2\mathrm{mod}{P}$
45 44 adantr ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to \forall {k}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{k}\cdot 2={k}\cdot 2\mathrm{mod}{P}$
46 oveq1 ${⊢}{k}={i}\to {k}\cdot 2={i}\cdot 2$
47 46 oveq1d ${⊢}{k}={i}\to {k}\cdot 2\mathrm{mod}{P}={i}\cdot 2\mathrm{mod}{P}$
48 46 47 eqeq12d ${⊢}{k}={i}\to \left({k}\cdot 2={k}\cdot 2\mathrm{mod}{P}↔{i}\cdot 2={i}\cdot 2\mathrm{mod}{P}\right)$
49 48 rspccva ${⊢}\left(\forall {k}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{k}\cdot 2={k}\cdot 2\mathrm{mod}{P}\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {i}\cdot 2={i}\cdot 2\mathrm{mod}{P}$
50 45 49 sylan ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {i}\cdot 2={i}\cdot 2\mathrm{mod}{P}$
51 50 breq2d ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(\frac{{P}}{2}<{i}\cdot 2↔\frac{{P}}{2}<{i}\cdot 2\mathrm{mod}{P}\right)$
52 42 51 bitrd ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)↔\frac{{P}}{2}<{i}\cdot 2\mathrm{mod}{P}\right)$
53 oveq1 ${⊢}{x}={i}\cdot 2\to {x}\mathrm{mod}{P}={i}\cdot 2\mathrm{mod}{P}$
54 53 eqcomd ${⊢}{x}={i}\cdot 2\to {i}\cdot 2\mathrm{mod}{P}={x}\mathrm{mod}{P}$
55 54 breq2d ${⊢}{x}={i}\cdot 2\to \left(\frac{{P}}{2}<{i}\cdot 2\mathrm{mod}{P}↔\frac{{P}}{2}<{x}\mathrm{mod}{P}\right)$
56 52 55 sylan9bb ${⊢}\left(\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\wedge {x}={i}\cdot 2\right)\to \left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)↔\frac{{P}}{2}<{x}\mathrm{mod}{P}\right)$
57 56 pm5.32da ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(\left({x}={i}\cdot 2\wedge {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\right)↔\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right)$
58 14 57 syl5bb ${⊢}\left(\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left(\left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\wedge {x}={i}\cdot 2\right)↔\left({x}={i}\cdot 2\wedge \frac{{P}}{2}<{x}\mathrm{mod}{P}\right)\right)$
59 58 rexbidva ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to \left(\exists {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}\left({i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\wedge {x}={i}\cdot 2\right)↔\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)$
60 13 59 bitrd ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to \left(\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2↔\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)$
61 60 bicomd ${⊢}\left(\left({P}\in ℙ\wedge ¬2\parallel {P}\right)\wedge {x}\in ℤ\right)\to \left(\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)↔\exists {i}\in \left(⌊\frac{{P}}{4}⌋+1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{x}={i}\cdot 2\right)$
62 61 rabbidva ${⊢}\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\}$