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