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 ) e. { 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 e. RR
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 e. NN
14		nnrp	|- ( 8 e. NN -> 8 e. RR+ )
15	13 14	ax-mp	|- 8 e. RR+
16		0le2	|- 0 <_ 2
17		2lt8	|- 2 < 8
18		modid	|- ( ( ( 2 e. RR /\ 8 e. RR+ ) /\ ( 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 ) e. { 1 , 7 } <-> 2 e. { 1 , 7 } )
21		2ex	|- 2 e. _V
22	21	elpr	|- ( 2 e. { 1 , 7 } <-> ( 2 = 1 \/ 2 = 7 ) )
23	20 22	bitr2i	|- ( ( 2 = 1 \/ 2 = 7 ) <-> ( 2 mod 8 ) e. { 1 , 7 } )
24	2 12 23	3bitri	|- ( ( 2 /L 2 ) = 1 <-> ( 2 mod 8 ) e. { 1 , 7 } )