Step | Hyp | Ref
| Expression |
1 | | elfzelz 13448 |
. . . 4
โข (๐ โ (0...3) โ ๐ โ
โค) |
2 | | iffalse 4500 |
. . . . . . . . . . . . . 14
โข (ยฌ
๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = 0) |
3 | 2 | ad2antll 728 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โค) โง (๐ฅ โ ๐ต โง ยฌ ๐ฅ โ ๐ด)) โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = 0) |
4 | | eldif 3925 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ (๐ต โ ๐ด) โ (๐ฅ โ ๐ต โง ยฌ ๐ฅ โ ๐ด)) |
5 | | itgss.2 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ (๐ต โ ๐ด)) โ ๐ถ = 0) |
6 | 5 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ (๐ต โ ๐ด)) โ ๐ถ = 0) |
7 | 6 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ (๐ต โ ๐ด)) โ (๐ถ / (iโ๐)) = (0 / (iโ๐))) |
8 | | ax-icn 11117 |
. . . . . . . . . . . . . . . . . . . . . 22
โข i โ
โ |
9 | | ine0 11597 |
. . . . . . . . . . . . . . . . . . . . . 22
โข i โ
0 |
10 | | expclz 13997 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ
โ) |
11 | 8, 9, 10 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โค โ
(iโ๐) โ
โ) |
12 | | expne0i 14007 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((i
โ โ โง i โ 0 โง ๐ โ โค) โ (iโ๐) โ 0) |
13 | 8, 9, 12 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โค โ
(iโ๐) โ
0) |
14 | 11, 13 | div0d 11937 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โค โ (0 /
(iโ๐)) =
0) |
15 | 14 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ (๐ต โ ๐ด)) โ (0 / (iโ๐)) = 0) |
16 | 7, 15 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ (๐ต โ ๐ด)) โ (๐ถ / (iโ๐)) = 0) |
17 | 16 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ (๐ต โ ๐ด)) โ (โโ(๐ถ / (iโ๐))) = (โโ0)) |
18 | | re0 15044 |
. . . . . . . . . . . . . . . . 17
โข
(โโ0) = 0 |
19 | 17, 18 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ (๐ต โ ๐ด)) โ (โโ(๐ถ / (iโ๐))) = 0) |
20 | 19 | ifeq1d 4510 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ (๐ต โ ๐ด)) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) = if(0 โค (โโ(๐ถ / (iโ๐))), 0, 0)) |
21 | | ifid 4531 |
. . . . . . . . . . . . . . 15
โข if(0 โค
(โโ(๐ถ /
(iโ๐))), 0, 0) =
0 |
22 | 20, 21 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ (๐ต โ ๐ด)) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) = 0) |
23 | 4, 22 | sylan2br 596 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ โค) โง (๐ฅ โ ๐ต โง ยฌ ๐ฅ โ ๐ด)) โ if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0) = 0) |
24 | 3, 23 | eqtr4d 2780 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ โค) โง (๐ฅ โ ๐ต โง ยฌ ๐ฅ โ ๐ด)) โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0)) |
25 | 24 | expr 458 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ ๐ต) โ (ยฌ ๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0))) |
26 | | iftrue 4497 |
. . . . . . . . . . 11
โข (๐ฅ โ ๐ด โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0)) |
27 | 25, 26 | pm2.61d2 181 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ ๐ต) โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0)) |
28 | | iftrue 4497 |
. . . . . . . . . . 11
โข (๐ฅ โ ๐ต โ if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0)) |
29 | 28 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ ๐ต) โ if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0)) |
30 | 27, 29 | eqtr4d 2780 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โค) โง ๐ฅ โ ๐ต) โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0)) |
31 | | itgss.1 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ด โ ๐ต) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ โค) โ ๐ด โ ๐ต) |
33 | 32 | sseld 3948 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โค) โ (๐ฅ โ ๐ด โ ๐ฅ โ ๐ต)) |
34 | 33 | con3dimp 410 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ โค) โง ยฌ ๐ฅ โ ๐ต) โ ยฌ ๐ฅ โ ๐ด) |
35 | 34, 2 | syl 17 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โค) โง ยฌ ๐ฅ โ ๐ต) โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = 0) |
36 | | iffalse 4500 |
. . . . . . . . . . 11
โข (ยฌ
๐ฅ โ ๐ต โ if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = 0) |
37 | 36 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โค) โง ยฌ ๐ฅ โ ๐ต) โ if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = 0) |
38 | 35, 37 | eqtr4d 2780 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โค) โง ยฌ ๐ฅ โ ๐ต) โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0)) |
39 | 30, 38 | pm2.61dan 812 |
. . . . . . . 8
โข ((๐ โง ๐ โ โค) โ if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) = if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0)) |
40 | | ifan 4544 |
. . . . . . . 8
โข if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if(๐ฅ โ ๐ด, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) |
41 | | ifan 4544 |
. . . . . . . 8
โข if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if(๐ฅ โ ๐ต, if(0 โค (โโ(๐ถ / (iโ๐))), (โโ(๐ถ / (iโ๐))), 0), 0) |
42 | 39, 40, 41 | 3eqtr4g 2802 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0) = if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) |
43 | 42 | mpteq2dv 5212 |
. . . . . 6
โข ((๐ โง ๐ โ โค) โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) |
44 | 43 | fveq2d 6851 |
. . . . 5
โข ((๐ โง ๐ โ โค) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))) = (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
45 | 44 | oveq2d 7378 |
. . . 4
โข ((๐ โง ๐ โ โค) โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) = ((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0))))) |
46 | 1, 45 | sylan2 594 |
. . 3
โข ((๐ โง ๐ โ (0...3)) โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0)))) = ((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0))))) |
47 | 46 | sumeq2dv 15595 |
. 2
โข (๐ โ ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))), 0)))) =
ฮฃ๐ โ
(0...3)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ต โง 0 โค (โโ(๐ถ / (iโ๐)))), (โโ(๐ถ / (iโ๐))), 0))))) |
48 | | eqid 2737 |
. . 3
โข
(โโ(๐ถ /
(iโ๐))) =
(โโ(๐ถ /
(iโ๐))) |
49 | 48 | dfitg 25150 |
. 2
โข
โซ๐ด๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
50 | 48 | dfitg 25150 |
. 2
โข
โซ๐ต๐ถ d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ต โง 0 โค
(โโ(๐ถ /
(iโ๐)))),
(โโ(๐ถ /
(iโ๐))),
0)))) |
51 | 47, 49, 50 | 3eqtr4g 2802 |
1
โข (๐ โ โซ๐ด๐ถ d๐ฅ = โซ๐ต๐ถ d๐ฅ) |