Theorem 2lgslem4

Description: Lemma 4 for 2lgs : special case of 2lgs for P = 2 . (Contributed by AV, 20-Jun-2021)

	Ref	Expression
Assertion	2lgslem4	$$⊢2{/}_{L}2=1\leftrightarrow 2\mathrm{mod}8\in \left\{1,7\right\}$$

Proof

Step	Hyp	Ref	Expression
1		2lgs2	$$⊢2{/}_{L}2=0$$
2	1	eqeq1i	$$⊢2{/}_{L}2=1\leftrightarrow 0=1$$
3		0ne1	$$⊢0\ne 1$$
4	3	neii	$$⊢\neg 0=1$$
5		1ne2	$$⊢1\ne 2$$
6	5	nesymi	$$⊢\neg 2=1$$
7		2re	$$⊢2\in ℝ$$
8		2lt7	$$⊢2<7$$
9	7 8	ltneii	$$⊢2\ne 7$$
10	9	neii	$$⊢\neg 2=7$$
11	6 10	pm3.2ni	$$⊢\neg \left(2=1\vee 2=7\right)$$
12	4 11	2false	$$⊢0=1\leftrightarrow \left(2=1\vee 2=7\right)$$
13		8nn	$$⊢8\in \mathbb{N}$$
14		nnrp	$$⊢8\in \mathbb{N}\to 8\in {ℝ}^{+}$$
15	13 14	ax-mp	$$⊢8\in {ℝ}^{+}$$
16		0le2	$$⊢0\le 2$$
17		2lt8	$$⊢2<8$$
18		modid	$$⊢\left(\left(2\in ℝ\wedge 8\in {ℝ}^{+}\right)\wedge \left(0\le 2\wedge 2<8\right)\right)\to 2\mathrm{mod}8=2$$
19	7 15 16 17 18	mp4an	$$⊢2\mathrm{mod}8=2$$
20	19	eleq1i	$$⊢2\mathrm{mod}8\in \left\{1,7\right\}\leftrightarrow 2\in \left\{1,7\right\}$$
21		2ex	$$⊢2\in \mathrm{V}$$
22	21	elpr	$$⊢2\in \left\{1,7\right\}\leftrightarrow \left(2=1\vee 2=7\right)$$
23	20 22	bitr2i	$$⊢\left(2=1\vee 2=7\right)\leftrightarrow 2\mathrm{mod}8\in \left\{1,7\right\}$$
24	2 12 23	3bitri	$$⊢2{/}_{L}2=1\leftrightarrow 2\mathrm{mod}8\in \left\{1,7\right\}$$