Step | Hyp | Ref
| Expression |
1 | | 1red 11163 |
. . 3
β’ (β€
β 1 β β) |
2 | | reex 11149 |
. . . . . . 7
β’ β
β V |
3 | | rpssre 12929 |
. . . . . . 7
β’
β+ β β |
4 | 2, 3 | ssexi 5284 |
. . . . . 6
β’
β+ β V |
5 | 4 | a1i 11 |
. . . . 5
β’ (β€
β β+ β V) |
6 | | fzfid 13885 |
. . . . . . . 8
β’ (π₯ β β+
β (1...(ββπ₯)) β Fin) |
7 | | rpre 12930 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β π₯ β
β) |
8 | | elfznn 13477 |
. . . . . . . . . . . 12
β’ (π β
(1...(ββπ₯))
β π β
β) |
9 | | nndivre 12201 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π β β) β (π₯ / π) β β) |
10 | 7, 8, 9 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β) |
11 | 10 | recnd 11190 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β) |
12 | | reflcl 13708 |
. . . . . . . . . . . 12
β’ ((π₯ / π) β β β (ββ(π₯ / π)) β β) |
13 | 10, 12 | syl 17 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ββ(π₯ /
π)) β
β) |
14 | 13 | recnd 11190 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ββ(π₯ /
π)) β
β) |
15 | 11, 14 | subcld 11519 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((π₯ / π) β (ββ(π₯ / π))) β β) |
16 | 8 | adantl 483 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β π β
β) |
17 | | mucl 26506 |
. . . . . . . . . . 11
β’ (π β β β
(ΞΌβπ) β
β€) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β€) |
19 | 18 | zcnd 12615 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
20 | 15, 19 | mulcld 11182 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) β β) |
21 | 6, 20 | fsumcl 15625 |
. . . . . . 7
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) β β) |
22 | | rpcn 12932 |
. . . . . . 7
β’ (π₯ β β+
β π₯ β
β) |
23 | | rpne0 12938 |
. . . . . . 7
β’ (π₯ β β+
β π₯ β
0) |
24 | 21, 22, 23 | divcld 11938 |
. . . . . 6
β’ (π₯ β β+
β (Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) β β) |
25 | 24 | adantl 483 |
. . . . 5
β’
((β€ β§ π₯
β β+) β (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) β β) |
26 | | ovexd 7397 |
. . . . 5
β’
((β€ β§ π₯
β β+) β (1 / π₯) β V) |
27 | | eqidd 2738 |
. . . . 5
β’ (β€
β (π₯ β
β+ β¦ (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯))) |
28 | | eqidd 2738 |
. . . . 5
β’ (β€
β (π₯ β
β+ β¦ (1 / π₯)) = (π₯ β β+ β¦ (1 /
π₯))) |
29 | 5, 25, 26, 27, 28 | offval2 7642 |
. . . 4
β’ (β€
β ((π₯ β
β+ β¦ (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) βf + (π₯ β β+ β¦ (1 /
π₯))) = (π₯ β β+ β¦
((Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) + (1 / π₯)))) |
30 | 3 | a1i 11 |
. . . . . 6
β’ (β€
β β+ β β) |
31 | 21 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) β β) |
32 | 22 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
π₯ β
β) |
33 | 23 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
π₯ β 0) |
34 | 31, 32, 33 | absdivd 15347 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβ(Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) = ((absβΞ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) / (absβπ₯))) |
35 | | rprege0 12937 |
. . . . . . . . . . . 12
β’ (π₯ β β+
β (π₯ β β
β§ 0 β€ π₯)) |
36 | | absid 15188 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ 0 β€
π₯) β (absβπ₯) = π₯) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
β’ (π₯ β β+
β (absβπ₯) =
π₯) |
38 | 37 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβπ₯) = π₯) |
39 | 38 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 1 β€ π₯) β
((absβΞ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) / (absβπ₯)) = ((absβΞ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) / π₯)) |
40 | 34, 39 | eqtrd 2777 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβ(Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) = ((absβΞ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) / π₯)) |
41 | 31 | abscld 15328 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβΞ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) β β) |
42 | | fzfid 13885 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(1...(ββπ₯))
β Fin) |
43 | 20 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) β β) |
44 | 43 | abscld 15328 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (absβ(((π₯ /
π) β
(ββ(π₯ / π))) Β· (ΞΌβπ))) β
β) |
45 | 42, 44 | fsumrecl 15626 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))(absβ(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) β β) |
46 | 7 | adantr 482 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 1 β€ π₯) β
π₯ β
β) |
47 | 42, 43 | fsumabs 15693 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβΞ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) β€ Ξ£π β (1...(ββπ₯))(absβ(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)))) |
48 | | reflcl 13708 |
. . . . . . . . . . . . 13
β’ (π₯ β β β
(ββπ₯) β
β) |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(ββπ₯) β
β) |
50 | | 1red 11163 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β 1 β β) |
51 | 15 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((π₯ / π) β (ββ(π₯ / π))) β β) |
52 | | fz1ssnn 13479 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1...(ββπ₯)) β β |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(1...(ββπ₯))
β β) |
54 | 53 | sselda 3949 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β π β
β) |
55 | 54, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β€) |
56 | 55 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
57 | 51, 56 | absmuld 15346 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (absβ(((π₯ /
π) β
(ββ(π₯ / π))) Β· (ΞΌβπ))) = ((absβ((π₯ / π) β (ββ(π₯ / π)))) Β· (absβ(ΞΌβπ)))) |
58 | 51 | abscld 15328 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (absβ((π₯ /
π) β
(ββ(π₯ / π)))) β
β) |
59 | 56 | abscld 15328 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β β) |
60 | 51 | absge0d 15336 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ((π₯ / π) β (ββ(π₯ / π))))) |
61 | 56 | absge0d 15336 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β 0 β€ (absβ(ΞΌβπ))) |
62 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β β+
β§ 1 β€ π₯) β
π₯ β
β+) |
63 | 8 | nnrpd 12962 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
(1...(ββπ₯))
β π β
β+) |
64 | | rpdivcl 12947 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β β+
β§ π β
β+) β (π₯ / π) β
β+) |
65 | 62, 63, 64 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β+) |
66 | 3, 65 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β) |
67 | 66, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (ββ(π₯ /
π)) β
β) |
68 | | flle 13711 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ / π) β β β (ββ(π₯ / π)) β€ (π₯ / π)) |
69 | 66, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (ββ(π₯ /
π)) β€ (π₯ / π)) |
70 | 67, 66, 69 | abssubge0d 15323 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (absβ((π₯ /
π) β
(ββ(π₯ / π)))) = ((π₯ / π) β (ββ(π₯ / π)))) |
71 | | fracle1 13715 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ / π) β β β ((π₯ / π) β (ββ(π₯ / π))) β€ 1) |
72 | 66, 71 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((π₯ / π) β (ββ(π₯ / π))) β€ 1) |
73 | 70, 72 | eqbrtrd 5132 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (absβ((π₯ /
π) β
(ββ(π₯ / π)))) β€ 1) |
74 | | mule1 26513 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β
(absβ(ΞΌβπ))
β€ 1) |
75 | 54, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (absβ(ΞΌβπ)) β€ 1) |
76 | 58, 50, 59, 50, 60, 61, 73, 75 | lemul12ad 12104 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((absβ((π₯ /
π) β
(ββ(π₯ / π)))) Β·
(absβ(ΞΌβπ)))
β€ (1 Β· 1)) |
77 | | 1t1e1 12322 |
. . . . . . . . . . . . . . . 16
β’ (1
Β· 1) = 1 |
78 | 76, 77 | breqtrdi 5151 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((absβ((π₯ /
π) β
(ββ(π₯ / π)))) Β·
(absβ(ΞΌβπ)))
β€ 1) |
79 | 57, 78 | eqbrtrd 5132 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (absβ(((π₯ /
π) β
(ββ(π₯ / π))) Β· (ΞΌβπ))) β€ 1) |
80 | 42, 44, 50, 79 | fsumle 15691 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))(absβ(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) β€ Ξ£π β (1...(ββπ₯))1) |
81 | | 1cnd 11157 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ 1 β€ π₯) β 1
β β) |
82 | | fsumconst 15682 |
. . . . . . . . . . . . . . 15
β’
(((1...(ββπ₯)) β Fin β§ 1 β β) β
Ξ£π β
(1...(ββπ₯))1 =
((β―β(1...(ββπ₯))) Β· 1)) |
83 | 42, 81, 82 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))1 =
((β―β(1...(ββπ₯))) Β· 1)) |
84 | | flge1nn 13733 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ 1 β€
π₯) β
(ββπ₯) β
β) |
85 | 7, 84 | sylan 581 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(ββπ₯) β
β) |
86 | 85 | nnnn0d 12480 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(ββπ₯) β
β0) |
87 | | hashfz1 14253 |
. . . . . . . . . . . . . . . 16
β’
((ββπ₯)
β β0 β (β―β(1...(ββπ₯))) = (ββπ₯)) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(β―β(1...(ββπ₯))) = (ββπ₯)) |
89 | 88 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ 1 β€ π₯) β
((β―β(1...(ββπ₯))) Β· 1) = ((ββπ₯) Β· 1)) |
90 | 49 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(ββπ₯) β
β) |
91 | 90 | mulid1d 11179 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ 1 β€ π₯) β
((ββπ₯) Β·
1) = (ββπ₯)) |
92 | 83, 89, 91 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))1 =
(ββπ₯)) |
93 | 80, 92 | breqtrd 5136 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))(absβ(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) β€ (ββπ₯)) |
94 | | flle 13711 |
. . . . . . . . . . . . 13
β’ (π₯ β β β
(ββπ₯) β€
π₯) |
95 | 46, 94 | syl 17 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(ββπ₯) β€
π₯) |
96 | 45, 49, 46, 93, 95 | letrd 11319 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))(absβ(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) β€ π₯) |
97 | 41, 45, 46, 47, 96 | letrd 11319 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβΞ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) β€ π₯) |
98 | 32 | mulid1d 11179 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(π₯ Β· 1) = π₯) |
99 | 97, 98 | breqtrrd 5138 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβΞ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) β€ (π₯ Β· 1)) |
100 | | 1red 11163 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β 1
β β) |
101 | 41, 100, 62 | ledivmuld 13017 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(((absβΞ£π
β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) / π₯) β€ 1 β (absβΞ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) β€ (π₯ Β· 1))) |
102 | 99, 101 | mpbird 257 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 1 β€ π₯) β
((absβΞ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ))) / π₯) β€ 1) |
103 | 40, 102 | eqbrtrd 5132 |
. . . . . . 7
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβ(Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) β€ 1) |
104 | 103 | adantl 483 |
. . . . . 6
β’
((β€ β§ (π₯
β β+ β§ 1 β€ π₯)) β (absβ(Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) β€ 1) |
105 | 30, 25, 1, 1, 104 | elo1d 15425 |
. . . . 5
β’ (β€
β (π₯ β
β+ β¦ (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) β π(1)) |
106 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
107 | | divrcnv 15744 |
. . . . . . 7
β’ (1 β
β β (π₯ β
β+ β¦ (1 / π₯)) βπ
0) |
108 | 106, 107 | ax-mp 5 |
. . . . . 6
β’ (π₯ β β+
β¦ (1 / π₯))
βπ 0 |
109 | | rlimo1 15506 |
. . . . . 6
β’ ((π₯ β β+
β¦ (1 / π₯))
βπ 0 β (π₯ β β+ β¦ (1 /
π₯)) β
π(1)) |
110 | 108, 109 | mp1i 13 |
. . . . 5
β’ (β€
β (π₯ β
β+ β¦ (1 / π₯)) β π(1)) |
111 | | o1add 15503 |
. . . . 5
β’ (((π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) β π(1) β§ (π₯ β β+
β¦ (1 / π₯)) β
π(1)) β ((π₯
β β+ β¦ (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) βf + (π₯ β β+ β¦ (1 /
π₯))) β
π(1)) |
112 | 105, 110,
111 | syl2anc 585 |
. . . 4
β’ (β€
β ((π₯ β
β+ β¦ (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯)) βf + (π₯ β β+ β¦ (1 /
π₯))) β
π(1)) |
113 | 29, 112 | eqeltrrd 2839 |
. . 3
β’ (β€
β (π₯ β
β+ β¦ ((Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) + (1 / π₯))) β π(1)) |
114 | | ovexd 7397 |
. . 3
β’
((β€ β§ π₯
β β+) β ((Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) + (1 / π₯)) β V) |
115 | 18 | zred 12614 |
. . . . . . 7
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β (ΞΌβπ)
β β) |
116 | 115, 16 | nndivred 12214 |
. . . . . 6
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
117 | 116 | recnd 11190 |
. . . . 5
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
118 | 6, 117 | fsumcl 15625 |
. . . 4
β’ (π₯ β β+
β Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π) β β) |
119 | 118 | adantl 483 |
. . 3
β’
((β€ β§ π₯
β β+) β Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π) β β) |
120 | 118 | adantr 482 |
. . . . . 6
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π) β β) |
121 | 120 | abscld 15328 |
. . . . 5
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβΞ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) β β) |
122 | 117 | adantlr 714 |
. . . . . . . . . 10
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((ΞΌβπ) /
π) β
β) |
123 | 42, 32, 122 | fsummulc2 15676 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(π₯ Β· Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) = Ξ£π β (1...(ββπ₯))(π₯ Β· ((ΞΌβπ) / π))) |
124 | 14, 19 | mulcld 11182 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ π β
(1...(ββπ₯)))
β ((ββ(π₯ /
π)) Β·
(ΞΌβπ)) β
β) |
125 | 124 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((ββ(π₯ /
π)) Β·
(ΞΌβπ)) β
β) |
126 | 42, 43, 125 | fsumadd 15632 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))((((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + ((ββ(π₯ / π)) Β· (ΞΌβπ))) = (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + Ξ£π β (1...(ββπ₯))((ββ(π₯ / π)) Β· (ΞΌβπ)))) |
127 | 11 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (π₯ / π) β
β) |
128 | 14 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (ββ(π₯ /
π)) β
β) |
129 | 127, 128 | npcand 11523 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (((π₯ / π) β (ββ(π₯ / π))) + (ββ(π₯ / π))) = (π₯ / π)) |
130 | 129 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((((π₯ / π) β (ββ(π₯ / π))) + (ββ(π₯ / π))) Β· (ΞΌβπ)) = ((π₯ / π) Β· (ΞΌβπ))) |
131 | 51, 128, 56 | adddird 11187 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((((π₯ / π) β (ββ(π₯ / π))) + (ββ(π₯ / π))) Β· (ΞΌβπ)) = ((((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + ((ββ(π₯ / π)) Β· (ΞΌβπ)))) |
132 | 32 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β π₯ β
β) |
133 | 54 | nnrpd 12962 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β π β
β+) |
134 | | rpcnne0 12940 |
. . . . . . . . . . . . . 14
β’ (π β β+
β (π β β
β§ π β
0)) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (π β β
β§ π β
0)) |
136 | | div23 11839 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§
(ΞΌβπ) β
β β§ (π β
β β§ π β 0))
β ((π₯ Β·
(ΞΌβπ)) / π) = ((π₯ / π) Β· (ΞΌβπ))) |
137 | | divass 11838 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§
(ΞΌβπ) β
β β§ (π β
β β§ π β 0))
β ((π₯ Β·
(ΞΌβπ)) / π) = (π₯ Β· ((ΞΌβπ) / π))) |
138 | 136, 137 | eqtr3d 2779 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§
(ΞΌβπ) β
β β§ (π β
β β§ π β 0))
β ((π₯ / π) Β· (ΞΌβπ)) = (π₯ Β· ((ΞΌβπ) / π))) |
139 | 132, 56, 135, 138 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((π₯ / π) Β· (ΞΌβπ)) = (π₯ Β· ((ΞΌβπ) / π))) |
140 | 130, 131,
139 | 3eqtr3d 2785 |
. . . . . . . . . . 11
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + ((ββ(π₯ / π)) Β· (ΞΌβπ))) = (π₯ Β· ((ΞΌβπ) / π))) |
141 | 140 | sumeq2dv 15595 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))((((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + ((ββ(π₯ / π)) Β· (ΞΌβπ))) = Ξ£π β (1...(ββπ₯))(π₯ Β· ((ΞΌβπ) / π))) |
142 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ (π = (π Β· π) β (ΞΌβπ) = (ΞΌβπ)) |
143 | | ssrab2 4042 |
. . . . . . . . . . . . . . . 16
β’ {π¦ β β β£ π¦ β₯ π} β β |
144 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β {π¦ β β β£ π¦ β₯ π}) |
145 | 143, 144 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β π β β) |
146 | 145, 17 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β€) |
147 | 146 | zcnd 12615 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ 1 β€ π₯) β§
(π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π})) β (ΞΌβπ) β β) |
148 | 142, 46, 147 | dvdsflsumcom 26553 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} (ΞΌβπ) = Ξ£π β (1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))(ΞΌβπ)) |
149 | 147 | 3impb 1116 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π}) β (ΞΌβπ) β β) |
150 | 149 | mulid1d 11179 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯))
β§ π β {π¦ β β β£ π¦ β₯ π}) β ((ΞΌβπ) Β· 1) = (ΞΌβπ)) |
151 | 150 | 2sumeq2dv 15597 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· 1) = Ξ£π β (1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} (ΞΌβπ)) |
152 | | eqidd 2738 |
. . . . . . . . . . . . . 14
β’ (π = 1 β 1 =
1) |
153 | | nnuz 12813 |
. . . . . . . . . . . . . . . 16
β’ β =
(β€β₯β1) |
154 | 85, 153 | eleqtrdi 2848 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(ββπ₯) β
(β€β₯β1)) |
155 | | eluzfz1 13455 |
. . . . . . . . . . . . . . 15
β’
((ββπ₯)
β (β€β₯β1) β 1 β
(1...(ββπ₯))) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β+
β§ 1 β€ π₯) β 1
β (1...(ββπ₯))) |
157 | | 1cnd 11157 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β 1 β β) |
158 | 152, 42, 53, 156, 157 | musumsum 26557 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} ((ΞΌβπ) Β· 1) = 1) |
159 | 151, 158 | eqtr3d 2779 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))Ξ£π β {π¦ β β β£ π¦ β₯ π} (ΞΌβπ) = 1) |
160 | | fzfid 13885 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (1...(ββ(π₯ / π))) β Fin) |
161 | | fsumconst 15682 |
. . . . . . . . . . . . . . 15
β’
(((1...(ββ(π₯ / π))) β Fin β§ (ΞΌβπ) β β) β
Ξ£π β
(1...(ββ(π₯ /
π)))(ΞΌβπ) =
((β―β(1...(ββ(π₯ / π)))) Β· (ΞΌβπ))) |
162 | 160, 56, 161 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))(ΞΌβπ) =
((β―β(1...(ββ(π₯ / π)))) Β· (ΞΌβπ))) |
163 | | rprege0 12937 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ / π) β β+ β ((π₯ / π) β β β§ 0 β€ (π₯ / π))) |
164 | | flge0nn0 13732 |
. . . . . . . . . . . . . . . 16
β’ (((π₯ / π) β β β§ 0 β€ (π₯ / π)) β (ββ(π₯ / π)) β
β0) |
165 | | hashfz1 14253 |
. . . . . . . . . . . . . . . 16
β’
((ββ(π₯ /
π)) β
β0 β (β―β(1...(ββ(π₯ / π)))) = (ββ(π₯ / π))) |
166 | 65, 163, 164, 165 | 4syl 19 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β (β―β(1...(ββ(π₯ / π)))) = (ββ(π₯ / π))) |
167 | 166 | oveq1d 7377 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β ((β―β(1...(ββ(π₯ / π)))) Β· (ΞΌβπ)) = ((ββ(π₯ / π)) Β· (ΞΌβπ))) |
168 | 162, 167 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ (((π₯ β β+
β§ 1 β€ π₯) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(1...(ββ(π₯ /
π)))(ΞΌβπ) = ((ββ(π₯ / π)) Β· (ΞΌβπ))) |
169 | 168 | sumeq2dv 15595 |
. . . . . . . . . . . 12
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))Ξ£π β (1...(ββ(π₯ / π)))(ΞΌβπ) = Ξ£π β (1...(ββπ₯))((ββ(π₯ / π)) Β· (ΞΌβπ))) |
170 | 148, 159,
169 | 3eqtr3rd 2786 |
. . . . . . . . . . 11
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))((ββ(π₯ / π)) Β· (ΞΌβπ)) = 1) |
171 | 170 | oveq2d 7378 |
. . . . . . . . . 10
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + Ξ£π β (1...(ββπ₯))((ββ(π₯ / π)) Β· (ΞΌβπ))) = (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + 1)) |
172 | 126, 141,
171 | 3eqtr3d 2785 |
. . . . . . . . 9
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))(π₯ Β· ((ΞΌβπ) / π)) = (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + 1)) |
173 | 123, 172 | eqtrd 2777 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(π₯ Β· Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) = (Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + 1)) |
174 | 173 | oveq1d 7377 |
. . . . . . 7
β’ ((π₯ β β+
β§ 1 β€ π₯) β
((π₯ Β· Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) / π₯) = ((Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + 1) / π₯)) |
175 | 120, 32, 33 | divcan3d 11943 |
. . . . . . 7
β’ ((π₯ β β+
β§ 1 β€ π₯) β
((π₯ Β· Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) / π₯) = Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π)) |
176 | | rpcnne0 12940 |
. . . . . . . . 9
β’ (π₯ β β+
β (π₯ β β
β§ π₯ β
0)) |
177 | 176 | adantr 482 |
. . . . . . . 8
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(π₯ β β β§
π₯ β 0)) |
178 | | divdir 11845 |
. . . . . . . 8
β’
((Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) β β β§ 1 β β
β§ (π₯ β β
β§ π₯ β 0)) β
((Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + 1) / π₯) = ((Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) + (1 / π₯))) |
179 | 31, 81, 177, 178 | syl3anc 1372 |
. . . . . . 7
β’ ((π₯ β β+
β§ 1 β€ π₯) β
((Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) + 1) / π₯) = ((Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) + (1 / π₯))) |
180 | 174, 175,
179 | 3eqtr3d 2785 |
. . . . . 6
β’ ((π₯ β β+
β§ 1 β€ π₯) β
Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π) = ((Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) + (1 / π₯))) |
181 | 180 | fveq2d 6851 |
. . . . 5
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβΞ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) = (absβ((Ξ£π β (1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) + (1 / π₯)))) |
182 | 121, 181 | eqled 11265 |
. . . 4
β’ ((π₯ β β+
β§ 1 β€ π₯) β
(absβΞ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) β€ (absβ((Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) + (1 / π₯)))) |
183 | 182 | adantl 483 |
. . 3
β’
((β€ β§ (π₯
β β+ β§ 1 β€ π₯)) β (absβΞ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) β€ (absβ((Ξ£π β
(1...(ββπ₯))(((π₯ / π) β (ββ(π₯ / π))) Β· (ΞΌβπ)) / π₯) + (1 / π₯)))) |
184 | 1, 113, 114, 119, 183 | o1le 15544 |
. 2
β’ (β€
β (π₯ β
β+ β¦ Ξ£π β (1...(ββπ₯))((ΞΌβπ) / π)) β π(1)) |
185 | 184 | mptru 1549 |
1
β’ (π₯ β β+
β¦ Ξ£π β
(1...(ββπ₯))((ΞΌβπ) / π)) β π(1) |