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