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) = 5 โ โ๐ โ โ0 ๐ = ((๐ ยท 8) + 5))) |
6 | 1, 4, 5 | sylancl 587 |
. . 3
โข (๐ โ โ โ ((๐ mod 8) = 5 โ โ๐ โ โ0
๐ = ((๐ ยท 8) + 5))) |
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) + 5)
= ((8 ยท ๐) +
5)) |
14 | 13 | eqeq2d 2748 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ โ0)
โ (๐ = ((๐ ยท 8) + 5) โ ๐ = ((8 ยท ๐) + 5))) |
15 | 14 | biimpa 478 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ = ((๐ ยท 8) + 5)) โ ๐ = ((8 ยท ๐) + 5)) |
16 | | 2lgslem2.n |
. . . . . . 7
โข ๐ = (((๐ โ 1) / 2) โ
(โโ(๐ /
4))) |
17 | 16 | 2lgslem3c 26749 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ = ((8 ยท
๐) + 5)) โ ๐ = ((2 ยท ๐) + 1)) |
18 | 7, 15, 17 | syl2an2r 684 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ = ((๐ ยท 8) + 5)) โ ๐ = ((2 ยท ๐) + 1)) |
19 | | oveq1 7365 |
. . . . . 6
โข (๐ = ((2 ยท ๐) + 1) โ (๐ mod 2) = (((2 ยท ๐) + 1) mod 2)) |
20 | | nn0z 12525 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โค) |
21 | | eqidd 2738 |
. . . . . . . 8
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
= ((2 ยท ๐) +
1)) |
22 | | 2tp1odd 16235 |
. . . . . . . 8
โข ((๐ โ โค โง ((2
ยท ๐) + 1) = ((2
ยท ๐) + 1)) โ
ยฌ 2 โฅ ((2 ยท ๐) + 1)) |
23 | 20, 21, 22 | syl2anc 585 |
. . . . . . 7
โข (๐ โ โ0
โ ยฌ 2 โฅ ((2 ยท ๐) + 1)) |
24 | | 2z 12536 |
. . . . . . . . . . 11
โข 2 โ
โค |
25 | 24 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 2 โ โค) |
26 | 25, 20 | zmulcld 12614 |
. . . . . . . . 9
โข (๐ โ โ0
โ (2 ยท ๐)
โ โค) |
27 | 26 | peano2zd 12611 |
. . . . . . . 8
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
โ โค) |
28 | | mod2eq1n2dvds 16230 |
. . . . . . . 8
โข (((2
ยท ๐) + 1) โ
โค โ ((((2 ยท ๐) + 1) mod 2) = 1 โ ยฌ 2 โฅ ((2
ยท ๐) +
1))) |
29 | 27, 28 | syl 17 |
. . . . . . 7
โข (๐ โ โ0
โ ((((2 ยท ๐) +
1) mod 2) = 1 โ ยฌ 2 โฅ ((2 ยท ๐) + 1))) |
30 | 23, 29 | mpbird 257 |
. . . . . 6
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) mod 2) = 1) |
31 | 19, 30 | sylan9eqr 2799 |
. . . . 5
โข ((๐ โ โ0
โง ๐ = ((2 ยท
๐) + 1)) โ (๐ mod 2) = 1) |
32 | 7, 18, 31 | syl2an2r 684 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ0)
โง ๐ = ((๐ ยท 8) + 5)) โ (๐ mod 2) = 1) |
33 | 32 | rexlimdva2 3155 |
. . 3
โข (๐ โ โ โ
(โ๐ โ
โ0 ๐ =
((๐ ยท 8) + 5) โ
(๐ mod 2) =
1)) |
34 | 6, 33 | syld 47 |
. 2
โข (๐ โ โ โ ((๐ mod 8) = 5 โ (๐ mod 2) = 1)) |
35 | 34 | imp 408 |
1
โข ((๐ โ โ โง (๐ mod 8) = 5) โ (๐ mod 2) = 1) |