Step | Hyp | Ref
| Expression |
1 | | oveq2 7410 |
. . . 4
โข (๐ = ๐ โ (0...๐) = (0...๐)) |
2 | 1 | eleq2d 2811 |
. . 3
โข (๐ = ๐ โ (๐ โ (0...๐) โ ๐ โ (0...๐))) |
3 | | fveq2 6882 |
. . . 4
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
4 | | fvoveq1 7425 |
. . . . 5
โข (๐ = ๐ โ (!โ(๐ โ ๐)) = (!โ(๐ โ ๐))) |
5 | 4 | oveq1d 7417 |
. . . 4
โข (๐ = ๐ โ ((!โ(๐ โ ๐)) ยท (!โ๐)) = ((!โ(๐ โ ๐)) ยท (!โ๐))) |
6 | 3, 5 | oveq12d 7420 |
. . 3
โข (๐ = ๐ โ ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))) = ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐)))) |
7 | 2, 6 | ifbieq1d 4545 |
. 2
โข (๐ = ๐ โ if(๐ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))), 0) = if(๐ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))), 0)) |
8 | | eleq1 2813 |
. . 3
โข (๐ = ๐พ โ (๐ โ (0...๐) โ ๐พ โ (0...๐))) |
9 | | oveq2 7410 |
. . . . . 6
โข (๐ = ๐พ โ (๐ โ ๐) = (๐ โ ๐พ)) |
10 | 9 | fveq2d 6886 |
. . . . 5
โข (๐ = ๐พ โ (!โ(๐ โ ๐)) = (!โ(๐ โ ๐พ))) |
11 | | fveq2 6882 |
. . . . 5
โข (๐ = ๐พ โ (!โ๐) = (!โ๐พ)) |
12 | 10, 11 | oveq12d 7420 |
. . . 4
โข (๐ = ๐พ โ ((!โ(๐ โ ๐)) ยท (!โ๐)) = ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) |
13 | 12 | oveq2d 7418 |
. . 3
โข (๐ = ๐พ โ ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) |
14 | 8, 13 | ifbieq1d 4545 |
. 2
โข (๐ = ๐พ โ if(๐ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))), 0) = if(๐พ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))), 0)) |
15 | | df-bc 14264 |
. 2
โข C =
(๐ โ
โ0, ๐
โ โค โฆ if(๐
โ (0...๐),
((!โ๐) /
((!โ(๐ โ ๐)) ยท (!โ๐))), 0)) |
16 | | ovex 7435 |
. . 3
โข
((!โ๐) /
((!โ(๐ โ ๐พ)) ยท (!โ๐พ))) โ V |
17 | | c0ex 11207 |
. . 3
โข 0 โ
V |
18 | 16, 17 | ifex 4571 |
. 2
โข if(๐พ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))), 0) โ V |
19 | 7, 14, 15, 18 | ovmpo 7561 |
1
โข ((๐ โ โ0
โง ๐พ โ โค)
โ (๐C๐พ) = if(๐พ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))), 0)) |