Step | Hyp | Ref
| Expression |
1 | | fzfid 13885 |
. . . 4
β’ ((π β§ π₯ β β+) β
(1...(ββπ₯))
β Fin) |
2 | | fzfid 13885 |
. . . 4
β’ ((π β§ π₯ β β+) β
(((ββπ₯) +
1)...(ββ(π₯β2))) β Fin) |
3 | | fzfid 13885 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π))) β Fin) |
4 | | elfznn 13477 |
. . . . . . 7
β’ (π β
(1...(ββπ₯))
β π β
β) |
5 | | elfzuz 13444 |
. . . . . . 7
β’ (π β (((ββπ₯) + 1)...(ββ((π₯β2) / π))) β π β
(β€β₯β((ββπ₯) + 1))) |
6 | 4, 5 | anim12i 614 |
. . . . . 6
β’ ((π β
(1...(ββπ₯))
β§ π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π)))) β (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) |
7 | 6 | a1i 11 |
. . . . 5
β’ ((π β§ π₯ β β+) β ((π β
(1...(ββπ₯))
β§ π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π)))) β (π β β β§ π β
(β€β₯β((ββπ₯) + 1))))) |
8 | | elfzuz 13444 |
. . . . . . 7
β’ (π β (((ββπ₯) + 1)...(ββ(π₯β2))) β π β
(β€β₯β((ββπ₯) + 1))) |
9 | | elfznn 13477 |
. . . . . . 7
β’ (π β
(1...(ββ((π₯β2) / π))) β π β β) |
10 | 8, 9 | anim12ci 615 |
. . . . . 6
β’ ((π β (((ββπ₯) + 1)...(ββ(π₯β2))) β§ π β
(1...(ββ((π₯β2) / π)))) β (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) |
11 | 10 | a1i 11 |
. . . . 5
β’ ((π β§ π₯ β β+) β ((π β (((ββπ₯) + 1)...(ββ(π₯β2))) β§ π β
(1...(ββ((π₯β2) / π)))) β (π β β β§ π β
(β€β₯β((ββπ₯) + 1))))) |
12 | | eluzelz 12780 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β((ββπ₯) + 1)) β π β β€) |
13 | 12 | ad2antll 728 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π β β€) |
14 | 13 | zred 12614 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π β β) |
15 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β π₯ β
β+) |
16 | | 2z 12542 |
. . . . . . . . . . . . 13
β’ 2 β
β€ |
17 | | rpexpcl 13993 |
. . . . . . . . . . . . 13
β’ ((π₯ β β+
β§ 2 β β€) β (π₯β2) β
β+) |
18 | 15, 16, 17 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β+) β (π₯β2) β
β+) |
19 | 18 | rpred 12964 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β β+) β (π₯β2) β
β) |
20 | 19 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π₯β2) β β) |
21 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π β β) |
22 | 21 | nnrpd 12962 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π β β+) |
23 | 14, 20, 22 | lemuldivd 13013 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π Β· π) β€ (π₯β2) β π β€ ((π₯β2) / π))) |
24 | 21 | nnred 12175 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π β β) |
25 | 15 | rprege0d 12971 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β (π₯ β β β§ 0 β€
π₯)) |
26 | | flge0nn0 13732 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ 0 β€
π₯) β
(ββπ₯) β
β0) |
27 | | nn0p1nn 12459 |
. . . . . . . . . . . . . 14
β’
((ββπ₯)
β β0 β ((ββπ₯) + 1) β β) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β β+) β
((ββπ₯) + 1)
β β) |
29 | 28 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((ββπ₯) + 1) β
β) |
30 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π β
(β€β₯β((ββπ₯) + 1))) |
31 | | eluznn 12850 |
. . . . . . . . . . . 12
β’
((((ββπ₯)
+ 1) β β β§ π
β (β€β₯β((ββπ₯) + 1))) β π β β) |
32 | 29, 30, 31 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π β β) |
33 | 32 | nnrpd 12962 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π β β+) |
34 | 24, 20, 33 | lemuldiv2d 13014 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π Β· π) β€ (π₯β2) β π β€ ((π₯β2) / π))) |
35 | 23, 34 | bitr3d 281 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β€ ((π₯β2) / π) β π β€ ((π₯β2) / π))) |
36 | | rpcn 12932 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β+
β π₯ β
β) |
37 | 36 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β β+) β π₯ β
β) |
38 | 37 | sqvald 14055 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β+) β (π₯β2) = (π₯ Β· π₯)) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π₯β2) = (π₯ Β· π₯)) |
40 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π₯ β β+) |
41 | 40 | rpred 12964 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π₯ β β) |
42 | | reflcl 13708 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β
(ββπ₯) β
β) |
43 | | peano2re 11335 |
. . . . . . . . . . . . . . . 16
β’
((ββπ₯)
β β β ((ββπ₯) + 1) β β) |
44 | 41, 42, 43 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((ββπ₯) + 1) β
β) |
45 | | fllep1 13713 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β β π₯ β€ ((ββπ₯) + 1)) |
46 | 41, 45 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π₯ β€ ((ββπ₯) + 1)) |
47 | | eluzle 12783 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β((ββπ₯) + 1)) β ((ββπ₯) + 1) β€ π) |
48 | 47 | ad2antll 728 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((ββπ₯) + 1) β€ π) |
49 | 41, 44, 14, 46, 48 | letrd 11319 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π₯ β€ π) |
50 | 41, 14, 40 | lemul1d 13007 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π₯ β€ π β (π₯ Β· π₯) β€ (π Β· π₯))) |
51 | 49, 50 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π₯ Β· π₯) β€ (π Β· π₯)) |
52 | 39, 51 | eqbrtrd 5132 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π₯β2) β€ (π Β· π₯)) |
53 | 20, 41, 33 | ledivmuld 13017 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (((π₯β2) / π) β€ π₯ β (π₯β2) β€ (π Β· π₯))) |
54 | 52, 53 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π₯β2) / π) β€ π₯) |
55 | | nnre 12167 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
56 | 55 | ad2antrl 727 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β π β β) |
57 | 20, 32 | nndivred 12214 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π₯β2) / π) β β) |
58 | | letr 11256 |
. . . . . . . . . . . 12
β’ ((π β β β§ ((π₯β2) / π) β β β§ π₯ β β) β ((π β€ ((π₯β2) / π) β§ ((π₯β2) / π) β€ π₯) β π β€ π₯)) |
59 | 56, 57, 41, 58 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π β€ ((π₯β2) / π) β§ ((π₯β2) / π) β€ π₯) β π β€ π₯)) |
60 | 54, 59 | mpan2d 693 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β€ ((π₯β2) / π) β π β€ π₯)) |
61 | 35, 60 | sylbid 239 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β€ ((π₯β2) / π) β π β€ π₯)) |
62 | 61 | pm4.71rd 564 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β€ ((π₯β2) / π) β (π β€ π₯ β§ π β€ ((π₯β2) / π)))) |
63 | | nnge1 12188 |
. . . . . . . . . . . . . 14
β’ (π β β β 1 β€
π) |
64 | 63 | ad2antrl 727 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β 1 β€ π) |
65 | | 1re 11162 |
. . . . . . . . . . . . . . 15
β’ 1 β
β |
66 | | 0lt1 11684 |
. . . . . . . . . . . . . . 15
β’ 0 <
1 |
67 | 65, 66 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’ (1 β
β β§ 0 < 1) |
68 | 22 | rpregt0d 12970 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β β β§ 0 < π)) |
69 | 18 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π₯β2) β
β+) |
70 | 69 | rpregt0d 12970 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π₯β2) β β β§ 0 < (π₯β2))) |
71 | | lediv2 12052 |
. . . . . . . . . . . . . 14
β’ (((1
β β β§ 0 < 1) β§ (π β β β§ 0 < π) β§ ((π₯β2) β β β§ 0 < (π₯β2))) β (1 β€ π β ((π₯β2) / π) β€ ((π₯β2) / 1))) |
72 | 67, 68, 70, 71 | mp3an2i 1467 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (1 β€ π β ((π₯β2) / π) β€ ((π₯β2) / 1))) |
73 | 64, 72 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π₯β2) / π) β€ ((π₯β2) / 1)) |
74 | 20 | recnd 11190 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π₯β2) β β) |
75 | 74 | div1d 11930 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π₯β2) / 1) = (π₯β2)) |
76 | 73, 75 | breqtrd 5136 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π₯β2) / π) β€ (π₯β2)) |
77 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β
(β€β₯β((ββπ₯) + 1))) β π β β) |
78 | | nndivre 12201 |
. . . . . . . . . . . . 13
β’ (((π₯β2) β β β§
π β β) β
((π₯β2) / π) β
β) |
79 | 19, 77, 78 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π₯β2) / π) β β) |
80 | | letr 11256 |
. . . . . . . . . . . 12
β’ ((π β β β§ ((π₯β2) / π) β β β§ (π₯β2) β β) β ((π β€ ((π₯β2) / π) β§ ((π₯β2) / π) β€ (π₯β2)) β π β€ (π₯β2))) |
81 | 14, 79, 20, 80 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π β€ ((π₯β2) / π) β§ ((π₯β2) / π) β€ (π₯β2)) β π β€ (π₯β2))) |
82 | 76, 81 | mpan2d 693 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β€ ((π₯β2) / π) β π β€ (π₯β2))) |
83 | 35, 82 | sylbird 260 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β€ ((π₯β2) / π) β π β€ (π₯β2))) |
84 | 83 | pm4.71rd 564 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β€ ((π₯β2) / π) β (π β€ (π₯β2) β§ π β€ ((π₯β2) / π)))) |
85 | 35, 62, 84 | 3bitr3d 309 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π β€ π₯ β§ π β€ ((π₯β2) / π)) β (π β€ (π₯β2) β§ π β€ ((π₯β2) / π)))) |
86 | | fznnfl 13774 |
. . . . . . . . . 10
β’ (π₯ β β β (π β
(1...(ββπ₯))
β (π β β
β§ π β€ π₯))) |
87 | 86 | baibd 541 |
. . . . . . . . 9
β’ ((π₯ β β β§ π β β) β (π β
(1...(ββπ₯))
β π β€ π₯)) |
88 | 41, 21, 87 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β (1...(ββπ₯)) β π β€ π₯)) |
89 | 79 | flcld 13710 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (ββ((π₯β2) / π)) β β€) |
90 | | elfz5 13440 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β((ββπ₯) + 1)) β§ (ββ((π₯β2) / π)) β β€) β (π β (((ββπ₯) + 1)...(ββ((π₯β2) / π))) β π β€ (ββ((π₯β2) / π)))) |
91 | 30, 89, 90 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β (((ββπ₯) + 1)...(ββ((π₯β2) / π))) β π β€ (ββ((π₯β2) / π)))) |
92 | | flge 13717 |
. . . . . . . . . 10
β’ ((((π₯β2) / π) β β β§ π β β€) β (π β€ ((π₯β2) / π) β π β€ (ββ((π₯β2) / π)))) |
93 | 79, 13, 92 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β€ ((π₯β2) / π) β π β€ (ββ((π₯β2) / π)))) |
94 | 91, 93 | bitr4d 282 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β (((ββπ₯) + 1)...(ββ((π₯β2) / π))) β π β€ ((π₯β2) / π))) |
95 | 88, 94 | anbi12d 632 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π β (1...(ββπ₯)) β§ π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))) β (π β€ π₯ β§ π β€ ((π₯β2) / π)))) |
96 | 20 | flcld 13710 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (ββ(π₯β2)) β
β€) |
97 | | elfz5 13440 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β((ββπ₯) + 1)) β§ (ββ(π₯β2)) β β€) β
(π β
(((ββπ₯) +
1)...(ββ(π₯β2))) β π β€ (ββ(π₯β2)))) |
98 | 30, 96, 97 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β (((ββπ₯) + 1)...(ββ(π₯β2))) β π β€ (ββ(π₯β2)))) |
99 | | flge 13717 |
. . . . . . . . . 10
β’ (((π₯β2) β β β§
π β β€) β
(π β€ (π₯β2) β π β€ (ββ(π₯β2)))) |
100 | 20, 13, 99 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β€ (π₯β2) β π β€ (ββ(π₯β2)))) |
101 | 98, 100 | bitr4d 282 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β (((ββπ₯) + 1)...(ββ(π₯β2))) β π β€ (π₯β2))) |
102 | | fznnfl 13774 |
. . . . . . . . . 10
β’ (((π₯β2) / π) β β β (π β (1...(ββ((π₯β2) / π))) β (π β β β§ π β€ ((π₯β2) / π)))) |
103 | 102 | baibd 541 |
. . . . . . . . 9
β’ ((((π₯β2) / π) β β β§ π β β) β (π β (1...(ββ((π₯β2) / π))) β π β€ ((π₯β2) / π))) |
104 | 57, 21, 103 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β (π β (1...(ββ((π₯β2) / π))) β π β€ ((π₯β2) / π))) |
105 | 101, 104 | anbi12d 632 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π β (((ββπ₯) + 1)...(ββ(π₯β2))) β§ π β (1...(ββ((π₯β2) / π)))) β (π β€ (π₯β2) β§ π β€ ((π₯β2) / π)))) |
106 | 85, 95, 105 | 3bitr4d 311 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ (π β β β§ π β
(β€β₯β((ββπ₯) + 1)))) β ((π β (1...(ββπ₯)) β§ π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))) β (π β (((ββπ₯) + 1)...(ββ(π₯β2))) β§ π β (1...(ββ((π₯β2) / π)))))) |
107 | 106 | ex 414 |
. . . . 5
β’ ((π β§ π₯ β β+) β ((π β β β§ π β
(β€β₯β((ββπ₯) + 1))) β ((π β (1...(ββπ₯)) β§ π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))) β (π β (((ββπ₯) + 1)...(ββ(π₯β2))) β§ π β (1...(ββ((π₯β2) / π))))))) |
108 | 7, 11, 107 | pm5.21ndd 381 |
. . . 4
β’ ((π β§ π₯ β β+) β ((π β
(1...(ββπ₯))
β§ π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π)))) β (π β (((ββπ₯) + 1)...(ββ(π₯β2))) β§ π β (1...(ββ((π₯β2) / π)))))) |
109 | | ssun2 4138 |
. . . . . . . 8
β’
(((ββπ₯)
+ 1)...(ββ((π₯β2) / π))) β ((1...(ββπ₯)) βͺ (((ββπ₯) + 1)...(ββ((π₯β2) / π)))) |
110 | 28 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ₯) +
1) β β) |
111 | | nnuz 12813 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
112 | 110, 111 | eleqtrdi 2848 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ₯) +
1) β (β€β₯β1)) |
113 | | dchrisum0lem1a 26850 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (π₯ β€ ((π₯β2) / π) β§ (ββ((π₯β2) / π)) β
(β€β₯β(ββπ₯)))) |
114 | 113 | simprd 497 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββ((π₯β2) / π)) β
(β€β₯β(ββπ₯))) |
115 | | fzsplit2 13473 |
. . . . . . . . 9
β’
((((ββπ₯)
+ 1) β (β€β₯β1) β§ (ββ((π₯β2) / π)) β
(β€β₯β(ββπ₯))) β (1...(ββ((π₯β2) / π))) = ((1...(ββπ₯)) βͺ (((ββπ₯) + 1)...(ββ((π₯β2) / π))))) |
116 | 112, 114,
115 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1...(ββ((π₯β2) / π))) = ((1...(ββπ₯)) βͺ (((ββπ₯) + 1)...(ββ((π₯β2) / π))))) |
117 | 109, 116 | sseqtrrid 4002 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π))) β (1...(ββ((π₯β2) / π)))) |
118 | 117 | sselda 3949 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π)))) β π β (1...(ββ((π₯β2) / π)))) |
119 | | rpvmasum2.g |
. . . . . . . . 9
β’ πΊ = (DChrβπ) |
120 | | rpvmasum.z |
. . . . . . . . 9
β’ π =
(β€/nβ€βπ) |
121 | | rpvmasum2.d |
. . . . . . . . 9
β’ π· = (BaseβπΊ) |
122 | | rpvmasum.l |
. . . . . . . . 9
β’ πΏ = (β€RHomβπ) |
123 | | rpvmasum2.w |
. . . . . . . . . . . . 13
β’ π = {π¦ β (π· β { 1 }) β£ Ξ£π β β ((π¦β(πΏβπ)) / π) = 0} |
124 | 123 | ssrab3 4045 |
. . . . . . . . . . . 12
β’ π β (π· β { 1 }) |
125 | | dchrisum0.b |
. . . . . . . . . . . 12
β’ (π β π β π) |
126 | 124, 125 | sselid 3947 |
. . . . . . . . . . 11
β’ (π β π β (π· β { 1 })) |
127 | 126 | eldifad 3927 |
. . . . . . . . . 10
β’ (π β π β π·) |
128 | 127 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β π β π·) |
129 | | elfzelz 13448 |
. . . . . . . . . 10
β’ (π β
(1...(ββ((π₯β2) / π))) β π β β€) |
130 | 129 | adantl 483 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β π β β€) |
131 | 119, 120,
121, 122, 128, 130 | dchrzrhcl 26609 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (πβ(πΏβπ)) β β) |
132 | | elfznn 13477 |
. . . . . . . . . . . 12
β’ (π β
(1...(ββ((π₯β2) / π))) β π β β) |
133 | 132 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β π β β) |
134 | 133 | nnrpd 12962 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β π β β+) |
135 | 134 | rpsqrtcld 15303 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (ββπ) β
β+) |
136 | 135 | rpcnd 12966 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (ββπ) β β) |
137 | 135 | rpne0d 12969 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (ββπ) β 0) |
138 | 131, 136,
137 | divcld 11938 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β ((πβ(πΏβπ)) / (ββπ)) β β) |
139 | 4 | adantl 483 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β) |
140 | 139 | nnrpd 12962 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β π β
β+) |
141 | 140 | rpsqrtcld 15303 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββπ)
β β+) |
142 | 141 | rpcnne0d 12973 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ)
β β β§ (ββπ) β 0)) |
143 | 142 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β ((ββπ) β β β§
(ββπ) β
0)) |
144 | 143 | simpld 496 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (ββπ) β β) |
145 | 143 | simprd 497 |
. . . . . . 7
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (ββπ) β 0) |
146 | 138, 144,
145 | divcld 11938 |
. . . . . 6
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(1...(ββ((π₯β2) / π)))) β (((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
147 | 118, 146 | syldan 592 |
. . . . 5
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π)))) β (((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
148 | 147 | anasss 468 |
. . . 4
β’ (((π β§ π₯ β β+) β§ (π β
(1...(ββπ₯))
β§ π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π))))) β (((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
149 | 1, 2, 3, 108, 148 | fsumcom2 15666 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = Ξ£π β (((ββπ₯) + 1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) |
150 | 149 | mpteq2dva 5210 |
. 2
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) = (π₯ β β+ β¦
Ξ£π β
(((ββπ₯) +
1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)))) |
151 | 65 | a1i 11 |
. . 3
β’ (π β 1 β
β) |
152 | | 2cn 12235 |
. . . . . . . 8
β’ 2 β
β |
153 | 15 | rpsqrtcld 15303 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β+) |
154 | 153 | rpcnd 12966 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
β) |
155 | | mulcl 11142 |
. . . . . . . 8
β’ ((2
β β β§ (ββπ₯) β β) β (2 Β·
(ββπ₯)) β
β) |
156 | 152, 154,
155 | sylancr 588 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β (2
Β· (ββπ₯))
β β) |
157 | 141 | rprecred 12975 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / (ββπ)) β β) |
158 | 1, 157 | fsumrecl 15626 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
β) |
159 | 158 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
β) |
160 | 159, 156 | subcld 11519 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯))) β β) |
161 | | 2re 12234 |
. . . . . . . . . . 11
β’ 2 β
β |
162 | | dchrisum0.c |
. . . . . . . . . . . . 13
β’ (π β πΆ β (0[,)+β)) |
163 | | elrege0 13378 |
. . . . . . . . . . . . 13
β’ (πΆ β (0[,)+β) β
(πΆ β β β§ 0
β€ πΆ)) |
164 | 162, 163 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β (πΆ β β β§ 0 β€ πΆ)) |
165 | 164 | simpld 496 |
. . . . . . . . . . 11
β’ (π β πΆ β β) |
166 | | remulcl 11143 |
. . . . . . . . . . 11
β’ ((2
β β β§ πΆ
β β) β (2 Β· πΆ) β β) |
167 | 161, 165,
166 | sylancr 588 |
. . . . . . . . . 10
β’ (π β (2 Β· πΆ) β
β) |
168 | 167 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β (2
Β· πΆ) β
β) |
169 | 168, 153 | rerpdivcld 12995 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β ((2
Β· πΆ) /
(ββπ₯)) β
β) |
170 | 169 | recnd 11190 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β ((2
Β· πΆ) /
(ββπ₯)) β
β) |
171 | 156, 160,
170 | adddird 11187 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (((2
Β· (ββπ₯))
+ (Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯)))) Β· ((2 Β· πΆ) / (ββπ₯))) = (((2 Β· (ββπ₯)) Β· ((2 Β· πΆ) / (ββπ₯))) + ((Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯))) Β· ((2 Β· πΆ) / (ββπ₯))))) |
172 | 156, 159 | pncan3d 11522 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β ((2
Β· (ββπ₯))
+ (Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯)))) = Ξ£π β (1...(ββπ₯))(1 / (ββπ))) |
173 | 172 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (((2
Β· (ββπ₯))
+ (Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯)))) Β· ((2 Β· πΆ) / (ββπ₯))) = (Ξ£π β (1...(ββπ₯))(1 / (ββπ)) Β· ((2 Β· πΆ) / (ββπ₯)))) |
174 | | 2cnd 12238 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β 2 β
β) |
175 | 174, 154,
170 | mulassd 11185 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β ((2
Β· (ββπ₯))
Β· ((2 Β· πΆ) /
(ββπ₯))) = (2
Β· ((ββπ₯)
Β· ((2 Β· πΆ) /
(ββπ₯))))) |
176 | 168 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β (2
Β· πΆ) β
β) |
177 | 153 | rpne0d 12969 |
. . . . . . . . . 10
β’ ((π β§ π₯ β β+) β
(ββπ₯) β
0) |
178 | 176, 154,
177 | divcan2d 11940 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
((ββπ₯) Β·
((2 Β· πΆ) /
(ββπ₯))) = (2
Β· πΆ)) |
179 | 178 | oveq2d 7378 |
. . . . . . . 8
β’ ((π β§ π₯ β β+) β (2
Β· ((ββπ₯)
Β· ((2 Β· πΆ) /
(ββπ₯)))) = (2
Β· (2 Β· πΆ))) |
180 | 175, 179 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β ((2
Β· (ββπ₯))
Β· ((2 Β· πΆ) /
(ββπ₯))) = (2
Β· (2 Β· πΆ))) |
181 | 180 | oveq1d 7377 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (((2
Β· (ββπ₯))
Β· ((2 Β· πΆ) /
(ββπ₯))) +
((Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯))) Β· ((2 Β· πΆ) / (ββπ₯)))) = ((2 Β· (2 Β· πΆ)) + ((Ξ£π β (1...(ββπ₯))(1 / (ββπ)) β (2 Β·
(ββπ₯)))
Β· ((2 Β· πΆ) /
(ββπ₯))))) |
182 | 171, 173,
181 | 3eqtr3d 2785 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯))) = ((2
Β· (2 Β· πΆ)) +
((Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯))) Β· ((2 Β· πΆ) / (ββπ₯))))) |
183 | 182 | mpteq2dva 5210 |
. . . 4
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯)))) =
(π₯ β
β+ β¦ ((2 Β· (2 Β· πΆ)) + ((Ξ£π β (1...(ββπ₯))(1 / (ββπ)) β (2 Β·
(ββπ₯)))
Β· ((2 Β· πΆ) /
(ββπ₯)))))) |
184 | | remulcl 11143 |
. . . . . . . 8
β’ ((2
β β β§ (2 Β· πΆ) β β) β (2 Β· (2
Β· πΆ)) β
β) |
185 | 161, 167,
184 | sylancr 588 |
. . . . . . 7
β’ (π β (2 Β· (2 Β·
πΆ)) β
β) |
186 | 185 | recnd 11190 |
. . . . . 6
β’ (π β (2 Β· (2 Β·
πΆ)) β
β) |
187 | 186 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β β+) β (2
Β· (2 Β· πΆ))
β β) |
188 | 160, 170 | mulcld 11182 |
. . . . 5
β’ ((π β§ π₯ β β+) β
((Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯))) Β· ((2 Β· πΆ) / (ββπ₯))) β β) |
189 | | rpssre 12929 |
. . . . . 6
β’
β+ β β |
190 | | o1const 15509 |
. . . . . 6
β’
((β+ β β β§ (2 Β· (2 Β·
πΆ)) β β) β
(π₯ β
β+ β¦ (2 Β· (2 Β· πΆ))) β π(1)) |
191 | 189, 186,
190 | sylancr 588 |
. . . . 5
β’ (π β (π₯ β β+ β¦ (2
Β· (2 Β· πΆ)))
β π(1)) |
192 | | eqid 2737 |
. . . . . . . 8
β’ (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯)))) = (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯)))) |
193 | 192 | divsqrsum 26347 |
. . . . . . 7
β’ (π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯)))) β dom
βπ |
194 | | rlimdmo1 15507 |
. . . . . . 7
β’ ((π₯ β β+
β¦ (Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯)))) β dom βπ
β (π₯ β
β+ β¦ (Ξ£π β (1...(ββπ₯))(1 / (ββπ)) β (2 Β·
(ββπ₯)))) β
π(1)) |
195 | 193, 194 | mp1i 13 |
. . . . . 6
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯)))) β π(1)) |
196 | 176, 154,
177 | divrecd 11941 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β ((2
Β· πΆ) /
(ββπ₯)) = ((2
Β· πΆ) Β· (1 /
(ββπ₯)))) |
197 | 196 | mpteq2dva 5210 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ ((2
Β· πΆ) /
(ββπ₯))) =
(π₯ β
β+ β¦ ((2 Β· πΆ) Β· (1 / (ββπ₯))))) |
198 | 153 | rprecred 12975 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β (1 /
(ββπ₯)) β
β) |
199 | 167 | recnd 11190 |
. . . . . . . . . 10
β’ (π β (2 Β· πΆ) β
β) |
200 | | rlimconst 15433 |
. . . . . . . . . 10
β’
((β+ β β β§ (2 Β· πΆ) β β) β (π₯ β β+
β¦ (2 Β· πΆ))
βπ (2 Β· πΆ)) |
201 | 189, 199,
200 | sylancr 588 |
. . . . . . . . 9
β’ (π β (π₯ β β+ β¦ (2
Β· πΆ))
βπ (2 Β· πΆ)) |
202 | | sqrtlim 26338 |
. . . . . . . . . 10
β’ (π₯ β β+
β¦ (1 / (ββπ₯))) βπ
0 |
203 | 202 | a1i 11 |
. . . . . . . . 9
β’ (π β (π₯ β β+ β¦ (1 /
(ββπ₯)))
βπ 0) |
204 | 168, 198,
201, 203 | rlimmul 15535 |
. . . . . . . 8
β’ (π β (π₯ β β+ β¦ ((2
Β· πΆ) Β· (1 /
(ββπ₯))))
βπ ((2 Β· πΆ) Β· 0)) |
205 | 197, 204 | eqbrtrd 5132 |
. . . . . . 7
β’ (π β (π₯ β β+ β¦ ((2
Β· πΆ) /
(ββπ₯)))
βπ ((2 Β· πΆ) Β· 0)) |
206 | | rlimo1 15506 |
. . . . . . 7
β’ ((π₯ β β+
β¦ ((2 Β· πΆ) /
(ββπ₯)))
βπ ((2 Β· πΆ) Β· 0) β (π₯ β β+ β¦ ((2
Β· πΆ) /
(ββπ₯))) β
π(1)) |
207 | 205, 206 | syl 17 |
. . . . . 6
β’ (π β (π₯ β β+ β¦ ((2
Β· πΆ) /
(ββπ₯))) β
π(1)) |
208 | 160, 170,
195, 207 | o1mul2 15514 |
. . . . 5
β’ (π β (π₯ β β+ β¦
((Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯))) Β· ((2 Β· πΆ) / (ββπ₯)))) β π(1)) |
209 | 187, 188,
191, 208 | o1add2 15513 |
. . . 4
β’ (π β (π₯ β β+ β¦ ((2
Β· (2 Β· πΆ)) +
((Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) β
(2 Β· (ββπ₯))) Β· ((2 Β· πΆ) / (ββπ₯))))) β π(1)) |
210 | 183, 209 | eqeltrd 2838 |
. . 3
β’ (π β (π₯ β β+ β¦
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯)))) β
π(1)) |
211 | 158, 169 | remulcld 11192 |
. . 3
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯))) β
β) |
212 | 3, 147 | fsumcl 15625 |
. . . 4
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
213 | 1, 212 | fsumcl 15625 |
. . 3
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)) β β) |
214 | 213 | abscld 15328 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β β) |
215 | 211 | recnd 11190 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯))) β
β) |
216 | 215 | abscld 15328 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(absβ(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯)))) β
β) |
217 | 212 | abscld 15328 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβΞ£π
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β β) |
218 | 1, 217 | fsumrecl 15626 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(absβΞ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β β) |
219 | 1, 212 | fsumabs 15693 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β€ Ξ£π β (1...(ββπ₯))(absβΞ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)))) |
220 | 169 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((2 Β· πΆ) /
(ββπ₯)) β
β) |
221 | 157, 220 | remulcld 11192 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((1 / (ββπ)) Β· ((2 Β· πΆ) / (ββπ₯))) β β) |
222 | 118, 138 | syldan 592 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β§ π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π)))) β ((πβ(πΏβπ)) / (ββπ)) β β) |
223 | 3, 222 | fsumcl 15625 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β Ξ£π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ)) β β) |
224 | 223 | abscld 15328 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβΞ£π
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ))) β β) |
225 | | rpvmasum.a |
. . . . . . . . . . 11
β’ (π β π β β) |
226 | | rpvmasum2.1 |
. . . . . . . . . . 11
β’ 1 =
(0gβπΊ) |
227 | | dchrisum0lem1.f |
. . . . . . . . . . 11
β’ πΉ = (π β β β¦ ((πβ(πΏβπ)) / (ββπ))) |
228 | | dchrisum0.s |
. . . . . . . . . . 11
β’ (π β seq1( + , πΉ) β π) |
229 | | dchrisum0.1 |
. . . . . . . . . . 11
β’ (π β βπ¦ β (1[,)+β)(absβ((seq1( + ,
πΉ)β(ββπ¦)) β π)) β€ (πΆ / (ββπ¦))) |
230 | 120, 122,
225, 119, 121, 226, 123, 125, 227, 162, 228, 229 | dchrisum0lem1b 26879 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβΞ£π
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ))) β€ ((2 Β· πΆ) / (ββπ₯))) |
231 | 224, 220,
141, 230 | lediv1dd 13022 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβΞ£π
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ))) / (ββπ)) β€ (((2 Β· πΆ) / (ββπ₯)) / (ββπ))) |
232 | 141 | rpcnd 12966 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββπ)
β β) |
233 | 141 | rpne0d 12969 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (ββπ)
β 0) |
234 | 223, 232,
233 | absdivd 15347 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(Ξ£π
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ)) / (ββπ))) = ((absβΞ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ))) / (absβ(ββπ)))) |
235 | 3, 232, 222, 233 | fsumdivc 15678 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (Ξ£π β
(((ββπ₯) +
1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ)) / (ββπ)) = Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) |
236 | 235 | fveq2d 6851 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(Ξ£π
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ)) / (ββπ))) = (absβΞ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)))) |
237 | 141 | rprege0d 12971 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((ββπ)
β β β§ 0 β€ (ββπ))) |
238 | | absid 15188 |
. . . . . . . . . . . 12
β’
(((ββπ)
β β β§ 0 β€ (ββπ)) β (absβ(ββπ)) = (ββπ)) |
239 | 237, 238 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβ(ββπ)) = (ββπ)) |
240 | 239 | oveq2d 7378 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβΞ£π
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ))) / (absβ(ββπ))) = ((absβΞ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ))) / (ββπ))) |
241 | 234, 236,
240 | 3eqtr3rd 2786 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((absβΞ£π
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π)))((πβ(πΏβπ)) / (ββπ))) / (ββπ)) = (absβΞ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ)))) |
242 | 170 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β ((2 Β· πΆ) /
(ββπ₯)) β
β) |
243 | 242, 232,
233 | divrec2d 11942 |
. . . . . . . . 9
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (((2 Β· πΆ) /
(ββπ₯)) /
(ββπ)) = ((1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯)))) |
244 | 231, 241,
243 | 3brtr3d 5141 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (absβΞ£π
β (((ββπ₯)
+ 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β€ ((1 / (ββπ)) Β· ((2 Β· πΆ) / (ββπ₯)))) |
245 | 1, 217, 221, 244 | fsumle 15691 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(absβΞ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β€ Ξ£π β (1...(ββπ₯))((1 / (ββπ)) Β· ((2 Β· πΆ) / (ββπ₯)))) |
246 | 157 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(1...(ββπ₯)))
β (1 / (ββπ)) β β) |
247 | 1, 170, 246 | fsummulc1 15677 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯))) =
Ξ£π β
(1...(ββπ₯))((1
/ (ββπ))
Β· ((2 Β· πΆ) /
(ββπ₯)))) |
248 | 245, 247 | breqtrrd 5138 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
Ξ£π β
(1...(ββπ₯))(absβΞ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β€ (Ξ£π β (1...(ββπ₯))(1 / (ββπ)) Β· ((2 Β· πΆ) / (ββπ₯)))) |
249 | 214, 218,
211, 219, 248 | letrd 11319 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β€ (Ξ£π β (1...(ββπ₯))(1 / (ββπ)) Β· ((2 Β· πΆ) / (ββπ₯)))) |
250 | 211 | leabsd 15306 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯))) β€
(absβ(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯))))) |
251 | 214, 211,
216, 249, 250 | letrd 11319 |
. . . 4
β’ ((π β§ π₯ β β+) β
(absβΞ£π β
(1...(ββπ₯))Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β€ (absβ(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯))))) |
252 | 251 | adantrr 716 |
. . 3
β’ ((π β§ (π₯ β β+ β§ 1 β€
π₯)) β
(absβΞ£π β
(1...(ββπ₯))Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β€ (absβ(Ξ£π β
(1...(ββπ₯))(1 /
(ββπ)) Β·
((2 Β· πΆ) /
(ββπ₯))))) |
253 | 151, 210,
211, 213, 252 | o1le 15544 |
. 2
β’ (π β (π₯ β β+ β¦
Ξ£π β
(1...(ββπ₯))Ξ£π β (((ββπ₯) + 1)...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β π(1)) |
254 | 150, 253 | eqeltrrd 2839 |
1
β’ (π β (π₯ β β+ β¦
Ξ£π β
(((ββπ₯) +
1)...(ββ(π₯β2)))Ξ£π β (1...(ββ((π₯β2) / π)))(((πβ(πΏβπ)) / (ββπ)) / (ββπ))) β π(1)) |