Step | Hyp | Ref
| Expression |
1 | | iblss.1 |
. . . 4
ā¢ (š ā š“ ā šµ) |
2 | 1 | resmptd 5991 |
. . 3
ā¢ (š ā ((š„ ā šµ ā¦ š¶) ā¾ š“) = (š„ ā š“ ā¦ š¶)) |
3 | | iblss.4 |
. . . . 5
ā¢ (š ā (š„ ā šµ ā¦ š¶) ā
šæ1) |
4 | | iblmbf 25054 |
. . . . 5
ā¢ ((š„ ā šµ ā¦ š¶) ā šæ1 ā (š„ ā šµ ā¦ š¶) ā MblFn) |
5 | 3, 4 | syl 17 |
. . . 4
ā¢ (š ā (š„ ā šµ ā¦ š¶) ā MblFn) |
6 | | iblss.2 |
. . . 4
ā¢ (š ā š“ ā dom vol) |
7 | | mbfres 24930 |
. . . 4
ā¢ (((š„ ā šµ ā¦ š¶) ā MblFn ā§ š“ ā dom vol) ā ((š„ ā šµ ā¦ š¶) ā¾ š“) ā MblFn) |
8 | 5, 6, 7 | syl2anc 585 |
. . 3
ā¢ (š ā ((š„ ā šµ ā¦ š¶) ā¾ š“) ā MblFn) |
9 | 2, 8 | eqeltrrd 2840 |
. 2
ā¢ (š ā (š„ ā š“ ā¦ š¶) ā MblFn) |
10 | | ifan 4538 |
. . . . . 6
ā¢ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0) = if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) |
11 | 1 | sselda 3943 |
. . . . . . . . 9
ā¢ ((š ā§ š„ ā š“) ā š„ ā šµ) |
12 | 11 | ad4ant14 751 |
. . . . . . . 8
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā š“) ā š„ ā šµ) |
13 | | iblss.3 |
. . . . . . . . . . . . . . 15
ā¢ ((š ā§ š„ ā šµ) ā š¶ ā š) |
14 | 5, 13 | mbfmptcl 24922 |
. . . . . . . . . . . . . 14
ā¢ ((š ā§ š„ ā šµ) ā š¶ ā ā) |
15 | 14 | ad4ant14 751 |
. . . . . . . . . . . . 13
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā š¶ ā ā) |
16 | | ax-icn 11044 |
. . . . . . . . . . . . . 14
ā¢ i ā
ā |
17 | | ine0 11524 |
. . . . . . . . . . . . . 14
ā¢ i ā
0 |
18 | | elfzelz 13370 |
. . . . . . . . . . . . . . 15
ā¢ (š ā (0...3) ā š ā
ā¤) |
19 | 18 | ad3antlr 730 |
. . . . . . . . . . . . . 14
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā š ā ā¤) |
20 | | expclz 13921 |
. . . . . . . . . . . . . 14
ā¢ ((i
ā ā ā§ i ā 0 ā§ š ā ā¤) ā (iāš) ā
ā) |
21 | 16, 17, 19, 20 | mp3an12i 1466 |
. . . . . . . . . . . . 13
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā (iāš) ā ā) |
22 | | expne0i 13929 |
. . . . . . . . . . . . . 14
ā¢ ((i
ā ā ā§ i ā 0 ā§ š ā ā¤) ā (iāš) ā 0) |
23 | 16, 17, 19, 22 | mp3an12i 1466 |
. . . . . . . . . . . . 13
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā (iāš) ā 0) |
24 | 15, 21, 23 | divcld 11865 |
. . . . . . . . . . . 12
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā (š¶ / (iāš)) ā ā) |
25 | 24 | recld 15013 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā (āā(š¶ / (iāš))) ā ā) |
26 | | 0re 11091 |
. . . . . . . . . . 11
ā¢ 0 ā
ā |
27 | | ifcl 4530 |
. . . . . . . . . . 11
ā¢
(((āā(š¶ /
(iāš))) ā ā
ā§ 0 ā ā) ā if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0) ā ā) |
28 | 25, 26, 27 | sylancl 587 |
. . . . . . . . . 10
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0) ā ā) |
29 | 28 | rexrd 11139 |
. . . . . . . . 9
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0) ā
ā*) |
30 | | max1 13033 |
. . . . . . . . . 10
ā¢ ((0
ā ā ā§ (āā(š¶ / (iāš))) ā ā) ā 0 ā¤ if(0 ā¤
(āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))),
0)) |
31 | 26, 25, 30 | sylancr 588 |
. . . . . . . . 9
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā 0 ā¤ if(0 ā¤
(āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))),
0)) |
32 | | elxrge0 13303 |
. . . . . . . . 9
ā¢ (if(0
ā¤ (āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))), 0) ā
(0[,]+ā) ā (if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0) ā ā* ā§ 0
ā¤ if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0))) |
33 | 29, 31, 32 | sylanbrc 584 |
. . . . . . . 8
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0) ā
(0[,]+ā)) |
34 | 12, 33 | syldan 592 |
. . . . . . 7
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā š“) ā if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0) ā
(0[,]+ā)) |
35 | | 0e0iccpnf 13305 |
. . . . . . . 8
ā¢ 0 ā
(0[,]+ā) |
36 | 35 | a1i 11 |
. . . . . . 7
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ Ā¬ š„ ā š“) ā 0 ā
(0[,]+ā)) |
37 | 34, 36 | ifclda 4520 |
. . . . . 6
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā ā) ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā
(0[,]+ā)) |
38 | 10, 37 | eqeltrid 2843 |
. . . . 5
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā ā) ā if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0) ā
(0[,]+ā)) |
39 | 38 | fmpttd 7058 |
. . . 4
ā¢ ((š ā§ š ā (0...3)) ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))),
0)):āā¶(0[,]+ā)) |
40 | | eqidd 2739 |
. . . . . 6
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) |
41 | | eqidd 2739 |
. . . . . 6
ā¢ ((š ā§ š„ ā šµ) ā (āā(š¶ / (iāš))) = (āā(š¶ / (iāš)))) |
42 | 40, 41, 3, 13 | iblitg 25055 |
. . . . 5
ā¢ ((š ā§ š ā ā¤) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā) |
43 | 18, 42 | sylan2 594 |
. . . 4
ā¢ ((š ā§ š ā (0...3)) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā) |
44 | | ifan 4538 |
. . . . . . 7
ā¢ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0) = if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) |
45 | 35 | a1i 11 |
. . . . . . . 8
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ Ā¬ š„ ā šµ) ā 0 ā
(0[,]+ā)) |
46 | 33, 45 | ifclda 4520 |
. . . . . . 7
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā ā) ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā
(0[,]+ā)) |
47 | 44, 46 | eqeltrid 2843 |
. . . . . 6
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā ā) ā if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0) ā
(0[,]+ā)) |
48 | 47 | fmpttd 7058 |
. . . . 5
ā¢ ((š ā§ š ā (0...3)) ā (š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))),
0)):āā¶(0[,]+ā)) |
49 | 28 | leidd 11655 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0) ā¤ if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0)) |
50 | | breq1 5107 |
. . . . . . . . . . . 12
ā¢ (if(0
ā¤ (āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))), 0) = if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā (if(0 ā¤
(āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))), 0) ā¤ if(0
ā¤ (āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))), 0) ā
if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā¤ if(0 ā¤
(āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))),
0))) |
51 | | breq1 5107 |
. . . . . . . . . . . 12
ā¢ (0 =
if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā (0 ā¤ if(0 ā¤
(āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))), 0) ā
if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā¤ if(0 ā¤
(āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))),
0))) |
52 | 50, 51 | ifboth 4524 |
. . . . . . . . . . 11
ā¢ ((if(0
ā¤ (āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))), 0) ā¤ if(0
ā¤ (āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))), 0) ā§ 0
ā¤ if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0)) ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā¤ if(0 ā¤
(āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))),
0)) |
53 | 49, 31, 52 | syl2anc 585 |
. . . . . . . . . 10
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā¤ if(0 ā¤
(āā(š¶ /
(iāš))),
(āā(š¶ /
(iāš))),
0)) |
54 | | iftrue 4491 |
. . . . . . . . . . 11
ā¢ (š„ ā šµ ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0)) |
55 | 54 | adantl 483 |
. . . . . . . . . 10
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0)) |
56 | 53, 55 | breqtrrd 5132 |
. . . . . . . . 9
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ š„ ā šµ) ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā¤ if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0)) |
57 | | 0le0 12188 |
. . . . . . . . . . 11
ā¢ 0 ā¤
0 |
58 | 57 | a1i 11 |
. . . . . . . . . 10
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ Ā¬ š„ ā šµ) ā 0 ā¤ 0) |
59 | 12 | stoic1a 1775 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ Ā¬ š„ ā šµ) ā Ā¬ š„ ā š“) |
60 | 59 | iffalsed 4496 |
. . . . . . . . . 10
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ Ā¬ š„ ā šµ) ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = 0) |
61 | | iffalse 4494 |
. . . . . . . . . . 11
ā¢ (Ā¬
š„ ā šµ ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = 0) |
62 | 61 | adantl 483 |
. . . . . . . . . 10
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ Ā¬ š„ ā šµ) ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = 0) |
63 | 58, 60, 62 | 3brtr4d 5136 |
. . . . . . . . 9
ā¢ ((((š ā§ š ā (0...3)) ā§ š„ ā ā) ā§ Ā¬ š„ ā šµ) ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā¤ if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0)) |
64 | 56, 63 | pm2.61dan 812 |
. . . . . . . 8
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā ā) ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) ā¤ if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0)) |
65 | 64, 10, 44 | 3brtr4g 5138 |
. . . . . . 7
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā ā) ā if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0) ā¤ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) |
66 | 65 | ralrimiva 3142 |
. . . . . 6
ā¢ ((š ā§ š ā (0...3)) ā āš„ ā ā if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0) ā¤ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) |
67 | | reex 11076 |
. . . . . . . 8
ā¢ ā
ā V |
68 | 67 | a1i 11 |
. . . . . . 7
ā¢ ((š ā§ š ā (0...3)) ā ā ā
V) |
69 | | eqidd 2739 |
. . . . . . 7
ā¢ ((š ā§ š ā (0...3)) ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) |
70 | | eqidd 2739 |
. . . . . . 7
ā¢ ((š ā§ š ā (0...3)) ā (š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) |
71 | 68, 38, 47, 69, 70 | ofrfval2 7629 |
. . . . . 6
ā¢ ((š ā§ š ā (0...3)) ā ((š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) ār ā¤ (š„ ā ā ā¦
if((š„ ā šµ ā§ 0 ā¤
(āā(š¶ /
(iāš)))),
(āā(š¶ /
(iāš))), 0)) ā
āš„ ā ā
if((š„ ā š“ ā§ 0 ā¤
(āā(š¶ /
(iāš)))),
(āā(š¶ /
(iāš))), 0) ā¤
if((š„ ā šµ ā§ 0 ā¤
(āā(š¶ /
(iāš)))),
(āā(š¶ /
(iāš))),
0))) |
72 | 66, 71 | mpbird 257 |
. . . . 5
ā¢ ((š ā§ š ā (0...3)) ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) ār ā¤ (š„ ā ā ā¦
if((š„ ā šµ ā§ 0 ā¤
(āā(š¶ /
(iāš)))),
(āā(š¶ /
(iāš))),
0))) |
73 | | itg2le 25026 |
. . . . 5
ā¢ (((š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(š¶ /
(iāš)))),
(āā(š¶ /
(iāš))),
0)):āā¶(0[,]+ā) ā§ (š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)):āā¶(0[,]+ā) ā§
(š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(š¶ /
(iāš)))),
(āā(š¶ /
(iāš))), 0))
ār ā¤ (š„
ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā¤
(ā«2ā(š„
ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)))) |
74 | 39, 48, 72, 73 | syl3anc 1372 |
. . . 4
ā¢ ((š ā§ š ā (0...3)) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā¤
(ā«2ā(š„
ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)))) |
75 | | itg2lecl 25025 |
. . . 4
ā¢ (((š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(š¶ /
(iāš)))),
(āā(š¶ /
(iāš))),
0)):āā¶(0[,]+ā) ā§ (ā«2ā(š„ ā ā ā¦
if((š„ ā šµ ā§ 0 ā¤
(āā(š¶ /
(iāš)))),
(āā(š¶ /
(iāš))), 0))) ā
ā ā§ (ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā¤
(ā«2ā(š„
ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)))) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā) |
76 | 39, 43, 74, 75 | syl3anc 1372 |
. . 3
ā¢ ((š ā§ š ā (0...3)) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā) |
77 | 76 | ralrimiva 3142 |
. 2
ā¢ (š ā āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā) |
78 | | eqidd 2739 |
. . 3
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) |
79 | | eqidd 2739 |
. . 3
ā¢ ((š ā§ š„ ā š“) ā (āā(š¶ / (iāš))) = (āā(š¶ / (iāš)))) |
80 | 11, 14 | syldan 592 |
. . 3
ā¢ ((š ā§ š„ ā š“) ā š¶ ā ā) |
81 | 78, 79, 80 | isibl2 25053 |
. 2
ā¢ (š ā ((š„ ā š“ ā¦ š¶) ā šæ1 ā
((š„ ā š“ ā¦ š¶) ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā))) |
82 | 9, 77, 81 | mpbir2and 712 |
1
ā¢ (š ā (š„ ā š“ ā¦ š¶) ā
šæ1) |