Step | Hyp | Ref
| Expression |
1 | | fvex 6904 |
. . . . . . . . 9
ā¢
(āā((šāš„) / (iāš))) ā V |
2 | | breq2 5152 |
. . . . . . . . . . 11
ā¢ (š¦ = (āā((šāš„) / (iāš))) ā (0 ā¤ š¦ ā 0 ā¤ (āā((šāš„) / (iāš))))) |
3 | 2 | anbi2d 629 |
. . . . . . . . . 10
ā¢ (š¦ = (āā((šāš„) / (iāš))) ā ((š„ ā dom š ā§ 0 ā¤ š¦) ā (š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))))) |
4 | | id 22 |
. . . . . . . . . 10
ā¢ (š¦ = (āā((šāš„) / (iāš))) ā š¦ = (āā((šāš„) / (iāš)))) |
5 | 3, 4 | ifbieq1d 4552 |
. . . . . . . . 9
ā¢ (š¦ = (āā((šāš„) / (iāš))) ā if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0) = if((š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))), (āā((šāš„) / (iāš))), 0)) |
6 | 1, 5 | csbie 3929 |
. . . . . . . 8
ā¢
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0) = if((š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))), (āā((šāš„) / (iāš))), 0) |
7 | | dmeq 5903 |
. . . . . . . . . . 11
ā¢ (š = š¹ ā dom š = dom š¹) |
8 | 7 | eleq2d 2819 |
. . . . . . . . . 10
ā¢ (š = š¹ ā (š„ ā dom š ā š„ ā dom š¹)) |
9 | | fveq1 6890 |
. . . . . . . . . . . 12
ā¢ (š = š¹ ā (šāš„) = (š¹āš„)) |
10 | 9 | fvoveq1d 7430 |
. . . . . . . . . . 11
ā¢ (š = š¹ ā (āā((šāš„) / (iāš))) = (āā((š¹āš„) / (iāš)))) |
11 | 10 | breq2d 5160 |
. . . . . . . . . 10
ā¢ (š = š¹ ā (0 ā¤ (āā((šāš„) / (iāš))) ā 0 ā¤ (āā((š¹āš„) / (iāš))))) |
12 | 8, 11 | anbi12d 631 |
. . . . . . . . 9
ā¢ (š = š¹ ā ((š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))) ā (š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))))) |
13 | 12, 10 | ifbieq1d 4552 |
. . . . . . . 8
ā¢ (š = š¹ ā if((š„ ā dom š ā§ 0 ā¤ (āā((šāš„) / (iāš)))), (āā((šāš„) / (iāš))), 0) = if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) |
14 | 6, 13 | eqtrid 2784 |
. . . . . . 7
ā¢ (š = š¹ ā ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0) = if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) |
15 | 14 | mpteq2dv 5250 |
. . . . . 6
ā¢ (š = š¹ ā (š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0)) = (š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) |
16 | 15 | fveq2d 6895 |
. . . . 5
ā¢ (š = š¹ ā (ā«2ā(š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0))) = (ā«2ā(š„ ā ā ā¦
if((š„ ā dom š¹ ā§ 0 ā¤
(āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)))) |
17 | 16 | eleq1d 2818 |
. . . 4
ā¢ (š = š¹ ā ((ā«2ā(š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0))) ā ā ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā)) |
18 | 17 | ralbidv 3177 |
. . 3
ā¢ (š = š¹ ā (āš ā
(0...3)(ā«2ā(š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0))) ā ā ā āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā)) |
19 | | df-ibl 25138 |
. . 3
ā¢
šæ1 = {š ā MblFn ā£ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦
ā¦(āā((šāš„) / (iāš))) / š¦ā¦if((š„ ā dom š ā§ 0 ā¤ š¦), š¦, 0))) ā ā} |
20 | 18, 19 | elrab2 3686 |
. 2
ā¢ (š¹ ā šæ1
ā (š¹ ā MblFn
ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā)) |
21 | | isibl.3 |
. . . . . . . . . . . 12
ā¢ (š ā dom š¹ = š“) |
22 | 21 | eleq2d 2819 |
. . . . . . . . . . 11
ā¢ (š ā (š„ ā dom š¹ ā š„ ā š“)) |
23 | 22 | anbi1d 630 |
. . . . . . . . . 10
ā¢ (š ā ((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))) ā (š„ ā š“ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))))) |
24 | 23 | ifbid 4551 |
. . . . . . . . 9
ā¢ (š ā if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) |
25 | | isibl.4 |
. . . . . . . . . . . 12
ā¢ ((š ā§ š„ ā š“) ā (š¹āš„) = šµ) |
26 | 25 | fvoveq1d 7430 |
. . . . . . . . . . 11
ā¢ ((š ā§ š„ ā š“) ā (āā((š¹āš„) / (iāš))) = (āā(šµ / (iāš)))) |
27 | | isibl.2 |
. . . . . . . . . . 11
ā¢ ((š ā§ š„ ā š“) ā š = (āā(šµ / (iāš)))) |
28 | 26, 27 | eqtr4d 2775 |
. . . . . . . . . 10
ā¢ ((š ā§ š„ ā š“) ā (āā((š¹āš„) / (iāš))) = š) |
29 | 28 | ibllem 25281 |
. . . . . . . . 9
ā¢ (š ā if((š„ ā š“ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ š), š, 0)) |
30 | 24, 29 | eqtrd 2772 |
. . . . . . . 8
ā¢ (š ā if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0) = if((š„ ā š“ ā§ 0 ā¤ š), š, 0)) |
31 | 30 | mpteq2dv 5250 |
. . . . . . 7
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0))) |
32 | | isibl.1 |
. . . . . . 7
ā¢ (š ā šŗ = (š„ ā ā ā¦ if((š„ ā š“ ā§ 0 ā¤ š), š, 0))) |
33 | 31, 32 | eqtr4d 2775 |
. . . . . 6
ā¢ (š ā (š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0)) = šŗ) |
34 | 33 | fveq2d 6895 |
. . . . 5
ā¢ (š ā
(ā«2ā(š„
ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) = (ā«2āšŗ)) |
35 | 34 | eleq1d 2818 |
. . . 4
ā¢ (š ā
((ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā ā
(ā«2āšŗ)
ā ā)) |
36 | 35 | ralbidv 3177 |
. . 3
ā¢ (š ā (āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā ā āš ā
(0...3)(ā«2āšŗ) ā ā)) |
37 | 36 | anbi2d 629 |
. 2
ā¢ (š ā ((š¹ ā MblFn ā§ āš ā
(0...3)(ā«2ā(š„ ā ā ā¦ if((š„ ā dom š¹ ā§ 0 ā¤ (āā((š¹āš„) / (iāš)))), (āā((š¹āš„) / (iāš))), 0))) ā ā) ā (š¹ ā MblFn ā§
āš ā
(0...3)(ā«2āšŗ) ā ā))) |
38 | 20, 37 | bitrid 282 |
1
ā¢ (š ā (š¹ ā šæ1 ā (š¹ ā MblFn ā§
āš ā
(0...3)(ā«2āšŗ) ā ā))) |