Step | Hyp | Ref
| Expression |
1 | | isibl.1 |
. . 3
ā¢ (š ā šŗ = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0))) |
2 | | nfv 1918 |
. . . . . . 7
ā¢
ā²š„ š¦ ā š“ |
3 | | nfcv 2908 |
. . . . . . . 8
ā¢
ā²š„0 |
4 | | nfcv 2908 |
. . . . . . . 8
ā¢
ā²š„
ā¤ |
5 | | nfcv 2908 |
. . . . . . . . 9
ā¢
ā²š„ā |
6 | | nffvmpt1 6854 |
. . . . . . . . . 10
ā¢
ā²š„((š„ ā š“ ā¦ šµ)āš¦) |
7 | | nfcv 2908 |
. . . . . . . . . 10
ā¢
ā²š„
/ |
8 | | nfcv 2908 |
. . . . . . . . . 10
ā¢
ā²š„(iāš) |
9 | 6, 7, 8 | nfov 7388 |
. . . . . . . . 9
ā¢
ā²š„(((š„ ā š“ ā¦ šµ)āš¦) / (iāš)) |
10 | 5, 9 | nffv 6853 |
. . . . . . . 8
ā¢
ā²š„(āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš))) |
11 | 3, 4, 10 | nfbr 5153 |
. . . . . . 7
ā¢
ā²š„0 ā¤
(āā(((š„ ā
š“ ā¦ šµ)āš¦) / (iāš))) |
12 | 2, 11 | nfan 1903 |
. . . . . 6
ā¢
ā²š„(š¦ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš)))) |
13 | 12, 10, 3 | nfif 4517 |
. . . . 5
ā¢
ā²š„if((š¦ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš))), 0) |
14 | | nfcv 2908 |
. . . . 5
ā¢
ā²š¦if((š„ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš))), 0) |
15 | | eleq1w 2821 |
. . . . . . 7
ā¢ (š¦ = š„ ā (š¦ ā š“ ā š„ ā š“)) |
16 | | fveq2 6843 |
. . . . . . . . 9
ā¢ (š¦ = š„ ā ((š„ ā š“ ā¦ šµ)āš¦) = ((š„ ā š“ ā¦ šµ)āš„)) |
17 | 16 | fvoveq1d 7380 |
. . . . . . . 8
ā¢ (š¦ = š„ ā (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš))) = (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš)))) |
18 | 17 | breq2d 5118 |
. . . . . . 7
ā¢ (š¦ = š„ ā (0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš))) ā 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš))))) |
19 | 15, 18 | anbi12d 632 |
. . . . . 6
ā¢ (š¦ = š„ ā ((š¦ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš)))) ā (š„ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš)))))) |
20 | 19, 17 | ifbieq1d 4511 |
. . . . 5
ā¢ (š¦ = š„ ā if((š¦ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš))), 0)) |
21 | 13, 14, 20 | cbvmpt 5217 |
. . . 4
ā¢ (š¦ ā ā ā¦
if((š¦ ā š“ ā§ 0 ā¤
(āā(((š„ ā
š“ ā¦ šµ)āš¦) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš))), 0)) |
22 | | simpr 486 |
. . . . . . . . 9
ā¢ ((š ā§ š„ ā š“) ā š„ ā š“) |
23 | | isibl2.3 |
. . . . . . . . 9
ā¢ ((š ā§ š„ ā š“) ā šµ ā š) |
24 | | eqid 2737 |
. . . . . . . . . 10
ā¢ (š„ ā š“ ā¦ šµ) = (š„ ā š“ ā¦ šµ) |
25 | 24 | fvmpt2 6960 |
. . . . . . . . 9
ā¢ ((š„ ā š“ ā§ šµ ā š) ā ((š„ ā š“ ā¦ šµ)āš„) = šµ) |
26 | 22, 23, 25 | syl2anc 585 |
. . . . . . . 8
ā¢ ((š ā§ š„ ā š“) ā ((š„ ā š“ ā¦ šµ)āš„) = šµ) |
27 | 26 | fvoveq1d 7380 |
. . . . . . 7
ā¢ ((š ā§ š„ ā š“) ā (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš))) = (āā(šµ / (iāš)))) |
28 | | isibl.2 |
. . . . . . 7
ā¢ ((š ā§ š„ ā š“) ā š = (āā(šµ / (iāš)))) |
29 | 27, 28 | eqtr4d 2780 |
. . . . . 6
ā¢ ((š ā§ š„ ā š“) ā (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš))) = š) |
30 | 29 | ibllem 25132 |
. . . . 5
ā¢ (š ā if((š„ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ š), š, 0)) |
31 | 30 | mpteq2dv 5208 |
. . . 4
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš„) / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0))) |
32 | 21, 31 | eqtrid 2789 |
. . 3
ā¢ (š ā (š¦ ā ā ā¦ if((š¦ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0))) |
33 | 1, 32 | eqtr4d 2780 |
. 2
ā¢ (š ā šŗ = (š¦ ā ā ā¦ if((š¦ ā š“ ā§ 0 ā¤ (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš)))), (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš))), 0))) |
34 | | eqidd 2738 |
. 2
ā¢ ((š ā§ š¦ ā š“) ā (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš))) = (āā(((š„ ā š“ ā¦ šµ)āš¦) / (iāš)))) |
35 | 24, 23 | dmmptd 6647 |
. 2
ā¢ (š ā dom (š„ ā š“ ā¦ šµ) = š“) |
36 | | eqidd 2738 |
. 2
ā¢ ((š ā§ š¦ ā š“) ā ((š„ ā š“ ā¦ šµ)āš¦) = ((š„ ā š“ ā¦ šµ)āš¦)) |
37 | 33, 34, 35, 36 | isibl 25133 |
1
ā¢ (š ā ((š„ ā š“ ā¦ šµ) ā šæ1 ā
((š„ ā š“ ā¦ šµ) ā MblFn ā§ āš ā
(0...3)(ā«2āšŗ) ā ā))) |