Step | Hyp | Ref
| Expression |
1 | | rpvmasum.a |
. . . . . . 7
β’ (π β π β β) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β β+) β π β
β) |
3 | | rpvmasum2.g |
. . . . . . 7
β’ πΊ = (DChrβπ) |
4 | | rpvmasum2.d |
. . . . . . 7
β’ π· = (BaseβπΊ) |
5 | 3, 4 | dchrfi 26619 |
. . . . . 6
β’ (π β β β π· β Fin) |
6 | 2, 5 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β β+) β π· β Fin) |
7 | | fzfid 13885 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β π·) β (1...(ββπ₯)) β Fin) |
8 | | rpvmasum.z |
. . . . . . . . . . . . 13
β’ π =
(β€/nβ€βπ) |
9 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
10 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β π β π·) |
11 | 3, 8, 4, 9, 10 | dchrf 26606 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β π:(Baseβπ)βΆβ) |
12 | | rpvmasum2.u |
. . . . . . . . . . . . . . 15
β’ π = (Unitβπ) |
13 | 9, 12 | unitss 20096 |
. . . . . . . . . . . . . 14
β’ π β (Baseβπ) |
14 | | rpvmasum2.b |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π) |
15 | 13, 14 | sselid 3947 |
. . . . . . . . . . . . 13
β’ (π β π΄ β (Baseβπ)) |
16 | 15 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π·) β π΄ β (Baseβπ)) |
17 | 11, 16 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ ((π β§ π β π·) β (πβπ΄) β β) |
18 | 17 | cjcld 15088 |
. . . . . . . . . 10
β’ ((π β§ π β π·) β (ββ(πβπ΄)) β β) |
19 | 18 | adantlr 714 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β π·) β (ββ(πβπ΄)) β β) |
20 | 19 | adantrl 715 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β π·)) β (ββ(πβπ΄)) β β) |
21 | 11 | ad4ant14 751 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β π·) β π:(Baseβπ)βΆβ) |
22 | 1 | nnnn0d 12480 |
. . . . . . . . . . . . . . 15
β’ (π β π β
β0) |
23 | | rpvmasum.l |
. . . . . . . . . . . . . . . 16
β’ πΏ = (β€RHomβπ) |
24 | 8, 9, 23 | znzrhfo 20970 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β πΏ:β€βontoβ(Baseβπ)) |
25 | | fof 6761 |
. . . . . . . . . . . . . . 15
β’ (πΏ:β€βontoβ(Baseβπ) β πΏ:β€βΆ(Baseβπ)) |
26 | 22, 24, 25 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ (π β πΏ:β€βΆ(Baseβπ)) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β πΏ:β€βΆ(Baseβπ)) |
28 | | elfzelz 13448 |
. . . . . . . . . . . . 13
β’ (π β
(1...(ββπ₯))
β π β
β€) |
29 | | ffvelcdm 7037 |
. . . . . . . . . . . . 13
β’ ((πΏ:β€βΆ(Baseβπ) β§ π β β€) β (πΏβπ) β (Baseβπ)) |
30 | 27, 28, 29 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (πΏβπ) β (Baseβπ)) |
31 | 30 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β π·) β (πΏβπ) β (Baseβπ)) |
32 | 21, 31 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β π·) β (πβ(πΏβπ)) β β) |
33 | 32 | anasss 468 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β π·)) β (πβ(πΏβπ)) β β) |
34 | | elfznn 13477 |
. . . . . . . . . . . . . 14
β’ (π β
(1...(ββπ₯))
β π β
β) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
36 | | vmacl 26483 |
. . . . . . . . . . . . 13
β’ (π β β β
(Ξβπ) β
β) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (Ξβπ)
β β) |
38 | 37, 35 | nndivred 12214 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
/ π) β
β) |
39 | 38 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((Ξβπ)
/ π) β
β) |
40 | 39 | adantrr 716 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β π·)) β ((Ξβπ) / π) β β) |
41 | 33, 40 | mulcld 11182 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β π·)) β ((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β β) |
42 | 20, 41 | mulcld 11182 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β π·)) β
((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β β) |
43 | 42 | anass1rs 654 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π β (1...(ββπ₯))) β
((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β β) |
44 | 7, 43 | fsumcl 15625 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β π·) β Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β β) |
45 | | relogcl 25947 |
. . . . . . . . 9
β’ (π₯ β β+
β (logβπ₯) β
β) |
46 | 45 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
47 | 46 | recnd 11190 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
48 | 47 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β π·) β (logβπ₯) β β) |
49 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
50 | | neg1cn 12274 |
. . . . . . . 8
β’ -1 β
β |
51 | | 0cn 11154 |
. . . . . . . 8
β’ 0 β
β |
52 | 50, 51 | ifcli 4538 |
. . . . . . 7
β’ if(π β π, -1, 0) β β |
53 | 49, 52 | ifcli 4538 |
. . . . . 6
β’ if(π = 1 , 1, if(π β π, -1, 0)) β β |
54 | | mulcl 11142 |
. . . . . 6
β’
(((logβπ₯)
β β β§ if(π =
1 , 1,
if(π β π, -1, 0)) β β) β
((logβπ₯) Β·
if(π = 1 , 1, if(π β π, -1, 0))) β β) |
55 | 48, 53, 54 | sylancl 587 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β π·) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))) β β) |
56 | 6, 44, 55 | fsumsub 15680 |
. . . 4
β’ ((π β§ π₯ β β+) β
Ξ£π β π· (Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = (Ξ£π β π· Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β Ξ£π β π· ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) |
57 | 41 | anass1rs 654 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π β (1...(ββπ₯))) β ((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β β) |
58 | 7, 57 | fsumcl 15625 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β π·) β Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β β) |
59 | 19, 58, 55 | subdid 11618 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β π·) β ((ββ(πβπ΄)) Β· (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) = (((ββ(πβπ΄)) Β· Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β ((ββ(πβπ΄)) Β· ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))))) |
60 | 7, 19, 57 | fsummulc2 15676 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β π·) β ((ββ(πβπ΄)) Β· Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π))) = Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
61 | 53 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β π·) β if(π = 1 , 1, if(π β π, -1, 0)) β β) |
62 | 19, 48, 61 | mul12d 11371 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β π·) β ((ββ(πβπ΄)) Β· ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = ((logβπ₯) Β· ((ββ(πβπ΄)) Β· if(π = 1 , 1, if(π β π, -1, 0))))) |
63 | | ovif2 7460 |
. . . . . . . . . 10
β’
((ββ(πβπ΄)) Β· if(π = 1 , 1, if(π β π, -1, 0))) = if(π = 1 , ((ββ(πβπ΄)) Β· 1), ((ββ(πβπ΄)) Β· if(π β π, -1, 0))) |
64 | | fveq1 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = 1 β (πβπ΄) = ( 1 βπ΄)) |
65 | | rpvmasum2.1 |
. . . . . . . . . . . . . . . . 17
β’ 1 =
(0gβπΊ) |
66 | 1 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ π β π·) β π β β) |
67 | 14 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ π β π·) β π΄ β π) |
68 | 3, 8, 65, 12, 66, 67 | dchr1 26621 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ π β π·) β ( 1 βπ΄) = 1) |
69 | 64, 68 | sylan9eqr 2799 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π = 1 ) β (πβπ΄) = 1) |
70 | 69 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π = 1 ) β
(ββ(πβπ΄)) = (ββ1)) |
71 | | 1re 11162 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
72 | | cjre 15031 |
. . . . . . . . . . . . . . 15
β’ (1 β
β β (ββ1) = 1) |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
(ββ1) = 1 |
74 | 70, 73 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π = 1 ) β
(ββ(πβπ΄)) = 1) |
75 | 74 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π = 1 ) β
((ββ(πβπ΄)) Β· 1) = (1 Β·
1)) |
76 | | 1t1e1 12322 |
. . . . . . . . . . . 12
β’ (1
Β· 1) = 1 |
77 | 75, 76 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π = 1 ) β
((ββ(πβπ΄)) Β· 1) = 1) |
78 | | df-ne 2945 |
. . . . . . . . . . . 12
β’ (π β 1 β Β¬ π = 1 ) |
79 | | ovif2 7460 |
. . . . . . . . . . . . 13
β’
((ββ(πβπ΄)) Β· if(π β π, -1, 0)) = if(π β π, ((ββ(πβπ΄)) Β· -1), ((ββ(πβπ΄)) Β· 0)) |
80 | | rpvmasum2.z1 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π) β π΄ = (1rβπ)) |
81 | 80 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π) β (πβπ΄) = (πβ(1rβπ))) |
82 | 81 | ad5ant15 758 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β β+)
β§ π β π·) β§ π β 1 ) β§ π β π) β (πβπ΄) = (πβ(1rβπ))) |
83 | 3, 8, 4 | dchrmhm 26605 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π· β ((mulGrpβπ) MndHom
(mulGrpββfld)) |
84 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β β+) β§ π β π·) β π β π·) |
85 | 83, 84 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β β+) β§ π β π·) β π β ((mulGrpβπ) MndHom
(mulGrpββfld))) |
86 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(mulGrpβπ) =
(mulGrpβπ) |
87 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(1rβπ) = (1rβπ) |
88 | 86, 87 | ringidval 19922 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(1rβπ) = (0gβ(mulGrpβπ)) |
89 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(mulGrpββfld) =
(mulGrpββfld) |
90 | | cnfld1 20838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 1 =
(1rββfld) |
91 | 89, 90 | ringidval 19922 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 1 =
(0gβ(mulGrpββfld)) |
92 | 88, 91 | mhm0 18617 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β ((mulGrpβπ) MndHom
(mulGrpββfld)) β (πβ(1rβπ)) = 1) |
93 | 85, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β β+) β§ π β π·) β (πβ(1rβπ)) = 1) |
94 | 93 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β β+)
β§ π β π·) β§ π β 1 ) β§ π β π) β (πβ(1rβπ)) = 1) |
95 | 82, 94 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β β+)
β§ π β π·) β§ π β 1 ) β§ π β π) β (πβπ΄) = 1) |
96 | 95 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β β+)
β§ π β π·) β§ π β 1 ) β§ π β π) β (ββ(πβπ΄)) = (ββ1)) |
97 | 96, 73 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π₯ β β+)
β§ π β π·) β§ π β 1 ) β§ π β π) β (ββ(πβπ΄)) = 1) |
98 | 97 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β β+)
β§ π β π·) β§ π β 1 ) β§ π β π) β ((ββ(πβπ΄)) Β· -1) = (1 Β·
-1)) |
99 | 50 | mulid2i 11167 |
. . . . . . . . . . . . . . . 16
β’ (1
Β· -1) = -1 |
100 | 98, 99 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β β+)
β§ π β π·) β§ π β 1 ) β§ π β π) β ((ββ(πβπ΄)) Β· -1) = -1) |
101 | 100 | ifeq1da 4522 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π β 1 ) β if(π β π, ((ββ(πβπ΄)) Β· -1), ((ββ(πβπ΄)) Β· 0)) = if(π β π, -1, ((ββ(πβπ΄)) Β· 0))) |
102 | 19 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π β 1 ) β
(ββ(πβπ΄)) β β) |
103 | 102 | mul01d 11361 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π β 1 ) β
((ββ(πβπ΄)) Β· 0) = 0) |
104 | 103 | ifeq2d 4511 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π β 1 ) β if(π β π, -1, ((ββ(πβπ΄)) Β· 0)) = if(π β π, -1, 0)) |
105 | 101, 104 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π β 1 ) β if(π β π, ((ββ(πβπ΄)) Β· -1), ((ββ(πβπ΄)) Β· 0)) = if(π β π, -1, 0)) |
106 | 79, 105 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ π β 1 ) β
((ββ(πβπ΄)) Β· if(π β π, -1, 0)) = if(π β π, -1, 0)) |
107 | 78, 106 | sylan2br 596 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β π·) β§ Β¬ π = 1 ) β
((ββ(πβπ΄)) Β· if(π β π, -1, 0)) = if(π β π, -1, 0)) |
108 | 77, 107 | ifeq12da 4524 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β π·) β if(π = 1 , ((ββ(πβπ΄)) Β· 1), ((ββ(πβπ΄)) Β· if(π β π, -1, 0))) = if(π = 1 , 1, if(π β π, -1, 0))) |
109 | 63, 108 | eqtrid 2789 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β π·) β ((ββ(πβπ΄)) Β· if(π = 1 , 1, if(π β π, -1, 0))) = if(π = 1 , 1, if(π β π, -1, 0))) |
110 | 109 | oveq2d 7378 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β π·) β ((logβπ₯) Β· ((ββ(πβπ΄)) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) |
111 | 62, 110 | eqtrd 2777 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β π·) β ((ββ(πβπ΄)) Β· ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) |
112 | 60, 111 | oveq12d 7380 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β π·) β (((ββ(πβπ΄)) Β· Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β ((ββ(πβπ΄)) Β· ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) = (Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) |
113 | 59, 112 | eqtrd 2777 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β π·) β ((ββ(πβπ΄)) Β· (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) = (Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) |
114 | 113 | sumeq2dv 15595 |
. . . 4
β’ ((π β§ π₯ β β+) β
Ξ£π β π· ((ββ(πβπ΄)) Β· (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) = Ξ£π β π· (Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) |
115 | | fzfid 13885 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
116 | | inss1 4193 |
. . . . . . . . 9
β’
((1...(ββπ₯)) β© π) β (1...(ββπ₯)) |
117 | | ssfi 9124 |
. . . . . . . . 9
β’
(((1...(ββπ₯)) β Fin β§
((1...(ββπ₯))
β© π) β
(1...(ββπ₯)))
β ((1...(ββπ₯)) β© π) β Fin) |
118 | 115, 116,
117 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((1...(ββπ₯))
β© π) β
Fin) |
119 | 2 | phicld 16651 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(Οβπ) β
β) |
120 | 119 | nncnd 12176 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
(Οβπ) β
β) |
121 | 116 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
((1...(ββπ₯))
β© π) β
(1...(ββπ₯))) |
122 | 121 | sselda 3949 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β π β
(1...(ββπ₯))) |
123 | 122, 39 | syldan 592 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β
((Ξβπ) / π) β
β) |
124 | 118, 120,
123 | fsummulc2 15676 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) = Ξ£π β ((1...(ββπ₯)) β© π)((Οβπ) Β· ((Ξβπ) / π))) |
125 | 120 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (Οβπ)
β β) |
126 | 125, 39 | mulcld 11182 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((Οβπ)
Β· ((Ξβπ) / π)) β β) |
127 | 122, 126 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β
((Οβπ) Β·
((Ξβπ) / π)) β
β) |
128 | 127 | ralrimiva 3144 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
βπ β
((1...(ββπ₯))
β© π)((Οβπ) Β· ((Ξβπ) / π)) β β) |
129 | 115 | olcd 873 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((1...(ββπ₯))
β (β€β₯β1) β¨ (1...(ββπ₯)) β Fin)) |
130 | | sumss2 15618 |
. . . . . . . 8
β’
(((((1...(ββπ₯)) β© π) β (1...(ββπ₯)) β§ βπ β
((1...(ββπ₯))
β© π)((Οβπ) Β· ((Ξβπ) / π)) β β) β§
((1...(ββπ₯))
β (β€β₯β1) β¨ (1...(ββπ₯)) β Fin)) β
Ξ£π β
((1...(ββπ₯))
β© π)((Οβπ) Β· ((Ξβπ) / π)) = Ξ£π β (1...(ββπ₯))if(π β ((1...(ββπ₯)) β© π), ((Οβπ) Β· ((Ξβπ) / π)), 0)) |
131 | 121, 128,
129, 130 | syl21anc 837 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)((Οβπ) Β· ((Ξβπ) / π)) = Ξ£π β (1...(ββπ₯))if(π β ((1...(ββπ₯)) β© π), ((Οβπ) Β· ((Ξβπ) / π)), 0)) |
132 | | elin 3931 |
. . . . . . . . . . . . 13
β’ (π β
((1...(ββπ₯))
β© π) β (π β
(1...(ββπ₯))
β§ π β π)) |
133 | 132 | baib 537 |
. . . . . . . . . . . 12
β’ (π β
(1...(ββπ₯))
β (π β
((1...(ββπ₯))
β© π) β π β π)) |
134 | 133 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π β
((1...(ββπ₯))
β© π) β π β π)) |
135 | | rpvmasum2.t |
. . . . . . . . . . . . 13
β’ π = (β‘πΏ β {π΄}) |
136 | 135 | eleq2i 2830 |
. . . . . . . . . . . 12
β’ (π β π β π β (β‘πΏ β {π΄})) |
137 | 27 | ffnd 6674 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β πΏ Fn β€) |
138 | | fniniseg 7015 |
. . . . . . . . . . . . . 14
β’ (πΏ Fn β€ β (π β (β‘πΏ β {π΄}) β (π β β€ β§ (πΏβπ) = π΄))) |
139 | 138 | baibd 541 |
. . . . . . . . . . . . 13
β’ ((πΏ Fn β€ β§ π β β€) β (π β (β‘πΏ β {π΄}) β (πΏβπ) = π΄)) |
140 | 137, 28, 139 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π β (β‘πΏ β {π΄}) β (πΏβπ) = π΄)) |
141 | 136, 140 | bitrid 283 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π β π β (πΏβπ) = π΄)) |
142 | 134, 141 | bitr2d 280 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((πΏβπ) = π΄ β π β ((1...(ββπ₯)) β© π))) |
143 | 39 | mul02d 11360 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (0 Β· ((Ξβπ) / π)) = 0) |
144 | 142, 143 | ifbieq2d 4517 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β if((πΏβπ) = π΄, ((Οβπ) Β· ((Ξβπ) / π)), (0 Β· ((Ξβπ) / π))) = if(π β ((1...(ββπ₯)) β© π), ((Οβπ) Β· ((Ξβπ) / π)), 0)) |
145 | | ovif 7459 |
. . . . . . . . . 10
β’
(if((πΏβπ) = π΄, (Οβπ), 0) Β· ((Ξβπ) / π)) = if((πΏβπ) = π΄, ((Οβπ) Β· ((Ξβπ) / π)), (0 Β· ((Ξβπ) / π))) |
146 | 1 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
147 | 146, 5 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π· β
Fin) |
148 | 18 | ad4ant14 751 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β π·) β (ββ(πβπ΄)) β β) |
149 | 32, 148 | mulcld 11182 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β π·) β ((πβ(πΏβπ)) Β· (ββ(πβπ΄))) β β) |
150 | 147, 39, 149 | fsummulc1 15677 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (Ξ£π β
π· ((πβ(πΏβπ)) Β· (ββ(πβπ΄))) Β· ((Ξβπ) / π)) = Ξ£π β π· (((πβ(πΏβπ)) Β· (ββ(πβπ΄))) Β· ((Ξβπ) / π))) |
151 | 14 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π΄ β π) |
152 | 3, 4, 8, 9, 12, 146, 30, 151 | sum2dchr 26638 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
π· ((πβ(πΏβπ)) Β· (ββ(πβπ΄))) = if((πΏβπ) = π΄, (Οβπ), 0)) |
153 | 152 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (Ξ£π β
π· ((πβ(πΏβπ)) Β· (ββ(πβπ΄))) Β· ((Ξβπ) / π)) = (if((πΏβπ) = π΄, (Οβπ), 0) Β· ((Ξβπ) / π))) |
154 | 39 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β π·) β ((Ξβπ) / π) β β) |
155 | | mulass 11146 |
. . . . . . . . . . . . . 14
β’ (((πβ(πΏβπ)) β β β§
(ββ(πβπ΄)) β β β§
((Ξβπ) / π) β β) β
(((πβ(πΏβπ)) Β· (ββ(πβπ΄))) Β· ((Ξβπ) / π)) = ((πβ(πΏβπ)) Β· ((ββ(πβπ΄)) Β· ((Ξβπ) / π)))) |
156 | | mul12 11327 |
. . . . . . . . . . . . . 14
β’ (((πβ(πΏβπ)) β β β§
(ββ(πβπ΄)) β β β§
((Ξβπ) / π) β β) β ((πβ(πΏβπ)) Β· ((ββ(πβπ΄)) Β· ((Ξβπ) / π))) = ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
157 | 155, 156 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((πβ(πΏβπ)) β β β§
(ββ(πβπ΄)) β β β§
((Ξβπ) / π) β β) β
(((πβ(πΏβπ)) Β· (ββ(πβπ΄))) Β· ((Ξβπ) / π)) = ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
158 | 32, 148, 154, 157 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β π·) β (((πβ(πΏβπ)) Β· (ββ(πβπ΄))) Β· ((Ξβπ) / π)) = ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
159 | 158 | sumeq2dv 15595 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
π· (((πβ(πΏβπ)) Β· (ββ(πβπ΄))) Β· ((Ξβπ) / π)) = Ξ£π β π· ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
160 | 150, 153,
159 | 3eqtr3d 2785 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (if((πΏβπ) = π΄, (Οβπ), 0) Β· ((Ξβπ) / π)) = Ξ£π β π· ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
161 | 145, 160 | eqtr3id 2791 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β if((πΏβπ) = π΄, ((Οβπ) Β· ((Ξβπ) / π)), (0 Β· ((Ξβπ) / π))) = Ξ£π β π· ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
162 | 144, 161 | eqtr3d 2779 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β if(π β
((1...(ββπ₯))
β© π),
((Οβπ) Β·
((Ξβπ) / π)), 0) = Ξ£π β π· ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
163 | 162 | sumeq2dv 15595 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))if(π β ((1...(ββπ₯)) β© π), ((Οβπ) Β· ((Ξβπ) / π)), 0) = Ξ£π β (1...(ββπ₯))Ξ£π β π· ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
164 | 124, 131,
163 | 3eqtrd 2781 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) = Ξ£π β (1...(ββπ₯))Ξ£π β π· ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
165 | 115, 6, 42 | fsumcom 15667 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))Ξ£π β π· ((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) = Ξ£π β π· Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
166 | 164, 165 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π₯ β β+) β
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) = Ξ£π β π· Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π)))) |
167 | 3 | dchrabl 26618 |
. . . . . . . . . 10
β’ (π β β β πΊ β Abel) |
168 | | ablgrp 19574 |
. . . . . . . . . 10
β’ (πΊ β Abel β πΊ β Grp) |
169 | 4, 65 | grpidcl 18785 |
. . . . . . . . . 10
β’ (πΊ β Grp β 1 β π·) |
170 | 2, 167, 168, 169 | 4syl 19 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β 1 β π·) |
171 | 47 | mulid1d 11179 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β· 1)
= (logβπ₯)) |
172 | 171, 47 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β· 1)
β β) |
173 | | iftrue 4497 |
. . . . . . . . . . 11
β’ (π = 1 β if(π = 1 , 1, if(π β π, -1, 0)) = 1) |
174 | 173 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π = 1 β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))) = ((logβπ₯) Β· 1)) |
175 | 174 | sumsn 15638 |
. . . . . . . . 9
β’ (( 1 β π· β§ ((logβπ₯) Β· 1) β β)
β Ξ£π β {
1 }
((logβπ₯) Β·
if(π = 1 , 1, if(π β π, -1, 0))) = ((logβπ₯) Β· 1)) |
176 | 170, 172,
175 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β { 1 }
((logβπ₯) Β·
if(π = 1 , 1, if(π β π, -1, 0))) = ((logβπ₯) Β· 1)) |
177 | | eldifsn 4752 |
. . . . . . . . . . 11
β’ (π β (π· β { 1 }) β (π β π· β§ π β 1 )) |
178 | | ifnefalse 4503 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β if(π = 1 , 1, if(π β π, -1, 0)) = if(π β π, -1, 0)) |
179 | 178 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β π· β§ π β 1 )) β if(π = 1 , 1, if(π β π, -1, 0)) = if(π β π, -1, 0)) |
180 | | negeq 11400 |
. . . . . . . . . . . . . . 15
β’ (if(π β π, 1, 0) = 1 β -if(π β π, 1, 0) = -1) |
181 | | negeq 11400 |
. . . . . . . . . . . . . . . 16
β’ (if(π β π, 1, 0) = 0 β -if(π β π, 1, 0) = -0) |
182 | | neg0 11454 |
. . . . . . . . . . . . . . . 16
β’ -0 =
0 |
183 | 181, 182 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
β’ (if(π β π, 1, 0) = 0 β -if(π β π, 1, 0) = 0) |
184 | 180, 183 | ifsb 4504 |
. . . . . . . . . . . . . 14
β’ -if(π β π, 1, 0) = if(π β π, -1, 0) |
185 | 179, 184 | eqtr4di 2795 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β π· β§ π β 1 )) β if(π = 1 , 1, if(π β π, -1, 0)) = -if(π β π, 1, 0)) |
186 | 185 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β π· β§ π β 1 )) β
((logβπ₯) Β·
if(π = 1 , 1, if(π β π, -1, 0))) = ((logβπ₯) Β· -if(π β π, 1, 0))) |
187 | 47 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β π· β§ π β 1 )) β (logβπ₯) β
β) |
188 | 49, 51 | ifcli 4538 |
. . . . . . . . . . . . 13
β’ if(π β π, 1, 0) β β |
189 | | mulneg2 11599 |
. . . . . . . . . . . . 13
β’
(((logβπ₯)
β β β§ if(π
β π, 1, 0) β
β) β ((logβπ₯) Β· -if(π β π, 1, 0)) = -((logβπ₯) Β· if(π β π, 1, 0))) |
190 | 187, 188,
189 | sylancl 587 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β π· β§ π β 1 )) β
((logβπ₯) Β·
-if(π β π, 1, 0)) = -((logβπ₯) Β· if(π β π, 1, 0))) |
191 | 186, 190 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β π· β§ π β 1 )) β
((logβπ₯) Β·
if(π = 1 , 1, if(π β π, -1, 0))) = -((logβπ₯) Β· if(π β π, 1, 0))) |
192 | 177, 191 | sylan2b 595 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β (π· β { 1 })) β
((logβπ₯) Β·
if(π = 1 , 1, if(π β π, -1, 0))) = -((logβπ₯) Β· if(π β π, 1, 0))) |
193 | 192 | sumeq2dv 15595 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β (π· β { 1 })((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))) = Ξ£π β (π· β { 1 })-((logβπ₯) Β· if(π β π, 1, 0))) |
194 | | diffi 9130 |
. . . . . . . . . . 11
β’ (π· β Fin β (π· β { 1 }) β
Fin) |
195 | 6, 194 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (π· β { 1 }) β
Fin) |
196 | 47 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β (π· β { 1 })) β
(logβπ₯) β
β) |
197 | | mulcl 11142 |
. . . . . . . . . . 11
β’
(((logβπ₯)
β β β§ if(π
β π, 1, 0) β
β) β ((logβπ₯) Β· if(π β π, 1, 0)) β β) |
198 | 196, 188,
197 | sylancl 587 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β (π· β { 1 })) β
((logβπ₯) Β·
if(π β π, 1, 0)) β
β) |
199 | 195, 198 | fsumneg 15679 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β (π· β { 1 })-((logβπ₯) Β· if(π β π, 1, 0)) = -Ξ£π β (π· β { 1 })((logβπ₯) Β· if(π β π, 1, 0))) |
200 | 188 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β (π· β { 1 })) β if(π β π, 1, 0) β β) |
201 | 195, 47, 200 | fsummulc2 15676 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β·
Ξ£π β (π· β { 1 })if(π β π, 1, 0)) = Ξ£π β (π· β { 1 })((logβπ₯) Β· if(π β π, 1, 0))) |
202 | | rpvmasum2.w |
. . . . . . . . . . . . . . . . 17
β’ π = {π¦ β (π· β { 1 }) β£ Ξ£π β β ((π¦β(πΏβπ)) / π) = 0} |
203 | 202 | ssrab3 4045 |
. . . . . . . . . . . . . . . 16
β’ π β (π· β { 1 }) |
204 | | difss 4096 |
. . . . . . . . . . . . . . . 16
β’ (π· β { 1 }) β π· |
205 | 203, 204 | sstri 3958 |
. . . . . . . . . . . . . . 15
β’ π β π· |
206 | | ssfi 9124 |
. . . . . . . . . . . . . . 15
β’ ((π· β Fin β§ π β π·) β π β Fin) |
207 | 6, 205, 206 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β π β Fin) |
208 | | fsumconst 15682 |
. . . . . . . . . . . . . 14
β’ ((π β Fin β§ 1 β
β) β Ξ£π
β π 1 =
((β―βπ) Β·
1)) |
209 | 207, 49, 208 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β
Ξ£π β π 1 = ((β―βπ) Β· 1)) |
210 | 203 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β π β (π· β { 1 })) |
211 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β 1 β
β) |
212 | 211 | ralrimivw 3148 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β
βπ β π 1 β
β) |
213 | 195 | olcd 873 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β ((π· β { 1 }) β
(β€β₯β1) β¨ (π· β { 1 }) β
Fin)) |
214 | | sumss2 15618 |
. . . . . . . . . . . . . 14
β’ (((π β (π· β { 1 }) β§ βπ β π 1 β β) β§ ((π· β { 1 }) β
(β€β₯β1) β¨ (π· β { 1 }) β Fin)) β
Ξ£π β π 1 = Ξ£π β (π· β { 1 })if(π β π, 1, 0)) |
215 | 210, 212,
213, 214 | syl21anc 837 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β
Ξ£π β π 1 = Ξ£π β (π· β { 1 })if(π β π, 1, 0)) |
216 | | hashcl 14263 |
. . . . . . . . . . . . . . . 16
β’ (π β Fin β
(β―βπ) β
β0) |
217 | 207, 216 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β
(β―βπ) β
β0) |
218 | 217 | nn0cnd 12482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β
(β―βπ) β
β) |
219 | 218 | mulid1d 11179 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β
((β―βπ) Β·
1) = (β―βπ)) |
220 | 209, 215,
219 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β
Ξ£π β (π· β { 1 })if(π β π, 1, 0) = (β―βπ)) |
221 | 220 | oveq2d 7378 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β·
Ξ£π β (π· β { 1 })if(π β π, 1, 0)) = ((logβπ₯) Β· (β―βπ))) |
222 | 201, 221 | eqtr3d 2779 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
Ξ£π β (π· β { 1 })((logβπ₯) Β· if(π β π, 1, 0)) = ((logβπ₯) Β· (β―βπ))) |
223 | 222 | negeqd 11402 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
-Ξ£π β (π· β { 1 })((logβπ₯) Β· if(π β π, 1, 0)) = -((logβπ₯) Β· (β―βπ))) |
224 | 193, 199,
223 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β (π· β { 1 })((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))) = -((logβπ₯) Β· (β―βπ))) |
225 | 176, 224 | oveq12d 7380 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(Ξ£π β { 1 }
((logβπ₯) Β·
if(π = 1 , 1, if(π β π, -1, 0))) + Ξ£π β (π· β { 1 })((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = (((logβπ₯) Β· 1) +
-((logβπ₯) Β·
(β―βπ)))) |
226 | 47, 218 | mulcld 11182 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β·
(β―βπ)) β
β) |
227 | 172, 226 | negsubd 11525 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(((logβπ₯) Β· 1)
+ -((logβπ₯) Β·
(β―βπ))) =
(((logβπ₯) Β· 1)
β ((logβπ₯)
Β· (β―βπ)))) |
228 | 225, 227 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(Ξ£π β { 1 }
((logβπ₯) Β·
if(π = 1 , 1, if(π β π, -1, 0))) + Ξ£π β (π· β { 1 })((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = (((logβπ₯) Β· 1) β
((logβπ₯) Β·
(β―βπ)))) |
229 | | disjdif 4436 |
. . . . . . . 8
β’ ({ 1 } β©
(π· β { 1 })) =
β
|
230 | 229 | a1i 11 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β ({ 1 } β©
(π· β { 1 })) =
β
) |
231 | | undif2 4441 |
. . . . . . . 8
β’ ({ 1 } βͺ
(π· β { 1 })) = ({
1 } βͺ
π·) |
232 | 170 | snssd 4774 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β { 1 } β
π·) |
233 | | ssequn1 4145 |
. . . . . . . . 9
β’ ({ 1 } β
π· β ({ 1 } βͺ π·) = π·) |
234 | 232, 233 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β ({ 1 } βͺ π·) = π·) |
235 | 231, 234 | eqtr2id 2790 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β π· = ({ 1 } βͺ (π· β { 1 }))) |
236 | 230, 235,
6, 55 | fsumsplit 15633 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β π· ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))) = (Ξ£π β { 1 } ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))) + Ξ£π β (π· β { 1 })((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) |
237 | 47, 211, 218 | subdid 11618 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β· (1
β (β―βπ)))
= (((logβπ₯) Β·
1) β ((logβπ₯)
Β· (β―βπ)))) |
238 | 228, 236,
237 | 3eqtr4rd 2788 |
. . . . 5
β’ ((π β§ π₯ β β+) β
((logβπ₯) Β· (1
β (β―βπ)))
= Ξ£π β π· ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) |
239 | 166, 238 | oveq12d 7380 |
. . . 4
β’ ((π β§ π₯ β β+) β
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ)))) = (Ξ£π β π· Ξ£π β (1...(ββπ₯))((ββ(πβπ΄)) Β· ((πβ(πΏβπ)) Β· ((Ξβπ) / π))) β Ξ£π β π· ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) |
240 | 56, 114, 239 | 3eqtr4d 2787 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β π· ((ββ(πβπ΄)) Β· (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) = (((Οβπ) Β· Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ))))) |
241 | 240 | mpteq2dva 5210 |
. 2
β’ (π β (π₯ β β+ β¦
Ξ£π β π· ((ββ(πβπ΄)) Β· (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))))) = (π₯ β β+ β¦
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ)))))) |
242 | | rpssre 12929 |
. . . 4
β’
β+ β β |
243 | 242 | a1i 11 |
. . 3
β’ (π β β+
β β) |
244 | 1, 5 | syl 17 |
. . 3
β’ (π β π· β Fin) |
245 | 17 | adantlr 714 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β π·) β (πβπ΄) β β) |
246 | 245 | cjcld 15088 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β π·) β (ββ(πβπ΄)) β β) |
247 | 58, 55 | subcld 11519 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β π·) β (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) β β) |
248 | 246, 247 | mulcld 11182 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β π·) β ((ββ(πβπ΄)) Β· (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) β
β) |
249 | 248 | anasss 468 |
. . 3
β’ ((π β§ (π₯ β β+ β§ π β π·)) β ((ββ(πβπ΄)) Β· (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) β
β) |
250 | 18 | adantr 482 |
. . . 4
β’ (((π β§ π β π·) β§ π₯ β β+) β
(ββ(πβπ΄)) β β) |
251 | 247 | an32s 651 |
. . . 4
β’ (((π β§ π β π·) β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) β β) |
252 | | o1const 15509 |
. . . . 5
β’
((β+ β β β§ (ββ(πβπ΄)) β β) β (π₯ β β+
β¦ (ββ(πβπ΄))) β π(1)) |
253 | 242, 18, 252 | sylancr 588 |
. . . 4
β’ ((π β§ π β π·) β (π₯ β β+ β¦
(ββ(πβπ΄))) β π(1)) |
254 | | fveq1 6846 |
. . . . . . . . . . . 12
β’ (π = 1 β (πβ(πΏβπ)) = ( 1 β(πΏβπ))) |
255 | 254 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π = 1 β ((πβ(πΏβπ)) Β· ((Ξβπ) / π)) = (( 1 β(πΏβπ)) Β· ((Ξβπ) / π))) |
256 | 255 | sumeq2sdv 15596 |
. . . . . . . . . 10
β’ (π = 1 β Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) = Ξ£π β (1...(ββπ₯))(( 1 β(πΏβπ)) Β· ((Ξβπ) / π))) |
257 | 256, 174 | oveq12d 7380 |
. . . . . . . . 9
β’ (π = 1 β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = (Ξ£π β (1...(ββπ₯))(( 1 β(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· 1))) |
258 | 257 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π = 1 ) β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = (Ξ£π β (1...(ββπ₯))(( 1 β(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· 1))) |
259 | 45 | recnd 11190 |
. . . . . . . . . 10
β’ (π₯ β β+
β (logβπ₯) β
β) |
260 | 259 | mulid1d 11179 |
. . . . . . . . 9
β’ (π₯ β β+
β ((logβπ₯)
Β· 1) = (logβπ₯)) |
261 | 260 | oveq2d 7378 |
. . . . . . . 8
β’ (π₯ β β+
β (Ξ£π β
(1...(ββπ₯))((
1
β(πΏβπ)) Β·
((Ξβπ) / π)) β ((logβπ₯) Β· 1)) = (Ξ£π β
(1...(ββπ₯))((
1
β(πΏβπ)) Β·
((Ξβπ) / π)) β (logβπ₯))) |
262 | 258, 261 | sylan9eq 2797 |
. . . . . . 7
β’ ((((π β§ π β π·) β§ π = 1 ) β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = (Ξ£π β (1...(ββπ₯))(( 1 β(πΏβπ)) Β· ((Ξβπ) / π)) β (logβπ₯))) |
263 | 262 | mpteq2dva 5210 |
. . . . . 6
β’ (((π β§ π β π·) β§ π = 1 ) β (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((
1
β(πΏβπ)) Β·
((Ξβπ) / π)) β (logβπ₯)))) |
264 | 8, 23, 1, 3, 4, 65 | rpvmasumlem 26851 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((
1
β(πΏβπ)) Β·
((Ξβπ) / π)) β (logβπ₯))) β
π(1)) |
265 | 264 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β π·) β§ π = 1 ) β (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((
1
β(πΏβπ)) Β·
((Ξβπ) / π)) β (logβπ₯))) β
π(1)) |
266 | 263, 265 | eqeltrd 2838 |
. . . . 5
β’ (((π β§ π β π·) β§ π = 1 ) β (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) β
π(1)) |
267 | 178 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π β 1 β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))) = ((logβπ₯) Β· if(π β π, -1, 0))) |
268 | 267 | oveq2d 7378 |
. . . . . . . . 9
β’ (π β 1 β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π β π, -1, 0)))) |
269 | 47 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π·) β§ π₯ β β+) β
(logβπ₯) β
β) |
270 | | mulcom 11144 |
. . . . . . . . . . . . . . 15
β’
(((logβπ₯)
β β β§ -1 β β) β ((logβπ₯) Β· -1) = (-1 Β·
(logβπ₯))) |
271 | 269, 50, 270 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π₯ β β+) β
((logβπ₯) Β· -1)
= (-1 Β· (logβπ₯))) |
272 | 269 | mulm1d 11614 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π·) β§ π₯ β β+) β (-1
Β· (logβπ₯)) =
-(logβπ₯)) |
273 | 271, 272 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π₯ β β+) β
((logβπ₯) Β· -1)
= -(logβπ₯)) |
274 | 269 | mul01d 11361 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π·) β§ π₯ β β+) β
((logβπ₯) Β· 0)
= 0) |
275 | 273, 274 | ifeq12d 4512 |
. . . . . . . . . . . 12
β’ (((π β§ π β π·) β§ π₯ β β+) β if(π β π, ((logβπ₯) Β· -1), ((logβπ₯) Β· 0)) = if(π β π, -(logβπ₯), 0)) |
276 | | ovif2 7460 |
. . . . . . . . . . . 12
β’
((logβπ₯)
Β· if(π β π, -1, 0)) = if(π β π, ((logβπ₯) Β· -1), ((logβπ₯) Β· 0)) |
277 | | negeq 11400 |
. . . . . . . . . . . . 13
β’ (if(π β π, (logβπ₯), 0) = (logβπ₯) β -if(π β π, (logβπ₯), 0) = -(logβπ₯)) |
278 | | negeq 11400 |
. . . . . . . . . . . . . 14
β’ (if(π β π, (logβπ₯), 0) = 0 β -if(π β π, (logβπ₯), 0) = -0) |
279 | 278, 182 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (if(π β π, (logβπ₯), 0) = 0 β -if(π β π, (logβπ₯), 0) = 0) |
280 | 277, 279 | ifsb 4504 |
. . . . . . . . . . . 12
β’ -if(π β π, (logβπ₯), 0) = if(π β π, -(logβπ₯), 0) |
281 | 275, 276,
280 | 3eqtr4g 2802 |
. . . . . . . . . . 11
β’ (((π β§ π β π·) β§ π₯ β β+) β
((logβπ₯) Β·
if(π β π, -1, 0)) = -if(π β π, (logβπ₯), 0)) |
282 | 281 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π β π, -1, 0))) = (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β -if(π β π, (logβπ₯), 0))) |
283 | 58 | an32s 651 |
. . . . . . . . . . 11
β’ (((π β§ π β π·) β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β β) |
284 | | ifcl 4536 |
. . . . . . . . . . . 12
β’
(((logβπ₯)
β β β§ 0 β β) β if(π β π, (logβπ₯), 0) β β) |
285 | 269, 51, 284 | sylancl 587 |
. . . . . . . . . . 11
β’ (((π β§ π β π·) β§ π₯ β β+) β if(π β π, (logβπ₯), 0) β β) |
286 | 283, 285 | subnegd 11526 |
. . . . . . . . . 10
β’ (((π β§ π β π·) β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β -if(π β π, (logβπ₯), 0)) = (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) |
287 | 282, 286 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π β§ π β π·) β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π β π, -1, 0))) = (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) |
288 | 268, 287 | sylan9eqr 2799 |
. . . . . . . 8
β’ ((((π β§ π β π·) β§ π₯ β β+) β§ π β 1 ) β (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) |
289 | 288 | an32s 651 |
. . . . . . 7
β’ ((((π β§ π β π·) β§ π β 1 ) β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))) = (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) |
290 | 289 | mpteq2dva 5210 |
. . . . . 6
β’ (((π β§ π β π·) β§ π β 1 ) β (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0)))) |
291 | 1 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β 1 ) β π β β) |
292 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β 1 ) β π β π·) |
293 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β 1 ) β π β 1 ) |
294 | | eqid 2737 |
. . . . . . . 8
β’ (π β β β¦ ((πβ(πΏβπ)) / π)) = (π β β β¦ ((πβ(πΏβπ)) / π)) |
295 | 8, 23, 291, 3, 4, 65, 292, 293, 294 | dchrmusumlema 26857 |
. . . . . . 7
β’ (((π β§ π β π·) β§ π β 1 ) β βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦))) |
296 | 1 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π·) β π β β) |
297 | 296 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β β) |
298 | 292 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β π·) |
299 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β 1 ) |
300 | | simprl 770 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β π β (0[,)+β)) |
301 | | simprrl 780 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘) |
302 | | simprrr 781 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)) |
303 | 8, 23, 297, 3, 4, 65, 298, 299, 294, 300, 301, 302, 202 | dchrvmaeq0 26868 |
. . . . . . . . . . 11
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β (π β π β π‘ = 0)) |
304 | | ifbi 4513 |
. . . . . . . . . . . . 13
β’ ((π β π β π‘ = 0) β if(π β π, (logβπ₯), 0) = if(π‘ = 0, (logβπ₯), 0)) |
305 | 304 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((π β π β π‘ = 0) β (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0)) = (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π‘ = 0, (logβπ₯), 0))) |
306 | 305 | mpteq2dv 5212 |
. . . . . . . . . . 11
β’ ((π β π β π‘ = 0) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π‘ = 0, (logβπ₯), 0)))) |
307 | 303, 306 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π‘ = 0, (logβπ₯), 0)))) |
308 | 8, 23, 297, 3, 4, 65, 298, 299, 294, 300, 301, 302 | dchrvmasumif 26867 |
. . . . . . . . . 10
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π‘ = 0, (logβπ₯), 0))) β π(1)) |
309 | 307, 308 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((((π β§ π β π·) β§ π β 1 ) β§ (π β (0[,)+β) β§
(seq1( + , (π β
β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)))) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) β π(1)) |
310 | 309 | rexlimdvaa 3154 |
. . . . . . . 8
β’ (((π β§ π β π·) β§ π β 1 ) β (βπ β (0[,)+β)(seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) β
π(1))) |
311 | 310 | exlimdv 1937 |
. . . . . . 7
β’ (((π β§ π β π·) β§ π β 1 ) β (βπ‘βπ β (0[,)+β)(seq1( + , (π β β β¦ ((πβ(πΏβπ)) / π))) β π‘ β§ βπ¦ β (1[,)+β)(absβ((seq1( + ,
(π β β β¦
((πβ(πΏβπ)) / π)))β(ββπ¦)) β π‘)) β€ (π / π¦)) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) β
π(1))) |
312 | 295, 311 | mpd 15 |
. . . . . 6
β’ (((π β§ π β π·) β§ π β 1 ) β (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) + if(π β π, (logβπ₯), 0))) β π(1)) |
313 | 290, 312 | eqeltrd 2838 |
. . . . 5
β’ (((π β§ π β π·) β§ π β 1 ) β (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) β
π(1)) |
314 | 266, 313 | pm2.61dane 3033 |
. . . 4
β’ ((π β§ π β π·) β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0))))) β
π(1)) |
315 | 250, 251,
253, 314 | o1mul2 15514 |
. . 3
β’ ((π β§ π β π·) β (π₯ β β+ β¦
((ββ(πβπ΄)) Β· (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))))) β
π(1)) |
316 | 243, 244,
249, 315 | fsumo1 15704 |
. 2
β’ (π β (π₯ β β+ β¦
Ξ£π β π· ((ββ(πβπ΄)) Β· (Ξ£π β (1...(ββπ₯))((πβ(πΏβπ)) Β· ((Ξβπ) / π)) β ((logβπ₯) Β· if(π = 1 , 1, if(π β π, -1, 0)))))) β
π(1)) |
317 | 241, 316 | eqeltrrd 2839 |
1
β’ (π β (π₯ β β+ β¦
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β ((logβπ₯) Β· (1 β (β―βπ))))) β
π(1)) |