Step | Hyp | Ref
| Expression |
1 | | fzofi 13879 |
. . . . . 6
β’ (π..^π) β Fin |
2 | 1 | a1i 11 |
. . . . 5
β’ (π β (π..^π) β Fin) |
3 | | dvfsumabs.x |
. . . . 5
β’ ((π β§ π β (π..^π)) β π β β) |
4 | | dvfsumabs.m |
. . . . . . . . . . . . 13
β’ (π β π β (β€β₯βπ)) |
5 | | eluzel2 12768 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β π β β€) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
7 | | eluzelz 12773 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯βπ) β π β β€) |
8 | 4, 7 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
9 | | fzval2 13427 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€) β (π...π) = ((π[,]π) β© β€)) |
10 | 6, 8, 9 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β (π...π) = ((π[,]π) β© β€)) |
11 | | inss1 4188 |
. . . . . . . . . . 11
β’ ((π[,]π) β© β€) β (π[,]π) |
12 | 10, 11 | eqsstrdi 3998 |
. . . . . . . . . 10
β’ (π β (π...π) β (π[,]π)) |
13 | 12 | sselda 3944 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π...π)) β π¦ β (π[,]π)) |
14 | | dvfsumabs.a |
. . . . . . . . . . . 12
β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) |
15 | | cncff 24256 |
. . . . . . . . . . . 12
β’ ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
17 | | eqid 2736 |
. . . . . . . . . . . 12
β’ (π₯ β (π[,]π) β¦ π΄) = (π₯ β (π[,]π) β¦ π΄) |
18 | 17 | fmpt 7058 |
. . . . . . . . . . 11
β’
(βπ₯ β
(π[,]π)π΄ β β β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
19 | 16, 18 | sylibr 233 |
. . . . . . . . . 10
β’ (π β βπ₯ β (π[,]π)π΄ β β) |
20 | | nfcsb1v 3880 |
. . . . . . . . . . . 12
β’
β²π₯β¦π¦ / π₯β¦π΄ |
21 | 20 | nfel1 2923 |
. . . . . . . . . . 11
β’
β²π₯β¦π¦ / π₯β¦π΄ β β |
22 | | csbeq1a 3869 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β π΄ = β¦π¦ / π₯β¦π΄) |
23 | 22 | eleq1d 2822 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π΄ β β β β¦π¦ / π₯β¦π΄ β β)) |
24 | 21, 23 | rspc 3569 |
. . . . . . . . . 10
β’ (π¦ β (π[,]π) β (βπ₯ β (π[,]π)π΄ β β β β¦π¦ / π₯β¦π΄ β β)) |
25 | 19, 24 | mpan9 507 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π[,]π)) β β¦π¦ / π₯β¦π΄ β β) |
26 | 13, 25 | syldan 591 |
. . . . . . . 8
β’ ((π β§ π¦ β (π...π)) β β¦π¦ / π₯β¦π΄ β β) |
27 | 26 | ralrimiva 3143 |
. . . . . . 7
β’ (π β βπ¦ β (π...π)β¦π¦ / π₯β¦π΄ β β) |
28 | | fzofzp1 13669 |
. . . . . . 7
β’ (π β (π..^π) β (π + 1) β (π...π)) |
29 | | csbeq1 3858 |
. . . . . . . . 9
β’ (π¦ = (π + 1) β β¦π¦ / π₯β¦π΄ = β¦(π + 1) / π₯β¦π΄) |
30 | 29 | eleq1d 2822 |
. . . . . . . 8
β’ (π¦ = (π + 1) β (β¦π¦ / π₯β¦π΄ β β β β¦(π + 1) / π₯β¦π΄ β β)) |
31 | 30 | rspccva 3580 |
. . . . . . 7
β’
((βπ¦ β
(π...π)β¦π¦ / π₯β¦π΄ β β β§ (π + 1) β (π...π)) β β¦(π + 1) / π₯β¦π΄ β β) |
32 | 27, 28, 31 | syl2an 596 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β β¦(π + 1) / π₯β¦π΄ β β) |
33 | | elfzofz 13588 |
. . . . . . 7
β’ (π β (π..^π) β π β (π...π)) |
34 | | csbeq1 3858 |
. . . . . . . . 9
β’ (π¦ = π β β¦π¦ / π₯β¦π΄ = β¦π / π₯β¦π΄) |
35 | 34 | eleq1d 2822 |
. . . . . . . 8
β’ (π¦ = π β (β¦π¦ / π₯β¦π΄ β β β β¦π / π₯β¦π΄ β β)) |
36 | 35 | rspccva 3580 |
. . . . . . 7
β’
((βπ¦ β
(π...π)β¦π¦ / π₯β¦π΄ β β β§ π β (π...π)) β β¦π / π₯β¦π΄ β β) |
37 | 27, 33, 36 | syl2an 596 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β β¦π / π₯β¦π΄ β β) |
38 | 32, 37 | subcld 11512 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄) β β) |
39 | 2, 3, 38 | fsumsub 15673 |
. . . 4
β’ (π β Ξ£π β (π..^π)(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) = (Ξ£π β (π..^π)π β Ξ£π β (π..^π)(β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) |
40 | | vex 3449 |
. . . . . . . 8
β’ π¦ β V |
41 | 40 | a1i 11 |
. . . . . . 7
β’ (π¦ = π β π¦ β V) |
42 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π¦ = π β (π₯ = π¦ β π₯ = π)) |
43 | 42 | biimpa 477 |
. . . . . . . 8
β’ ((π¦ = π β§ π₯ = π¦) β π₯ = π) |
44 | | dvfsumabs.c |
. . . . . . . 8
β’ (π₯ = π β π΄ = πΆ) |
45 | 43, 44 | syl 17 |
. . . . . . 7
β’ ((π¦ = π β§ π₯ = π¦) β π΄ = πΆ) |
46 | 41, 45 | csbied 3893 |
. . . . . 6
β’ (π¦ = π β β¦π¦ / π₯β¦π΄ = πΆ) |
47 | 40 | a1i 11 |
. . . . . . 7
β’ (π¦ = π β π¦ β V) |
48 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π¦ = π β (π₯ = π¦ β π₯ = π)) |
49 | 48 | biimpa 477 |
. . . . . . . 8
β’ ((π¦ = π β§ π₯ = π¦) β π₯ = π) |
50 | | dvfsumabs.d |
. . . . . . . 8
β’ (π₯ = π β π΄ = π·) |
51 | 49, 50 | syl 17 |
. . . . . . 7
β’ ((π¦ = π β§ π₯ = π¦) β π΄ = π·) |
52 | 47, 51 | csbied 3893 |
. . . . . 6
β’ (π¦ = π β β¦π¦ / π₯β¦π΄ = π·) |
53 | 34, 29, 46, 52, 4, 26 | telfsumo2 15688 |
. . . . 5
β’ (π β Ξ£π β (π..^π)(β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄) = (π· β πΆ)) |
54 | 53 | oveq2d 7373 |
. . . 4
β’ (π β (Ξ£π β (π..^π)π β Ξ£π β (π..^π)(β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) = (Ξ£π β (π..^π)π β (π· β πΆ))) |
55 | 39, 54 | eqtrd 2776 |
. . 3
β’ (π β Ξ£π β (π..^π)(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) = (Ξ£π β (π..^π)π β (π· β πΆ))) |
56 | 55 | fveq2d 6846 |
. 2
β’ (π β (absβΞ£π β (π..^π)(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) = (absβ(Ξ£π β (π..^π)π β (π· β πΆ)))) |
57 | 3, 38 | subcld 11512 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) β β) |
58 | 2, 57 | fsumcl 15618 |
. . . 4
β’ (π β Ξ£π β (π..^π)(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) β β) |
59 | 58 | abscld 15321 |
. . 3
β’ (π β (absβΞ£π β (π..^π)(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) β β) |
60 | 57 | abscld 15321 |
. . . 4
β’ ((π β§ π β (π..^π)) β (absβ(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) β β) |
61 | 2, 60 | fsumrecl 15619 |
. . 3
β’ (π β Ξ£π β (π..^π)(absβ(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) β β) |
62 | | dvfsumabs.y |
. . . 4
β’ ((π β§ π β (π..^π)) β π β β) |
63 | 2, 62 | fsumrecl 15619 |
. . 3
β’ (π β Ξ£π β (π..^π)π β β) |
64 | 2, 57 | fsumabs 15686 |
. . 3
β’ (π β (absβΞ£π β (π..^π)(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) β€ Ξ£π β (π..^π)(absβ(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)))) |
65 | | elfzoelz 13572 |
. . . . . . . . . 10
β’ (π β (π..^π) β π β β€) |
66 | 65 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β π β β€) |
67 | 66 | zred 12607 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β π β β) |
68 | 67 | rexrd 11205 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β π β β*) |
69 | | peano2re 11328 |
. . . . . . . . 9
β’ (π β β β (π + 1) β
β) |
70 | 67, 69 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (π + 1) β β) |
71 | 70 | rexrd 11205 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β (π + 1) β
β*) |
72 | 67 | lep1d 12086 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β π β€ (π + 1)) |
73 | | ubicc2 13382 |
. . . . . . 7
β’ ((π β β*
β§ (π + 1) β
β* β§ π
β€ (π + 1)) β (π + 1) β (π[,](π + 1))) |
74 | 68, 71, 72, 73 | syl3anc 1371 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π + 1) β (π[,](π + 1))) |
75 | | lbicc2 13381 |
. . . . . . 7
β’ ((π β β*
β§ (π + 1) β
β* β§ π
β€ (π + 1)) β π β (π[,](π + 1))) |
76 | 68, 71, 72, 75 | syl3anc 1371 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β π β (π[,](π + 1))) |
77 | 6 | zred 12607 |
. . . . . . . . . . . 12
β’ (π β π β β) |
78 | 77 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β π β β) |
79 | 8 | zred 12607 |
. . . . . . . . . . . 12
β’ (π β π β β) |
80 | 79 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β π β β) |
81 | | elfzole1 13580 |
. . . . . . . . . . . 12
β’ (π β (π..^π) β π β€ π) |
82 | 81 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β π β€ π) |
83 | 28 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (π + 1) β (π...π)) |
84 | | elfzle2 13445 |
. . . . . . . . . . . 12
β’ ((π + 1) β (π...π) β (π + 1) β€ π) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (π + 1) β€ π) |
86 | | iccss 13332 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β) β§ (π β€ π β§ (π + 1) β€ π)) β (π[,](π + 1)) β (π[,]π)) |
87 | 78, 80, 82, 85, 86 | syl22anc 837 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π[,](π + 1)) β (π[,]π)) |
88 | 87 | resmptd 5994 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β ((π₯ β (π[,]π) β¦ ((π Β· π₯) β π΄)) βΎ (π[,](π + 1))) = (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))) |
89 | | eqid 2736 |
. . . . . . . . . . 11
β’
(TopOpenββfld) =
(TopOpenββfld) |
90 | 89 | subcn 24229 |
. . . . . . . . . . . 12
β’ β
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
91 | 90 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β β β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
92 | | iccssre 13346 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β) β (π[,]π) β β) |
93 | 77, 79, 92 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ (π β (π[,]π) β β) |
94 | 93 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π..^π)) β (π[,]π) β β) |
95 | | ax-resscn 11108 |
. . . . . . . . . . . . . 14
β’ β
β β |
96 | 94, 95 | sstrdi 3956 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β (π[,]π) β β) |
97 | | ssid 3966 |
. . . . . . . . . . . . . 14
β’ β
β β |
98 | 97 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β β β
β) |
99 | | cncfmptc 24275 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π[,]π) β β β§ β β
β) β (π₯ β
(π[,]π) β¦ π) β ((π[,]π)βcnββ)) |
100 | 3, 96, 98, 99 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (π₯ β (π[,]π) β¦ π) β ((π[,]π)βcnββ)) |
101 | | cncfmptid 24276 |
. . . . . . . . . . . . 13
β’ (((π[,]π) β β β§ β β
β) β (π₯ β
(π[,]π) β¦ π₯) β ((π[,]π)βcnββ)) |
102 | 96, 97, 101 | sylancl 586 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (π₯ β (π[,]π) β¦ π₯) β ((π[,]π)βcnββ)) |
103 | 100, 102 | mulcncf 24810 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (π₯ β (π[,]π) β¦ (π Β· π₯)) β ((π[,]π)βcnββ)) |
104 | 14 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) |
105 | 89, 91, 103, 104 | cncfmpt2f 24278 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π₯ β (π[,]π) β¦ ((π Β· π₯) β π΄)) β ((π[,]π)βcnββ)) |
106 | | rescncf 24260 |
. . . . . . . . . 10
β’ ((π[,](π + 1)) β (π[,]π) β ((π₯ β (π[,]π) β¦ ((π Β· π₯) β π΄)) β ((π[,]π)βcnββ) β ((π₯ β (π[,]π) β¦ ((π Β· π₯) β π΄)) βΎ (π[,](π + 1))) β ((π[,](π + 1))βcnββ))) |
107 | 87, 105, 106 | sylc 65 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β ((π₯ β (π[,]π) β¦ ((π Β· π₯) β π΄)) βΎ (π[,](π + 1))) β ((π[,](π + 1))βcnββ)) |
108 | 88, 107 | eqeltrrd 2838 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)) β ((π[,](π + 1))βcnββ)) |
109 | 95 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β β β
β) |
110 | 87, 94 | sstrd 3954 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (π[,](π + 1)) β β) |
111 | 87 | sselda 3944 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π[,](π + 1))) β π₯ β (π[,]π)) |
112 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π..^π)) β§ π₯ β (π[,]π)) β π β β) |
113 | 96 | sselda 3944 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π..^π)) β§ π₯ β (π[,]π)) β π₯ β β) |
114 | 112, 113 | mulcld 11175 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π..^π)) β§ π₯ β (π[,]π)) β (π Β· π₯) β β) |
115 | 19 | r19.21bi 3234 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (π[,]π)) β π΄ β β) |
116 | 115 | adantlr 713 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π..^π)) β§ π₯ β (π[,]π)) β π΄ β β) |
117 | 114, 116 | subcld 11512 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π[,]π)) β ((π Β· π₯) β π΄) β β) |
118 | 111, 117 | syldan 591 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π₯ β (π[,](π + 1))) β ((π Β· π₯) β π΄) β β) |
119 | 89 | tgioo2 24166 |
. . . . . . . . . . . 12
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
120 | | iccntr 24184 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π + 1) β β) β
((intβ(topGenβran (,)))β(π[,](π + 1))) = (π(,)(π + 1))) |
121 | 67, 70, 120 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β ((intβ(topGenβran
(,)))β(π[,](π + 1))) = (π(,)(π + 1))) |
122 | 109, 110,
118, 119, 89, 121 | dvmptntr 25335 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))) = (β D (π₯ β (π(,)(π + 1)) β¦ ((π Β· π₯) β π΄)))) |
123 | | reelprrecn 11143 |
. . . . . . . . . . . . 13
β’ β
β {β, β} |
124 | 123 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β β β {β,
β}) |
125 | | ioossicc 13350 |
. . . . . . . . . . . . . 14
β’ (π(,)π) β (π[,]π) |
126 | 125 | sseli 3940 |
. . . . . . . . . . . . 13
β’ (π₯ β (π(,)π) β π₯ β (π[,]π)) |
127 | 126, 117 | sylan2 593 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β ((π Β· π₯) β π΄) β β) |
128 | | ovex 7390 |
. . . . . . . . . . . . 13
β’ (π β π΅) β V |
129 | 128 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β (π β π΅) β V) |
130 | 126, 114 | sylan2 593 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β (π Β· π₯) β β) |
131 | 3 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β π β β) |
132 | 125, 96 | sstrid 3955 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π..^π)) β (π(,)π) β β) |
133 | 132 | sselda 3944 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β π₯ β β) |
134 | | 1cnd 11150 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β 1 β β) |
135 | 109 | sselda 3944 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π..^π)) β§ π₯ β β) β π₯ β β) |
136 | | 1cnd 11150 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (π..^π)) β§ π₯ β β) β 1 β
β) |
137 | 124 | dvmptid 25321 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π..^π)) β (β D (π₯ β β β¦ π₯)) = (π₯ β β β¦ 1)) |
138 | 125, 94 | sstrid 3955 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π..^π)) β (π(,)π) β β) |
139 | | iooretop 24129 |
. . . . . . . . . . . . . . . . 17
β’ (π(,)π) β (topGenβran
(,)) |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π..^π)) β (π(,)π) β (topGenβran
(,))) |
141 | 124, 135,
136, 137, 138, 119, 89, 140 | dvmptres 25327 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)π) β¦ π₯)) = (π₯ β (π(,)π) β¦ 1)) |
142 | 124, 133,
134, 141, 3 | dvmptcmul 25328 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)π) β¦ (π Β· π₯))) = (π₯ β (π(,)π) β¦ (π Β· 1))) |
143 | 3 | mulid1d 11172 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π..^π)) β (π Β· 1) = π) |
144 | 143 | mpteq2dv 5207 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π..^π)) β (π₯ β (π(,)π) β¦ (π Β· 1)) = (π₯ β (π(,)π) β¦ π)) |
145 | 142, 144 | eqtrd 2776 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)π) β¦ (π Β· π₯))) = (π₯ β (π(,)π) β¦ π)) |
146 | 126, 116 | sylan2 593 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β π΄ β β) |
147 | | dvfsumabs.v |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) |
148 | 147 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β π΅ β π) |
149 | | dvfsumabs.b |
. . . . . . . . . . . . . 14
β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
150 | 149 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
151 | 124, 130,
131, 145, 146, 148, 150 | dvmptsub 25331 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)π) β¦ ((π Β· π₯) β π΄))) = (π₯ β (π(,)π) β¦ (π β π΅))) |
152 | 78 | rexrd 11205 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π..^π)) β π β
β*) |
153 | | iooss1 13299 |
. . . . . . . . . . . . . 14
β’ ((π β β*
β§ π β€ π) β (π(,)(π + 1)) β (π(,)(π + 1))) |
154 | 152, 82, 153 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (π(,)(π + 1))) |
155 | 80 | rexrd 11205 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (π..^π)) β π β
β*) |
156 | | iooss2 13300 |
. . . . . . . . . . . . . 14
β’ ((π β β*
β§ (π + 1) β€ π) β (π(,)(π + 1)) β (π(,)π)) |
157 | 155, 85, 156 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (π(,)π)) |
158 | 154, 157 | sstrd 3954 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (π(,)π)) |
159 | | iooretop 24129 |
. . . . . . . . . . . . 13
β’ (π(,)(π + 1)) β (topGenβran
(,)) |
160 | 159 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (topGenβran
(,))) |
161 | 124, 127,
129, 151, 158, 119, 89, 160 | dvmptres 25327 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)(π + 1)) β¦ ((π Β· π₯) β π΄))) = (π₯ β (π(,)(π + 1)) β¦ (π β π΅))) |
162 | 122, 161 | eqtrd 2776 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))) = (π₯ β (π(,)(π + 1)) β¦ (π β π΅))) |
163 | 162 | dmeqd 5861 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β dom (β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))) = dom (π₯ β (π(,)(π + 1)) β¦ (π β π΅))) |
164 | | eqid 2736 |
. . . . . . . . . 10
β’ (π₯ β (π(,)(π + 1)) β¦ (π β π΅)) = (π₯ β (π(,)(π + 1)) β¦ (π β π΅)) |
165 | 128, 164 | dmmpti 6645 |
. . . . . . . . 9
β’ dom
(π₯ β (π(,)(π + 1)) β¦ (π β π΅)) = (π(,)(π + 1)) |
166 | 163, 165 | eqtrdi 2792 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β dom (β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))) = (π(,)(π + 1))) |
167 | 162 | adantr 481 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β (β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))) = (π₯ β (π(,)(π + 1)) β¦ (π β π΅))) |
168 | 167 | fveq1d 6844 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ₯) = ((π₯ β (π(,)(π + 1)) β¦ (π β π΅))βπ₯)) |
169 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β π₯ β (π(,)(π + 1))) |
170 | 164 | fvmpt2 6959 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (π(,)(π + 1)) β§ (π β π΅) β V) β ((π₯ β (π(,)(π + 1)) β¦ (π β π΅))βπ₯) = (π β π΅)) |
171 | 169, 128,
170 | sylancl 586 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β ((π₯ β (π(,)(π + 1)) β¦ (π β π΅))βπ₯) = (π β π΅)) |
172 | 168, 171 | eqtrd 2776 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ₯) = (π β π΅)) |
173 | 172 | fveq2d 6846 |
. . . . . . . . . . 11
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β (absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ₯)) = (absβ(π β π΅))) |
174 | | dvfsumabs.l |
. . . . . . . . . . . 12
β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β (absβ(π β π΅)) β€ π) |
175 | 174 | anassrs 468 |
. . . . . . . . . . 11
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β (absβ(π β π΅)) β€ π) |
176 | 173, 175 | eqbrtrd 5127 |
. . . . . . . . . 10
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β (absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ₯)) β€ π) |
177 | 176 | ralrimiva 3143 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β βπ₯ β (π(,)(π + 1))(absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ₯)) β€ π) |
178 | | nfcv 2907 |
. . . . . . . . . . . 12
β’
β²π₯abs |
179 | | nfcv 2907 |
. . . . . . . . . . . . . 14
β’
β²π₯β |
180 | | nfcv 2907 |
. . . . . . . . . . . . . 14
β’
β²π₯
D |
181 | | nfmpt1 5213 |
. . . . . . . . . . . . . 14
β’
β²π₯(π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)) |
182 | 179, 180,
181 | nfov 7387 |
. . . . . . . . . . . . 13
β’
β²π₯(β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))) |
183 | | nfcv 2907 |
. . . . . . . . . . . . 13
β’
β²π₯π¦ |
184 | 182, 183 | nffv 6852 |
. . . . . . . . . . . 12
β’
β²π₯((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ¦) |
185 | 178, 184 | nffv 6852 |
. . . . . . . . . . 11
β’
β²π₯(absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ¦)) |
186 | | nfcv 2907 |
. . . . . . . . . . 11
β’
β²π₯
β€ |
187 | | nfcv 2907 |
. . . . . . . . . . 11
β’
β²π₯π |
188 | 185, 186,
187 | nfbr 5152 |
. . . . . . . . . 10
β’
β²π₯(absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ¦)) β€ π |
189 | | 2fveq3 6847 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ₯)) = (absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ¦))) |
190 | 189 | breq1d 5115 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ₯)) β€ π β (absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ¦)) β€ π)) |
191 | 188, 190 | rspc 3569 |
. . . . . . . . 9
β’ (π¦ β (π(,)(π + 1)) β (βπ₯ β (π(,)(π + 1))(absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ₯)) β€ π β (absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ¦)) β€ π)) |
192 | 177, 191 | mpan9 507 |
. . . . . . . 8
β’ (((π β§ π β (π..^π)) β§ π¦ β (π(,)(π + 1))) β (absβ((β D (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)))βπ¦)) β€ π) |
193 | 67, 70, 108, 166, 62, 192 | dvlip 25357 |
. . . . . . 7
β’ (((π β§ π β (π..^π)) β§ ((π + 1) β (π[,](π + 1)) β§ π β (π[,](π + 1)))) β (absβ(((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))β(π + 1)) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))βπ))) β€ (π Β· (absβ((π + 1) β π)))) |
194 | 193 | ex 413 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (((π + 1) β (π[,](π + 1)) β§ π β (π[,](π + 1))) β (absβ(((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))β(π + 1)) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))βπ))) β€ (π Β· (absβ((π + 1) β π))))) |
195 | 74, 76, 194 | mp2and 697 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (absβ(((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))β(π + 1)) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))βπ))) β€ (π Β· (absβ((π + 1) β π)))) |
196 | | ovex 7390 |
. . . . . . . . 9
β’ ((π Β· (π + 1)) β β¦(π + 1) / π₯β¦π΄) β V |
197 | | nfcv 2907 |
. . . . . . . . . 10
β’
β²π₯(π + 1) |
198 | | nfcv 2907 |
. . . . . . . . . . 11
β’
β²π₯(π Β· (π + 1)) |
199 | | nfcv 2907 |
. . . . . . . . . . 11
β’
β²π₯
β |
200 | | nfcsb1v 3880 |
. . . . . . . . . . 11
β’
β²π₯β¦(π + 1) / π₯β¦π΄ |
201 | 198, 199,
200 | nfov 7387 |
. . . . . . . . . 10
β’
β²π₯((π Β· (π + 1)) β β¦(π + 1) / π₯β¦π΄) |
202 | | oveq2 7365 |
. . . . . . . . . . 11
β’ (π₯ = (π + 1) β (π Β· π₯) = (π Β· (π + 1))) |
203 | | csbeq1a 3869 |
. . . . . . . . . . 11
β’ (π₯ = (π + 1) β π΄ = β¦(π + 1) / π₯β¦π΄) |
204 | 202, 203 | oveq12d 7375 |
. . . . . . . . . 10
β’ (π₯ = (π + 1) β ((π Β· π₯) β π΄) = ((π Β· (π + 1)) β β¦(π + 1) / π₯β¦π΄)) |
205 | | eqid 2736 |
. . . . . . . . . 10
β’ (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)) = (π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄)) |
206 | 197, 201,
204, 205 | fvmptf 6969 |
. . . . . . . . 9
β’ (((π + 1) β (π[,](π + 1)) β§ ((π Β· (π + 1)) β β¦(π + 1) / π₯β¦π΄) β V) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))β(π + 1)) = ((π Β· (π + 1)) β β¦(π + 1) / π₯β¦π΄)) |
207 | 74, 196, 206 | sylancl 586 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))β(π + 1)) = ((π Β· (π + 1)) β β¦(π + 1) / π₯β¦π΄)) |
208 | 67 | recnd 11183 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β π β β) |
209 | 3, 208 | mulcld 11175 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π Β· π) β β) |
210 | 209, 37 | subcld 11512 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β ((π Β· π) β β¦π / π₯β¦π΄) β β) |
211 | | nfcv 2907 |
. . . . . . . . . 10
β’
β²π₯π |
212 | | nfcv 2907 |
. . . . . . . . . . 11
β’
β²π₯(π Β· π) |
213 | | nfcsb1v 3880 |
. . . . . . . . . . 11
β’
β²π₯β¦π / π₯β¦π΄ |
214 | 212, 199,
213 | nfov 7387 |
. . . . . . . . . 10
β’
β²π₯((π Β· π) β β¦π / π₯β¦π΄) |
215 | | oveq2 7365 |
. . . . . . . . . . 11
β’ (π₯ = π β (π Β· π₯) = (π Β· π)) |
216 | | csbeq1a 3869 |
. . . . . . . . . . 11
β’ (π₯ = π β π΄ = β¦π / π₯β¦π΄) |
217 | 215, 216 | oveq12d 7375 |
. . . . . . . . . 10
β’ (π₯ = π β ((π Β· π₯) β π΄) = ((π Β· π) β β¦π / π₯β¦π΄)) |
218 | 211, 214,
217, 205 | fvmptf 6969 |
. . . . . . . . 9
β’ ((π β (π[,](π + 1)) β§ ((π Β· π) β β¦π / π₯β¦π΄) β β) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))βπ) = ((π Β· π) β β¦π / π₯β¦π΄)) |
219 | 76, 210, 218 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))βπ) = ((π Β· π) β β¦π / π₯β¦π΄)) |
220 | 207, 219 | oveq12d 7375 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β (((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))β(π + 1)) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))βπ)) = (((π Β· (π + 1)) β β¦(π + 1) / π₯β¦π΄) β ((π Β· π) β β¦π / π₯β¦π΄))) |
221 | | peano2cn 11327 |
. . . . . . . . . 10
β’ (π β β β (π + 1) β
β) |
222 | 208, 221 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π + 1) β β) |
223 | 3, 222 | mulcld 11175 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (π Β· (π + 1)) β β) |
224 | 223, 209,
32, 37 | sub4d 11561 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β (((π Β· (π + 1)) β (π Β· π)) β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) = (((π Β· (π + 1)) β β¦(π + 1) / π₯β¦π΄) β ((π Β· π) β β¦π / π₯β¦π΄))) |
225 | | 1cnd 11150 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β 1 β β) |
226 | 208, 225 | pncan2d 11514 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β ((π + 1) β π) = 1) |
227 | 226 | oveq2d 7373 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π Β· ((π + 1) β π)) = (π Β· 1)) |
228 | 3, 222, 208 | subdid 11611 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π Β· ((π + 1) β π)) = ((π Β· (π + 1)) β (π Β· π))) |
229 | 227, 228,
143 | 3eqtr3d 2784 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β ((π Β· (π + 1)) β (π Β· π)) = π) |
230 | 229 | oveq1d 7372 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β (((π Β· (π + 1)) β (π Β· π)) β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) = (π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) |
231 | 220, 224,
230 | 3eqtr2rd 2783 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) = (((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))β(π + 1)) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))βπ))) |
232 | 231 | fveq2d 6846 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (absβ(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) = (absβ(((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))β(π + 1)) β ((π₯ β (π[,](π + 1)) β¦ ((π Β· π₯) β π΄))βπ)))) |
233 | 226 | fveq2d 6846 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (absβ((π + 1) β π)) = (absβ1)) |
234 | | abs1 15182 |
. . . . . . . 8
β’
(absβ1) = 1 |
235 | 233, 234 | eqtrdi 2792 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β (absβ((π + 1) β π)) = 1) |
236 | 235 | oveq2d 7373 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π Β· (absβ((π + 1) β π))) = (π Β· 1)) |
237 | 62 | recnd 11183 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β π β β) |
238 | 237 | mulid1d 11172 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π Β· 1) = π) |
239 | 236, 238 | eqtr2d 2777 |
. . . . 5
β’ ((π β§ π β (π..^π)) β π = (π Β· (absβ((π + 1) β π)))) |
240 | 195, 232,
239 | 3brtr4d 5137 |
. . . 4
β’ ((π β§ π β (π..^π)) β (absβ(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) β€ π) |
241 | 2, 60, 62, 240 | fsumle 15684 |
. . 3
β’ (π β Ξ£π β (π..^π)(absβ(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) β€ Ξ£π β (π..^π)π) |
242 | 59, 61, 63, 64, 241 | letrd 11312 |
. 2
β’ (π β (absβΞ£π β (π..^π)(π β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄))) β€ Ξ£π β (π..^π)π) |
243 | 56, 242 | eqbrtrrd 5129 |
1
β’ (π β (absβ(Ξ£π β (π..^π)π β (π· β πΆ))) β€ Ξ£π β (π..^π)π) |