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