Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . . 5
โข (๐ = if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) โ (๐ + (๐พ ยท (absโ๐ท))) = (if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) + (๐พ ยท (absโ๐ท)))) |
2 | 1 | eleq1d 2819 |
. . . 4
โข (๐ = if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) โ ((๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)) โ (if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
3 | 2 | notbid 318 |
. . 3
โข (๐ = if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) โ (ยฌ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)) โ ยฌ
(if(๐ โ
(0...((absโ๐ท) โ
1)), ๐, 0) + (๐พ ยท (absโ๐ท))) โ
(0...((absโ๐ท) โ
1)))) |
4 | 3 | imbi2d 341 |
. 2
โข (๐ = if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) โ ((๐พ โ 0 โ ยฌ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1))) โ (๐พ โ 0 โ ยฌ (if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ
1))))) |
5 | | neeq1 3003 |
. . 3
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ (๐พ โ 0 โ if(๐พ โ โค, ๐พ, 0) โ 0)) |
6 | | oveq1 7365 |
. . . . . 6
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ (๐พ ยท (absโ๐ท)) = (if(๐พ โ โค, ๐พ, 0) ยท (absโ๐ท))) |
7 | 6 | oveq2d 7374 |
. . . . 5
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ (if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) + (๐พ ยท (absโ๐ท))) = (if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) + (if(๐พ โ โค, ๐พ, 0) ยท (absโ๐ท)))) |
8 | 7 | eleq1d 2819 |
. . . 4
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ ((if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)) โ (if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) + (if(๐พ โ โค, ๐พ, 0) ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |
9 | 8 | notbid 318 |
. . 3
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ (ยฌ (if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)) โ ยฌ
(if(๐ โ
(0...((absโ๐ท) โ
1)), ๐, 0) + (if(๐พ โ โค, ๐พ, 0) ยท (absโ๐ท))) โ
(0...((absโ๐ท) โ
1)))) |
10 | 5, 9 | imbi12d 345 |
. 2
โข (๐พ = if(๐พ โ โค, ๐พ, 0) โ ((๐พ โ 0 โ ยฌ (if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1))) โ (if(๐พ โ โค, ๐พ, 0) โ 0 โ ยฌ
(if(๐ โ
(0...((absโ๐ท) โ
1)), ๐, 0) + (if(๐พ โ โค, ๐พ, 0) ยท (absโ๐ท))) โ
(0...((absโ๐ท) โ
1))))) |
11 | | divalglem7.1 |
. . . 4
โข ๐ท โ โค |
12 | | divalglem7.2 |
. . . 4
โข ๐ท โ 0 |
13 | | nnabscl 15216 |
. . . 4
โข ((๐ท โ โค โง ๐ท โ 0) โ (absโ๐ท) โ
โ) |
14 | 11, 12, 13 | mp2an 691 |
. . 3
โข
(absโ๐ท) โ
โ |
15 | | 0z 12515 |
. . . . 5
โข 0 โ
โค |
16 | | 0le0 12259 |
. . . . 5
โข 0 โค
0 |
17 | 14 | nngt0i 12197 |
. . . . 5
โข 0 <
(absโ๐ท) |
18 | 14 | nnzi 12532 |
. . . . . 6
โข
(absโ๐ท) โ
โค |
19 | | elfzm11 13518 |
. . . . . 6
โข ((0
โ โค โง (absโ๐ท) โ โค) โ (0 โ
(0...((absโ๐ท) โ
1)) โ (0 โ โค โง 0 โค 0 โง 0 < (absโ๐ท)))) |
20 | 15, 18, 19 | mp2an 691 |
. . . . 5
โข (0 โ
(0...((absโ๐ท) โ
1)) โ (0 โ โค โง 0 โค 0 โง 0 < (absโ๐ท))) |
21 | 15, 16, 17, 20 | mpbir3an 1342 |
. . . 4
โข 0 โ
(0...((absโ๐ท) โ
1)) |
22 | 21 | elimel 4556 |
. . 3
โข if(๐ โ (0...((absโ๐ท) โ 1)), ๐, 0) โ (0...((absโ๐ท) โ 1)) |
23 | 15 | elimel 4556 |
. . 3
โข if(๐พ โ โค, ๐พ, 0) โ
โค |
24 | 14, 22, 23 | divalglem6 16285 |
. 2
โข (if(๐พ โ โค, ๐พ, 0) โ 0 โ ยฌ
(if(๐ โ
(0...((absโ๐ท) โ
1)), ๐, 0) + (if(๐พ โ โค, ๐พ, 0) ยท (absโ๐ท))) โ
(0...((absโ๐ท) โ
1))) |
25 | 4, 10, 24 | dedth2h 4546 |
1
โข ((๐ โ (0...((absโ๐ท) โ 1)) โง ๐พ โ โค) โ (๐พ โ 0 โ ยฌ (๐ + (๐พ ยท (absโ๐ท))) โ (0...((absโ๐ท) โ 1)))) |