Step | Hyp | Ref
| Expression |
1 | | nnuz 12814 |
. . 3
β’ β =
(β€β₯β1) |
2 | | 1zzd 12542 |
. . 3
β’ (π β 1 β
β€) |
3 | | itg2i1fseq.3 |
. . . . . 6
β’ (π β π:ββΆdom
β«1) |
4 | 3 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β§ π β β) β (πβπ) β dom
β«1) |
5 | | itg1cl 25072 |
. . . . 5
β’ ((πβπ) β dom β«1 β
(β«1β(πβπ)) β β) |
6 | 4, 5 | syl 17 |
. . . 4
β’ ((π β§ π β β) β
(β«1β(πβπ)) β β) |
7 | | itg2i1fseq.6 |
. . . 4
β’ π = (π β β β¦
(β«1β(πβπ))) |
8 | 6, 7 | fmptd 7066 |
. . 3
β’ (π β π:ββΆβ) |
9 | 3 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β§ π β β) β (πβπ) β dom
β«1) |
10 | | peano2nn 12173 |
. . . . . 6
β’ (π β β β (π + 1) β
β) |
11 | | ffvelcdm 7036 |
. . . . . 6
β’ ((π:ββΆdom
β«1 β§ (π
+ 1) β β) β (πβ(π + 1)) β dom
β«1) |
12 | 3, 10, 11 | syl2an 597 |
. . . . 5
β’ ((π β§ π β β) β (πβ(π + 1)) β dom
β«1) |
13 | | itg2i1fseq.4 |
. . . . . . 7
β’ (π β βπ β β (0π
βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) |
14 | | simpr 486 |
. . . . . . . 8
β’
((0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β (πβπ) βr β€ (πβ(π + 1))) |
15 | 14 | ralimi 3083 |
. . . . . . 7
β’
(βπ β
β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β βπ β β (πβπ) βr β€ (πβ(π + 1))) |
16 | 13, 15 | syl 17 |
. . . . . 6
β’ (π β βπ β β (πβπ) βr β€ (πβ(π + 1))) |
17 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
18 | | fvoveq1 7384 |
. . . . . . . 8
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
19 | 17, 18 | breq12d 5122 |
. . . . . . 7
β’ (π = π β ((πβπ) βr β€ (πβ(π + 1)) β (πβπ) βr β€ (πβ(π + 1)))) |
20 | 19 | rspccva 3582 |
. . . . . 6
β’
((βπ β
β (πβπ) βr β€
(πβ(π + 1)) β§ π β β) β (πβπ) βr β€ (πβ(π + 1))) |
21 | 16, 20 | sylan 581 |
. . . . 5
β’ ((π β§ π β β) β (πβπ) βr β€ (πβ(π + 1))) |
22 | | itg1le 25101 |
. . . . 5
β’ (((πβπ) β dom β«1 β§ (πβ(π + 1)) β dom β«1 β§
(πβπ) βr β€ (πβ(π + 1))) β
(β«1β(πβπ)) β€ (β«1β(πβ(π + 1)))) |
23 | 9, 12, 21, 22 | syl3anc 1372 |
. . . 4
β’ ((π β§ π β β) β
(β«1β(πβπ)) β€ (β«1β(πβ(π + 1)))) |
24 | | 2fveq3 6851 |
. . . . . 6
β’ (π = π β (β«1β(πβπ)) = (β«1β(πβπ))) |
25 | | fvex 6859 |
. . . . . 6
β’
(β«1β(πβπ)) β V |
26 | 24, 7, 25 | fvmpt 6952 |
. . . . 5
β’ (π β β β (πβπ) = (β«1β(πβπ))) |
27 | 26 | adantl 483 |
. . . 4
β’ ((π β§ π β β) β (πβπ) = (β«1β(πβπ))) |
28 | | 2fveq3 6851 |
. . . . . . 7
β’ (π = (π + 1) β (β«1β(πβπ)) = (β«1β(πβ(π + 1)))) |
29 | | fvex 6859 |
. . . . . . 7
β’
(β«1β(πβ(π + 1))) β V |
30 | 28, 7, 29 | fvmpt 6952 |
. . . . . 6
β’ ((π + 1) β β β
(πβ(π + 1)) =
(β«1β(πβ(π + 1)))) |
31 | 10, 30 | syl 17 |
. . . . 5
β’ (π β β β (πβ(π + 1)) = (β«1β(πβ(π + 1)))) |
32 | 31 | adantl 483 |
. . . 4
β’ ((π β§ π β β) β (πβ(π + 1)) = (β«1β(πβ(π + 1)))) |
33 | 23, 27, 32 | 3brtr4d 5141 |
. . 3
β’ ((π β§ π β β) β (πβπ) β€ (πβ(π + 1))) |
34 | | itg2i1fseq2.7 |
. . . 4
β’ (π β π β β) |
35 | | itg2i1fseq2.8 |
. . . . . 6
β’ ((π β§ π β β) β
(β«1β(πβπ)) β€ π) |
36 | 27, 35 | eqbrtrd 5131 |
. . . . 5
β’ ((π β§ π β β) β (πβπ) β€ π) |
37 | 36 | ralrimiva 3140 |
. . . 4
β’ (π β βπ β β (πβπ) β€ π) |
38 | | brralrspcev 5169 |
. . . 4
β’ ((π β β β§
βπ β β
(πβπ) β€ π) β βπ§ β β βπ β β (πβπ) β€ π§) |
39 | 34, 37, 38 | syl2anc 585 |
. . 3
β’ (π β βπ§ β β βπ β β (πβπ) β€ π§) |
40 | 1, 2, 8, 33, 39 | climsup 15563 |
. 2
β’ (π β π β sup(ran π, β, < )) |
41 | | itg2i1fseq.1 |
. . . 4
β’ (π β πΉ β MblFn) |
42 | | itg2i1fseq.2 |
. . . 4
β’ (π β πΉ:ββΆ(0[,)+β)) |
43 | | itg2i1fseq.5 |
. . . 4
β’ (π β βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) |
44 | 41, 42, 3, 13, 43, 7 | itg2i1fseq 25143 |
. . 3
β’ (π β
(β«2βπΉ)
= sup(ran π,
β*, < )) |
45 | 8 | frnd 6680 |
. . . 4
β’ (π β ran π β β) |
46 | 7, 6 | dmmptd 6650 |
. . . . . 6
β’ (π β dom π = β) |
47 | | 1nn 12172 |
. . . . . . 7
β’ 1 β
β |
48 | | ne0i 4298 |
. . . . . . 7
β’ (1 β
β β β β β
) |
49 | 47, 48 | mp1i 13 |
. . . . . 6
β’ (π β β β
β
) |
50 | 46, 49 | eqnetrd 3008 |
. . . . 5
β’ (π β dom π β β
) |
51 | | dm0rn0 5884 |
. . . . . 6
β’ (dom
π = β
β ran
π =
β
) |
52 | 51 | necon3bii 2993 |
. . . . 5
β’ (dom
π β β
β ran
π β
β
) |
53 | 50, 52 | sylib 217 |
. . . 4
β’ (π β ran π β β
) |
54 | | ffn 6672 |
. . . . . . 7
β’ (π:ββΆβ β
π Fn
β) |
55 | | breq1 5112 |
. . . . . . . 8
β’ (π¦ = (πβπ) β (π¦ β€ π§ β (πβπ) β€ π§)) |
56 | 55 | ralrn 7042 |
. . . . . . 7
β’ (π Fn β β
(βπ¦ β ran π π¦ β€ π§ β βπ β β (πβπ) β€ π§)) |
57 | 8, 54, 56 | 3syl 18 |
. . . . . 6
β’ (π β (βπ¦ β ran π π¦ β€ π§ β βπ β β (πβπ) β€ π§)) |
58 | 57 | rexbidv 3172 |
. . . . 5
β’ (π β (βπ§ β β βπ¦ β ran π π¦ β€ π§ β βπ§ β β βπ β β (πβπ) β€ π§)) |
59 | 39, 58 | mpbird 257 |
. . . 4
β’ (π β βπ§ β β βπ¦ β ran π π¦ β€ π§) |
60 | | supxrre 13255 |
. . . 4
β’ ((ran
π β β β§ ran
π β β
β§
βπ§ β β
βπ¦ β ran π π¦ β€ π§) β sup(ran π, β*, < ) = sup(ran
π, β, <
)) |
61 | 45, 53, 59, 60 | syl3anc 1372 |
. . 3
β’ (π β sup(ran π, β*, < ) = sup(ran
π, β, <
)) |
62 | 44, 61 | eqtrd 2773 |
. 2
β’ (π β
(β«2βπΉ)
= sup(ran π, β, <
)) |
63 | 40, 62 | breqtrrd 5137 |
1
β’ (π β π β (β«2βπΉ)) |