Step | Hyp | Ref
| Expression |
1 | | fzofi 13879 |
. . . 4
β’ (π..^π) β Fin |
2 | 1 | a1i 11 |
. . 3
β’ (π β (π..^π) β Fin) |
3 | | dvfsumle.x |
. . 3
β’ ((π β§ π β (π..^π)) β π β β) |
4 | | dvfsumle.m |
. . . . . . . . . . 11
β’ (π β π β (β€β₯βπ)) |
5 | | eluzel2 12768 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β π β β€) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
β’ (π β π β β€) |
7 | | eluzelz 12773 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β π β β€) |
8 | 4, 7 | syl 17 |
. . . . . . . . . 10
β’ (π β π β β€) |
9 | | fzval2 13427 |
. . . . . . . . . 10
β’ ((π β β€ β§ π β β€) β (π...π) = ((π[,]π) β© β€)) |
10 | 6, 8, 9 | syl2anc 584 |
. . . . . . . . 9
β’ (π β (π...π) = ((π[,]π) β© β€)) |
11 | | inss1 4188 |
. . . . . . . . 9
β’ ((π[,]π) β© β€) β (π[,]π) |
12 | 10, 11 | eqsstrdi 3998 |
. . . . . . . 8
β’ (π β (π...π) β (π[,]π)) |
13 | 12 | sselda 3944 |
. . . . . . 7
β’ ((π β§ π¦ β (π...π)) β π¦ β (π[,]π)) |
14 | | dvfsumle.a |
. . . . . . . . . 10
β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) |
15 | | cncff 24256 |
. . . . . . . . . 10
β’ ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
β’ (π β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
17 | | eqid 2736 |
. . . . . . . . . 10
β’ (π₯ β (π[,]π) β¦ π΄) = (π₯ β (π[,]π) β¦ π΄) |
18 | 17 | fmpt 7058 |
. . . . . . . . 9
β’
(βπ₯ β
(π[,]π)π΄ β β β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
19 | 16, 18 | sylibr 233 |
. . . . . . . 8
β’ (π β βπ₯ β (π[,]π)π΄ β β) |
20 | | nfcsb1v 3880 |
. . . . . . . . . 10
β’
β²π₯β¦π¦ / π₯β¦π΄ |
21 | 20 | nfel1 2923 |
. . . . . . . . 9
β’
β²π₯β¦π¦ / π₯β¦π΄ β β |
22 | | csbeq1a 3869 |
. . . . . . . . . 10
β’ (π₯ = π¦ β π΄ = β¦π¦ / π₯β¦π΄) |
23 | 22 | eleq1d 2822 |
. . . . . . . . 9
β’ (π₯ = π¦ β (π΄ β β β β¦π¦ / π₯β¦π΄ β β)) |
24 | 21, 23 | rspc 3569 |
. . . . . . . 8
β’ (π¦ β (π[,]π) β (βπ₯ β (π[,]π)π΄ β β β β¦π¦ / π₯β¦π΄ β β)) |
25 | 19, 24 | mpan9 507 |
. . . . . . 7
β’ ((π β§ π¦ β (π[,]π)) β β¦π¦ / π₯β¦π΄ β β) |
26 | 13, 25 | syldan 591 |
. . . . . 6
β’ ((π β§ π¦ β (π...π)) β β¦π¦ / π₯β¦π΄ β β) |
27 | 26 | ralrimiva 3143 |
. . . . 5
β’ (π β βπ¦ β (π...π)β¦π¦ / π₯β¦π΄ β β) |
28 | | fzofzp1 13669 |
. . . . 5
β’ (π β (π..^π) β (π + 1) β (π...π)) |
29 | | csbeq1 3858 |
. . . . . . 7
β’ (π¦ = (π + 1) β β¦π¦ / π₯β¦π΄ = β¦(π + 1) / π₯β¦π΄) |
30 | 29 | eleq1d 2822 |
. . . . . 6
β’ (π¦ = (π + 1) β (β¦π¦ / π₯β¦π΄ β β β β¦(π + 1) / π₯β¦π΄ β β)) |
31 | 30 | rspccva 3580 |
. . . . 5
β’
((βπ¦ β
(π...π)β¦π¦ / π₯β¦π΄ β β β§ (π + 1) β (π...π)) β β¦(π + 1) / π₯β¦π΄ β β) |
32 | 27, 28, 31 | syl2an 596 |
. . . 4
β’ ((π β§ π β (π..^π)) β β¦(π + 1) / π₯β¦π΄ β β) |
33 | | elfzofz 13588 |
. . . . 5
β’ (π β (π..^π) β π β (π...π)) |
34 | | csbeq1 3858 |
. . . . . . 7
β’ (π¦ = π β β¦π¦ / π₯β¦π΄ = β¦π / π₯β¦π΄) |
35 | 34 | eleq1d 2822 |
. . . . . 6
β’ (π¦ = π β (β¦π¦ / π₯β¦π΄ β β β β¦π / π₯β¦π΄ β β)) |
36 | 35 | rspccva 3580 |
. . . . 5
β’
((βπ¦ β
(π...π)β¦π¦ / π₯β¦π΄ β β β§ π β (π...π)) β β¦π / π₯β¦π΄ β β) |
37 | 27, 33, 36 | syl2an 596 |
. . . 4
β’ ((π β§ π β (π..^π)) β β¦π / π₯β¦π΄ β β) |
38 | 32, 37 | resubcld 11583 |
. . 3
β’ ((π β§ π β (π..^π)) β (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄) β β) |
39 | | elfzoelz 13572 |
. . . . . . . . . 10
β’ (π β (π..^π) β π β β€) |
40 | 39 | adantl 482 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β π β β€) |
41 | 40 | zred 12607 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β π β β) |
42 | 41 | recnd 11183 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β π β β) |
43 | | ax-1cn 11109 |
. . . . . . 7
β’ 1 β
β |
44 | | pncan2 11408 |
. . . . . . 7
β’ ((π β β β§ 1 β
β) β ((π + 1)
β π) =
1) |
45 | 42, 43, 44 | sylancl 586 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β ((π + 1) β π) = 1) |
46 | 45 | oveq2d 7373 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (π Β· ((π + 1) β π)) = (π Β· 1)) |
47 | 3 | recnd 11183 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β π β β) |
48 | | peano2re 11328 |
. . . . . . . 8
β’ (π β β β (π + 1) β
β) |
49 | 41, 48 | syl 17 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β (π + 1) β β) |
50 | 49 | recnd 11183 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π + 1) β β) |
51 | 47, 50, 42 | subdid 11611 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (π Β· ((π + 1) β π)) = ((π Β· (π + 1)) β (π Β· π))) |
52 | 47 | mulid1d 11172 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (π Β· 1) = π) |
53 | 46, 51, 52 | 3eqtr3d 2784 |
. . . 4
β’ ((π β§ π β (π..^π)) β ((π Β· (π + 1)) β (π Β· π)) = π) |
54 | | eqid 2736 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
55 | 54 | mulcn 24230 |
. . . . . 6
β’ Β·
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
56 | 6 | zred 12607 |
. . . . . . . . . . 11
β’ (π β π β β) |
57 | 56 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β π β β) |
58 | 8 | zred 12607 |
. . . . . . . . . . 11
β’ (π β π β β) |
59 | 58 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β π β β) |
60 | | elfzole1 13580 |
. . . . . . . . . . 11
β’ (π β (π..^π) β π β€ π) |
61 | 60 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β π β€ π) |
62 | 28 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (π + 1) β (π...π)) |
63 | | elfzle2 13445 |
. . . . . . . . . . 11
β’ ((π + 1) β (π...π) β (π + 1) β€ π) |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π + 1) β€ π) |
65 | | iccss 13332 |
. . . . . . . . . 10
β’ (((π β β β§ π β β) β§ (π β€ π β§ (π + 1) β€ π)) β (π[,](π + 1)) β (π[,]π)) |
66 | 57, 59, 61, 64, 65 | syl22anc 837 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π[,](π + 1)) β (π[,]π)) |
67 | | iccssre 13346 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β (π[,]π) β β) |
68 | 56, 58, 67 | syl2anc 584 |
. . . . . . . . . 10
β’ (π β (π[,]π) β β) |
69 | 68 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π[,]π) β β) |
70 | 66, 69 | sstrd 3954 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (π[,](π + 1)) β β) |
71 | | ax-resscn 11108 |
. . . . . . . 8
β’ β
β β |
72 | 70, 71 | sstrdi 3956 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β (π[,](π + 1)) β β) |
73 | 71 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β β β
β) |
74 | | cncfmptc 24275 |
. . . . . . 7
β’ ((π β β β§ (π[,](π + 1)) β β β§ β β
β) β (π¦ β
(π[,](π + 1)) β¦ π) β ((π[,](π + 1))βcnββ)) |
75 | 3, 72, 73, 74 | syl3anc 1371 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π¦ β (π[,](π + 1)) β¦ π) β ((π[,](π + 1))βcnββ)) |
76 | | cncfmptid 24276 |
. . . . . . 7
β’ (((π[,](π + 1)) β β β§ β β
β) β (π¦ β
(π[,](π + 1)) β¦ π¦) β ((π[,](π + 1))βcnββ)) |
77 | 70, 71, 76 | sylancl 586 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π¦ β (π[,](π + 1)) β¦ π¦) β ((π[,](π + 1))βcnββ)) |
78 | | remulcl 11136 |
. . . . . 6
β’ ((π β β β§ π¦ β β) β (π Β· π¦) β β) |
79 | 54, 55, 75, 77, 71, 78 | cncfmpt2ss 24279 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (π¦ β (π[,](π + 1)) β¦ (π Β· π¦)) β ((π[,](π + 1))βcnββ)) |
80 | | reelprrecn 11143 |
. . . . . . . 8
β’ β
β {β, β} |
81 | 80 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β β β {β,
β}) |
82 | 57 | rexrd 11205 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β π β
β*) |
83 | | iooss1 13299 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π β€ π) β (π(,)(π + 1)) β (π(,)(π + 1))) |
84 | 82, 61, 83 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (π(,)(π + 1))) |
85 | 59 | rexrd 11205 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β π β
β*) |
86 | | iooss2 13300 |
. . . . . . . . . . 11
β’ ((π β β*
β§ (π + 1) β€ π) β (π(,)(π + 1)) β (π(,)π)) |
87 | 85, 64, 86 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (π(,)π)) |
88 | 84, 87 | sstrd 3954 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (π(,)π)) |
89 | | ioossicc 13350 |
. . . . . . . . . 10
β’ (π(,)π) β (π[,]π) |
90 | 69, 71 | sstrdi 3956 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π[,]π) β β) |
91 | 89, 90 | sstrid 3955 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π(,)π) β β) |
92 | 88, 91 | sstrd 3954 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β β) |
93 | 92 | sselda 3944 |
. . . . . . 7
β’ (((π β§ π β (π..^π)) β§ π¦ β (π(,)(π + 1))) β π¦ β β) |
94 | | 1cnd 11150 |
. . . . . . 7
β’ (((π β§ π β (π..^π)) β§ π¦ β (π(,)(π + 1))) β 1 β
β) |
95 | 73 | sselda 3944 |
. . . . . . . 8
β’ (((π β§ π β (π..^π)) β§ π¦ β β) β π¦ β β) |
96 | | 1cnd 11150 |
. . . . . . . 8
β’ (((π β§ π β (π..^π)) β§ π¦ β β) β 1 β
β) |
97 | 81 | dvmptid 25321 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (β D (π¦ β β β¦ π¦)) = (π¦ β β β¦ 1)) |
98 | | ioossre 13325 |
. . . . . . . . 9
β’ (π(,)(π + 1)) β β |
99 | 98 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β β) |
100 | 54 | tgioo2 24166 |
. . . . . . . 8
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
101 | | iooretop 24129 |
. . . . . . . . 9
β’ (π(,)(π + 1)) β (topGenβran
(,)) |
102 | 101 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (topGenβran
(,))) |
103 | 81, 95, 96, 97, 99, 100, 54, 102 | dvmptres 25327 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β (β D (π¦ β (π(,)(π + 1)) β¦ π¦)) = (π¦ β (π(,)(π + 1)) β¦ 1)) |
104 | 81, 93, 94, 103, 47 | dvmptcmul 25328 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (β D (π¦ β (π(,)(π + 1)) β¦ (π Β· π¦))) = (π¦ β (π(,)(π + 1)) β¦ (π Β· 1))) |
105 | 52 | mpteq2dv 5207 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π¦ β (π(,)(π + 1)) β¦ (π Β· 1)) = (π¦ β (π(,)(π + 1)) β¦ π)) |
106 | 104, 105 | eqtrd 2776 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (β D (π¦ β (π(,)(π + 1)) β¦ (π Β· π¦))) = (π¦ β (π(,)(π + 1)) β¦ π)) |
107 | | nfcv 2907 |
. . . . . . 7
β’
β²π¦π΄ |
108 | 107, 20, 22 | cbvmpt 5216 |
. . . . . 6
β’ (π₯ β (π[,](π + 1)) β¦ π΄) = (π¦ β (π[,](π + 1)) β¦ β¦π¦ / π₯β¦π΄) |
109 | 66 | resmptd 5994 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β ((π₯ β (π[,]π) β¦ π΄) βΎ (π[,](π + 1))) = (π₯ β (π[,](π + 1)) β¦ π΄)) |
110 | 14 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) |
111 | | rescncf 24260 |
. . . . . . . 8
β’ ((π[,](π + 1)) β (π[,]π) β ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ) β ((π₯ β (π[,]π) β¦ π΄) βΎ (π[,](π + 1))) β ((π[,](π + 1))βcnββ))) |
112 | 66, 110, 111 | sylc 65 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β ((π₯ β (π[,]π) β¦ π΄) βΎ (π[,](π + 1))) β ((π[,](π + 1))βcnββ)) |
113 | 109, 112 | eqeltrrd 2838 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π₯ β (π[,](π + 1)) β¦ π΄) β ((π[,](π + 1))βcnββ)) |
114 | 108, 113 | eqeltrrid 2842 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (π¦ β (π[,](π + 1)) β¦ β¦π¦ / π₯β¦π΄) β ((π[,](π + 1))βcnββ)) |
115 | 16 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
116 | 115, 18 | sylibr 233 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β βπ₯ β (π[,]π)π΄ β β) |
117 | 89 | sseli 3940 |
. . . . . . . 8
β’ (π¦ β (π(,)π) β π¦ β (π[,]π)) |
118 | 24 | impcom 408 |
. . . . . . . 8
β’
((βπ₯ β
(π[,]π)π΄ β β β§ π¦ β (π[,]π)) β β¦π¦ / π₯β¦π΄ β β) |
119 | 116, 117,
118 | syl2an 596 |
. . . . . . 7
β’ (((π β§ π β (π..^π)) β§ π¦ β (π(,)π)) β β¦π¦ / π₯β¦π΄ β β) |
120 | 119 | recnd 11183 |
. . . . . 6
β’ (((π β§ π β (π..^π)) β§ π¦ β (π(,)π)) β β¦π¦ / π₯β¦π΄ β β) |
121 | 89 | sseli 3940 |
. . . . . . . . . . . 12
β’ (π₯ β (π(,)π) β π₯ β (π[,]π)) |
122 | 16 | fvmptelcdm 7061 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π[,]π)) β π΄ β β) |
123 | 122 | adantlr 713 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π₯ β (π[,]π)) β π΄ β β) |
124 | 121, 123 | sylan2 593 |
. . . . . . . . . . 11
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β π΄ β β) |
125 | 124 | fmpttd 7063 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π₯ β (π(,)π) β¦ π΄):(π(,)π)βΆβ) |
126 | | ioossre 13325 |
. . . . . . . . . 10
β’ (π(,)π) β β |
127 | | dvfre 25315 |
. . . . . . . . . 10
β’ (((π₯ β (π(,)π) β¦ π΄):(π(,)π)βΆβ β§ (π(,)π) β β) β (β D (π₯ β (π(,)π) β¦ π΄)):dom (β D (π₯ β (π(,)π) β¦ π΄))βΆβ) |
128 | 125, 126,
127 | sylancl 586 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)π) β¦ π΄)):dom (β D (π₯ β (π(,)π) β¦ π΄))βΆβ) |
129 | | dvfsumle.b |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
130 | 129 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
131 | 130 | dmeqd 5861 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β dom (β D (π₯ β (π(,)π) β¦ π΄)) = dom (π₯ β (π(,)π) β¦ π΅)) |
132 | | dvfsumle.v |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) |
133 | 132 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β π΅ β π) |
134 | 133 | ralrimiva 3143 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β βπ₯ β (π(,)π)π΅ β π) |
135 | | dmmptg 6194 |
. . . . . . . . . . . 12
β’
(βπ₯ β
(π(,)π)π΅ β π β dom (π₯ β (π(,)π) β¦ π΅) = (π(,)π)) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β dom (π₯ β (π(,)π) β¦ π΅) = (π(,)π)) |
137 | 131, 136 | eqtrd 2776 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β dom (β D (π₯ β (π(,)π) β¦ π΄)) = (π(,)π)) |
138 | 130, 137 | feq12d 6656 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β ((β D (π₯ β (π(,)π) β¦ π΄)):dom (β D (π₯ β (π(,)π) β¦ π΄))βΆβ β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ)) |
139 | 128, 138 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β (π..^π)) β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ) |
140 | | eqid 2736 |
. . . . . . . . 9
β’ (π₯ β (π(,)π) β¦ π΅) = (π₯ β (π(,)π) β¦ π΅) |
141 | 140 | fmpt 7058 |
. . . . . . . 8
β’
(βπ₯ β
(π(,)π)π΅ β β β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ) |
142 | 139, 141 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β (π..^π)) β βπ₯ β (π(,)π)π΅ β β) |
143 | | nfcsb1v 3880 |
. . . . . . . . 9
β’
β²π₯β¦π¦ / π₯β¦π΅ |
144 | 143 | nfel1 2923 |
. . . . . . . 8
β’
β²π₯β¦π¦ / π₯β¦π΅ β β |
145 | | csbeq1a 3869 |
. . . . . . . . 9
β’ (π₯ = π¦ β π΅ = β¦π¦ / π₯β¦π΅) |
146 | 145 | eleq1d 2822 |
. . . . . . . 8
β’ (π₯ = π¦ β (π΅ β β β β¦π¦ / π₯β¦π΅ β β)) |
147 | 144, 146 | rspc 3569 |
. . . . . . 7
β’ (π¦ β (π(,)π) β (βπ₯ β (π(,)π)π΅ β β β β¦π¦ / π₯β¦π΅ β β)) |
148 | 142, 147 | mpan9 507 |
. . . . . 6
β’ (((π β§ π β (π..^π)) β§ π¦ β (π(,)π)) β β¦π¦ / π₯β¦π΅ β β) |
149 | 107, 20, 22 | cbvmpt 5216 |
. . . . . . . 8
β’ (π₯ β (π(,)π) β¦ π΄) = (π¦ β (π(,)π) β¦ β¦π¦ / π₯β¦π΄) |
150 | 149 | oveq2i 7368 |
. . . . . . 7
β’ (β
D (π₯ β (π(,)π) β¦ π΄)) = (β D (π¦ β (π(,)π) β¦ β¦π¦ / π₯β¦π΄)) |
151 | | nfcv 2907 |
. . . . . . . 8
β’
β²π¦π΅ |
152 | 151, 143,
145 | cbvmpt 5216 |
. . . . . . 7
β’ (π₯ β (π(,)π) β¦ π΅) = (π¦ β (π(,)π) β¦ β¦π¦ / π₯β¦π΅) |
153 | 130, 150,
152 | 3eqtr3g 2799 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (β D (π¦ β (π(,)π) β¦ β¦π¦ / π₯β¦π΄)) = (π¦ β (π(,)π) β¦ β¦π¦ / π₯β¦π΅)) |
154 | 81, 120, 148, 153, 88, 100, 54, 102 | dvmptres 25327 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (β D (π¦ β (π(,)(π + 1)) β¦ β¦π¦ / π₯β¦π΄)) = (π¦ β (π(,)(π + 1)) β¦ β¦π¦ / π₯β¦π΅)) |
155 | | dvfsumle.l |
. . . . . . . 8
β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π β€ π΅) |
156 | 155 | anassrs 468 |
. . . . . . 7
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β π β€ π΅) |
157 | 156 | ralrimiva 3143 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β βπ₯ β (π(,)(π + 1))π β€ π΅) |
158 | | nfcv 2907 |
. . . . . . . 8
β’
β²π₯π |
159 | | nfcv 2907 |
. . . . . . . 8
β’
β²π₯
β€ |
160 | 158, 159,
143 | nfbr 5152 |
. . . . . . 7
β’
β²π₯ π β€ β¦π¦ / π₯β¦π΅ |
161 | 145 | breq2d 5117 |
. . . . . . 7
β’ (π₯ = π¦ β (π β€ π΅ β π β€ β¦π¦ / π₯β¦π΅)) |
162 | 160, 161 | rspc 3569 |
. . . . . 6
β’ (π¦ β (π(,)(π + 1)) β (βπ₯ β (π(,)(π + 1))π β€ π΅ β π β€ β¦π¦ / π₯β¦π΅)) |
163 | 157, 162 | mpan9 507 |
. . . . 5
β’ (((π β§ π β (π..^π)) β§ π¦ β (π(,)(π + 1))) β π β€ β¦π¦ / π₯β¦π΅) |
164 | 41 | rexrd 11205 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β π β β*) |
165 | 49 | rexrd 11205 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β (π + 1) β
β*) |
166 | 41 | lep1d 12086 |
. . . . . 6
β’ ((π β§ π β (π..^π)) β π β€ (π + 1)) |
167 | | lbicc2 13381 |
. . . . . 6
β’ ((π β β*
β§ (π + 1) β
β* β§ π
β€ (π + 1)) β π β (π[,](π + 1))) |
168 | 164, 165,
166, 167 | syl3anc 1371 |
. . . . 5
β’ ((π β§ π β (π..^π)) β π β (π[,](π + 1))) |
169 | | ubicc2 13382 |
. . . . . 6
β’ ((π β β*
β§ (π + 1) β
β* β§ π
β€ (π + 1)) β (π + 1) β (π[,](π + 1))) |
170 | 164, 165,
166, 169 | syl3anc 1371 |
. . . . 5
β’ ((π β§ π β (π..^π)) β (π + 1) β (π[,](π + 1))) |
171 | | oveq2 7365 |
. . . . 5
β’ (π¦ = π β (π Β· π¦) = (π Β· π)) |
172 | | oveq2 7365 |
. . . . 5
β’ (π¦ = (π + 1) β (π Β· π¦) = (π Β· (π + 1))) |
173 | 41, 49, 79, 106, 114, 154, 163, 168, 170, 166, 171, 34, 172, 29 | dvle 25371 |
. . . 4
β’ ((π β§ π β (π..^π)) β ((π Β· (π + 1)) β (π Β· π)) β€ (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) |
174 | 53, 173 | eqbrtrrd 5129 |
. . 3
β’ ((π β§ π β (π..^π)) β π β€ (β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) |
175 | 2, 3, 38, 174 | fsumle 15684 |
. 2
β’ (π β Ξ£π β (π..^π)π β€ Ξ£π β (π..^π)(β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄)) |
176 | | vex 3449 |
. . . . 5
β’ π¦ β V |
177 | 176 | a1i 11 |
. . . 4
β’ (π¦ = π β π¦ β V) |
178 | | eqeq2 2748 |
. . . . . 6
β’ (π¦ = π β (π₯ = π¦ β π₯ = π)) |
179 | 178 | biimpa 477 |
. . . . 5
β’ ((π¦ = π β§ π₯ = π¦) β π₯ = π) |
180 | | dvfsumle.c |
. . . . 5
β’ (π₯ = π β π΄ = πΆ) |
181 | 179, 180 | syl 17 |
. . . 4
β’ ((π¦ = π β§ π₯ = π¦) β π΄ = πΆ) |
182 | 177, 181 | csbied 3893 |
. . 3
β’ (π¦ = π β β¦π¦ / π₯β¦π΄ = πΆ) |
183 | 176 | a1i 11 |
. . . 4
β’ (π¦ = π β π¦ β V) |
184 | | eqeq2 2748 |
. . . . . 6
β’ (π¦ = π β (π₯ = π¦ β π₯ = π)) |
185 | 184 | biimpa 477 |
. . . . 5
β’ ((π¦ = π β§ π₯ = π¦) β π₯ = π) |
186 | | dvfsumle.d |
. . . . 5
β’ (π₯ = π β π΄ = π·) |
187 | 185, 186 | syl 17 |
. . . 4
β’ ((π¦ = π β§ π₯ = π¦) β π΄ = π·) |
188 | 183, 187 | csbied 3893 |
. . 3
β’ (π¦ = π β β¦π¦ / π₯β¦π΄ = π·) |
189 | 26 | recnd 11183 |
. . 3
β’ ((π β§ π¦ β (π...π)) β β¦π¦ / π₯β¦π΄ β β) |
190 | 34, 29, 182, 188, 4, 189 | telfsumo2 15688 |
. 2
β’ (π β Ξ£π β (π..^π)(β¦(π + 1) / π₯β¦π΄ β β¦π / π₯β¦π΄) = (π· β πΆ)) |
191 | 175, 190 | breqtrd 5131 |
1
β’ (π β Ξ£π β (π..^π)π β€ (π· β πΆ)) |