Step | Hyp | Ref
| Expression |
1 | | mbfi1fseq.1 |
. 2
โข (๐ โ ๐น โ MblFn) |
2 | | mbfi1fseq.2 |
. 2
โข (๐ โ ๐น:โโถ(0[,)+โ)) |
3 | | oveq2 7311 |
. . . . . 6
โข (๐ = ๐ โ (2โ๐) = (2โ๐)) |
4 | 3 | oveq2d 7319 |
. . . . 5
โข (๐ = ๐ โ ((๐นโ๐ง) ยท (2โ๐)) = ((๐นโ๐ง) ยท (2โ๐))) |
5 | 4 | fveq2d 6804 |
. . . 4
โข (๐ = ๐ โ (โโ((๐นโ๐ง) ยท (2โ๐))) = (โโ((๐นโ๐ง) ยท (2โ๐)))) |
6 | 5, 3 | oveq12d 7321 |
. . 3
โข (๐ = ๐ โ ((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)) = ((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐))) |
7 | | fveq2 6800 |
. . . . 5
โข (๐ง = ๐ฆ โ (๐นโ๐ง) = (๐นโ๐ฆ)) |
8 | 7 | fvoveq1d 7325 |
. . . 4
โข (๐ง = ๐ฆ โ (โโ((๐นโ๐ง) ยท (2โ๐))) = (โโ((๐นโ๐ฆ) ยท (2โ๐)))) |
9 | 8 | oveq1d 7318 |
. . 3
โข (๐ง = ๐ฆ โ ((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)) = ((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐))) |
10 | 6, 9 | cbvmpov 7398 |
. 2
โข (๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐))) = (๐ โ โ, ๐ฆ โ โ โฆ
((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐))) |
11 | | eleq1w 2819 |
. . . . . 6
โข (๐ฆ = ๐ฅ โ (๐ฆ โ (-๐[,]๐) โ ๐ฅ โ (-๐[,]๐))) |
12 | | oveq2 7311 |
. . . . . . . 8
โข (๐ฆ = ๐ฅ โ (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ) = (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ)) |
13 | 12 | breq1d 5091 |
. . . . . . 7
โข (๐ฆ = ๐ฅ โ ((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ) โค ๐ โ (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐)) |
14 | 13, 12 | ifbieq1d 4489 |
. . . . . 6
โข (๐ฆ = ๐ฅ โ if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ), ๐) = if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐)) |
15 | 11, 14 | ifbieq1d 4489 |
. . . . 5
โข (๐ฆ = ๐ฅ โ if(๐ฆ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ), ๐), 0) = if(๐ฅ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐), 0)) |
16 | 15 | cbvmptv 5194 |
. . . 4
โข (๐ฆ โ โ โฆ if(๐ฆ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ), ๐), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐), 0)) |
17 | | negeq 11255 |
. . . . . . . 8
โข (๐ = ๐ โ -๐ = -๐) |
18 | | id 22 |
. . . . . . . 8
โข (๐ = ๐ โ ๐ = ๐) |
19 | 17, 18 | oveq12d 7321 |
. . . . . . 7
โข (๐ = ๐ โ (-๐[,]๐) = (-๐[,]๐)) |
20 | 19 | eleq2d 2822 |
. . . . . 6
โข (๐ = ๐ โ (๐ฅ โ (-๐[,]๐) โ ๐ฅ โ (-๐[,]๐))) |
21 | | oveq1 7310 |
. . . . . . . 8
โข (๐ = ๐ โ (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) = (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ)) |
22 | 21, 18 | breq12d 5094 |
. . . . . . 7
โข (๐ = ๐ โ ((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐ โ (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐)) |
23 | 22, 21, 18 | ifbieq12d 4493 |
. . . . . 6
โข (๐ = ๐ โ if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐) = if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐)) |
24 | 20, 23 | ifbieq1d 4489 |
. . . . 5
โข (๐ = ๐ โ if(๐ฅ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐), 0) = if(๐ฅ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐), 0)) |
25 | 24 | mpteq2dv 5183 |
. . . 4
โข (๐ = ๐ โ (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐), 0))) |
26 | 16, 25 | eqtrid 2788 |
. . 3
โข (๐ = ๐ โ (๐ฆ โ โ โฆ if(๐ฆ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ), ๐), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐), 0))) |
27 | 26 | cbvmptv 5194 |
. 2
โข (๐ โ โ โฆ (๐ฆ โ โ โฆ if(๐ฆ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฆ), ๐), 0))) = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ) โค ๐, (๐(๐ โ โ, ๐ง โ โ โฆ
((โโ((๐นโ๐ง) ยท (2โ๐))) / (2โ๐)))๐ฅ), ๐), 0))) |
28 | 1, 2, 10, 27 | mbfi1fseqlem6 24926 |
1
โข (๐ โ โ๐(๐:โโถdom โซ1 โง
โ๐ โ โ
(0๐ โr โค (๐โ๐) โง (๐โ๐) โr โค (๐โ(๐ + 1))) โง โ๐ฅ โ โ (๐ โ โ โฆ ((๐โ๐)โ๐ฅ)) โ (๐นโ๐ฅ))) |