Step | Hyp | Ref
| Expression |
1 | | iblss2.1 |
. . 3
ā¢ (š ā š“ ā šµ) |
2 | | iblss2.2 |
. . 3
ā¢ (š ā šµ ā dom vol) |
3 | | iblss2.3 |
. . 3
ā¢ ((š ā§ š„ ā š“) ā š¶ ā š) |
4 | | iblss2.4 |
. . 3
ā¢ ((š ā§ š„ ā (šµ ā š“)) ā š¶ = 0) |
5 | | iblss2.5 |
. . . 4
ā¢ (š ā (š„ ā š“ ā¦ š¶) ā
šæ1) |
6 | | iblmbf 25135 |
. . . 4
ā¢ ((š„ ā š“ ā¦ š¶) ā šæ1 ā (š„ ā š“ ā¦ š¶) ā MblFn) |
7 | 5, 6 | syl 17 |
. . 3
ā¢ (š ā (š„ ā š“ ā¦ š¶) ā MblFn) |
8 | 1, 2, 3, 4, 7 | mbfss 25013 |
. 2
ā¢ (š ā (š„ ā šµ ā¦ š¶) ā MblFn) |
9 | 1 | adantr 482 |
. . . . . . . . . . 11
ā¢ ((š ā§ š ā (0...3)) ā š“ ā šµ) |
10 | 9 | sselda 3945 |
. . . . . . . . . 10
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā š“) ā š„ ā šµ) |
11 | 10 | iftrued 4495 |
. . . . . . . . 9
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā š“) ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0)) |
12 | | iftrue 4493 |
. . . . . . . . . 10
ā¢ (š„ ā š“ ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0)) |
13 | 12 | adantl 483 |
. . . . . . . . 9
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā š“) ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0)) |
14 | 11, 13 | eqtr4d 2780 |
. . . . . . . 8
ā¢ (((š ā§ š ā (0...3)) ā§ š„ ā š“) ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0)) |
15 | | ifid 4527 |
. . . . . . . . 9
ā¢ if(š„ ā šµ, 0, 0) = 0 |
16 | | simplll 774 |
. . . . . . . . . . . . . . . . 17
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā š) |
17 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā š„ ā šµ) |
18 | | simplr 768 |
. . . . . . . . . . . . . . . . . 18
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā Ā¬ š„ ā š“) |
19 | 17, 18 | eldifd 3922 |
. . . . . . . . . . . . . . . . 17
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā š„ ā (šµ ā š“)) |
20 | 16, 19, 4 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā š¶ = 0) |
21 | 20 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā (š¶ / (iāš)) = (0 / (iāš))) |
22 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā š ā (0...3)) |
23 | | elfzelz 13442 |
. . . . . . . . . . . . . . . 16
ā¢ (š ā (0...3) ā š ā
ā¤) |
24 | | ax-icn 11111 |
. . . . . . . . . . . . . . . . 17
ā¢ i ā
ā |
25 | | ine0 11591 |
. . . . . . . . . . . . . . . . 17
ā¢ i ā
0 |
26 | | expclz 13991 |
. . . . . . . . . . . . . . . . . 18
ā¢ ((i
ā ā ā§ i ā 0 ā§ š ā ā¤) ā (iāš) ā
ā) |
27 | | expne0i 14001 |
. . . . . . . . . . . . . . . . . 18
ā¢ ((i
ā ā ā§ i ā 0 ā§ š ā ā¤) ā (iāš) ā 0) |
28 | 26, 27 | div0d 11931 |
. . . . . . . . . . . . . . . . 17
ā¢ ((i
ā ā ā§ i ā 0 ā§ š ā ā¤) ā (0 / (iāš)) = 0) |
29 | 24, 25, 28 | mp3an12 1452 |
. . . . . . . . . . . . . . . 16
ā¢ (š ā ā¤ ā (0 /
(iāš)) =
0) |
30 | 22, 23, 29 | 3syl 18 |
. . . . . . . . . . . . . . 15
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā (0 / (iāš)) = 0) |
31 | 21, 30 | eqtrd 2777 |
. . . . . . . . . . . . . 14
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā (š¶ / (iāš)) = 0) |
32 | 31 | fveq2d 6847 |
. . . . . . . . . . . . 13
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā (āā(š¶ / (iāš))) = (āā0)) |
33 | | re0 15038 |
. . . . . . . . . . . . 13
ā¢
(āā0) = 0 |
34 | 32, 33 | eqtrdi 2793 |
. . . . . . . . . . . 12
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā (āā(š¶ / (iāš))) = 0) |
35 | 34 | ifeq1d 4506 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0) = if(0 ā¤ (āā(š¶ / (iāš))), 0, 0)) |
36 | | ifid 4527 |
. . . . . . . . . . 11
ā¢ if(0 ā¤
(āā(š¶ /
(iāš))), 0, 0) =
0 |
37 | 35, 36 | eqtrdi 2793 |
. . . . . . . . . 10
ā¢ ((((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā§ š„ ā šµ) ā if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0) = 0) |
38 | 37 | ifeq1da 4518 |
. . . . . . . . 9
ā¢ (((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = if(š„ ā šµ, 0, 0)) |
39 | | iffalse 4496 |
. . . . . . . . . 10
ā¢ (Ā¬
š„ ā š“ ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = 0) |
40 | 39 | adantl 483 |
. . . . . . . . 9
ā¢ (((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = 0) |
41 | 15, 38, 40 | 3eqtr4a 2803 |
. . . . . . . 8
ā¢ (((š ā§ š ā (0...3)) ā§ Ā¬ š„ ā š“) ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0)) |
42 | 14, 41 | pm2.61dan 812 |
. . . . . . 7
ā¢ ((š ā§ š ā (0...3)) ā if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) = if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0)) |
43 | | ifan 4540 |
. . . . . . 7
ā¢ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0) = if(š„ ā šµ, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) |
44 | | ifan 4540 |
. . . . . . 7
ā¢ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0) = if(š„ ā š“, if(0 ā¤ (āā(š¶ / (iāš))), (āā(š¶ / (iāš))), 0), 0) |
45 | 42, 43, 44 | 3eqtr4g 2802 |
. . . . . 6
ā¢ ((š ā§ š ā (0...3)) ā if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) |
46 | 45 | mpteq2dv 5208 |
. . . . 5
ā¢ ((š ā§ š ā (0...3)) ā (š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) |
47 | 46 | fveq2d 6847 |
. . . 4
ā¢ ((š ā§ š ā (0...3)) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) = (ā«2ā(š„ ā ā ā¦
if((š„ ā š“ ā§ 0 ā¤
(āā(š¶ /
(iāš)))),
(āā(š¶ /
(iāš))),
0)))) |
48 | | eqidd 2738 |
. . . . . 6
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) |
49 | | eqidd 2738 |
. . . . . 6
ā¢ ((š ā§ š„ ā š“) ā (āā(š¶ / (iāš))) = (āā(š¶ / (iāš)))) |
50 | 48, 49, 5, 3 | iblitg 25136 |
. . . . 5
ā¢ ((š ā§ š ā ā¤) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā) |
51 | 23, 50 | sylan2 594 |
. . . 4
ā¢ ((š ā§ š ā (0...3)) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā) |
52 | 47, 51 | eqeltrd 2838 |
. . 3
ā¢ ((š ā§ š ā (0...3)) ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā) |
53 | 52 | ralrimiva 3144 |
. 2
ā¢ (š ā āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā) |
54 | | eqidd 2738 |
. . 3
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) |
55 | | eqidd 2738 |
. . 3
ā¢ ((š ā§ š„ ā šµ) ā (āā(š¶ / (iāš))) = (āā(š¶ / (iāš)))) |
56 | | elun 4109 |
. . . . . 6
ā¢ (š„ ā (š“ āŖ (šµ ā š“)) ā (š„ ā š“ āØ š„ ā (šµ ā š“))) |
57 | | undif2 4437 |
. . . . . . . 8
ā¢ (š“ āŖ (šµ ā š“)) = (š“ āŖ šµ) |
58 | | ssequn1 4141 |
. . . . . . . . 9
ā¢ (š“ ā šµ ā (š“ āŖ šµ) = šµ) |
59 | 1, 58 | sylib 217 |
. . . . . . . 8
ā¢ (š ā (š“ āŖ šµ) = šµ) |
60 | 57, 59 | eqtrid 2789 |
. . . . . . 7
ā¢ (š ā (š“ āŖ (šµ ā š“)) = šµ) |
61 | 60 | eleq2d 2824 |
. . . . . 6
ā¢ (š ā (š„ ā (š“ āŖ (šµ ā š“)) ā š„ ā šµ)) |
62 | 56, 61 | bitr3id 285 |
. . . . 5
ā¢ (š ā ((š„ ā š“ āØ š„ ā (šµ ā š“)) ā š„ ā šµ)) |
63 | 62 | biimpar 479 |
. . . 4
ā¢ ((š ā§ š„ ā šµ) ā (š„ ā š“ āØ š„ ā (šµ ā š“))) |
64 | 7, 3 | mbfmptcl 25003 |
. . . . 5
ā¢ ((š ā§ š„ ā š“) ā š¶ ā ā) |
65 | | 0cn 11148 |
. . . . . 6
ā¢ 0 ā
ā |
66 | 4, 65 | eqeltrdi 2846 |
. . . . 5
ā¢ ((š ā§ š„ ā (šµ ā š“)) ā š¶ ā ā) |
67 | 64, 66 | jaodan 957 |
. . . 4
ā¢ ((š ā§ (š„ ā š“ āØ š„ ā (šµ ā š“))) ā š¶ ā ā) |
68 | 63, 67 | syldan 592 |
. . 3
ā¢ ((š ā§ š„ ā šµ) ā š¶ ā ā) |
69 | 54, 55, 68 | isibl2 25134 |
. 2
ā¢ (š ā ((š„ ā šµ ā¦ š¶) ā šæ1 ā
((š„ ā šµ ā¦ š¶) ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā šµ ā§ 0 ā¤ (āā(š¶ / (iāš)))), (āā(š¶ / (iāš))), 0))) ā ā))) |
70 | 8, 53, 69 | mpbir2and 712 |
1
ā¢ (š ā (š„ ā šµ ā¦ š¶) ā
šæ1) |