Step | Hyp | Ref
| Expression |
1 | | rpvmasum.z |
. . 3
β’ π =
(β€/nβ€βπ) |
2 | | rpvmasum.l |
. . 3
β’ πΏ = (β€RHomβπ) |
3 | | rpvmasum.a |
. . 3
β’ (π β π β β) |
4 | | rpvmasum.u |
. . 3
β’ π = (Unitβπ) |
5 | | rpvmasum.b |
. . 3
β’ (π β π΄ β π) |
6 | | rpvmasum.t |
. . 3
β’ π = (β‘πΏ β {π΄}) |
7 | 1, 2, 3, 4, 5, 6 | rpvmasum 26890 |
. 2
β’ (π β (π₯ β β+ β¦
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β (logβπ₯))) β π(1)) |
8 | 3 | phicld 16651 |
. . . . . . 7
β’ (π β (Οβπ) β
β) |
9 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(Οβπ) β
β) |
10 | 9 | nncnd 12176 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(Οβπ) β
β) |
11 | | fzfid 13885 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
12 | | inss1 4193 |
. . . . . . . 8
β’
((1...(ββπ₯)) β© π) β (1...(ββπ₯)) |
13 | | ssfi 9124 |
. . . . . . . 8
β’
(((1...(ββπ₯)) β Fin β§
((1...(ββπ₯))
β© π) β
(1...(ββπ₯)))
β ((1...(ββπ₯)) β© π) β Fin) |
14 | 11, 12, 13 | sylancl 587 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
((1...(ββπ₯))
β© π) β
Fin) |
15 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β π β
((1...(ββπ₯))
β© π)) |
16 | 15 | elin1d 4163 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β π β
(1...(ββπ₯))) |
17 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β
(1...(ββπ₯))
β π β
β) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β π β
β) |
19 | | vmacl 26483 |
. . . . . . . . 9
β’ (π β β β
(Ξβπ) β
β) |
20 | | nndivre 12201 |
. . . . . . . . 9
β’
(((Ξβπ)
β β β§ π
β β) β ((Ξβπ) / π) β β) |
21 | 19, 20 | mpancom 687 |
. . . . . . . 8
β’ (π β β β
((Ξβπ) / π) β
β) |
22 | 18, 21 | syl 17 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β
((Ξβπ) / π) β
β) |
23 | 14, 22 | fsumrecl 15626 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π) β β) |
24 | 23 | recnd 11190 |
. . . . 5
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π) β β) |
25 | 10, 24 | mulcld 11182 |
. . . 4
β’ ((π β§ π₯ β β+) β
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β β) |
26 | | relogcl 25947 |
. . . . . 6
β’ (π₯ β β+
β (logβπ₯) β
β) |
27 | 26 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
28 | 27 | recnd 11190 |
. . . 4
β’ ((π β§ π₯ β β+) β
(logβπ₯) β
β) |
29 | 25, 28 | subcld 11519 |
. . 3
β’ ((π β§ π₯ β β+) β
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β (logβπ₯)) β β) |
30 | | inss1 4193 |
. . . . . . . 8
β’
((1...(ββπ₯)) β© (β β© π)) β (1...(ββπ₯)) |
31 | | ssfi 9124 |
. . . . . . . 8
β’
(((1...(ββπ₯)) β Fin β§
((1...(ββπ₯))
β© (β β© π))
β (1...(ββπ₯))) β ((1...(ββπ₯)) β© (β β© π)) β Fin) |
32 | 11, 30, 31 | sylancl 587 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
((1...(ββπ₯))
β© (β β© π))
β Fin) |
33 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β β© π)))
β π β
((1...(ββπ₯))
β© (β β© π))) |
34 | 33 | elin1d 4163 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β β© π)))
β π β
(1...(ββπ₯))) |
35 | 34, 17 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β β© π)))
β π β
β) |
36 | | nnrp 12933 |
. . . . . . . . . 10
β’ (π β β β π β
β+) |
37 | 36 | relogcld 25994 |
. . . . . . . . 9
β’ (π β β β
(logβπ) β
β) |
38 | 37, 36 | rerpdivcld 12995 |
. . . . . . . 8
β’ (π β β β
((logβπ) / π) β
β) |
39 | 35, 38 | syl 17 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β β© π)))
β ((logβπ) /
π) β
β) |
40 | 32, 39 | fsumrecl 15626 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© (β β© π))((logβπ) / π) β β) |
41 | 40 | recnd 11190 |
. . . . 5
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© (β β© π))((logβπ) / π) β β) |
42 | 10, 41 | mulcld 11182 |
. . . 4
β’ ((π β§ π₯ β β+) β
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β β© π))((logβπ) / π)) β β) |
43 | 42, 28 | subcld 11519 |
. . 3
β’ ((π β§ π₯ β β+) β
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β β© π))((logβπ) / π)) β (logβπ₯)) β β) |
44 | 10, 24, 41 | subdid 11618 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
((Οβπ) Β·
(Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π) β Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π))) = (((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© π)((Ξβπ) / π)) β ((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π)))) |
45 | 19 | recnd 11190 |
. . . . . . . . . . 11
β’ (π β β β
(Ξβπ) β
β) |
46 | | 0re 11164 |
. . . . . . . . . . . . 13
β’ 0 β
β |
47 | | ifcl 4536 |
. . . . . . . . . . . . 13
β’
(((logβπ)
β β β§ 0 β β) β if(π β β, (logβπ), 0) β
β) |
48 | 37, 46, 47 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β β β if(π β β,
(logβπ), 0) β
β) |
49 | 48 | recnd 11190 |
. . . . . . . . . . 11
β’ (π β β β if(π β β,
(logβπ), 0) β
β) |
50 | 36 | rpcnne0d 12973 |
. . . . . . . . . . 11
β’ (π β β β (π β β β§ π β 0)) |
51 | | divsubdir 11856 |
. . . . . . . . . . 11
β’
(((Ξβπ)
β β β§ if(π
β β, (logβπ), 0) β β β§ (π β β β§ π β 0)) β
(((Ξβπ)
β if(π β
β, (logβπ), 0))
/ π) =
(((Ξβπ) /
π) β (if(π β β,
(logβπ), 0) / π))) |
52 | 45, 49, 50, 51 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β β β
(((Ξβπ)
β if(π β
β, (logβπ), 0))
/ π) =
(((Ξβπ) /
π) β (if(π β β,
(logβπ), 0) / π))) |
53 | 18, 52 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β
(((Ξβπ)
β if(π β
β, (logβπ), 0))
/ π) =
(((Ξβπ) /
π) β (if(π β β,
(logβπ), 0) / π))) |
54 | 53 | sumeq2dv 15595 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π) = Ξ£π β ((1...(ββπ₯)) β© π)(((Ξβπ) / π) β (if(π β β, (logβπ), 0) / π))) |
55 | 21 | recnd 11190 |
. . . . . . . . . 10
β’ (π β β β
((Ξβπ) / π) β
β) |
56 | 18, 55 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β
((Ξβπ) / π) β
β) |
57 | 48, 36 | rerpdivcld 12995 |
. . . . . . . . . . 11
β’ (π β β β (if(π β β,
(logβπ), 0) / π) β
β) |
58 | 57 | recnd 11190 |
. . . . . . . . . 10
β’ (π β β β (if(π β β,
(logβπ), 0) / π) β
β) |
59 | 18, 58 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β (if(π β β,
(logβπ), 0) / π) β
β) |
60 | 14, 56, 59 | fsumsub 15680 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) / π) β (if(π β β, (logβπ), 0) / π)) = (Ξ£π β ((1...(ββπ₯)) β© π)((Ξβπ) / π) β Ξ£π β ((1...(ββπ₯)) β© π)(if(π β β, (logβπ), 0) / π))) |
61 | | inss2 4194 |
. . . . . . . . . . . 12
β’ (β
β© π) β π |
62 | | sslin 4199 |
. . . . . . . . . . . 12
β’ ((β
β© π) β π β
((1...(ββπ₯))
β© (β β© π))
β ((1...(ββπ₯)) β© π)) |
63 | 61, 62 | mp1i 13 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β
((1...(ββπ₯))
β© (β β© π))
β ((1...(ββπ₯)) β© π)) |
64 | 35, 58 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β β© π)))
β (if(π β
β, (logβπ), 0)
/ π) β
β) |
65 | | eldif 3925 |
. . . . . . . . . . . . . . . 16
β’ (π β
(((1...(ββπ₯))
β© π) β
((1...(ββπ₯))
β© (β β© π)))
β (π β
((1...(ββπ₯))
β© π) β§ Β¬ π β
((1...(ββπ₯))
β© (β β© π)))) |
66 | | incom 4166 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (β
β© π) = (π β© β) |
67 | 66 | ineq2i 4174 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1...(ββπ₯)) β© (β β© π)) = ((1...(ββπ₯)) β© (π β© β)) |
68 | | inass 4184 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((1...(ββπ₯)) β© π) β© β) =
((1...(ββπ₯))
β© (π β©
β)) |
69 | 67, 68 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . . 19
β’
((1...(ββπ₯)) β© (β β© π)) = (((1...(ββπ₯)) β© π) β© β) |
70 | 69 | elin2 4162 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
((1...(ββπ₯))
β© (β β© π))
β (π β
((1...(ββπ₯))
β© π) β§ π β
β)) |
71 | 70 | simplbi2 502 |
. . . . . . . . . . . . . . . . 17
β’ (π β
((1...(ββπ₯))
β© π) β (π β β β π β
((1...(ββπ₯))
β© (β β© π)))) |
72 | 71 | con3dimp 410 |
. . . . . . . . . . . . . . . 16
β’ ((π β
((1...(ββπ₯))
β© π) β§ Β¬ π β
((1...(ββπ₯))
β© (β β© π)))
β Β¬ π β
β) |
73 | 65, 72 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ (π β
(((1...(ββπ₯))
β© π) β
((1...(ββπ₯))
β© (β β© π)))
β Β¬ π β
β) |
74 | 73 | adantl 483 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ π β
(((1...(ββπ₯))
β© π) β
((1...(ββπ₯))
β© (β β© π))))
β Β¬ π β
β) |
75 | 74 | iffalsed 4502 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(((1...(ββπ₯))
β© π) β
((1...(ββπ₯))
β© (β β© π))))
β if(π β β,
(logβπ), 0) =
0) |
76 | 75 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(((1...(ββπ₯))
β© π) β
((1...(ββπ₯))
β© (β β© π))))
β (if(π β
β, (logβπ), 0)
/ π) = (0 / π)) |
77 | | eldifi 4091 |
. . . . . . . . . . . . . 14
β’ (π β
(((1...(ββπ₯))
β© π) β
((1...(ββπ₯))
β© (β β© π)))
β π β
((1...(ββπ₯))
β© π)) |
78 | 77, 18 | sylan2 594 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
(((1...(ββπ₯))
β© π) β
((1...(ββπ₯))
β© (β β© π))))
β π β
β) |
79 | | div0 11850 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β 0) β (0 / π) = 0) |
80 | 50, 79 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β β β (0 /
π) = 0) |
81 | 78, 80 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(((1...(ββπ₯))
β© π) β
((1...(ββπ₯))
β© (β β© π))))
β (0 / π) =
0) |
82 | 76, 81 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(((1...(ββπ₯))
β© π) β
((1...(ββπ₯))
β© (β β© π))))
β (if(π β
β, (logβπ), 0)
/ π) = 0) |
83 | 63, 64, 82, 14 | fsumss 15617 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© (β β© π))(if(π β β, (logβπ), 0) / π) = Ξ£π β ((1...(ββπ₯)) β© π)(if(π β β, (logβπ), 0) / π)) |
84 | | inss2 4194 |
. . . . . . . . . . . . . . 15
β’
((1...(ββπ₯)) β© (β β© π)) β (β β© π) |
85 | | inss1 4193 |
. . . . . . . . . . . . . . 15
β’ (β
β© π) β
β |
86 | 84, 85 | sstri 3958 |
. . . . . . . . . . . . . 14
β’
((1...(ββπ₯)) β© (β β© π)) β β |
87 | 86, 33 | sselid 3947 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β β© π)))
β π β
β) |
88 | 87 | iftrued 4499 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β β© π)))
β if(π β β,
(logβπ), 0) =
(logβπ)) |
89 | 88 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© (β β© π)))
β (if(π β
β, (logβπ), 0)
/ π) = ((logβπ) / π)) |
90 | 89 | sumeq2dv 15595 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© (β β© π))(if(π β β, (logβπ), 0) / π) = Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π)) |
91 | 83, 90 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)(if(π β β,
(logβπ), 0) / π) = Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π)) |
92 | 91 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
(Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π) β Ξ£π β ((1...(ββπ₯)) β© π)(if(π β β, (logβπ), 0) / π)) = (Ξ£π β ((1...(ββπ₯)) β© π)((Ξβπ) / π) β Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π))) |
93 | 54, 60, 92 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π) = (Ξ£π β ((1...(ββπ₯)) β© π)((Ξβπ) / π) β Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π))) |
94 | 93 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π)) = ((Οβπ) Β· (Ξ£π β ((1...(ββπ₯)) β© π)((Ξβπ) / π) β Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π)))) |
95 | 25, 42, 28 | nnncan2d 11554 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
((((Οβπ)
Β· Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β (logβπ₯)) β (((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π)) β (logβπ₯))) = (((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© π)((Ξβπ) / π)) β ((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π)))) |
96 | 44, 94, 95 | 3eqtr4d 2787 |
. . . . 5
β’ ((π β§ π₯ β β+) β
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π)) = ((((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© π)((Ξβπ) / π)) β (logβπ₯)) β (((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π)) β (logβπ₯)))) |
97 | 96 | mpteq2dva 5210 |
. . . 4
β’ (π β (π₯ β β+ β¦
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π))) = (π₯ β β+ β¦
((((Οβπ)
Β· Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β (logβπ₯)) β (((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π)) β (logβπ₯))))) |
98 | 19, 48 | resubcld 11590 |
. . . . . . . . 9
β’ (π β β β
((Ξβπ) β
if(π β β,
(logβπ), 0)) β
β) |
99 | 98, 36 | rerpdivcld 12995 |
. . . . . . . 8
β’ (π β β β
(((Ξβπ)
β if(π β
β, (logβπ), 0))
/ π) β
β) |
100 | 18, 99 | syl 17 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β
(((Ξβπ)
β if(π β
β, (logβπ), 0))
/ π) β
β) |
101 | 14, 100 | fsumrecl 15626 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π) β β) |
102 | 101 | recnd 11190 |
. . . . 5
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π) β β) |
103 | | rpssre 12929 |
. . . . . 6
β’
β+ β β |
104 | 8 | nncnd 12176 |
. . . . . 6
β’ (π β (Οβπ) β
β) |
105 | | o1const 15509 |
. . . . . 6
β’
((β+ β β β§ (Οβπ) β β) β (π₯ β β+
β¦ (Οβπ))
β π(1)) |
106 | 103, 104,
105 | sylancr 588 |
. . . . 5
β’ (π β (π₯ β β+ β¦
(Οβπ)) β
π(1)) |
107 | 103 | a1i 11 |
. . . . . 6
β’ (π β β+
β β) |
108 | | 1red 11163 |
. . . . . 6
β’ (π β 1 β
β) |
109 | | 2re 12234 |
. . . . . . 7
β’ 2 β
β |
110 | 109 | a1i 11 |
. . . . . 6
β’ (π β 2 β
β) |
111 | | breq1 5113 |
. . . . . . . . . . . . . 14
β’
((logβπ) =
if(π β β,
(logβπ), 0) β
((logβπ) β€
(Ξβπ) β
if(π β β,
(logβπ), 0) β€
(Ξβπ))) |
112 | | breq1 5113 |
. . . . . . . . . . . . . 14
β’ (0 =
if(π β β,
(logβπ), 0) β (0
β€ (Ξβπ)
β if(π β β,
(logβπ), 0) β€
(Ξβπ))) |
113 | 37 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β) β
(logβπ) β
β) |
114 | | vmaprm 26482 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
(Ξβπ) =
(logβπ)) |
115 | 114 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β) β
(Ξβπ) =
(logβπ)) |
116 | 115 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β) β
(logβπ) =
(Ξβπ)) |
117 | 113, 116 | eqled 11265 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β) β
(logβπ) β€
(Ξβπ)) |
118 | | vmage0 26486 |
. . . . . . . . . . . . . . 15
β’ (π β β β 0 β€
(Ξβπ)) |
119 | 118 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ Β¬
π β β) β 0
β€ (Ξβπ)) |
120 | 111, 112,
117, 119 | ifbothda 4529 |
. . . . . . . . . . . . 13
β’ (π β β β if(π β β,
(logβπ), 0) β€
(Ξβπ)) |
121 | 19, 48 | subge0d 11752 |
. . . . . . . . . . . . 13
β’ (π β β β (0 β€
((Ξβπ) β
if(π β β,
(logβπ), 0)) β
if(π β β,
(logβπ), 0) β€
(Ξβπ))) |
122 | 120, 121 | mpbird 257 |
. . . . . . . . . . . 12
β’ (π β β β 0 β€
((Ξβπ) β
if(π β β,
(logβπ),
0))) |
123 | 98, 36, 122 | divge0d 13004 |
. . . . . . . . . . 11
β’ (π β β β 0 β€
(((Ξβπ)
β if(π β
β, (logβπ), 0))
/ π)) |
124 | 18, 123 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
((1...(ββπ₯))
β© π)) β 0 β€
(((Ξβπ)
β if(π β
β, (logβπ), 0))
/ π)) |
125 | 14, 100, 124 | fsumge0 15687 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β 0 β€
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π)) |
126 | 101, 125 | absidd 15314 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π)) = Ξ£π β ((1...(ββπ₯)) β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π)) |
127 | 17 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
128 | 127, 99 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((Ξβπ)
β if(π β
β, (logβπ), 0))
/ π) β
β) |
129 | 11, 128 | fsumrecl 15626 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((Ξβπ) β if(π β β, (logβπ), 0)) / π) β β) |
130 | 109 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β 2 β
β) |
131 | 127, 123 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β 0 β€ (((Ξβπ) β if(π β β, (logβπ), 0)) / π)) |
132 | 12 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
((1...(ββπ₯))
β© π) β
(1...(ββπ₯))) |
133 | 11, 128, 131, 132 | fsumless 15688 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π) β€ Ξ£π β (1...(ββπ₯))(((Ξβπ) β if(π β β, (logβπ), 0)) / π)) |
134 | 107 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β π₯ β
β) |
135 | 134 | flcld 13710 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β€) |
136 | | rplogsumlem2 26849 |
. . . . . . . . . 10
β’
((ββπ₯)
β β€ β Ξ£π β (1...(ββπ₯))(((Ξβπ) β if(π β β, (logβπ), 0)) / π) β€ 2) |
137 | 135, 136 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(((Ξβπ) β if(π β β, (logβπ), 0)) / π) β€ 2) |
138 | 101, 129,
130, 133, 137 | letrd 11319 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π) β€ 2) |
139 | 126, 138 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π)) β€ 2) |
140 | 139 | adantrr 716 |
. . . . . 6
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π)) β€ 2) |
141 | 107, 102,
108, 110, 140 | elo1d 15425 |
. . . . 5
β’ (π β (π₯ β β+ β¦
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π)) β π(1)) |
142 | 10, 102, 106, 141 | o1mul2 15514 |
. . . 4
β’ (π β (π₯ β β+ β¦
((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)(((Ξβπ) β if(π β β, (logβπ), 0)) / π))) β π(1)) |
143 | 97, 142 | eqeltrrd 2839 |
. . 3
β’ (π β (π₯ β β+ β¦
((((Οβπ)
Β· Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β (logβπ₯)) β (((Οβπ) Β· Ξ£π β ((1...(ββπ₯)) β© (β β© π))((logβπ) / π)) β (logβπ₯)))) β π(1)) |
144 | 29, 43, 143 | o1dif 15519 |
. 2
β’ (π β ((π₯ β β+ β¦
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© π)((Ξβπ) / π)) β (logβπ₯))) β π(1) β (π₯ β β+
β¦ (((Οβπ)
Β· Ξ£π β
((1...(ββπ₯))
β© (β β© π))((logβπ) / π)) β (logβπ₯))) β π(1))) |
145 | 7, 144 | mpbid 231 |
1
β’ (π β (π₯ β β+ β¦
(((Οβπ) Β·
Ξ£π β
((1...(ββπ₯))
β© (β β© π))((logβπ) / π)) β (logβπ₯))) β π(1)) |