Step | Hyp | Ref
| Expression |
1 | | nnnn0 12421 |
. . . 4
โข (๐ โ โ โ ๐ โ
โ0) |
2 | | 8nn 12249 |
. . . . 5
โข 8 โ
โ |
3 | | nnrp 12927 |
. . . . 5
โข (8 โ
โ โ 8 โ โ+) |
4 | 2, 3 | ax-mp 5 |
. . . 4
โข 8 โ
โ+ |
5 | | modmuladdnn0 13821 |
. . . 4
โข ((๐ โ โ0
โง 8 โ โ+) โ ((๐ mod 8) = 7 โ โ๐ โ โ0 ๐ = ((๐ ยท 8) + 7))) |
6 | 1, 4, 5 | sylancl 587 |
. . 3
โข (๐ โ โ โ ((๐ mod 8) = 7 โ โ๐ โ โ0
๐ = ((๐ ยท 8) + 7))) |
7 | | simpr 486 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โ0)
โ ๐ โ
โ0) |
8 | | nn0cn 12424 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โ) |
9 | | 8cn 12251 |
. . . . . . . . . . . 12
โข 8 โ
โ |
10 | 9 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ 8 โ โ) |
11 | 8, 10 | mulcomd 11177 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ ยท 8) = (8
ยท ๐)) |
12 | 11 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ ยท 8) = (8
ยท ๐)) |
13 | 12 | oveq1d 7373 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ0)
โ ((๐ ยท 8) + 7)
= ((8 ยท ๐) +
7)) |
14 | 13 | eqeq2d 2748 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ = ((๐ ยท 8) + 7) โ ๐ = ((8 ยท ๐) + 7))) |
15 | 14 | biimpa 478 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ = ((๐ ยท 8) + 7)) โ ๐ = ((8 ยท ๐) + 7)) |
16 | | 2lgslem2.n |
. . . . . . 7
โข ๐ = (((๐ โ 1) / 2) โ
(โโ(๐ /
4))) |
17 | 16 | 2lgslem3d 26750 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ = ((8 ยท
๐) + 7)) โ ๐ = ((2 ยท ๐) + 2)) |
18 | 7, 15, 17 | syl2an2r 684 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ = ((๐ ยท 8) + 7)) โ ๐ = ((2 ยท ๐) + 2)) |
19 | | oveq1 7365 |
. . . . . 6
โข (๐ = ((2 ยท ๐) + 2) โ (๐ mod 2) = (((2 ยท ๐) + 2) mod 2)) |
20 | | 2t1e2 12317 |
. . . . . . . . . . . 12
โข (2
ยท 1) = 2 |
21 | 20 | eqcomi 2746 |
. . . . . . . . . . 11
โข 2 = (2
ยท 1) |
22 | 21 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 2 = (2 ยท 1)) |
23 | 22 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((2 ยท ๐) + 2)
= ((2 ยท ๐) + (2
ยท 1))) |
24 | | 2cnd 12232 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 2 โ โ) |
25 | | 1cnd 11151 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 1 โ โ) |
26 | | adddi 11141 |
. . . . . . . . . . 11
โข ((2
โ โ โง ๐
โ โ โง 1 โ โ) โ (2 ยท (๐ + 1)) = ((2 ยท ๐) + (2 ยท 1))) |
27 | 26 | eqcomd 2743 |
. . . . . . . . . 10
โข ((2
โ โ โง ๐
โ โ โง 1 โ โ) โ ((2 ยท ๐) + (2 ยท 1)) = (2 ยท (๐ + 1))) |
28 | 24, 8, 25, 27 | syl3anc 1372 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((2 ยท ๐) + (2
ยท 1)) = (2 ยท (๐ + 1))) |
29 | 8, 25 | addcld 11175 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
30 | 24, 29 | mulcomd 11177 |
. . . . . . . . 9
โข (๐ โ โ0
โ (2 ยท (๐ + 1))
= ((๐ + 1) ยท
2)) |
31 | 23, 28, 30 | 3eqtrd 2781 |
. . . . . . . 8
โข (๐ โ โ0
โ ((2 ยท ๐) + 2)
= ((๐ + 1) ยท
2)) |
32 | 31 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ โ0
โ (((2 ยท ๐) +
2) mod 2) = (((๐ + 1)
ยท 2) mod 2)) |
33 | | peano2nn0 12454 |
. . . . . . . . 9
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
34 | 33 | nn0zd 12526 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ + 1) โ
โค) |
35 | | 2rp 12921 |
. . . . . . . 8
โข 2 โ
โ+ |
36 | | mulmod0 13783 |
. . . . . . . 8
โข (((๐ + 1) โ โค โง 2
โ โ+) โ (((๐ + 1) ยท 2) mod 2) =
0) |
37 | 34, 35, 36 | sylancl 587 |
. . . . . . 7
โข (๐ โ โ0
โ (((๐ + 1) ยท
2) mod 2) = 0) |
38 | 32, 37 | eqtrd 2777 |
. . . . . 6
โข (๐ โ โ0
โ (((2 ยท ๐) +
2) mod 2) = 0) |
39 | 19, 38 | sylan9eqr 2799 |
. . . . 5
โข ((๐ โ โ0
โง ๐ = ((2 ยท
๐) + 2)) โ (๐ mod 2) = 0) |
40 | 7, 18, 39 | syl2an2r 684 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ = ((๐ ยท 8) + 7)) โ (๐ mod 2) = 0) |
41 | 40 | rexlimdva2 3155 |
. . 3
โข (๐ โ โ โ
(โ๐ โ
โ0 ๐ =
((๐ ยท 8) + 7) โ
(๐ mod 2) =
0)) |
42 | 6, 41 | syld 47 |
. 2
โข (๐ โ โ โ ((๐ mod 8) = 7 โ (๐ mod 2) = 0)) |
43 | 42 | imp 408 |
1
โข ((๐ โ โ โง (๐ mod 8) = 7) โ (๐ mod 2) = 0) |