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 mod 8 ) ∈ { 1 , 7 } )

Proof

Step	Hyp	Ref	Expression
1		2lgs2	⊢ ( 2 /L 2 ) = 0
2	1	eqeq1i	⊢ ( ( 2 /L 2 ) = 1 ↔ 0 = 1 )
3		0ne1	⊢ 0 ≠ 1
4	3	neii	⊢ ¬ 0 = 1
5		1ne2	⊢ 1 ≠ 2
6	5	nesymi	⊢ ¬ 2 = 1
7		2re	⊢ 2 ∈ ℝ
8		2lt7	⊢ 2 < 7
9	7 8	ltneii	⊢ 2 ≠ 7
10	9	neii	⊢ ¬ 2 = 7
11	6 10	pm3.2ni	⊢ ¬ ( 2 = 1 ∨ 2 = 7 )
12	4 11	2false	⊢ ( 0 = 1 ↔ ( 2 = 1 ∨ 2 = 7 ) )
13		8nn	⊢ 8 ∈ ℕ
14		nnrp	⊢ ( 8 ∈ ℕ → 8 ∈ ℝ+ )
15	13 14	ax-mp	⊢ 8 ∈ ℝ+
16		0le2	⊢ 0 ≤ 2
17		2lt8	⊢ 2 < 8
18		modid	⊢ ( ( ( 2 ∈ ℝ ∧ 8 ∈ ℝ+ ) ∧ ( 0 ≤ 2 ∧ 2 < 8 ) ) → ( 2 mod 8 ) = 2 )
19	7 15 16 17 18	mp4an	⊢ ( 2 mod 8 ) = 2
20	19	eleq1i	⊢ ( ( 2 mod 8 ) ∈ { 1 , 7 } ↔ 2 ∈ { 1 , 7 } )
21		2ex	⊢ 2 ∈ V
22	21	elpr	⊢ ( 2 ∈ { 1 , 7 } ↔ ( 2 = 1 ∨ 2 = 7 ) )
23	20 22	bitr2i	⊢ ( ( 2 = 1 ∨ 2 = 7 ) ↔ ( 2 mod 8 ) ∈ { 1 , 7 } )
24	2 12 23	3bitri	⊢ ( ( 2 /L 2 ) = 1 ↔ ( 2 mod 8 ) ∈ { 1 , 7 } )