Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . 4
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
2 | 1 | eleq2d 2820 |
. . 3
โข (๐ = ๐ โ (๐ โ (0...๐) โ ๐ โ (0...๐))) |
3 | | fveq2 6843 |
. . . 4
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
4 | | fvoveq1 7381 |
. . . . 5
โข (๐ = ๐ โ (!โ(๐ โ ๐)) = (!โ(๐ โ ๐))) |
5 | 4 | oveq1d 7373 |
. . . 4
โข (๐ = ๐ โ ((!โ(๐ โ ๐)) ยท (!โ๐)) = ((!โ(๐ โ ๐)) ยท (!โ๐))) |
6 | 3, 5 | oveq12d 7376 |
. . 3
โข (๐ = ๐ โ ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))) = ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
7 | 2, 6 | ifbieq1d 4511 |
. 2
โข (๐ = ๐ โ if(๐ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))), 0) = if(๐ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))), 0)) |
8 | | eleq1 2822 |
. . 3
โข (๐ = ๐พ โ (๐ โ (0...๐) โ ๐พ โ (0...๐))) |
9 | | oveq2 7366 |
. . . . . 6
โข (๐ = ๐พ โ (๐ โ ๐) = (๐ โ ๐พ)) |
10 | 9 | fveq2d 6847 |
. . . . 5
โข (๐ = ๐พ โ (!โ(๐ โ ๐)) = (!โ(๐ โ ๐พ))) |
11 | | fveq2 6843 |
. . . . 5
โข (๐ = ๐พ โ (!โ๐) = (!โ๐พ)) |
12 | 10, 11 | oveq12d 7376 |
. . . 4
โข (๐ = ๐พ โ ((!โ(๐ โ ๐)) ยท (!โ๐)) = ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) |
13 | 12 | oveq2d 7374 |
. . 3
โข (๐ = ๐พ โ ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
14 | 8, 13 | ifbieq1d 4511 |
. 2
โข (๐ = ๐พ โ if(๐ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))), 0) = if(๐พ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))), 0)) |
15 | | df-bc 14209 |
. 2
โข C =
(๐ โ
โ0, ๐
โ โค โฆ if(๐
โ (0...๐),
((!โ๐) /
((!โ(๐ โ ๐)) ยท (!โ๐))), 0)) |
16 | | ovex 7391 |
. . 3
โข
((!โ๐) /
((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) โ V |
17 | | c0ex 11154 |
. . 3
โข 0 โ
V |
18 | 16, 17 | ifex 4537 |
. 2
โข if(๐พ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))), 0) โ V |
19 | 7, 14, 15, 18 | ovmpo 7516 |
1
โข ((๐ โ โ0
โง ๐พ โ โค)
โ (๐C๐พ) = if(๐พ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))), 0)) |