Step | Hyp | Ref
| Expression |
1 | | fvex 6859 |
. . . . . . . . 9
ā¢
(āā((šāš„) / (iāš))) ā V |
2 | | breq2 5113 |
. . . . . . . . . . 11
ā¢ (š¦ = (āā((šāš„) / (iāš))) ā (0 ā¤ š¦ ā 0 ā¤ (āā((šāš„) / (iāš))))) |
3 | 2 | anbi2d 630 |
. . . . . . . . . 10
ā¢ (š¦ = (āā((šāš„) / (iāš))) ā ((š„ ā dom š ā§ 0 ā¤ š¦) ā (š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))))) |
4 | | id 22 |
. . . . . . . . . 10
ā¢ (š¦ = (āā((šāš„) / (iāš))) ā š¦ = (āā((šāš„) / (iāš)))) |
5 | 3, 4 | ifbieq1d 4514 |
. . . . . . . . 9
ā¢ (š¦ = (āā((šāš„) / (iāš))) ā if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0) = if((š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))), (āā((šāš„) / (iāš))), 0)) |
6 | 1, 5 | csbie 3895 |
. . . . . . . 8
ā¢
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0) = if((š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))), (āā((šāš„) / (iāš))), 0) |
7 | | dmeq 5863 |
. . . . . . . . . . 11
ā¢ (š = š¹ ā dom š = dom š¹) |
8 | 7 | eleq2d 2820 |
. . . . . . . . . 10
ā¢ (š = š¹ ā (š„ ā dom š ā š„ ā dom š¹)) |
9 | | fveq1 6845 |
. . . . . . . . . . . 12
ā¢ (š = š¹ ā (šāš„) = (š¹āš„)) |
10 | 9 | fvoveq1d 7383 |
. . . . . . . . . . 11
ā¢ (š = š¹ ā (āā((šāš„) / (iāš))) = (āā((š¹āš„) / (iāš)))) |
11 | 10 | breq2d 5121 |
. . . . . . . . . 10
ā¢ (š = š¹ ā (0 ā¤ (āā((šāš„) / (iāš))) ā 0 ā¤ (āā((š¹āš„) / (iāš))))) |
12 | 8, 11 | anbi12d 632 |
. . . . . . . . 9
ā¢ (š = š¹ ā ((š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))) ā (š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))))) |
13 | 12, 10 | ifbieq1d 4514 |
. . . . . . . 8
ā¢ (š = š¹ ā if((š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))), (āā((šāš„) / (iāš))), 0) = if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) |
14 | 6, 13 | eqtrid 2785 |
. . . . . . 7
ā¢ (š = š¹ ā ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0) = if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) |
15 | 14 | mpteq2dv 5211 |
. . . . . 6
ā¢ (š = š¹ ā (š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0)) = (š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) |
16 | 15 | fveq2d 6850 |
. . . . 5
ā¢ (š = š¹ ā (ā«2ā(š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0))) = (ā«2ā(š„ ā ā ā¦
if((š„ ā dom š¹ ā§ 0 ā¤
(āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)))) |
17 | 16 | eleq1d 2819 |
. . . 4
ā¢ (š = š¹ ā ((ā«2ā(š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0))) ā ā ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā)) |
18 | 17 | ralbidv 3171 |
. . 3
ā¢ (š = š¹ ā (āš ā
(0...3)(ā«2ā(š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0))) ā ā ā āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā)) |
19 | | df-ibl 25009 |
. . 3
ā¢
šæ1 = {š ā MblFn ā£ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0))) ā ā} |
20 | 18, 19 | elrab2 3652 |
. 2
ā¢ (š¹ ā šæ1
ā (š¹ ā MblFn
ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā)) |
21 | | isibl.3 |
. . . . . . . . . . . 12
ā¢ (š ā dom š¹ = š“) |
22 | 21 | eleq2d 2820 |
. . . . . . . . . . 11
ā¢ (š ā (š„ ā dom š¹ ā š„ ā š“)) |
23 | 22 | anbi1d 631 |
. . . . . . . . . 10
ā¢ (š ā ((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))) ā (š„ ā š“ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))))) |
24 | 23 | ifbid 4513 |
. . . . . . . . 9
ā¢ (š ā if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) |
25 | | isibl.4 |
. . . . . . . . . . . 12
ā¢ ((š ā§ š„ ā š“) ā (š¹āš„) = šµ) |
26 | 25 | fvoveq1d 7383 |
. . . . . . . . . . 11
ā¢ ((š ā§ š„ ā š“) ā (āā((š¹āš„) / (iāš))) = (āā(šµ / (iāš)))) |
27 | | isibl.2 |
. . . . . . . . . . 11
ā¢ ((š ā§ š„ ā š“) ā š = (āā(šµ / (iāš)))) |
28 | 26, 27 | eqtr4d 2776 |
. . . . . . . . . 10
ā¢ ((š ā§ š„ ā š“) ā (āā((š¹āš„) / (iāš))) = š) |
29 | 28 | ibllem 25152 |
. . . . . . . . 9
ā¢ (š ā if((š„ ā š“ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ š), š, 0)) |
30 | 24, 29 | eqtrd 2773 |
. . . . . . . 8
ā¢ (š ā if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ š), š, 0)) |
31 | 30 | mpteq2dv 5211 |
. . . . . . 7
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0))) |
32 | | isibl.1 |
. . . . . . 7
ā¢ (š ā šŗ = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0))) |
33 | 31, 32 | eqtr4d 2776 |
. . . . . 6
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) = šŗ) |
34 | 33 | fveq2d 6850 |
. . . . 5
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) = (ā«2āšŗ)) |
35 | 34 | eleq1d 2819 |
. . . 4
ā¢ (š ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā ā
(ā«2āšŗ)
ā ā)) |
36 | 35 | ralbidv 3171 |
. . 3
ā¢ (š ā (āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā ā āš ā
(0...3)(ā«2āšŗ) ā ā)) |
37 | 36 | anbi2d 630 |
. 2
ā¢ (š ā ((š¹ ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā) ā (š¹ ā MblFn ā§
āš ā
(0...3)(ā«2āšŗ) ā ā))) |
38 | 20, 37 | bitrid 283 |
1
ā¢ (š ā (š¹ ā šæ1 ā (š¹ ā MblFn ā§
āš ā
(0...3)(ā«2āšŗ) ā ā))) |