# Metamath Proof Explorer

## 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↔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↔0=1$
3 0ne1 ${⊢}0\ne 1$
4 3 neii ${⊢}¬0=1$
5 1ne2 ${⊢}1\ne 2$
6 5 nesymi ${⊢}¬2=1$
7 2re ${⊢}2\in ℝ$
8 2lt7 ${⊢}2<7$
9 7 8 ltneii ${⊢}2\ne 7$
10 9 neii ${⊢}¬2=7$
11 6 10 pm3.2ni ${⊢}¬\left(2=1\vee 2=7\right)$
12 4 11 2false ${⊢}0=1↔\left(2=1\vee 2=7\right)$
13 8nn ${⊢}8\in ℕ$
14 nnrp ${⊢}8\in ℕ\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\}↔2\in \left\{1,7\right\}$
21 2ex ${⊢}2\in \mathrm{V}$
22 21 elpr ${⊢}2\in \left\{1,7\right\}↔\left(2=1\vee 2=7\right)$
23 20 22 bitr2i ${⊢}\left(2=1\vee 2=7\right)↔2\mathrm{mod}8\in \left\{1,7\right\}$
24 2 12 23 3bitri ${⊢}2{/}_{L}2=1↔2\mathrm{mod}8\in \left\{1,7\right\}$