Metamath Proof Explorer

Theorem 2lgslem1a1

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

Ref Expression
Assertion 2lgslem1a1 ${⊢}\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to \forall {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{i}\cdot 2={i}\cdot 2\mathrm{mod}{P}$

Proof

Step Hyp Ref Expression
1 nnrp ${⊢}{P}\in ℕ\to {P}\in {ℝ}^{+}$
2 1 adantr ${⊢}\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to {P}\in {ℝ}^{+}$
3 elfzelz ${⊢}{i}\in \left(1\dots \frac{{P}-1}{2}\right)\to {i}\in ℤ$
4 zre ${⊢}{i}\in ℤ\to {i}\in ℝ$
5 2re ${⊢}2\in ℝ$
6 5 a1i ${⊢}{i}\in ℤ\to 2\in ℝ$
7 4 6 remulcld ${⊢}{i}\in ℤ\to {i}\cdot 2\in ℝ$
8 3 7 syl ${⊢}{i}\in \left(1\dots \frac{{P}-1}{2}\right)\to {i}\cdot 2\in ℝ$
9 2 8 anim12ci ${⊢}\left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to \left({i}\cdot 2\in ℝ\wedge {P}\in {ℝ}^{+}\right)$
10 elfznn ${⊢}{i}\in \left(1\dots \frac{{P}-1}{2}\right)\to {i}\in ℕ$
11 nnre ${⊢}{i}\in ℕ\to {i}\in ℝ$
12 nnnn0 ${⊢}{i}\in ℕ\to {i}\in {ℕ}_{0}$
13 12 nn0ge0d ${⊢}{i}\in ℕ\to 0\le {i}$
14 0le2 ${⊢}0\le 2$
15 5 14 pm3.2i ${⊢}\left(2\in ℝ\wedge 0\le 2\right)$
16 15 a1i ${⊢}{i}\in ℕ\to \left(2\in ℝ\wedge 0\le 2\right)$
17 mulge0 ${⊢}\left(\left({i}\in ℝ\wedge 0\le {i}\right)\wedge \left(2\in ℝ\wedge 0\le 2\right)\right)\to 0\le {i}\cdot 2$
18 11 13 16 17 syl21anc ${⊢}{i}\in ℕ\to 0\le {i}\cdot 2$
19 10 18 syl ${⊢}{i}\in \left(1\dots \frac{{P}-1}{2}\right)\to 0\le {i}\cdot 2$
20 19 adantl ${⊢}\left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to 0\le {i}\cdot 2$
21 elfz2 ${⊢}{i}\in \left(1\dots \frac{{P}-1}{2}\right)↔\left(\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\wedge \left(1\le {i}\wedge {i}\le \frac{{P}-1}{2}\right)\right)$
22 4 3ad2ant3 ${⊢}\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\to {i}\in ℝ$
23 zre ${⊢}\frac{{P}-1}{2}\in ℤ\to \frac{{P}-1}{2}\in ℝ$
24 23 3ad2ant2 ${⊢}\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\to \frac{{P}-1}{2}\in ℝ$
25 2pos ${⊢}0<2$
26 5 25 pm3.2i ${⊢}\left(2\in ℝ\wedge 0<2\right)$
27 26 a1i ${⊢}\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\to \left(2\in ℝ\wedge 0<2\right)$
28 lemul1 ${⊢}\left({i}\in ℝ\wedge \frac{{P}-1}{2}\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left({i}\le \frac{{P}-1}{2}↔{i}\cdot 2\le \left(\frac{{P}-1}{2}\right)\cdot 2\right)$
29 22 24 27 28 syl3anc ${⊢}\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\to \left({i}\le \frac{{P}-1}{2}↔{i}\cdot 2\le \left(\frac{{P}-1}{2}\right)\cdot 2\right)$
30 nncn ${⊢}{P}\in ℕ\to {P}\in ℂ$
31 peano2cnm ${⊢}{P}\in ℂ\to {P}-1\in ℂ$
32 30 31 syl ${⊢}{P}\in ℕ\to {P}-1\in ℂ$
33 2cnd ${⊢}{P}\in ℕ\to 2\in ℂ$
34 2ne0 ${⊢}2\ne 0$
35 34 a1i ${⊢}{P}\in ℕ\to 2\ne 0$
36 32 33 35 divcan1d ${⊢}{P}\in ℕ\to \left(\frac{{P}-1}{2}\right)\cdot 2={P}-1$
37 36 adantr ${⊢}\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to \left(\frac{{P}-1}{2}\right)\cdot 2={P}-1$
38 37 adantl ${⊢}\left(\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({P}\in ℕ\wedge ¬2\parallel {P}\right)\right)\to \left(\frac{{P}-1}{2}\right)\cdot 2={P}-1$
39 38 breq2d ${⊢}\left(\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({P}\in ℕ\wedge ¬2\parallel {P}\right)\right)\to \left({i}\cdot 2\le \left(\frac{{P}-1}{2}\right)\cdot 2↔{i}\cdot 2\le {P}-1\right)$
40 id ${⊢}{i}\in ℤ\to {i}\in ℤ$
41 2z ${⊢}2\in ℤ$
42 41 a1i ${⊢}{i}\in ℤ\to 2\in ℤ$
43 40 42 zmulcld ${⊢}{i}\in ℤ\to {i}\cdot 2\in ℤ$
44 43 3ad2ant3 ${⊢}\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\to {i}\cdot 2\in ℤ$
45 nnz ${⊢}{P}\in ℕ\to {P}\in ℤ$
46 45 adantr ${⊢}\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to {P}\in ℤ$
47 zltlem1 ${⊢}\left({i}\cdot 2\in ℤ\wedge {P}\in ℤ\right)\to \left({i}\cdot 2<{P}↔{i}\cdot 2\le {P}-1\right)$
48 44 46 47 syl2an ${⊢}\left(\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({P}\in ℕ\wedge ¬2\parallel {P}\right)\right)\to \left({i}\cdot 2<{P}↔{i}\cdot 2\le {P}-1\right)$
49 48 biimprd ${⊢}\left(\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({P}\in ℕ\wedge ¬2\parallel {P}\right)\right)\to \left({i}\cdot 2\le {P}-1\to {i}\cdot 2<{P}\right)$
50 39 49 sylbid ${⊢}\left(\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\wedge \left({P}\in ℕ\wedge ¬2\parallel {P}\right)\right)\to \left({i}\cdot 2\le \left(\frac{{P}-1}{2}\right)\cdot 2\to {i}\cdot 2<{P}\right)$
51 50 ex ${⊢}\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\to \left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to \left({i}\cdot 2\le \left(\frac{{P}-1}{2}\right)\cdot 2\to {i}\cdot 2<{P}\right)\right)$
52 51 com23 ${⊢}\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\to \left({i}\cdot 2\le \left(\frac{{P}-1}{2}\right)\cdot 2\to \left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to {i}\cdot 2<{P}\right)\right)$
53 29 52 sylbid ${⊢}\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\to \left({i}\le \frac{{P}-1}{2}\to \left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to {i}\cdot 2<{P}\right)\right)$
54 53 a1d ${⊢}\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\to \left(1\le {i}\to \left({i}\le \frac{{P}-1}{2}\to \left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to {i}\cdot 2<{P}\right)\right)\right)$
55 54 imp32 ${⊢}\left(\left(1\in ℤ\wedge \frac{{P}-1}{2}\in ℤ\wedge {i}\in ℤ\right)\wedge \left(1\le {i}\wedge {i}\le \frac{{P}-1}{2}\right)\right)\to \left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to {i}\cdot 2<{P}\right)$
56 21 55 sylbi ${⊢}{i}\in \left(1\dots \frac{{P}-1}{2}\right)\to \left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to {i}\cdot 2<{P}\right)$
57 56 impcom ${⊢}\left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {i}\cdot 2<{P}$
58 modid ${⊢}\left(\left({i}\cdot 2\in ℝ\wedge {P}\in {ℝ}^{+}\right)\wedge \left(0\le {i}\cdot 2\wedge {i}\cdot 2<{P}\right)\right)\to {i}\cdot 2\mathrm{mod}{P}={i}\cdot 2$
59 9 20 57 58 syl12anc ${⊢}\left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {i}\cdot 2\mathrm{mod}{P}={i}\cdot 2$
60 59 eqcomd ${⊢}\left(\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\wedge {i}\in \left(1\dots \frac{{P}-1}{2}\right)\right)\to {i}\cdot 2={i}\cdot 2\mathrm{mod}{P}$
61 60 ralrimiva ${⊢}\left({P}\in ℕ\wedge ¬2\parallel {P}\right)\to \forall {i}\in \left(1\dots \frac{{P}-1}{2}\right)\phantom{\rule{.4em}{0ex}}{i}\cdot 2={i}\cdot 2\mathrm{mod}{P}$