Step | Hyp | Ref
| Expression |
1 | | iblitg.1 |
. . . . 5
⢠(š ā šŗ = (š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠š), š, 0))) |
2 | 1 | adantr 480 |
. . . 4
⢠((š ā§ š¾ ā ā¤) ā šŗ = (š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠š), š, 0))) |
3 | | iblitg.2 |
. . . . . . . 8
⢠((š ā§ š„ ā š“) ā š = (āā(šµ / (iāš¾)))) |
4 | 3 | adantlr 712 |
. . . . . . 7
⢠(((š ā§ š¾ ā ā¤) ā§ š„ ā š“) ā š = (āā(šµ / (iāš¾)))) |
5 | | iexpcyc 14178 |
. . . . . . . . . 10
⢠(š¾ ā ⤠ā
(iā(š¾ mod 4)) =
(iāš¾)) |
6 | 5 | oveq2d 7428 |
. . . . . . . . 9
⢠(š¾ ā ⤠ā (šµ / (iā(š¾ mod 4))) = (šµ / (iāš¾))) |
7 | 6 | fveq2d 6895 |
. . . . . . . 8
⢠(š¾ ā ⤠ā
(āā(šµ /
(iā(š¾ mod 4)))) =
(āā(šµ /
(iāš¾)))) |
8 | 7 | ad2antlr 724 |
. . . . . . 7
⢠(((š ā§ š¾ ā ā¤) ā§ š„ ā š“) ā (āā(šµ / (iā(š¾ mod 4)))) = (āā(šµ / (iāš¾)))) |
9 | 4, 8 | eqtr4d 2774 |
. . . . . 6
⢠(((š ā§ š¾ ā ā¤) ā§ š„ ā š“) ā š = (āā(šµ / (iā(š¾ mod 4))))) |
10 | 9 | ibllem 25614 |
. . . . 5
⢠((š ā§ š¾ ā ā¤) ā if((š„ ā š“ ā§ 0 ⤠š), š, 0) = if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0)) |
11 | 10 | mpteq2dv 5250 |
. . . 4
⢠((š ā§ š¾ ā ā¤) ā (š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠š), š, 0)) = (š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0))) |
12 | 2, 11 | eqtrd 2771 |
. . 3
⢠((š ā§ š¾ ā ā¤) ā šŗ = (š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0))) |
13 | 12 | fveq2d 6895 |
. 2
⢠((š ā§ š¾ ā ā¤) ā
(ā«2āšŗ)
= (ā«2ā(š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0)))) |
14 | | oveq2 7420 |
. . . . . . . . . . 11
⢠(š = (š¾ mod 4) ā (iāš) = (iā(š¾ mod 4))) |
15 | 14 | oveq2d 7428 |
. . . . . . . . . 10
⢠(š = (š¾ mod 4) ā (šµ / (iāš)) = (šµ / (iā(š¾ mod 4)))) |
16 | 15 | fveq2d 6895 |
. . . . . . . . 9
⢠(š = (š¾ mod 4) ā (āā(šµ / (iāš))) = (āā(šµ / (iā(š¾ mod 4))))) |
17 | 16 | breq2d 5160 |
. . . . . . . 8
⢠(š = (š¾ mod 4) ā (0 ⤠(āā(šµ / (iāš))) ā 0 ⤠(āā(šµ / (iā(š¾ mod 4)))))) |
18 | 17 | anbi2d 628 |
. . . . . . 7
⢠(š = (š¾ mod 4) ā ((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))) ā (š„ ā š“ ā§ 0 ⤠(āā(šµ / (iā(š¾ mod 4))))))) |
19 | 18, 16 | ifbieq1d 4552 |
. . . . . 6
⢠(š = (š¾ mod 4) ā if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0) = if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0)) |
20 | 19 | mpteq2dv 5250 |
. . . . 5
⢠(š = (š¾ mod 4) ā (š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0)) = (š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0))) |
21 | 20 | fveq2d 6895 |
. . . 4
⢠(š = (š¾ mod 4) ā
(ā«2ā(š„
ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) = (ā«2ā(š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(šµ /
(iā(š¾ mod 4))))),
(āā(šµ /
(iā(š¾ mod 4)))),
0)))) |
22 | 21 | eleq1d 2817 |
. . 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 2732 |
. . . . . . 7
⢠(š ā (š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0)) = (š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) |
25 | | eqidd 2732 |
. . . . . . 7
⢠((š ā§ š„ ā š“) ā (āā(šµ / (iāš))) = (āā(šµ / (iāš)))) |
26 | | iblitg.4 |
. . . . . . 7
⢠((š ā§ š„ ā š“) ā šµ ā š) |
27 | 24, 25, 26 | isibl2 25616 |
. . . . . 6
⢠(š ā ((š„ ā š“ ⦠šµ) ā šæ1 ā
((š„ ā š“ ⦠šµ) ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā))) |
28 | 23, 27 | mpbid 231 |
. . . . 5
⢠(š ā ((š„ ā š“ ⦠šµ) ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā)) |
29 | 28 | simprd 495 |
. . . 4
⢠(š ā āš ā
(0...3)(ā«2ā(š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā) |
30 | 29 | adantr 480 |
. . 3
⢠((š ā§ š¾ ā ā¤) ā āš ā
(0...3)(ā«2ā(š„ ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā) |
31 | | 4nn 12302 |
. . . . . 6
⢠4 ā
ā |
32 | | zmodfz 13865 |
. . . . . 6
⢠((š¾ ā ⤠⧠4 ā
ā) ā (š¾ mod 4)
ā (0...(4 ā 1))) |
33 | 31, 32 | mpan2 688 |
. . . . 5
⢠(š¾ ā ⤠ā (š¾ mod 4) ā (0...(4 ā
1))) |
34 | | 4m1e3 12348 |
. . . . . 6
⢠(4
ā 1) = 3 |
35 | 34 | oveq2i 7423 |
. . . . 5
⢠(0...(4
ā 1)) = (0...3) |
36 | 33, 35 | eleqtrdi 2842 |
. . . 4
⢠(š¾ ā ⤠ā (š¾ mod 4) ā
(0...3)) |
37 | 36 | adantl 481 |
. . 3
⢠((š ā§ š¾ ā ā¤) ā (š¾ mod 4) ā (0...3)) |
38 | 22, 30, 37 | rspcdva 3613 |
. 2
⢠((š ā§ š¾ ā ā¤) ā
(ā«2ā(š„
ā ā ⦠if((š„ ā š“ ā§ 0 ⤠(āā(šµ / (iā(š¾ mod 4))))), (āā(šµ / (iā(š¾ mod 4)))), 0))) ā
ā) |
39 | 13, 38 | eqeltrd 2832 |
1
⢠((š ā§ š¾ ā ā¤) ā
(ā«2āšŗ)
ā ā) |