Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. . 3
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) |
2 | | eqidd 2734 |
. . 3
ā¢ ((š ā§ š„ ā š“) ā (āā(šµ / (iāš))) = (āā(šµ / (iāš)))) |
3 | | itgcnlem1.v |
. . 3
ā¢ ((š ā§ š„ ā š“) ā šµ ā ā) |
4 | 1, 2, 3 | isibl2 25154 |
. 2
ā¢ (š ā ((š„ ā š“ ā¦ šµ) ā šæ1 ā
((š„ ā š“ ā¦ šµ) ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā))) |
5 | | c0ex 11157 |
. . . . . . . 8
ā¢ 0 ā
V |
6 | | 1ex 11159 |
. . . . . . . 8
ā¢ 1 ā
V |
7 | | ax-icn 11118 |
. . . . . . . . . . 11
ā¢ i ā
ā |
8 | | exp0 13980 |
. . . . . . . . . . 11
ā¢ (i ā
ā ā (iā0) = 1) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
ā¢
(iā0) = 1 |
10 | 9 | itgvallem 25172 |
. . . . . . . . 9
ā¢ (š = 0 ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) = (ā«2ā(š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(šµ / 1))),
(āā(šµ / 1)),
0)))) |
11 | 10 | eleq1d 2819 |
. . . . . . . 8
ā¢ (š = 0 ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / 1))), (āā(šµ / 1)), 0))) ā
ā)) |
12 | | exp1 13982 |
. . . . . . . . . . 11
ā¢ (i ā
ā ā (iā1) = i) |
13 | 7, 12 | ax-mp 5 |
. . . . . . . . . 10
ā¢
(iā1) = i |
14 | 13 | itgvallem 25172 |
. . . . . . . . 9
ā¢ (š = 1 ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) = (ā«2ā(š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(šµ / i))),
(āā(šµ / i)),
0)))) |
15 | 14 | eleq1d 2819 |
. . . . . . . 8
ā¢ (š = 1 ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / i))), (āā(šµ / i)), 0))) ā
ā)) |
16 | 5, 6, 11, 15 | ralpr 4665 |
. . . . . . 7
ā¢
(āš ā
{0, 1} (ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / 1))), (āā(šµ / 1)), 0))) ā ā
ā§ (ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / i))), (āā(šµ / i)), 0))) ā
ā)) |
17 | 3 | div1d 11931 |
. . . . . . . . . . . . . 14
ā¢ ((š ā§ š„ ā š“) ā (šµ / 1) = šµ) |
18 | 17 | fveq2d 6850 |
. . . . . . . . . . . . 13
ā¢ ((š ā§ š„ ā š“) ā (āā(šµ / 1)) = (āāšµ)) |
19 | 18 | ibllem 25152 |
. . . . . . . . . . . 12
ā¢ (š ā if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / 1))), (āā(šµ / 1)), 0) = if((š„ ā š“ ā§ 0 ā¤ (āāšµ)), (āāšµ), 0)) |
20 | 19 | mpteq2dv 5211 |
. . . . . . . . . . 11
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / 1))), (āā(šµ / 1)), 0)) = (š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āāšµ)),
(āāšµ),
0))) |
21 | 20 | fveq2d 6850 |
. . . . . . . . . 10
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / 1))), (āā(šµ / 1)), 0))) =
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āāšµ)), (āāšµ), 0)))) |
22 | | itgcnlem.r |
. . . . . . . . . 10
ā¢ š
=
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āāšµ)), (āāšµ), 0))) |
23 | 21, 22 | eqtr4di 2791 |
. . . . . . . . 9
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / 1))), (āā(šµ / 1)), 0))) = š
) |
24 | 23 | eleq1d 2819 |
. . . . . . . 8
ā¢ (š ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / 1))), (āā(šµ / 1)), 0))) ā ā
ā š
ā
ā)) |
25 | | itgcnlem.t |
. . . . . . . . . 10
ā¢ š =
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āāšµ)), (āāšµ), 0))) |
26 | | imval 15001 |
. . . . . . . . . . . . . 14
ā¢ (šµ ā ā ā
(āāšµ) =
(āā(šµ /
i))) |
27 | 3, 26 | syl 17 |
. . . . . . . . . . . . 13
ā¢ ((š ā§ š„ ā š“) ā (āāšµ) = (āā(šµ / i))) |
28 | 27 | ibllem 25152 |
. . . . . . . . . . . 12
ā¢ (š ā if((š„ ā š“ ā§ 0 ā¤ (āāšµ)), (āāšµ), 0) = if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / i))), (āā(šµ / i)), 0)) |
29 | 28 | mpteq2dv 5211 |
. . . . . . . . . . 11
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āāšµ)), (āāšµ), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / i))), (āā(šµ / i)), 0))) |
30 | 29 | fveq2d 6850 |
. . . . . . . . . 10
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āāšµ)), (āāšµ), 0))) =
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / i))), (āā(šµ / i)), 0)))) |
31 | 25, 30 | eqtr2id 2786 |
. . . . . . . . 9
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / i))), (āā(šµ / i)), 0))) = š) |
32 | 31 | eleq1d 2819 |
. . . . . . . 8
ā¢ (š ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / i))), (āā(šµ / i)), 0))) ā ā
ā š ā
ā)) |
33 | 24, 32 | anbi12d 632 |
. . . . . . 7
ā¢ (š ā
(((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / 1))), (āā(šµ / 1)), 0))) ā ā
ā§ (ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / i))), (āā(šµ / i)), 0))) ā ā)
ā (š
ā ā
ā§ š ā
ā))) |
34 | 16, 33 | bitrid 283 |
. . . . . 6
ā¢ (š ā (āš ā {0, 1}
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā (š
ā ā ā§ š ā
ā))) |
35 | | 2ex 12238 |
. . . . . . . 8
ā¢ 2 ā
V |
36 | | 3ex 12243 |
. . . . . . . 8
ā¢ 3 ā
V |
37 | | i2 14115 |
. . . . . . . . . 10
ā¢
(iā2) = -1 |
38 | 37 | itgvallem 25172 |
. . . . . . . . 9
ā¢ (š = 2 ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) = (ā«2ā(š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(šµ / -1))),
(āā(šµ / -1)),
0)))) |
39 | 38 | eleq1d 2819 |
. . . . . . . 8
ā¢ (š = 2 ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -1))), (āā(šµ / -1)), 0))) ā
ā)) |
40 | | i3 14116 |
. . . . . . . . . 10
ā¢
(iā3) = -i |
41 | 40 | itgvallem 25172 |
. . . . . . . . 9
ā¢ (š = 3 ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) = (ā«2ā(š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(šµ / -i))),
(āā(šµ / -i)),
0)))) |
42 | 41 | eleq1d 2819 |
. . . . . . . 8
ā¢ (š = 3 ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -i))), (āā(šµ / -i)), 0))) ā
ā)) |
43 | 35, 36, 39, 42 | ralpr 4665 |
. . . . . . 7
ā¢
(āš ā
{2, 3} (ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -1))), (āā(šµ / -1)), 0))) ā ā
ā§ (ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -i))), (āā(šµ / -i)), 0))) ā
ā)) |
44 | | itgcnlem.s |
. . . . . . . . . 10
ā¢ š =
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ -(āāšµ)), -(āāšµ), 0))) |
45 | 3 | renegd 15103 |
. . . . . . . . . . . . . 14
ā¢ ((š ā§ š„ ā š“) ā (āā-šµ) = -(āāšµ)) |
46 | | ax-1cn 11117 |
. . . . . . . . . . . . . . . . . . 19
ā¢ 1 ā
ā |
47 | 46 | negnegi 11479 |
. . . . . . . . . . . . . . . . . 18
ā¢ --1 =
1 |
48 | 47 | oveq2i 7372 |
. . . . . . . . . . . . . . . . 17
ā¢ (-šµ / --1) = (-šµ / 1) |
49 | 3 | negcld 11507 |
. . . . . . . . . . . . . . . . . 18
ā¢ ((š ā§ š„ ā š“) ā -šµ ā ā) |
50 | 49 | div1d 11931 |
. . . . . . . . . . . . . . . . 17
ā¢ ((š ā§ š„ ā š“) ā (-šµ / 1) = -šµ) |
51 | 48, 50 | eqtrid 2785 |
. . . . . . . . . . . . . . . 16
ā¢ ((š ā§ š„ ā š“) ā (-šµ / --1) = -šµ) |
52 | 46 | negcli 11477 |
. . . . . . . . . . . . . . . . . 18
ā¢ -1 ā
ā |
53 | | neg1ne0 12277 |
. . . . . . . . . . . . . . . . . 18
ā¢ -1 ā
0 |
54 | | div2neg 11886 |
. . . . . . . . . . . . . . . . . 18
ā¢ ((šµ ā ā ā§ -1 ā
ā ā§ -1 ā 0) ā (-šµ / --1) = (šµ / -1)) |
55 | 52, 53, 54 | mp3an23 1454 |
. . . . . . . . . . . . . . . . 17
ā¢ (šµ ā ā ā (-šµ / --1) = (šµ / -1)) |
56 | 3, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
ā¢ ((š ā§ š„ ā š“) ā (-šµ / --1) = (šµ / -1)) |
57 | 51, 56 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
ā¢ ((š ā§ š„ ā š“) ā -šµ = (šµ / -1)) |
58 | 57 | fveq2d 6850 |
. . . . . . . . . . . . . 14
ā¢ ((š ā§ š„ ā š“) ā (āā-šµ) = (āā(šµ / -1))) |
59 | 45, 58 | eqtr3d 2775 |
. . . . . . . . . . . . 13
ā¢ ((š ā§ š„ ā š“) ā -(āāšµ) = (āā(šµ / -1))) |
60 | 59 | ibllem 25152 |
. . . . . . . . . . . 12
ā¢ (š ā if((š„ ā š“ ā§ 0 ā¤ -(āāšµ)), -(āāšµ), 0) = if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -1))), (āā(šµ / -1)), 0)) |
61 | 60 | mpteq2dv 5211 |
. . . . . . . . . . 11
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ -(āāšµ)), -(āāšµ), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -1))), (āā(šµ / -1)), 0))) |
62 | 61 | fveq2d 6850 |
. . . . . . . . . 10
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ -(āāšµ)), -(āāšµ), 0))) =
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -1))), (āā(šµ / -1)), 0)))) |
63 | 44, 62 | eqtr2id 2786 |
. . . . . . . . 9
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -1))), (āā(šµ / -1)), 0))) = š) |
64 | 63 | eleq1d 2819 |
. . . . . . . 8
ā¢ (š ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -1))), (āā(šµ / -1)), 0))) ā ā
ā š ā
ā)) |
65 | | itgcnlem.u |
. . . . . . . . . 10
ā¢ š =
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ -(āāšµ)), -(āāšµ), 0))) |
66 | | imval 15001 |
. . . . . . . . . . . . . . 15
ā¢ (-šµ ā ā ā
(āā-šµ) =
(āā(-šµ /
i))) |
67 | 49, 66 | syl 17 |
. . . . . . . . . . . . . 14
ā¢ ((š ā§ š„ ā š“) ā (āā-šµ) = (āā(-šµ / i))) |
68 | 3 | imnegd 15104 |
. . . . . . . . . . . . . 14
ā¢ ((š ā§ š„ ā š“) ā (āā-šµ) = -(āāšµ)) |
69 | 7 | negnegi 11479 |
. . . . . . . . . . . . . . . . . 18
ā¢ --i =
i |
70 | 69 | eqcomi 2742 |
. . . . . . . . . . . . . . . . 17
ā¢ i =
--i |
71 | 70 | oveq2i 7372 |
. . . . . . . . . . . . . . . 16
ā¢ (-šµ / i) = (-šµ / --i) |
72 | 7 | negcli 11477 |
. . . . . . . . . . . . . . . . . 18
ā¢ -i ā
ā |
73 | | ine0 11598 |
. . . . . . . . . . . . . . . . . . 19
ā¢ i ā
0 |
74 | 7, 73 | negne0i 11484 |
. . . . . . . . . . . . . . . . . 18
ā¢ -i ā
0 |
75 | | div2neg 11886 |
. . . . . . . . . . . . . . . . . 18
ā¢ ((šµ ā ā ā§ -i ā
ā ā§ -i ā 0) ā (-šµ / --i) = (šµ / -i)) |
76 | 72, 74, 75 | mp3an23 1454 |
. . . . . . . . . . . . . . . . 17
ā¢ (šµ ā ā ā (-šµ / --i) = (šµ / -i)) |
77 | 3, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
ā¢ ((š ā§ š„ ā š“) ā (-šµ / --i) = (šµ / -i)) |
78 | 71, 77 | eqtrid 2785 |
. . . . . . . . . . . . . . 15
ā¢ ((š ā§ š„ ā š“) ā (-šµ / i) = (šµ / -i)) |
79 | 78 | fveq2d 6850 |
. . . . . . . . . . . . . 14
ā¢ ((š ā§ š„ ā š“) ā (āā(-šµ / i)) = (āā(šµ / -i))) |
80 | 67, 68, 79 | 3eqtr3d 2781 |
. . . . . . . . . . . . 13
ā¢ ((š ā§ š„ ā š“) ā -(āāšµ) = (āā(šµ / -i))) |
81 | 80 | ibllem 25152 |
. . . . . . . . . . . 12
ā¢ (š ā if((š„ ā š“ ā§ 0 ā¤ -(āāšµ)), -(āāšµ), 0) = if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -i))), (āā(šµ / -i)), 0)) |
82 | 81 | mpteq2dv 5211 |
. . . . . . . . . . 11
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ -(āāšµ)), -(āāšµ), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -i))), (āā(šµ / -i)), 0))) |
83 | 82 | fveq2d 6850 |
. . . . . . . . . 10
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ -(āāšµ)), -(āāšµ), 0))) =
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -i))), (āā(šµ / -i)), 0)))) |
84 | 65, 83 | eqtr2id 2786 |
. . . . . . . . 9
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -i))), (āā(šµ / -i)), 0))) = š) |
85 | 84 | eleq1d 2819 |
. . . . . . . 8
ā¢ (š ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -i))), (āā(šµ / -i)), 0))) ā ā
ā š ā
ā)) |
86 | 64, 85 | anbi12d 632 |
. . . . . . 7
ā¢ (š ā
(((ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -1))), (āā(šµ / -1)), 0))) ā ā
ā§ (ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / -i))), (āā(šµ / -i)), 0))) ā ā)
ā (š ā ā
ā§ š ā
ā))) |
87 | 43, 86 | bitrid 283 |
. . . . . 6
ā¢ (š ā (āš ā {2, 3}
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā (š ā ā ā§ š ā
ā))) |
88 | 34, 87 | anbi12d 632 |
. . . . 5
ā¢ (š ā ((āš ā {0, 1}
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā§ āš ā {2, 3}
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā) ā ((š
ā ā ā§ š ā ā) ā§ (š ā ā ā§ š ā
ā)))) |
89 | | fz0to3un2pr 13552 |
. . . . . . 7
ā¢ (0...3) =
({0, 1} āŖ {2, 3}) |
90 | 89 | raleqi 3310 |
. . . . . 6
ā¢
(āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā āš ā ({0, 1} āŖ {2,
3})(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā) |
91 | | ralunb 4155 |
. . . . . 6
ā¢
(āš ā
({0, 1} āŖ {2, 3})(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā
(āš ā {0, 1}
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā§ āš ā {2, 3}
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā)) |
92 | 90, 91 | bitri 275 |
. . . . 5
ā¢
(āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā
(āš ā {0, 1}
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā§ āš ā {2, 3}
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā)) |
93 | | an4 655 |
. . . . 5
ā¢ (((š
ā ā ā§ š ā ā) ā§ (š ā ā ā§ š ā ā)) ā ((š
ā ā ā§ š ā ā) ā§ (š ā ā ā§ š ā
ā))) |
94 | 88, 92, 93 | 3bitr4g 314 |
. . . 4
ā¢ (š ā (āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā ā ((š
ā ā ā§ š ā ā) ā§ (š ā ā ā§ š ā
ā)))) |
95 | 94 | anbi2d 630 |
. . 3
ā¢ (š ā (((š„ ā š“ ā¦ šµ) ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā) ā ((š„ ā š“ ā¦ šµ) ā MblFn ā§ ((š
ā ā ā§ š ā ā) ā§ (š ā ā ā§ š ā ā))))) |
96 | | 3anass 1096 |
. . 3
ā¢ (((š„ ā š“ ā¦ šµ) ā MblFn ā§ (š
ā ā ā§ š ā ā) ā§ (š ā ā ā§ š ā ā)) ā ((š„ ā š“ ā¦ šµ) ā MblFn ā§ ((š
ā ā ā§ š ā ā) ā§ (š ā ā ā§ š ā ā)))) |
97 | 95, 96 | bitr4di 289 |
. 2
ā¢ (š ā (((š„ ā š“ ā¦ šµ) ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(šµ / (iāš)))), (āā(šµ / (iāš))), 0))) ā ā) ā ((š„ ā š“ ā¦ šµ) ā MblFn ā§ (š
ā ā ā§ š ā ā) ā§ (š ā ā ā§ š ā ā)))) |
98 | 4, 97 | bitrd 279 |
1
ā¢ (š ā ((š„ ā š“ ā¦ šµ) ā šæ1 ā
((š„ ā š“ ā¦ šµ) ā MblFn ā§ (š
ā ā ā§ š ā ā) ā§ (š ā ā ā§ š ā ā)))) |