Step | Hyp | Ref
| Expression |
1 | | 4nn 12243 |
. . . . 5
โข 4 โ
โ |
2 | 1 | a1i 11 |
. . . 4
โข (๐ โ โค โ 4 โ
โ) |
3 | | 3nn0 12438 |
. . . . . 6
โข 3 โ
โ0 |
4 | 3 | a1i 11 |
. . . . 5
โข (๐ โ โค โ 3 โ
โ0) |
5 | | 3lt4 12334 |
. . . . 5
โข 3 <
4 |
6 | 4, 5 | jctir 522 |
. . . 4
โข (๐ โ โค โ (3 โ
โ0 โง 3 < 4)) |
7 | | modremain 16297 |
. . . 4
โข ((๐ โ โค โง 4 โ
โ โง (3 โ โ0 โง 3 < 4)) โ ((๐ mod 4) = 3 โ โ๐ง โ โค ((๐ง ยท 4) + 3) = ๐)) |
8 | 2, 6, 7 | mpd3an23 1464 |
. . 3
โข (๐ โ โค โ ((๐ mod 4) = 3 โ โ๐ง โ โค ((๐ง ยท 4) + 3) = ๐)) |
9 | | 2cnd 12238 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ง โ โค) โ 2 โ
โ) |
10 | | simpr 486 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ง โ โค) โ ๐ง โ
โค) |
11 | | 4z 12544 |
. . . . . . . . . . . . . 14
โข 4 โ
โค |
12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ง โ โค) โ 4 โ
โค) |
13 | 10, 12 | zmulcld 12620 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ง โ โค) โ (๐ง ยท 4) โ
โค) |
14 | 13 | zcnd 12615 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ง โ โค) โ (๐ง ยท 4) โ
โ) |
15 | | 3cn 12241 |
. . . . . . . . . . . 12
โข 3 โ
โ |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ง โ โค) โ 3 โ
โ) |
17 | 9, 14, 16 | adddid 11186 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ง โ โค) โ (2
ยท ((๐ง ยท 4) +
3)) = ((2 ยท (๐ง
ยท 4)) + (2 ยท 3))) |
18 | 10 | zcnd 12615 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ง โ โค) โ ๐ง โ
โ) |
19 | | 4cn 12245 |
. . . . . . . . . . . . . 14
โข 4 โ
โ |
20 | 19 | a1i 11 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ง โ โค) โ 4 โ
โ) |
21 | 9, 18, 20 | mul12d 11371 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ง โ โค) โ (2
ยท (๐ง ยท 4)) =
(๐ง ยท (2 ยท
4))) |
22 | | 2cn 12235 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
23 | | 4t2e8 12328 |
. . . . . . . . . . . . . 14
โข (4
ยท 2) = 8 |
24 | 19, 22, 23 | mulcomli 11171 |
. . . . . . . . . . . . 13
โข (2
ยท 4) = 8 |
25 | 24 | oveq2i 7373 |
. . . . . . . . . . . 12
โข (๐ง ยท (2 ยท 4)) =
(๐ง ยท
8) |
26 | 21, 25 | eqtrdi 2793 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ง โ โค) โ (2
ยท (๐ง ยท 4)) =
(๐ง ยท
8)) |
27 | | 3t2e6 12326 |
. . . . . . . . . . . . 13
โข (3
ยท 2) = 6 |
28 | 15, 22, 27 | mulcomli 11171 |
. . . . . . . . . . . 12
โข (2
ยท 3) = 6 |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โ โค โง ๐ง โ โค) โ (2
ยท 3) = 6) |
30 | 26, 29 | oveq12d 7380 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ง โ โค) โ ((2
ยท (๐ง ยท 4)) +
(2 ยท 3)) = ((๐ง
ยท 8) + 6)) |
31 | 17, 30 | eqtrd 2777 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ง โ โค) โ (2
ยท ((๐ง ยท 4) +
3)) = ((๐ง ยท 8) +
6)) |
32 | 31 | oveq1d 7377 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ง โ โค) โ ((2
ยท ((๐ง ยท 4) +
3)) + 1) = (((๐ง ยท 8)
+ 6) + 1)) |
33 | | id 22 |
. . . . . . . . . . . . 13
โข (๐ง โ โค โ ๐ง โ
โค) |
34 | | 8nn 12255 |
. . . . . . . . . . . . . . 15
โข 8 โ
โ |
35 | 34 | nnzi 12534 |
. . . . . . . . . . . . . 14
โข 8 โ
โค |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ง โ โค โ 8 โ
โค) |
37 | 33, 36 | zmulcld 12620 |
. . . . . . . . . . . 12
โข (๐ง โ โค โ (๐ง ยท 8) โ
โค) |
38 | 37 | zcnd 12615 |
. . . . . . . . . . 11
โข (๐ง โ โค โ (๐ง ยท 8) โ
โ) |
39 | | 6cn 12251 |
. . . . . . . . . . . 12
โข 6 โ
โ |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
โข (๐ง โ โค โ 6 โ
โ) |
41 | | 1cnd 11157 |
. . . . . . . . . . 11
โข (๐ง โ โค โ 1 โ
โ) |
42 | 38, 40, 41 | addassd 11184 |
. . . . . . . . . 10
โข (๐ง โ โค โ (((๐ง ยท 8) + 6) + 1) = ((๐ง ยท 8) + (6 +
1))) |
43 | | 6p1e7 12308 |
. . . . . . . . . . . 12
โข (6 + 1) =
7 |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
โข (๐ง โ โค โ (6 + 1) =
7) |
45 | 44 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ง โ โค โ ((๐ง ยท 8) + (6 + 1)) =
((๐ง ยท 8) +
7)) |
46 | 42, 45 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ง โ โค โ (((๐ง ยท 8) + 6) + 1) = ((๐ง ยท 8) +
7)) |
47 | 46 | adantl 483 |
. . . . . . . 8
โข ((๐ โ โค โง ๐ง โ โค) โ (((๐ง ยท 8) + 6) + 1) = ((๐ง ยท 8) +
7)) |
48 | 32, 47 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โ โค โง ๐ง โ โค) โ ((2
ยท ((๐ง ยท 4) +
3)) + 1) = ((๐ง ยท 8)
+ 7)) |
49 | 48 | oveq1d 7377 |
. . . . . 6
โข ((๐ โ โค โง ๐ง โ โค) โ (((2
ยท ((๐ง ยท 4) +
3)) + 1) mod 8) = (((๐ง
ยท 8) + 7) mod 8)) |
50 | | nnrp 12933 |
. . . . . . . . 9
โข (8 โ
โ โ 8 โ โ+) |
51 | 34, 50 | mp1i 13 |
. . . . . . . 8
โข (๐ง โ โค โ 8 โ
โ+) |
52 | | 0xr 11209 |
. . . . . . . . . 10
โข 0 โ
โ* |
53 | 52 | a1i 11 |
. . . . . . . . 9
โข (๐ง โ โค โ 0 โ
โ*) |
54 | | 8re 12256 |
. . . . . . . . . . 11
โข 8 โ
โ |
55 | 54 | rexri 11220 |
. . . . . . . . . 10
โข 8 โ
โ* |
56 | 55 | a1i 11 |
. . . . . . . . 9
โข (๐ง โ โค โ 8 โ
โ*) |
57 | | 7re 12253 |
. . . . . . . . . . 11
โข 7 โ
โ |
58 | 57 | rexri 11220 |
. . . . . . . . . 10
โข 7 โ
โ* |
59 | 58 | a1i 11 |
. . . . . . . . 9
โข (๐ง โ โค โ 7 โ
โ*) |
60 | | 0re 11164 |
. . . . . . . . . . 11
โข 0 โ
โ |
61 | | 7pos 12271 |
. . . . . . . . . . 11
โข 0 <
7 |
62 | 60, 57, 61 | ltleii 11285 |
. . . . . . . . . 10
โข 0 โค
7 |
63 | 62 | a1i 11 |
. . . . . . . . 9
โข (๐ง โ โค โ 0 โค
7) |
64 | | 7lt8 12352 |
. . . . . . . . . 10
โข 7 <
8 |
65 | 64 | a1i 11 |
. . . . . . . . 9
โข (๐ง โ โค โ 7 <
8) |
66 | 53, 56, 59, 63, 65 | elicod 13321 |
. . . . . . . 8
โข (๐ง โ โค โ 7 โ
(0[,)8)) |
67 | | muladdmodid 13823 |
. . . . . . . 8
โข ((๐ง โ โค โง 8 โ
โ+ โง 7 โ (0[,)8)) โ (((๐ง ยท 8) + 7) mod 8) =
7) |
68 | 51, 66, 67 | mpd3an23 1464 |
. . . . . . 7
โข (๐ง โ โค โ (((๐ง ยท 8) + 7) mod 8) =
7) |
69 | 68 | adantl 483 |
. . . . . 6
โข ((๐ โ โค โง ๐ง โ โค) โ (((๐ง ยท 8) + 7) mod 8) =
7) |
70 | 49, 69 | eqtrd 2777 |
. . . . 5
โข ((๐ โ โค โง ๐ง โ โค) โ (((2
ยท ((๐ง ยท 4) +
3)) + 1) mod 8) = 7) |
71 | | oveq2 7370 |
. . . . . . . 8
โข (((๐ง ยท 4) + 3) = ๐ โ (2 ยท ((๐ง ยท 4) + 3)) = (2 ยท
๐)) |
72 | 71 | oveq1d 7377 |
. . . . . . 7
โข (((๐ง ยท 4) + 3) = ๐ โ ((2 ยท ((๐ง ยท 4) + 3)) + 1) = ((2
ยท ๐) +
1)) |
73 | 72 | oveq1d 7377 |
. . . . . 6
โข (((๐ง ยท 4) + 3) = ๐ โ (((2 ยท ((๐ง ยท 4) + 3)) + 1) mod 8) =
(((2 ยท ๐) + 1) mod
8)) |
74 | 73 | eqeq1d 2739 |
. . . . 5
โข (((๐ง ยท 4) + 3) = ๐ โ ((((2 ยท ((๐ง ยท 4) + 3)) + 1) mod 8) =
7 โ (((2 ยท ๐) +
1) mod 8) = 7)) |
75 | 70, 74 | syl5ibcom 244 |
. . . 4
โข ((๐ โ โค โง ๐ง โ โค) โ (((๐ง ยท 4) + 3) = ๐ โ (((2 ยท ๐) + 1) mod 8) =
7)) |
76 | 75 | rexlimdva 3153 |
. . 3
โข (๐ โ โค โ
(โ๐ง โ โค
((๐ง ยท 4) + 3) =
๐ โ (((2 ยท
๐) + 1) mod 8) =
7)) |
77 | 8, 76 | sylbid 239 |
. 2
โข (๐ โ โค โ ((๐ mod 4) = 3 โ (((2 ยท
๐) + 1) mod 8) =
7)) |
78 | 77 | imp 408 |
1
โข ((๐ โ โค โง (๐ mod 4) = 3) โ (((2
ยท ๐) + 1) mod 8) =
7) |