Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
โข
(โโ(๐ต /
(iโ๐))) =
(โโ(๐ต /
(iโ๐))) |
2 | 1 | dfitg 25157 |
. . 3
โข
โซ๐ด๐ต d๐ฅ = ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))),
0)))) |
3 | | nn0uz 12813 |
. . . . 5
โข
โ0 = (โคโฅโ0) |
4 | | df-3 12225 |
. . . . 5
โข 3 = (2 +
1) |
5 | | oveq2 7369 |
. . . . . . 7
โข (๐ = 3 โ (iโ๐) = (iโ3)) |
6 | | i3 14116 |
. . . . . . 7
โข
(iโ3) = -i |
7 | 5, 6 | eqtrdi 2789 |
. . . . . 6
โข (๐ = 3 โ (iโ๐) = -i) |
8 | 6 | itgvallem 25172 |
. . . . . 6
โข (๐ = 3 โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) = (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต / -i))),
(โโ(๐ต / -i)),
0)))) |
9 | 7, 8 | oveq12d 7379 |
. . . . 5
โข (๐ = 3 โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)))) = (-i ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -i))), (โโ(๐ต / -i)), 0))))) |
10 | | ax-icn 11118 |
. . . . . . . 8
โข i โ
โ |
11 | 10 | a1i 11 |
. . . . . . 7
โข (๐ โ i โ
โ) |
12 | | expcl 13994 |
. . . . . . 7
โข ((i
โ โ โง ๐
โ โ0) โ (iโ๐) โ โ) |
13 | 11, 12 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(iโ๐) โ
โ) |
14 | | nn0z 12532 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โค) |
15 | | eqidd 2734 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) |
16 | | eqidd 2734 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(๐ต / (iโ๐))) = (โโ(๐ต / (iโ๐)))) |
17 | | itgcnlem.i |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ
๐ฟ1) |
18 | | itgcnlem.v |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ ๐) |
19 | 15, 16, 17, 18 | iblitg 25156 |
. . . . . . . 8
โข ((๐ โง ๐ โ โค) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) โ โ) |
20 | 19 | recnd 11191 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) โ โ) |
21 | 14, 20 | sylan2 594 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) โ โ) |
22 | 13, 21 | mulcld 11183 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ
((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)))) โ โ) |
23 | | df-2 12224 |
. . . . . 6
โข 2 = (1 +
1) |
24 | | oveq2 7369 |
. . . . . . . 8
โข (๐ = 2 โ (iโ๐) = (iโ2)) |
25 | | i2 14115 |
. . . . . . . 8
โข
(iโ2) = -1 |
26 | 24, 25 | eqtrdi 2789 |
. . . . . . 7
โข (๐ = 2 โ (iโ๐) = -1) |
27 | 25 | itgvallem 25172 |
. . . . . . 7
โข (๐ = 2 โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) = (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต / -1))),
(โโ(๐ต / -1)),
0)))) |
28 | 26, 27 | oveq12d 7379 |
. . . . . 6
โข (๐ = 2 โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)))) = (-1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -1))), (โโ(๐ต / -1)), 0))))) |
29 | | 1e0p1 12668 |
. . . . . . 7
โข 1 = (0 +
1) |
30 | | oveq2 7369 |
. . . . . . . . 9
โข (๐ = 1 โ (iโ๐) = (iโ1)) |
31 | | exp1 13982 |
. . . . . . . . . 10
โข (i โ
โ โ (iโ1) = i) |
32 | 10, 31 | ax-mp 5 |
. . . . . . . . 9
โข
(iโ1) = i |
33 | 30, 32 | eqtrdi 2789 |
. . . . . . . 8
โข (๐ = 1 โ (iโ๐) = i) |
34 | 32 | itgvallem 25172 |
. . . . . . . 8
โข (๐ = 1 โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) = (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต / i))),
(โโ(๐ต / i)),
0)))) |
35 | 33, 34 | oveq12d 7379 |
. . . . . . 7
โข (๐ = 1 โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)))) = (i ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / i))), (โโ(๐ต / i)), 0))))) |
36 | | 0z 12518 |
. . . . . . . . . 10
โข 0 โ
โค |
37 | | itgcnlem.r |
. . . . . . . . . . . . . 14
โข ๐
=
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) |
38 | | iblmbf 25155 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
39 | 17, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (๐ฅ โ ๐ด โฆ ๐ต) โ MblFn) |
40 | 39, 18 | mbfmptcl 25023 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ ๐ด) โ ๐ต โ โ) |
41 | 40 | div1d 11931 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ ๐ด) โ (๐ต / 1) = ๐ต) |
42 | 41 | fveq2d 6850 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(๐ต / 1)) = (โโ๐ต)) |
43 | 42 | ibllem 25152 |
. . . . . . . . . . . . . . . 16
โข (๐ โ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0)) |
44 | 43 | mpteq2dv 5211 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0)) = (๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ๐ต)),
(โโ๐ต),
0))) |
45 | 44 | fveq2d 6850 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0)))) |
46 | 37, 45 | eqtr4id 2792 |
. . . . . . . . . . . . 13
โข (๐ โ ๐
= (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต / 1))),
(โโ(๐ต / 1)),
0)))) |
47 | 46 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (๐ โ (1 ยท ๐
) = (1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0))))) |
48 | | itgcnlem.s |
. . . . . . . . . . . . . . . . . 18
โข ๐ =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) |
49 | | itgcnlem.t |
. . . . . . . . . . . . . . . . . 18
โข ๐ =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) |
50 | | itgcnlem.u |
. . . . . . . . . . . . . . . . . 18
โข ๐ =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) |
51 | 37, 48, 49, 50, 18 | iblcnlem 25176 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ ๐ฟ1 โ
((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง (๐
โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ)))) |
52 | 17, 51 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((๐ฅ โ ๐ด โฆ ๐ต) โ MblFn โง (๐
โ โ โง ๐ โ โ) โง (๐ โ โ โง ๐ โ โ))) |
53 | 52 | simp2d 1144 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐
โ โ โง ๐ โ โ)) |
54 | 53 | simpld 496 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐
โ โ) |
55 | 54 | recnd 11191 |
. . . . . . . . . . . . 13
โข (๐ โ ๐
โ โ) |
56 | 55 | mulid2d 11181 |
. . . . . . . . . . . 12
โข (๐ โ (1 ยท ๐
) = ๐
) |
57 | 47, 56 | eqtr3d 2775 |
. . . . . . . . . . 11
โข (๐ โ (1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0)))) = ๐
) |
58 | 57, 55 | eqeltrd 2834 |
. . . . . . . . . 10
โข (๐ โ (1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0)))) โ
โ) |
59 | | oveq2 7369 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ (iโ๐) = (iโ0)) |
60 | | exp0 13980 |
. . . . . . . . . . . . . 14
โข (i โ
โ โ (iโ0) = 1) |
61 | 10, 60 | ax-mp 5 |
. . . . . . . . . . . . 13
โข
(iโ0) = 1 |
62 | 59, 61 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (iโ๐) = 1) |
63 | 61 | itgvallem 25172 |
. . . . . . . . . . . 12
โข (๐ = 0 โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0))) = (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต / 1))),
(โโ(๐ต / 1)),
0)))) |
64 | 62, 63 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ = 0 โ ((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)))) = (1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0))))) |
65 | 64 | fsum1 15640 |
. . . . . . . . . 10
โข ((0
โ โค โง (1 ยท (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0)))) โ โ)
โ ฮฃ๐ โ
(0...0)((iโ๐) ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / (iโ๐)))), (โโ(๐ต / (iโ๐))), 0)))) = (1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0))))) |
66 | 36, 58, 65 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ ฮฃ๐ โ (0...0)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) = (1
ยท (โซ2โ(๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / 1))), (โโ(๐ต / 1)), 0))))) |
67 | 66, 57 | eqtrd 2773 |
. . . . . . . 8
โข (๐ โ ฮฃ๐ โ (0...0)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) = ๐
) |
68 | | 0nn0 12436 |
. . . . . . . 8
โข 0 โ
โ0 |
69 | 67, 68 | jctil 521 |
. . . . . . 7
โข (๐ โ (0 โ
โ0 โง ฮฃ๐ โ (0...0)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) = ๐
)) |
70 | | imval 15001 |
. . . . . . . . . . . . . 14
โข (๐ต โ โ โ
(โโ๐ต) =
(โโ(๐ต /
i))) |
71 | 40, 70 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ๐ต) = (โโ(๐ต / i))) |
72 | 71 | ibllem 25152 |
. . . . . . . . . . . 12
โข (๐ โ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / i))), (โโ(๐ต / i)), 0)) |
73 | 72 | mpteq2dv 5211 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / i))), (โโ(๐ต / i)), 0))) |
74 | 73 | fveq2d 6850 |
. . . . . . . . . 10
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ๐ต)), (โโ๐ต), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / i))), (โโ(๐ต / i)), 0)))) |
75 | 49, 74 | eqtr2id 2786 |
. . . . . . . . 9
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / i))), (โโ(๐ต / i)), 0))) = ๐) |
76 | 75 | oveq2d 7377 |
. . . . . . . 8
โข (๐ โ (i ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / i))), (โโ(๐ต / i)), 0)))) = (i ยท
๐)) |
77 | 76 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ (๐
+ (i ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / i))), (โโ(๐ต / i)), 0))))) = (๐
+ (i ยท ๐))) |
78 | 3, 29, 35, 22, 69, 77 | fsump1i 15662 |
. . . . . 6
โข (๐ โ (1 โ
โ0 โง ฮฃ๐ โ (0...1)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) =
(๐
+ (i ยท ๐)))) |
79 | 40 | renegd 15103 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ-๐ต) = -(โโ๐ต)) |
80 | | ax-1cn 11117 |
. . . . . . . . . . . . . . . . . . . 20
โข 1 โ
โ |
81 | 80 | negnegi 11479 |
. . . . . . . . . . . . . . . . . . 19
โข --1 =
1 |
82 | 81 | oveq2i 7372 |
. . . . . . . . . . . . . . . . . 18
โข (-๐ต / --1) = (-๐ต / 1) |
83 | 40 | negcld 11507 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ฅ โ ๐ด) โ -๐ต โ โ) |
84 | 83 | div1d 11931 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ฅ โ ๐ด) โ (-๐ต / 1) = -๐ต) |
85 | 82, 84 | eqtrid 2785 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ ๐ด) โ (-๐ต / --1) = -๐ต) |
86 | 80 | negcli 11477 |
. . . . . . . . . . . . . . . . . . 19
โข -1 โ
โ |
87 | | neg1ne0 12277 |
. . . . . . . . . . . . . . . . . . 19
โข -1 โ
0 |
88 | | div2neg 11886 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ต โ โ โง -1 โ
โ โง -1 โ 0) โ (-๐ต / --1) = (๐ต / -1)) |
89 | 86, 87, 88 | mp3an23 1454 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต โ โ โ (-๐ต / --1) = (๐ต / -1)) |
90 | 40, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ฅ โ ๐ด) โ (-๐ต / --1) = (๐ต / -1)) |
91 | 85, 90 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ฅ โ ๐ด) โ -๐ต = (๐ต / -1)) |
92 | 91 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ-๐ต) = (โโ(๐ต / -1))) |
93 | 79, 92 | eqtr3d 2775 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ๐ต) = (โโ(๐ต / -1))) |
94 | 93 | ibllem 25152 |
. . . . . . . . . . . . 13
โข (๐ โ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -1))), (โโ(๐ต / -1)), 0)) |
95 | 94 | mpteq2dv 5211 |
. . . . . . . . . . . 12
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -1))), (โโ(๐ต / -1)), 0))) |
96 | 95 | fveq2d 6850 |
. . . . . . . . . . 11
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -1))), (โโ(๐ต / -1)), 0)))) |
97 | 48, 96 | eqtrid 2785 |
. . . . . . . . . 10
โข (๐ โ ๐ = (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต / -1))),
(โโ(๐ต / -1)),
0)))) |
98 | 97 | oveq2d 7377 |
. . . . . . . . 9
โข (๐ โ (-1 ยท ๐) = (-1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -1))), (โโ(๐ต / -1)), 0))))) |
99 | 53 | simprd 497 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
100 | 99 | recnd 11191 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
101 | 100 | mulm1d 11615 |
. . . . . . . . 9
โข (๐ โ (-1 ยท ๐) = -๐) |
102 | 98, 101 | eqtr3d 2775 |
. . . . . . . 8
โข (๐ โ (-1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -1))), (โโ(๐ต / -1)), 0)))) = -๐) |
103 | 102 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ ((๐
+ (i ยท ๐)) + (-1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -1))), (โโ(๐ต / -1)), 0))))) = ((๐
+ (i ยท ๐)) + -๐)) |
104 | 52 | simp3d 1145 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ โ โง ๐ โ โ)) |
105 | 104 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
106 | 105 | recnd 11191 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
107 | | mulcl 11143 |
. . . . . . . . . 10
โข ((i
โ โ โง ๐
โ โ) โ (i ยท ๐) โ โ) |
108 | 10, 106, 107 | sylancr 588 |
. . . . . . . . 9
โข (๐ โ (i ยท ๐) โ
โ) |
109 | 55, 108 | addcld 11182 |
. . . . . . . 8
โข (๐ โ (๐
+ (i ยท ๐)) โ โ) |
110 | 109, 100 | negsubd 11526 |
. . . . . . 7
โข (๐ โ ((๐
+ (i ยท ๐)) + -๐) = ((๐
+ (i ยท ๐)) โ ๐)) |
111 | 55, 108, 100 | addsubd 11541 |
. . . . . . 7
โข (๐ โ ((๐
+ (i ยท ๐)) โ ๐) = ((๐
โ ๐) + (i ยท ๐))) |
112 | 103, 110,
111 | 3eqtrd 2777 |
. . . . . 6
โข (๐ โ ((๐
+ (i ยท ๐)) + (-1 ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -1))), (โโ(๐ต / -1)), 0))))) = ((๐
โ ๐) + (i ยท ๐))) |
113 | 3, 23, 28, 22, 78, 112 | fsump1i 15662 |
. . . . 5
โข (๐ โ (2 โ
โ0 โง ฮฃ๐ โ (0...2)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) =
((๐
โ ๐) + (i ยท ๐)))) |
114 | | imval 15001 |
. . . . . . . . . . . . . 14
โข (-๐ต โ โ โ
(โโ-๐ต) =
(โโ(-๐ต /
i))) |
115 | 83, 114 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ-๐ต) = (โโ(-๐ต / i))) |
116 | 40 | imnegd 15104 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ-๐ต) = -(โโ๐ต)) |
117 | 10 | negnegi 11479 |
. . . . . . . . . . . . . . . . 17
โข --i =
i |
118 | 117 | eqcomi 2742 |
. . . . . . . . . . . . . . . 16
โข i =
--i |
119 | 118 | oveq2i 7372 |
. . . . . . . . . . . . . . 15
โข (-๐ต / i) = (-๐ต / --i) |
120 | 10 | negcli 11477 |
. . . . . . . . . . . . . . . . 17
โข -i โ
โ |
121 | | ine0 11598 |
. . . . . . . . . . . . . . . . . 18
โข i โ
0 |
122 | 10, 121 | negne0i 11484 |
. . . . . . . . . . . . . . . . 17
โข -i โ
0 |
123 | | div2neg 11886 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ โ โง -i โ
โ โง -i โ 0) โ (-๐ต / --i) = (๐ต / -i)) |
124 | 120, 122,
123 | mp3an23 1454 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ โ โ (-๐ต / --i) = (๐ต / -i)) |
125 | 40, 124 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ฅ โ ๐ด) โ (-๐ต / --i) = (๐ต / -i)) |
126 | 119, 125 | eqtrid 2785 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ฅ โ ๐ด) โ (-๐ต / i) = (๐ต / -i)) |
127 | 126 | fveq2d 6850 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ฅ โ ๐ด) โ (โโ(-๐ต / i)) = (โโ(๐ต / -i))) |
128 | 115, 116,
127 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ฅ โ ๐ด) โ -(โโ๐ต) = (โโ(๐ต / -i))) |
129 | 128 | ibllem 25152 |
. . . . . . . . . . 11
โข (๐ โ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0) = if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -i))), (โโ(๐ต / -i)), 0)) |
130 | 129 | mpteq2dv 5211 |
. . . . . . . . . 10
โข (๐ โ (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0)) = (๐ฅ โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -i))), (โโ(๐ต / -i)), 0))) |
131 | 130 | fveq2d 6850 |
. . . . . . . . 9
โข (๐ โ
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค -(โโ๐ต)), -(โโ๐ต), 0))) =
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -i))), (โโ(๐ต / -i)), 0)))) |
132 | 50, 131 | eqtrid 2785 |
. . . . . . . 8
โข (๐ โ ๐ = (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต / -i))),
(โโ(๐ต / -i)),
0)))) |
133 | 132 | oveq2d 7377 |
. . . . . . 7
โข (๐ โ (-i ยท ๐) = (-i ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -i))), (โโ(๐ต / -i)), 0))))) |
134 | 104 | simprd 497 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
135 | 134 | recnd 11191 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
136 | | mulneg12 11601 |
. . . . . . . 8
โข ((i
โ โ โง ๐
โ โ) โ (-i ยท ๐) = (i ยท -๐)) |
137 | 10, 135, 136 | sylancr 588 |
. . . . . . 7
โข (๐ โ (-i ยท ๐) = (i ยท -๐)) |
138 | 133, 137 | eqtr3d 2775 |
. . . . . 6
โข (๐ โ (-i ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -i))), (โโ(๐ต / -i)), 0)))) = (i ยท
-๐)) |
139 | 138 | oveq2d 7377 |
. . . . 5
โข (๐ โ (((๐
โ ๐) + (i ยท ๐)) + (-i ยท
(โซ2โ(๐ฅ
โ โ โฆ if((๐ฅ โ ๐ด โง 0 โค (โโ(๐ต / -i))), (โโ(๐ต / -i)), 0))))) = (((๐
โ ๐) + (i ยท ๐)) + (i ยท -๐))) |
140 | 3, 4, 9, 22, 113, 139 | fsump1i 15662 |
. . . 4
โข (๐ โ (3 โ
โ0 โง ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) =
(((๐
โ ๐) + (i ยท ๐)) + (i ยท -๐)))) |
141 | 140 | simprd 497 |
. . 3
โข (๐ โ ฮฃ๐ โ (0...3)((iโ๐) ยท (โซ2โ(๐ฅ โ โ โฆ
if((๐ฅ โ ๐ด โง 0 โค
(โโ(๐ต /
(iโ๐)))),
(โโ(๐ต /
(iโ๐))), 0)))) =
(((๐
โ ๐) + (i ยท ๐)) + (i ยท -๐))) |
142 | 2, 141 | eqtrid 2785 |
. 2
โข (๐ โ โซ๐ด๐ต d๐ฅ = (((๐
โ ๐) + (i ยท ๐)) + (i ยท -๐))) |
143 | 55, 100 | subcld 11520 |
. . 3
โข (๐ โ (๐
โ ๐) โ โ) |
144 | 135 | negcld 11507 |
. . . 4
โข (๐ โ -๐ โ โ) |
145 | | mulcl 11143 |
. . . 4
โข ((i
โ โ โง -๐
โ โ) โ (i ยท -๐) โ โ) |
146 | 10, 144, 145 | sylancr 588 |
. . 3
โข (๐ โ (i ยท -๐) โ
โ) |
147 | 143, 108,
146 | addassd 11185 |
. 2
โข (๐ โ (((๐
โ ๐) + (i ยท ๐)) + (i ยท -๐)) = ((๐
โ ๐) + ((i ยท ๐) + (i ยท -๐)))) |
148 | 11, 106, 144 | adddid 11187 |
. . . 4
โข (๐ โ (i ยท (๐ + -๐)) = ((i ยท ๐) + (i ยท -๐))) |
149 | 106, 135 | negsubd 11526 |
. . . . 5
โข (๐ โ (๐ + -๐) = (๐ โ ๐)) |
150 | 149 | oveq2d 7377 |
. . . 4
โข (๐ โ (i ยท (๐ + -๐)) = (i ยท (๐ โ ๐))) |
151 | 148, 150 | eqtr3d 2775 |
. . 3
โข (๐ โ ((i ยท ๐) + (i ยท -๐)) = (i ยท (๐ โ ๐))) |
152 | 151 | oveq2d 7377 |
. 2
โข (๐ โ ((๐
โ ๐) + ((i ยท ๐) + (i ยท -๐))) = ((๐
โ ๐) + (i ยท (๐ โ ๐)))) |
153 | 142, 147,
152 | 3eqtrd 2777 |
1
โข (๐ โ โซ๐ด๐ต d๐ฅ = ((๐
โ ๐) + (i ยท (๐ โ ๐)))) |