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 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 } )