Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ ๐ฆ = ๐) |
2 | 1 | eqeq1d 2735 |
. . 3
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ (๐ฆ = 0 โ ๐ = 0)) |
3 | 1 | breq2d 5121 |
. . . 4
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ (0 < ๐ฆ โ 0 < ๐)) |
4 | | simpl 484 |
. . . . . . . 8
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ ๐ฅ = ๐ด) |
5 | 4 | sneqd 4602 |
. . . . . . 7
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ {๐ฅ} = {๐ด}) |
6 | 5 | xpeq2d 5667 |
. . . . . 6
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ (โ ร {๐ฅ}) = (โ ร {๐ด})) |
7 | 6 | seqeq3d 13923 |
. . . . 5
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ seq1( ยท , (โ ร
{๐ฅ})) = seq1( ยท ,
(โ ร {๐ด}))) |
8 | 7, 1 | fveq12d 6853 |
. . . 4
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ (seq1( ยท , (โ ร
{๐ฅ}))โ๐ฆ) = (seq1( ยท , (โ
ร {๐ด}))โ๐)) |
9 | 1 | negeqd 11403 |
. . . . . 6
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ -๐ฆ = -๐) |
10 | 7, 9 | fveq12d 6853 |
. . . . 5
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ (seq1( ยท , (โ ร
{๐ฅ}))โ-๐ฆ) = (seq1( ยท , (โ
ร {๐ด}))โ-๐)) |
11 | 10 | oveq2d 7377 |
. . . 4
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ (1 / (seq1( ยท , (โ
ร {๐ฅ}))โ-๐ฆ)) = (1 / (seq1( ยท ,
(โ ร {๐ด}))โ-๐))) |
12 | 3, 8, 11 | ifbieq12d 4518 |
. . 3
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ if(0 < ๐ฆ, (seq1( ยท , (โ ร {๐ฅ}))โ๐ฆ), (1 / (seq1( ยท , (โ ร
{๐ฅ}))โ-๐ฆ))) = if(0 < ๐, (seq1( ยท , (โ
ร {๐ด}))โ๐), (1 / (seq1( ยท ,
(โ ร {๐ด}))โ-๐)))) |
13 | 2, 12 | ifbieq2d 4516 |
. 2
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐) โ if(๐ฆ = 0, 1, if(0 < ๐ฆ, (seq1( ยท , (โ ร {๐ฅ}))โ๐ฆ), (1 / (seq1( ยท , (โ ร
{๐ฅ}))โ-๐ฆ)))) = if(๐ = 0, 1, if(0 < ๐, (seq1( ยท , (โ ร {๐ด}))โ๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ-๐))))) |
14 | | df-exp 13977 |
. 2
โข โ =
(๐ฅ โ โ, ๐ฆ โ โค โฆ if(๐ฆ = 0, 1, if(0 < ๐ฆ, (seq1( ยท , (โ
ร {๐ฅ}))โ๐ฆ), (1 / (seq1( ยท ,
(โ ร {๐ฅ}))โ-๐ฆ))))) |
15 | | 1ex 11159 |
. . 3
โข 1 โ
V |
16 | | fvex 6859 |
. . . 4
โข (seq1(
ยท , (โ ร {๐ด}))โ๐) โ V |
17 | | ovex 7394 |
. . . 4
โข (1 /
(seq1( ยท , (โ ร {๐ด}))โ-๐)) โ V |
18 | 16, 17 | ifex 4540 |
. . 3
โข if(0 <
๐, (seq1( ยท ,
(โ ร {๐ด}))โ๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ-๐))) โ V |
19 | 15, 18 | ifex 4540 |
. 2
โข if(๐ = 0, 1, if(0 < ๐, (seq1( ยท , (โ
ร {๐ด}))โ๐), (1 / (seq1( ยท ,
(โ ร {๐ด}))โ-๐)))) โ V |
20 | 13, 14, 19 | ovmpoa 7514 |
1
โข ((๐ด โ โ โง ๐ โ โค) โ (๐ดโ๐) = if(๐ = 0, 1, if(0 < ๐, (seq1( ยท , (โ ร {๐ด}))โ๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ-๐))))) |