Step | Hyp | Ref
| Expression |
1 | | knoppndvlem6.w |
. . . 4
โข ๐ = (๐ค โ โ โฆ ฮฃ๐ โ โ0
((๐นโ๐ค)โ๐)) |
2 | | fveq2 6890 |
. . . . . 6
โข (๐ค = ๐ด โ (๐นโ๐ค) = (๐นโ๐ด)) |
3 | 2 | fveq1d 6892 |
. . . . 5
โข (๐ค = ๐ด โ ((๐นโ๐ค)โ๐) = ((๐นโ๐ด)โ๐)) |
4 | 3 | sumeq2sdv 15654 |
. . . 4
โข (๐ค = ๐ด โ ฮฃ๐ โ โ0 ((๐นโ๐ค)โ๐) = ฮฃ๐ โ โ0 ((๐นโ๐ด)โ๐)) |
5 | | knoppndvlem6.a |
. . . . . 6
โข ๐ด = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐) |
6 | 5 | a1i 11 |
. . . . 5
โข (๐ โ ๐ด = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) |
7 | | knoppndvlem6.n |
. . . . . 6
โข (๐ โ ๐ โ โ) |
8 | | knoppndvlem6.j |
. . . . . . 7
โข (๐ โ ๐ฝ โ
โ0) |
9 | 8 | nn0zd 12588 |
. . . . . 6
โข (๐ โ ๐ฝ โ โค) |
10 | | knoppndvlem6.m |
. . . . . 6
โข (๐ โ ๐ โ โค) |
11 | 7, 9, 10 | knoppndvlem1 35691 |
. . . . 5
โข (๐ โ ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐) โ โ) |
12 | 6, 11 | eqeltrd 2831 |
. . . 4
โข (๐ โ ๐ด โ โ) |
13 | | sumex 15638 |
. . . . 5
โข
ฮฃ๐ โ
โ0 ((๐นโ๐ด)โ๐) โ V |
14 | 13 | a1i 11 |
. . . 4
โข (๐ โ ฮฃ๐ โ โ0 ((๐นโ๐ด)โ๐) โ V) |
15 | 1, 4, 12, 14 | fvmptd3 7020 |
. . 3
โข (๐ โ (๐โ๐ด) = ฮฃ๐ โ โ0 ((๐นโ๐ด)โ๐)) |
16 | | nn0uz 12868 |
. . . 4
โข
โ0 = (โคโฅโ0) |
17 | | eqid 2730 |
. . . 4
โข
(โคโฅโ(๐ฝ + 1)) =
(โคโฅโ(๐ฝ + 1)) |
18 | | peano2nn0 12516 |
. . . . 5
โข (๐ฝ โ โ0
โ (๐ฝ + 1) โ
โ0) |
19 | 8, 18 | syl 17 |
. . . 4
โข (๐ โ (๐ฝ + 1) โ
โ0) |
20 | | eqidd 2731 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ((๐นโ๐ด)โ๐) = ((๐นโ๐ด)โ๐)) |
21 | | knoppndvlem6.t |
. . . . . 6
โข ๐ = (๐ฅ โ โ โฆ
(absโ((โโ(๐ฅ + (1 / 2))) โ ๐ฅ))) |
22 | | knoppndvlem6.f |
. . . . . 6
โข ๐น = (๐ฆ โ โ โฆ (๐ โ โ0 โฆ ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ฆ))))) |
23 | 7 | adantr 479 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ) |
24 | | knoppndvlem6.c |
. . . . . . . . 9
โข (๐ โ ๐ถ โ (-1(,)1)) |
25 | 24 | knoppndvlem3 35693 |
. . . . . . . 8
โข (๐ โ (๐ถ โ โ โง (absโ๐ถ) < 1)) |
26 | 25 | simpld 493 |
. . . . . . 7
โข (๐ โ ๐ถ โ โ) |
27 | 26 | adantr 479 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ๐ถ โ
โ) |
28 | 12 | adantr 479 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ๐ด โ
โ) |
29 | | simpr 483 |
. . . . . 6
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ0) |
30 | 21, 22, 23, 27, 28, 29 | knoppcnlem3 35674 |
. . . . 5
โข ((๐ โง ๐ โ โ0) โ ((๐นโ๐ด)โ๐) โ โ) |
31 | 30 | recnd 11246 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ((๐นโ๐ด)โ๐) โ โ) |
32 | 21, 22, 1, 12, 24, 7 | knoppndvlem4 35694 |
. . . . 5
โข (๐ โ seq0( + , (๐นโ๐ด)) โ (๐โ๐ด)) |
33 | | seqex 13972 |
. . . . . 6
โข seq0( + ,
(๐นโ๐ด)) โ V |
34 | | fvex 6903 |
. . . . . 6
โข (๐โ๐ด) โ V |
35 | 33, 34 | breldm 5907 |
. . . . 5
โข (seq0( +
, (๐นโ๐ด)) โ (๐โ๐ด) โ seq0( + , (๐นโ๐ด)) โ dom โ ) |
36 | 32, 35 | syl 17 |
. . . 4
โข (๐ โ seq0( + , (๐นโ๐ด)) โ dom โ ) |
37 | 16, 17, 19, 20, 31, 36 | isumsplit 15790 |
. . 3
โข (๐ โ ฮฃ๐ โ โ0 ((๐นโ๐ด)โ๐) = (ฮฃ๐ โ (0...((๐ฝ + 1) โ 1))((๐นโ๐ด)โ๐) + ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))((๐นโ๐ด)โ๐))) |
38 | 8 | nn0cnd 12538 |
. . . . . . 7
โข (๐ โ ๐ฝ โ โ) |
39 | | 1cnd 11213 |
. . . . . . 7
โข (๐ โ 1 โ
โ) |
40 | 38, 39 | pncand 11576 |
. . . . . 6
โข (๐ โ ((๐ฝ + 1) โ 1) = ๐ฝ) |
41 | 40 | oveq2d 7427 |
. . . . 5
โข (๐ โ (0...((๐ฝ + 1) โ 1)) = (0...๐ฝ)) |
42 | 41 | sumeq1d 15651 |
. . . 4
โข (๐ โ ฮฃ๐ โ (0...((๐ฝ + 1) โ 1))((๐นโ๐ด)โ๐) = ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐)) |
43 | 42 | oveq1d 7426 |
. . 3
โข (๐ โ (ฮฃ๐ โ (0...((๐ฝ + 1) โ 1))((๐นโ๐ด)โ๐) + ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))((๐นโ๐ด)โ๐)) = (ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐) + ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))((๐นโ๐ด)โ๐))) |
44 | 15, 37, 43 | 3eqtrd 2774 |
. 2
โข (๐ โ (๐โ๐ด) = (ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐) + ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))((๐นโ๐ด)โ๐))) |
45 | 12 | adantr 479 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ๐ด โ โ) |
46 | | eluznn0 12905 |
. . . . . . . . 9
โข (((๐ฝ + 1) โ โ0
โง ๐ โ
(โคโฅโ(๐ฝ + 1))) โ ๐ โ โ0) |
47 | 19, 46 | sylan 578 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ๐ โ
โ0) |
48 | 22, 45, 47 | knoppcnlem1 35672 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ((๐นโ๐ด)โ๐) = ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)))) |
49 | 5 | a1i 11 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ๐ด = ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) |
50 | 49 | oveq2d 7427 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ (((2 ยท
๐)โ๐) ยท ๐ด) = (((2 ยท ๐)โ๐) ยท ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐))) |
51 | 7 | adantr 479 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ๐ โ โ) |
52 | 47 | nn0zd 12588 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ๐ โ
โค) |
53 | 9 | adantr 479 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ๐ฝ โ โค) |
54 | 10 | adantr 479 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ๐ โ โค) |
55 | | eluzle 12839 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ(๐ฝ + 1)) โ (๐ฝ + 1) โค ๐) |
56 | 55 | adantl 480 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ (๐ฝ + 1) โค ๐) |
57 | 53, 52 | jca 510 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ (๐ฝ โ โค โง ๐ โ
โค)) |
58 | | zltp1le 12616 |
. . . . . . . . . . . . 13
โข ((๐ฝ โ โค โง ๐ โ โค) โ (๐ฝ < ๐ โ (๐ฝ + 1) โค ๐)) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ (๐ฝ < ๐ โ (๐ฝ + 1) โค ๐)) |
60 | 56, 59 | mpbird 256 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ๐ฝ < ๐) |
61 | 51, 52, 53, 54, 60 | knoppndvlem2 35692 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ (((2 ยท
๐)โ๐) ยท ((((2 ยท ๐)โ-๐ฝ) / 2) ยท ๐)) โ โค) |
62 | 50, 61 | eqeltrd 2831 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ (((2 ยท
๐)โ๐) ยท ๐ด) โ โค) |
63 | 21, 62 | dnizeq0 35654 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ (๐โ(((2 ยท ๐)โ๐) ยท ๐ด)) = 0) |
64 | 63 | oveq2d 7427 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ((๐ถโ๐) ยท (๐โ(((2 ยท ๐)โ๐) ยท ๐ด))) = ((๐ถโ๐) ยท 0)) |
65 | 26 | recnd 11246 |
. . . . . . . . . 10
โข (๐ โ ๐ถ โ โ) |
66 | 65 | adantr 479 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ๐ถ โ โ) |
67 | 66, 47 | expcld 14115 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ (๐ถโ๐) โ โ) |
68 | 67 | mul01d 11417 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ((๐ถโ๐) ยท 0) = 0) |
69 | 48, 64, 68 | 3eqtrd 2774 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ(๐ฝ + 1))) โ ((๐นโ๐ด)โ๐) = 0) |
70 | 69 | sumeq2dv 15653 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))((๐นโ๐ด)โ๐) = ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))0) |
71 | | ssidd 4004 |
. . . . . . 7
โข (๐ โ
(โคโฅโ(๐ฝ + 1)) โ
(โคโฅโ(๐ฝ + 1))) |
72 | 71 | orcd 869 |
. . . . . 6
โข (๐ โ
((โคโฅโ(๐ฝ + 1)) โ
(โคโฅโ(๐ฝ + 1)) โจ
(โคโฅโ(๐ฝ + 1)) โ Fin)) |
73 | | sumz 15672 |
. . . . . 6
โข
(((โคโฅโ(๐ฝ + 1)) โ
(โคโฅโ(๐ฝ + 1)) โจ
(โคโฅโ(๐ฝ + 1)) โ Fin) โ ฮฃ๐ โ
(โคโฅโ(๐ฝ + 1))0 = 0) |
74 | 72, 73 | syl 17 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))0 = 0) |
75 | 70, 74 | eqtrd 2770 |
. . . 4
โข (๐ โ ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))((๐นโ๐ด)โ๐) = 0) |
76 | 75 | oveq2d 7427 |
. . 3
โข (๐ โ (ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐) + ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))((๐นโ๐ด)โ๐)) = (ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐) + 0)) |
77 | 21, 22, 12, 26, 7 | knoppndvlem5 35695 |
. . . . 5
โข (๐ โ ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐) โ โ) |
78 | 77 | recnd 11246 |
. . . 4
โข (๐ โ ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐) โ โ) |
79 | 78 | addridd 11418 |
. . 3
โข (๐ โ (ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐) + 0) = ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐)) |
80 | 76, 79 | eqtrd 2770 |
. 2
โข (๐ โ (ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐) + ฮฃ๐ โ (โคโฅโ(๐ฝ + 1))((๐นโ๐ด)โ๐)) = ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐)) |
81 | 44, 80 | eqtrd 2770 |
1
โข (๐ โ (๐โ๐ด) = ฮฃ๐ โ (0...๐ฝ)((๐นโ๐ด)โ๐)) |