Step | Hyp | Ref
| Expression |
1 | | zre 12510 |
. . . 4
โข (๐พ โ โค โ ๐พ โ
โ) |
2 | | 4re 12244 |
. . . . 5
โข 4 โ
โ |
3 | | 4pos 12267 |
. . . . 5
โข 0 <
4 |
4 | 2, 3 | elrpii 12925 |
. . . 4
โข 4 โ
โ+ |
5 | | modval 13783 |
. . . 4
โข ((๐พ โ โ โง 4 โ
โ+) โ (๐พ mod 4) = (๐พ โ (4 ยท (โโ(๐พ / 4))))) |
6 | 1, 4, 5 | sylancl 587 |
. . 3
โข (๐พ โ โค โ (๐พ mod 4) = (๐พ โ (4 ยท (โโ(๐พ / 4))))) |
7 | 6 | oveq2d 7378 |
. 2
โข (๐พ โ โค โ
(iโ(๐พ mod 4)) =
(iโ(๐พ โ (4
ยท (โโ(๐พ
/ 4)))))) |
8 | | 4z 12544 |
. . . . 5
โข 4 โ
โค |
9 | | 4nn 12243 |
. . . . . . 7
โข 4 โ
โ |
10 | | nndivre 12201 |
. . . . . . 7
โข ((๐พ โ โ โง 4 โ
โ) โ (๐พ / 4)
โ โ) |
11 | 1, 9, 10 | sylancl 587 |
. . . . . 6
โข (๐พ โ โค โ (๐พ / 4) โ
โ) |
12 | 11 | flcld 13710 |
. . . . 5
โข (๐พ โ โค โ
(โโ(๐พ / 4))
โ โค) |
13 | | zmulcl 12559 |
. . . . 5
โข ((4
โ โค โง (โโ(๐พ / 4)) โ โค) โ (4 ยท
(โโ(๐พ / 4)))
โ โค) |
14 | 8, 12, 13 | sylancr 588 |
. . . 4
โข (๐พ โ โค โ (4
ยท (โโ(๐พ
/ 4))) โ โค) |
15 | | ax-icn 11117 |
. . . . 5
โข i โ
โ |
16 | | ine0 11597 |
. . . . 5
โข i โ
0 |
17 | | expsub 14023 |
. . . . 5
โข (((i
โ โ โง i โ 0) โง (๐พ โ โค โง (4 ยท
(โโ(๐พ / 4)))
โ โค)) โ (iโ(๐พ โ (4 ยท (โโ(๐พ / 4))))) = ((iโ๐พ) / (iโ(4 ยท
(โโ(๐พ /
4)))))) |
18 | 15, 16, 17 | mpanl12 701 |
. . . 4
โข ((๐พ โ โค โง (4
ยท (โโ(๐พ
/ 4))) โ โค) โ (iโ(๐พ โ (4 ยท (โโ(๐พ / 4))))) = ((iโ๐พ) / (iโ(4 ยท
(โโ(๐พ /
4)))))) |
19 | 14, 18 | mpdan 686 |
. . 3
โข (๐พ โ โค โ
(iโ(๐พ โ (4
ยท (โโ(๐พ
/ 4))))) = ((iโ๐พ) /
(iโ(4 ยท (โโ(๐พ / 4)))))) |
20 | | expmulz 14021 |
. . . . . . . 8
โข (((i
โ โ โง i โ 0) โง (4 โ โค โง
(โโ(๐พ / 4))
โ โค)) โ (iโ(4 ยท (โโ(๐พ / 4)))) =
((iโ4)โ(โโ(๐พ / 4)))) |
21 | 15, 16, 20 | mpanl12 701 |
. . . . . . 7
โข ((4
โ โค โง (โโ(๐พ / 4)) โ โค) โ (iโ(4
ยท (โโ(๐พ
/ 4)))) = ((iโ4)โ(โโ(๐พ / 4)))) |
22 | 8, 12, 21 | sylancr 588 |
. . . . . 6
โข (๐พ โ โค โ
(iโ(4 ยท (โโ(๐พ / 4)))) =
((iโ4)โ(โโ(๐พ / 4)))) |
23 | | i4 14115 |
. . . . . . . 8
โข
(iโ4) = 1 |
24 | 23 | oveq1i 7372 |
. . . . . . 7
โข
((iโ4)โ(โโ(๐พ / 4))) = (1โ(โโ(๐พ / 4))) |
25 | | 1exp 14004 |
. . . . . . . 8
โข
((โโ(๐พ /
4)) โ โค โ (1โ(โโ(๐พ / 4))) = 1) |
26 | 12, 25 | syl 17 |
. . . . . . 7
โข (๐พ โ โค โ
(1โ(โโ(๐พ /
4))) = 1) |
27 | 24, 26 | eqtrid 2789 |
. . . . . 6
โข (๐พ โ โค โ
((iโ4)โ(โโ(๐พ / 4))) = 1) |
28 | 22, 27 | eqtrd 2777 |
. . . . 5
โข (๐พ โ โค โ
(iโ(4 ยท (โโ(๐พ / 4)))) = 1) |
29 | 28 | oveq2d 7378 |
. . . 4
โข (๐พ โ โค โ
((iโ๐พ) / (iโ(4
ยท (โโ(๐พ
/ 4))))) = ((iโ๐พ) /
1)) |
30 | | expclz 13997 |
. . . . . 6
โข ((i
โ โ โง i โ 0 โง ๐พ โ โค) โ (iโ๐พ) โ
โ) |
31 | 15, 16, 30 | mp3an12 1452 |
. . . . 5
โข (๐พ โ โค โ
(iโ๐พ) โ
โ) |
32 | 31 | div1d 11930 |
. . . 4
โข (๐พ โ โค โ
((iโ๐พ) / 1) =
(iโ๐พ)) |
33 | 29, 32 | eqtrd 2777 |
. . 3
โข (๐พ โ โค โ
((iโ๐พ) / (iโ(4
ยท (โโ(๐พ
/ 4))))) = (iโ๐พ)) |
34 | 19, 33 | eqtrd 2777 |
. 2
โข (๐พ โ โค โ
(iโ(๐พ โ (4
ยท (โโ(๐พ
/ 4))))) = (iโ๐พ)) |
35 | 7, 34 | eqtrd 2777 |
1
โข (๐พ โ โค โ
(iโ(๐พ mod 4)) =
(iโ๐พ)) |