Step | Hyp | Ref
| Expression |
1 | | iblitg.1 |
. . . . 5
ā¢ (š ā šŗ = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0))) |
2 | 1 | adantr 482 |
. . . 4
ā¢ ((š ā§ š¾ ā ā¤) ā šŗ = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0))) |
3 | | iblitg.2 |
. . . . . . . 8
ā¢ ((š ā§ š„ ā š“) ā š = (āā(šµ / (iāš¾)))) |
4 | 3 | adantlr 713 |
. . . . . . 7
ā¢ (((š ā§ š¾ ā ā¤) ā§ š„ ā š“) ā š = (āā(šµ / (iāš¾)))) |
5 | | iexpcyc 13965 |
. . . . . . . . . 10
ā¢ (š¾ ā ā¤ ā
(iā(š¾ mod 4)) =
(iāš¾)) |
6 | 5 | oveq2d 7319 |
. . . . . . . . 9
ā¢ (š¾ ā ā¤ ā (šµ / (iā(š¾ mod 4))) = (šµ / (iāš¾))) |
7 | 6 | fveq2d 6804 |
. . . . . . . 8
ā¢ (š¾ ā ā¤ ā
(āā(šµ /
(iā(š¾ mod 4)))) =
(āā(šµ /
(iāš¾)))) |
8 | 7 | ad2antlr 725 |
. . . . . . 7
ā¢ (((š ā§ š¾ ā ā¤) ā§ š„ ā š“) ā (āā(šµ / (iā(š¾ mod 4)))) = (āā(šµ / (iāš¾)))) |
9 | 4, 8 | eqtr4d 2779 |
. . . . . 6
ā¢ (((š ā§ š¾ ā ā¤) ā§ š„ ā š“) ā š = (āā(šµ / (iā(š¾ mod 4))))) |
10 | 9 | ibllem 24970 |
. . . . 5
ā¢ ((š ā§ š¾ ā ā¤) ā if((š„ ā š“ ā§ 0 ā¤ š), š, 0) = if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0)) |
11 | 10 | mpteq2dv 5183 |
. . . 4
ā¢ ((š ā§ š¾ ā ā¤) ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0))) |
12 | 2, 11 | eqtrd 2776 |
. . 3
ā¢ ((š ā§ š¾ ā ā¤) ā šŗ = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0))) |
13 | 12 | fveq2d 6804 |
. 2
ā¢ ((š ā§ š¾ ā ā¤) ā
(ā«2āšŗ)
= (ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0)))) |
14 | | oveq2 7311 |
. . . . . . . . . . 11
ā¢ (š = (š¾ mod 4) ā (iāš) = (iā(š¾ mod 4))) |
15 | 14 | oveq2d 7319 |
. . . . . . . . . 10
ā¢ (š = (š¾ mod 4) ā (šµ / (iāš)) = (šµ / (iā(š¾ mod 4)))) |
16 | 15 | fveq2d 6804 |
. . . . . . . . 9
ā¢ (š = (š¾ mod 4) ā (āā(šµ / (iāš))) = (āā(šµ / (iā(š¾ mod 4))))) |
17 | 16 | breq2d 5093 |
. . . . . . . 8
ā¢ (š = (š¾ mod 4) ā (0 ā¤ (āā(šµ / (iāš))) ā 0 ā¤ (āā(šµ / (iā(š¾ mod 4)))))) |
18 | 17 | anbi2d 630 |
. . . . . . 7
ā¢ (š = (š¾ mod 4) ā ((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))) ā (š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iā(š¾ mod 4))))))) |
19 | 18, 16 | ifbieq1d 4489 |
. . . . . 6
ā¢ (š = (š¾ mod 4) ā if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0)) |
20 | 19 | mpteq2dv 5183 |
. . . . 5
ā¢ (š = (š¾ mod 4) ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0))) |
21 | 20 | fveq2d 6804 |
. . . 4
ā¢ (š = (š¾ mod 4) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) = (ā«2ā(š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(šµ /
(iā(š¾ mod 4))))),
(āā(šµ /
(iā(š¾ mod 4)))),
0)))) |
22 | 21 | eleq1d 2821 |
. . 3
ā¢ (š = (š¾ mod 4) ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0))) ā
ā)) |
23 | | iblitg.3 |
. . . . . 6
ā¢ (š ā (š„ ā š“ ā¦ šµ) ā
šæ1) |
24 | | eqidd 2737 |
. . . . . . 7
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) |
25 | | eqidd 2737 |
. . . . . . 7
ā¢ ((š ā§ š„ ā š“) ā (āā(šµ / (iāš))) = (āā(šµ / (iāš)))) |
26 | | iblitg.4 |
. . . . . . 7
ā¢ ((š ā§ š„ ā š“) ā šµ ā š) |
27 | 24, 25, 26 | isibl2 24972 |
. . . . . 6
ā¢ (š ā ((š„ ā š“ ā¦ šµ) ā šæ1 ā
((š„ ā š“ ā¦ šµ) ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā))) |
28 | 23, 27 | mpbid 232 |
. . . . 5
ā¢ (š ā ((š„ ā š“ ā¦ šµ) ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā)) |
29 | 28 | simprd 497 |
. . . 4
ā¢ (š ā āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā) |
30 | 29 | adantr 482 |
. . 3
ā¢ ((š ā§ š¾ ā ā¤) ā āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā) |
31 | | 4nn 12098 |
. . . . . 6
ā¢ 4 ā
ā |
32 | | zmodfz 13655 |
. . . . . 6
ā¢ ((š¾ ā ā¤ ā§ 4 ā
ā) ā (š¾ mod 4)
ā (0...(4 ā 1))) |
33 | 31, 32 | mpan2 689 |
. . . . 5
ā¢ (š¾ ā ā¤ ā (š¾ mod 4) ā (0...(4 ā
1))) |
34 | | 4m1e3 12144 |
. . . . . 6
ā¢ (4
ā 1) = 3 |
35 | 34 | oveq2i 7314 |
. . . . 5
ā¢ (0...(4
ā 1)) = (0...3) |
36 | 33, 35 | eleqtrdi 2847 |
. . . 4
ā¢ (š¾ ā ā¤ ā (š¾ mod 4) ā
(0...3)) |
37 | 36 | adantl 483 |
. . 3
ā¢ ((š ā§ š¾ ā ā¤) ā (š¾ mod 4) ā (0...3)) |
38 | 22, 30, 37 | rspcdva 3567 |
. 2
ā¢ ((š ā§ š¾ ā ā¤) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0))) ā
ā) |
39 | 13, 38 | eqeltrd 2837 |
1
ā¢ ((š ā§ š¾ ā ā¤) ā
(ā«2āšŗ)
ā ā) |