Step | Hyp | Ref
| Expression |
1 | | zq 9628 |
. . . 4
โข (๐พ โ โค โ ๐พ โ
โ) |
2 | | 4z 9285 |
. . . . . 6
โข 4 โ
โค |
3 | | zq 9628 |
. . . . . 6
โข (4 โ
โค โ 4 โ โ) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
โข 4 โ
โ |
5 | | 4pos 9018 |
. . . . 5
โข 0 <
4 |
6 | | modqval 10326 |
. . . . 5
โข ((๐พ โ โ โง 4 โ
โ โง 0 < 4) โ (๐พ mod 4) = (๐พ โ (4 ยท (โโ(๐พ / 4))))) |
7 | 4, 5, 6 | mp3an23 1329 |
. . . 4
โข (๐พ โ โ โ (๐พ mod 4) = (๐พ โ (4 ยท (โโ(๐พ / 4))))) |
8 | 1, 7 | syl 14 |
. . 3
โข (๐พ โ โค โ (๐พ mod 4) = (๐พ โ (4 ยท (โโ(๐พ / 4))))) |
9 | 8 | oveq2d 5893 |
. 2
โข (๐พ โ โค โ
(iโ(๐พ mod 4)) =
(iโ(๐พ โ (4
ยท (โโ(๐พ
/ 4)))))) |
10 | | 4nn 9084 |
. . . . . . 7
โข 4 โ
โ |
11 | | znq 9626 |
. . . . . . 7
โข ((๐พ โ โค โง 4 โ
โ) โ (๐พ / 4)
โ โ) |
12 | 10, 11 | mpan2 425 |
. . . . . 6
โข (๐พ โ โค โ (๐พ / 4) โ
โ) |
13 | 12 | flqcld 10279 |
. . . . 5
โข (๐พ โ โค โ
(โโ(๐พ / 4))
โ โค) |
14 | | zmulcl 9308 |
. . . . 5
โข ((4
โ โค โง (โโ(๐พ / 4)) โ โค) โ (4 ยท
(โโ(๐พ / 4)))
โ โค) |
15 | 2, 13, 14 | sylancr 414 |
. . . 4
โข (๐พ โ โค โ (4
ยท (โโ(๐พ
/ 4))) โ โค) |
16 | | ax-icn 7908 |
. . . . 5
โข i โ
โ |
17 | | iap0 9144 |
. . . . 5
โข i #
0 |
18 | | expsubap 10570 |
. . . . 5
โข (((i
โ โ โง i # 0) โง (๐พ โ โค โง (4 ยท
(โโ(๐พ / 4)))
โ โค)) โ (iโ(๐พ โ (4 ยท (โโ(๐พ / 4))))) = ((iโ๐พ) / (iโ(4 ยท
(โโ(๐พ /
4)))))) |
19 | 16, 17, 18 | mpanl12 436 |
. . . 4
โข ((๐พ โ โค โง (4
ยท (โโ(๐พ
/ 4))) โ โค) โ (iโ(๐พ โ (4 ยท (โโ(๐พ / 4))))) = ((iโ๐พ) / (iโ(4 ยท
(โโ(๐พ /
4)))))) |
20 | 15, 19 | mpdan 421 |
. . 3
โข (๐พ โ โค โ
(iโ(๐พ โ (4
ยท (โโ(๐พ
/ 4))))) = ((iโ๐พ) /
(iโ(4 ยท (โโ(๐พ / 4)))))) |
21 | | expmulzap 10568 |
. . . . . . . 8
โข (((i
โ โ โง i # 0) โง (4 โ โค โง (โโ(๐พ / 4)) โ โค)) โ
(iโ(4 ยท (โโ(๐พ / 4)))) =
((iโ4)โ(โโ(๐พ / 4)))) |
22 | 16, 17, 21 | mpanl12 436 |
. . . . . . 7
โข ((4
โ โค โง (โโ(๐พ / 4)) โ โค) โ (iโ(4
ยท (โโ(๐พ
/ 4)))) = ((iโ4)โ(โโ(๐พ / 4)))) |
23 | 2, 13, 22 | sylancr 414 |
. . . . . 6
โข (๐พ โ โค โ
(iโ(4 ยท (โโ(๐พ / 4)))) =
((iโ4)โ(โโ(๐พ / 4)))) |
24 | | i4 10625 |
. . . . . . . 8
โข
(iโ4) = 1 |
25 | 24 | oveq1i 5887 |
. . . . . . 7
โข
((iโ4)โ(โโ(๐พ / 4))) = (1โ(โโ(๐พ / 4))) |
26 | | 1exp 10551 |
. . . . . . . 8
โข
((โโ(๐พ /
4)) โ โค โ (1โ(โโ(๐พ / 4))) = 1) |
27 | 13, 26 | syl 14 |
. . . . . . 7
โข (๐พ โ โค โ
(1โ(โโ(๐พ /
4))) = 1) |
28 | 25, 27 | eqtrid 2222 |
. . . . . 6
โข (๐พ โ โค โ
((iโ4)โ(โโ(๐พ / 4))) = 1) |
29 | 23, 28 | eqtrd 2210 |
. . . . 5
โข (๐พ โ โค โ
(iโ(4 ยท (โโ(๐พ / 4)))) = 1) |
30 | 29 | oveq2d 5893 |
. . . 4
โข (๐พ โ โค โ
((iโ๐พ) / (iโ(4
ยท (โโ(๐พ
/ 4))))) = ((iโ๐พ) /
1)) |
31 | | expclzap 10547 |
. . . . . 6
โข ((i
โ โ โง i # 0 โง ๐พ โ โค) โ (iโ๐พ) โ
โ) |
32 | 16, 17, 31 | mp3an12 1327 |
. . . . 5
โข (๐พ โ โค โ
(iโ๐พ) โ
โ) |
33 | 32 | div1d 8739 |
. . . 4
โข (๐พ โ โค โ
((iโ๐พ) / 1) =
(iโ๐พ)) |
34 | 30, 33 | eqtrd 2210 |
. . 3
โข (๐พ โ โค โ
((iโ๐พ) / (iโ(4
ยท (โโ(๐พ
/ 4))))) = (iโ๐พ)) |
35 | 20, 34 | eqtrd 2210 |
. 2
โข (๐พ โ โค โ
(iโ(๐พ โ (4
ยท (โโ(๐พ
/ 4))))) = (iโ๐พ)) |
36 | 9, 35 | eqtrd 2210 |
1
โข (๐พ โ โค โ
(iโ(๐พ mod 4)) =
(iโ๐พ)) |