Step | Hyp | Ref
| Expression |
1 | | dvfsumle.m |
. . . 4
β’ (π β π β (β€β₯βπ)) |
2 | | df-neg 11443 |
. . . . . 6
β’ -π΄ = (0 β π΄) |
3 | 2 | mpteq2i 5252 |
. . . . 5
β’ (π₯ β (π[,]π) β¦ -π΄) = (π₯ β (π[,]π) β¦ (0 β π΄)) |
4 | | eqid 2732 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
5 | 4 | subcn 24373 |
. . . . . 6
β’ β
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
6 | | 0red 11213 |
. . . . . . 7
β’ (π β 0 β
β) |
7 | | eluzel2 12823 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β π β β€) |
8 | 1, 7 | syl 17 |
. . . . . . . . . 10
β’ (π β π β β€) |
9 | 8 | zred 12662 |
. . . . . . . . 9
β’ (π β π β β) |
10 | | eluzelz 12828 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β π β β€) |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
β’ (π β π β β€) |
12 | 11 | zred 12662 |
. . . . . . . . 9
β’ (π β π β β) |
13 | | iccssre 13402 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β (π[,]π) β β) |
14 | 9, 12, 13 | syl2anc 584 |
. . . . . . . 8
β’ (π β (π[,]π) β β) |
15 | | ax-resscn 11163 |
. . . . . . . 8
β’ β
β β |
16 | 14, 15 | sstrdi 3993 |
. . . . . . 7
β’ (π β (π[,]π) β β) |
17 | 15 | a1i 11 |
. . . . . . 7
β’ (π β β β
β) |
18 | | cncfmptc 24419 |
. . . . . . 7
β’ ((0
β β β§ (π[,]π) β β β§ β β
β) β (π₯ β
(π[,]π) β¦ 0) β ((π[,]π)βcnββ)) |
19 | 6, 16, 17, 18 | syl3anc 1371 |
. . . . . 6
β’ (π β (π₯ β (π[,]π) β¦ 0) β ((π[,]π)βcnββ)) |
20 | | dvfsumle.a |
. . . . . 6
β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) |
21 | | resubcl 11520 |
. . . . . 6
β’ ((0
β β β§ π΄
β β) β (0 β π΄) β β) |
22 | 4, 5, 19, 20, 15, 21 | cncfmpt2ss 24423 |
. . . . 5
β’ (π β (π₯ β (π[,]π) β¦ (0 β π΄)) β ((π[,]π)βcnββ)) |
23 | 3, 22 | eqeltrid 2837 |
. . . 4
β’ (π β (π₯ β (π[,]π) β¦ -π΄) β ((π[,]π)βcnββ)) |
24 | | negex 11454 |
. . . . 5
β’ -π΅ β V |
25 | 24 | a1i 11 |
. . . 4
β’ ((π β§ π₯ β (π(,)π)) β -π΅ β V) |
26 | | reelprrecn 11198 |
. . . . . 6
β’ β
β {β, β} |
27 | 26 | a1i 11 |
. . . . 5
β’ (π β β β {β,
β}) |
28 | | ioossicc 13406 |
. . . . . . . 8
β’ (π(,)π) β (π[,]π) |
29 | 28 | sseli 3977 |
. . . . . . 7
β’ (π₯ β (π(,)π) β π₯ β (π[,]π)) |
30 | | cncff 24400 |
. . . . . . . . 9
β’ ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
31 | 20, 30 | syl 17 |
. . . . . . . 8
β’ (π β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
32 | 31 | fvmptelcdm 7109 |
. . . . . . 7
β’ ((π β§ π₯ β (π[,]π)) β π΄ β β) |
33 | 29, 32 | sylan2 593 |
. . . . . 6
β’ ((π β§ π₯ β (π(,)π)) β π΄ β β) |
34 | 33 | recnd 11238 |
. . . . 5
β’ ((π β§ π₯ β (π(,)π)) β π΄ β β) |
35 | | dvfsumle.v |
. . . . 5
β’ ((π β§ π₯ β (π(,)π)) β π΅ β π) |
36 | | dvfsumle.b |
. . . . 5
β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
37 | 27, 34, 35, 36 | dvmptneg 25474 |
. . . 4
β’ (π β (β D (π₯ β (π(,)π) β¦ -π΄)) = (π₯ β (π(,)π) β¦ -π΅)) |
38 | | dvfsumle.c |
. . . . 5
β’ (π₯ = π β π΄ = πΆ) |
39 | 38 | negeqd 11450 |
. . . 4
β’ (π₯ = π β -π΄ = -πΆ) |
40 | | dvfsumle.d |
. . . . 5
β’ (π₯ = π β π΄ = π·) |
41 | 40 | negeqd 11450 |
. . . 4
β’ (π₯ = π β -π΄ = -π·) |
42 | | dvfsumle.x |
. . . . 5
β’ ((π β§ π β (π..^π)) β π β β) |
43 | 42 | renegcld 11637 |
. . . 4
β’ ((π β§ π β (π..^π)) β -π β β) |
44 | | dvfsumge.l |
. . . . 5
β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π΅ β€ π) |
45 | 9 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β π β β) |
46 | 45 | rexrd 11260 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β π β
β*) |
47 | | elfzole1 13636 |
. . . . . . . . . . . 12
β’ (π β (π..^π) β π β€ π) |
48 | 47 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β π β€ π) |
49 | | iooss1 13355 |
. . . . . . . . . . 11
β’ ((π β β*
β§ π β€ π) β (π(,)(π + 1)) β (π(,)(π + 1))) |
50 | 46, 48, 49 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (π(,)(π + 1))) |
51 | 12 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β π β β) |
52 | 51 | rexrd 11260 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β π β
β*) |
53 | | fzofzp1 13725 |
. . . . . . . . . . . . 13
β’ (π β (π..^π) β (π + 1) β (π...π)) |
54 | 53 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β (π + 1) β (π...π)) |
55 | | elfzle2 13501 |
. . . . . . . . . . . 12
β’ ((π + 1) β (π...π) β (π + 1) β€ π) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (π + 1) β€ π) |
57 | | iooss2 13356 |
. . . . . . . . . . 11
β’ ((π β β*
β§ (π + 1) β€ π) β (π(,)(π + 1)) β (π(,)π)) |
58 | 52, 56, 57 | syl2anc 584 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (π(,)π)) |
59 | 50, 58 | sstrd 3991 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π(,)(π + 1)) β (π(,)π)) |
60 | 59 | sselda 3981 |
. . . . . . . 8
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β π₯ β (π(,)π)) |
61 | 32 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (π..^π)) β§ π₯ β (π[,]π)) β π΄ β β) |
62 | 29, 61 | sylan2 593 |
. . . . . . . . . . . 12
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β π΄ β β) |
63 | 62 | fmpttd 7111 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (π₯ β (π(,)π) β¦ π΄):(π(,)π)βΆβ) |
64 | | ioossre 13381 |
. . . . . . . . . . 11
β’ (π(,)π) β β |
65 | | dvfre 25459 |
. . . . . . . . . . 11
β’ (((π₯ β (π(,)π) β¦ π΄):(π(,)π)βΆβ β§ (π(,)π) β β) β (β D (π₯ β (π(,)π) β¦ π΄)):dom (β D (π₯ β (π(,)π) β¦ π΄))βΆβ) |
66 | 63, 64, 65 | sylancl 586 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)π) β¦ π΄)):dom (β D (π₯ β (π(,)π) β¦ π΄))βΆβ) |
67 | 36 | adantr 481 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
68 | 67 | dmeqd 5903 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β dom (β D (π₯ β (π(,)π) β¦ π΄)) = dom (π₯ β (π(,)π) β¦ π΅)) |
69 | 35 | adantlr 713 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β π΅ β π) |
70 | 69 | ralrimiva 3146 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π..^π)) β βπ₯ β (π(,)π)π΅ β π) |
71 | | dmmptg 6238 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
(π(,)π)π΅ β π β dom (π₯ β (π(,)π) β¦ π΅) = (π(,)π)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π..^π)) β dom (π₯ β (π(,)π) β¦ π΅) = (π(,)π)) |
73 | 68, 72 | eqtrd 2772 |
. . . . . . . . . . 11
β’ ((π β§ π β (π..^π)) β dom (β D (π₯ β (π(,)π) β¦ π΄)) = (π(,)π)) |
74 | 67, 73 | feq12d 6702 |
. . . . . . . . . 10
β’ ((π β§ π β (π..^π)) β ((β D (π₯ β (π(,)π) β¦ π΄)):dom (β D (π₯ β (π(,)π) β¦ π΄))βΆβ β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ)) |
75 | 66, 74 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π β (π..^π)) β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ) |
76 | 75 | fvmptelcdm 7109 |
. . . . . . . 8
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)π)) β π΅ β β) |
77 | 60, 76 | syldan 591 |
. . . . . . 7
β’ (((π β§ π β (π..^π)) β§ π₯ β (π(,)(π + 1))) β π΅ β β) |
78 | 77 | anasss 467 |
. . . . . 6
β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π΅ β β) |
79 | 42 | adantrr 715 |
. . . . . 6
β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β π β β) |
80 | 78, 79 | lenegd 11789 |
. . . . 5
β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β (π΅ β€ π β -π β€ -π΅)) |
81 | 44, 80 | mpbid 231 |
. . . 4
β’ ((π β§ (π β (π..^π) β§ π₯ β (π(,)(π + 1)))) β -π β€ -π΅) |
82 | 1, 23, 25, 37, 39, 41, 43, 81 | dvfsumle 25529 |
. . 3
β’ (π β Ξ£π β (π..^π)-π β€ (-π· β -πΆ)) |
83 | | fzofi 13935 |
. . . . 5
β’ (π..^π) β Fin |
84 | 83 | a1i 11 |
. . . 4
β’ (π β (π..^π) β Fin) |
85 | 42 | recnd 11238 |
. . . 4
β’ ((π β§ π β (π..^π)) β π β β) |
86 | 84, 85 | fsumneg 15729 |
. . 3
β’ (π β Ξ£π β (π..^π)-π = -Ξ£π β (π..^π)π) |
87 | 40 | eleq1d 2818 |
. . . . . . 7
β’ (π₯ = π β (π΄ β β β π· β β)) |
88 | | eqid 2732 |
. . . . . . . . 9
β’ (π₯ β (π[,]π) β¦ π΄) = (π₯ β (π[,]π) β¦ π΄) |
89 | 88 | fmpt 7106 |
. . . . . . . 8
β’
(βπ₯ β
(π[,]π)π΄ β β β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
90 | 31, 89 | sylibr 233 |
. . . . . . 7
β’ (π β βπ₯ β (π[,]π)π΄ β β) |
91 | 9 | rexrd 11260 |
. . . . . . . 8
β’ (π β π β
β*) |
92 | 12 | rexrd 11260 |
. . . . . . . 8
β’ (π β π β
β*) |
93 | | eluzle 12831 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β π β€ π) |
94 | 1, 93 | syl 17 |
. . . . . . . 8
β’ (π β π β€ π) |
95 | | ubicc2 13438 |
. . . . . . . 8
β’ ((π β β*
β§ π β
β* β§ π
β€ π) β π β (π[,]π)) |
96 | 91, 92, 94, 95 | syl3anc 1371 |
. . . . . . 7
β’ (π β π β (π[,]π)) |
97 | 87, 90, 96 | rspcdva 3613 |
. . . . . 6
β’ (π β π· β β) |
98 | 97 | recnd 11238 |
. . . . 5
β’ (π β π· β β) |
99 | 38 | eleq1d 2818 |
. . . . . . 7
β’ (π₯ = π β (π΄ β β β πΆ β β)) |
100 | | lbicc2 13437 |
. . . . . . . 8
β’ ((π β β*
β§ π β
β* β§ π
β€ π) β π β (π[,]π)) |
101 | 91, 92, 94, 100 | syl3anc 1371 |
. . . . . . 7
β’ (π β π β (π[,]π)) |
102 | 99, 90, 101 | rspcdva 3613 |
. . . . . 6
β’ (π β πΆ β β) |
103 | 102 | recnd 11238 |
. . . . 5
β’ (π β πΆ β β) |
104 | 98, 103 | neg2subd 11584 |
. . . 4
β’ (π β (-π· β -πΆ) = (πΆ β π·)) |
105 | 98, 103 | negsubdi2d 11583 |
. . . 4
β’ (π β -(π· β πΆ) = (πΆ β π·)) |
106 | 104, 105 | eqtr4d 2775 |
. . 3
β’ (π β (-π· β -πΆ) = -(π· β πΆ)) |
107 | 82, 86, 106 | 3brtr3d 5178 |
. 2
β’ (π β -Ξ£π β (π..^π)π β€ -(π· β πΆ)) |
108 | 97, 102 | resubcld 11638 |
. . 3
β’ (π β (π· β πΆ) β β) |
109 | 84, 42 | fsumrecl 15676 |
. . 3
β’ (π β Ξ£π β (π..^π)π β β) |
110 | 108, 109 | lenegd 11789 |
. 2
β’ (π β ((π· β πΆ) β€ Ξ£π β (π..^π)π β -Ξ£π β (π..^π)π β€ -(π· β πΆ))) |
111 | 107, 110 | mpbird 256 |
1
β’ (π β (π· β πΆ) β€ Ξ£π β (π..^π)π) |