Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π β (πβπ) = (πβπ)) |
2 | 1 | fveq1d 6848 |
. . . . . . . 8
β’ (π = π β ((πβπ)βπ₯) = ((πβπ)βπ₯)) |
3 | 2 | cbvmptv 5222 |
. . . . . . 7
β’ (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ₯)) |
4 | | fveq2 6846 |
. . . . . . . 8
β’ (π₯ = π¦ β ((πβπ)βπ₯) = ((πβπ)βπ¦)) |
5 | 4 | mpteq2dv 5211 |
. . . . . . 7
β’ (π₯ = π¦ β (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ¦))) |
6 | 3, 5 | eqtrid 2785 |
. . . . . 6
β’ (π₯ = π¦ β (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ¦))) |
7 | 6 | rneqd 5897 |
. . . . 5
β’ (π₯ = π¦ β ran (π β β β¦ ((πβπ)βπ₯)) = ran (π β β β¦ ((πβπ)βπ¦))) |
8 | 7 | supeq1d 9390 |
. . . 4
β’ (π₯ = π¦ β sup(ran (π β β β¦ ((πβπ)βπ₯)), β, < ) = sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < )) |
9 | 8 | cbvmptv 5222 |
. . 3
β’ (π₯ β β β¦ sup(ran
(π β β β¦
((πβπ)βπ₯)), β, < )) = (π¦ β β β¦ sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < )) |
10 | | itg2i1fseq.3 |
. . . . 5
β’ (π β π:ββΆdom
β«1) |
11 | 10 | ffvelcdmda 7039 |
. . . 4
β’ ((π β§ π β β) β (πβπ) β dom
β«1) |
12 | | i1fmbf 25062 |
. . . 4
β’ ((πβπ) β dom β«1 β (πβπ) β MblFn) |
13 | 11, 12 | syl 17 |
. . 3
β’ ((π β§ π β β) β (πβπ) β MblFn) |
14 | | i1ff 25063 |
. . . . 5
β’ ((πβπ) β dom β«1 β (πβπ):ββΆβ) |
15 | 11, 14 | syl 17 |
. . . 4
β’ ((π β§ π β β) β (πβπ):ββΆβ) |
16 | | itg2i1fseq.4 |
. . . . . 6
β’ (π β βπ β β (0π
βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) |
17 | 1 | breq2d 5121 |
. . . . . . . 8
β’ (π = π β (0π
βr β€ (πβπ) β 0π
βr β€ (πβπ))) |
18 | | fvoveq1 7384 |
. . . . . . . . 9
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
19 | 1, 18 | breq12d 5122 |
. . . . . . . 8
β’ (π = π β ((πβπ) βr β€ (πβ(π + 1)) β (πβπ) βr β€ (πβ(π + 1)))) |
20 | 17, 19 | anbi12d 632 |
. . . . . . 7
β’ (π = π β ((0π
βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β (0π
βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))))) |
21 | 20 | rspccva 3582 |
. . . . . 6
β’
((βπ β
β (0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1))) β§ π β β) β
(0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) |
22 | 16, 21 | sylan 581 |
. . . . 5
β’ ((π β§ π β β) β
(0π βr β€ (πβπ) β§ (πβπ) βr β€ (πβ(π + 1)))) |
23 | 22 | simpld 496 |
. . . 4
β’ ((π β§ π β β) β 0π
βr β€ (πβπ)) |
24 | | 0plef 25059 |
. . . 4
β’ ((πβπ):ββΆ(0[,)+β) β
((πβπ):ββΆβ β§
0π βr β€ (πβπ))) |
25 | 15, 23, 24 | sylanbrc 584 |
. . 3
β’ ((π β§ π β β) β (πβπ):ββΆ(0[,)+β)) |
26 | 22 | simprd 497 |
. . 3
β’ ((π β§ π β β) β (πβπ) βr β€ (πβ(π + 1))) |
27 | | rge0ssre 13382 |
. . . . 5
β’
(0[,)+β) β β |
28 | | itg2i1fseq.2 |
. . . . . 6
β’ (π β πΉ:ββΆ(0[,)+β)) |
29 | 28 | ffvelcdmda 7039 |
. . . . 5
β’ ((π β§ π¦ β β) β (πΉβπ¦) β (0[,)+β)) |
30 | 27, 29 | sselid 3946 |
. . . 4
β’ ((π β§ π¦ β β) β (πΉβπ¦) β β) |
31 | | itg2i1fseq.1 |
. . . . . . . . 9
β’ (π β πΉ β MblFn) |
32 | | itg2i1fseq.5 |
. . . . . . . . 9
β’ (π β βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) |
33 | 31, 28, 10, 16, 32 | itg2i1fseqle 25142 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβπ) βr β€ πΉ) |
34 | 15 | ffnd 6673 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβπ) Fn β) |
35 | 28 | ffnd 6673 |
. . . . . . . . . 10
β’ (π β πΉ Fn β) |
36 | 35 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΉ Fn β) |
37 | | reex 11150 |
. . . . . . . . . 10
β’ β
β V |
38 | 37 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β β) β β β
V) |
39 | | inidm 4182 |
. . . . . . . . 9
β’ (β
β© β) = β |
40 | | eqidd 2734 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π¦ β β) β ((πβπ)βπ¦) = ((πβπ)βπ¦)) |
41 | | eqidd 2734 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π¦ β β) β (πΉβπ¦) = (πΉβπ¦)) |
42 | 34, 36, 38, 38, 39, 40, 41 | ofrfval 7631 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πβπ) βr β€ πΉ β βπ¦ β β ((πβπ)βπ¦) β€ (πΉβπ¦))) |
43 | 33, 42 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π β β) β βπ¦ β β ((πβπ)βπ¦) β€ (πΉβπ¦)) |
44 | 43 | r19.21bi 3233 |
. . . . . 6
β’ (((π β§ π β β) β§ π¦ β β) β ((πβπ)βπ¦) β€ (πΉβπ¦)) |
45 | 44 | an32s 651 |
. . . . 5
β’ (((π β§ π¦ β β) β§ π β β) β ((πβπ)βπ¦) β€ (πΉβπ¦)) |
46 | 45 | ralrimiva 3140 |
. . . 4
β’ ((π β§ π¦ β β) β βπ β β ((πβπ)βπ¦) β€ (πΉβπ¦)) |
47 | | brralrspcev 5169 |
. . . 4
β’ (((πΉβπ¦) β β β§ βπ β β ((πβπ)βπ¦) β€ (πΉβπ¦)) β βπ§ β β βπ β β ((πβπ)βπ¦) β€ π§) |
48 | 30, 46, 47 | syl2anc 585 |
. . 3
β’ ((π β§ π¦ β β) β βπ§ β β βπ β β ((πβπ)βπ¦) β€ π§) |
49 | 1 | fveq2d 6850 |
. . . . . 6
β’ (π = π β (β«2β(πβπ)) = (β«2β(πβπ))) |
50 | 49 | cbvmptv 5222 |
. . . . 5
β’ (π β β β¦
(β«2β(πβπ))) = (π β β β¦
(β«2β(πβπ))) |
51 | 50 | rneqi 5896 |
. . . 4
β’ ran
(π β β β¦
(β«2β(πβπ))) = ran (π β β β¦
(β«2β(πβπ))) |
52 | 51 | supeq1i 9391 |
. . 3
β’ sup(ran
(π β β β¦
(β«2β(πβπ))), β*, < ) = sup(ran
(π β β β¦
(β«2β(πβπ))), β*, <
) |
53 | 9, 13, 25, 26, 48, 52 | itg2mono 25141 |
. 2
β’ (π β
(β«2β(π₯
β β β¦ sup(ran (π β β β¦ ((πβπ)βπ₯)), β, < ))) = sup(ran (π β β β¦
(β«2β(πβπ))), β*, <
)) |
54 | 28 | feqmptd 6914 |
. . . . 5
β’ (π β πΉ = (π¦ β β β¦ (πΉβπ¦))) |
55 | 1 | fveq1d 6848 |
. . . . . . . . . 10
β’ (π = π β ((πβπ)βπ¦) = ((πβπ)βπ¦)) |
56 | 55 | cbvmptv 5222 |
. . . . . . . . 9
β’ (π β β β¦ ((πβπ)βπ¦)) = (π β β β¦ ((πβπ)βπ¦)) |
57 | 56 | rneqi 5896 |
. . . . . . . 8
β’ ran
(π β β β¦
((πβπ)βπ¦)) = ran (π β β β¦ ((πβπ)βπ¦)) |
58 | 57 | supeq1i 9391 |
. . . . . . 7
β’ sup(ran
(π β β β¦
((πβπ)βπ¦)), β, < ) = sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < ) |
59 | | nnuz 12814 |
. . . . . . . . 9
β’ β =
(β€β₯β1) |
60 | | 1zzd 12542 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β 1 β
β€) |
61 | 15 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π¦ β β) β ((πβπ)βπ¦) β β) |
62 | 61 | an32s 651 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π β β) β ((πβπ)βπ¦) β β) |
63 | 62, 56 | fmptd 7066 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (π β β β¦ ((πβπ)βπ¦)):ββΆβ) |
64 | | peano2nn 12173 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π + 1) β
β) |
65 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . 17
β’ ((π:ββΆdom
β«1 β§ (π
+ 1) β β) β (πβ(π + 1)) β dom
β«1) |
66 | 10, 64, 65 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πβ(π + 1)) β dom
β«1) |
67 | | i1ff 25063 |
. . . . . . . . . . . . . . . 16
β’ ((πβ(π + 1)) β dom β«1 β
(πβ(π +
1)):ββΆβ) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πβ(π +
1)):ββΆβ) |
69 | 68 | ffnd 6673 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πβ(π + 1)) Fn β) |
70 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π¦ β β) β ((πβ(π + 1))βπ¦) = ((πβ(π + 1))βπ¦)) |
71 | 34, 69, 38, 38, 39, 40, 70 | ofrfval 7631 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((πβπ) βr β€ (πβ(π + 1)) β βπ¦ β β ((πβπ)βπ¦) β€ ((πβ(π + 1))βπ¦))) |
72 | 26, 71 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β βπ¦ β β ((πβπ)βπ¦) β€ ((πβ(π + 1))βπ¦)) |
73 | 72 | r19.21bi 3233 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π¦ β β) β ((πβπ)βπ¦) β€ ((πβ(π + 1))βπ¦)) |
74 | 73 | an32s 651 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π β β) β ((πβπ)βπ¦) β€ ((πβ(π + 1))βπ¦)) |
75 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π β β β¦ ((πβπ)βπ¦)) = (π β β β¦ ((πβπ)βπ¦)) |
76 | | fvex 6859 |
. . . . . . . . . . . 12
β’ ((πβπ)βπ¦) β V |
77 | 55, 75, 76 | fvmpt 6952 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦ ((πβπ)βπ¦))βπ) = ((πβπ)βπ¦)) |
78 | 77 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π β β) β ((π β β β¦ ((πβπ)βπ¦))βπ) = ((πβπ)βπ¦)) |
79 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β (πβπ) = (πβ(π + 1))) |
80 | 79 | fveq1d 6848 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β ((πβπ)βπ¦) = ((πβ(π + 1))βπ¦)) |
81 | | fvex 6859 |
. . . . . . . . . . . . 13
β’ ((πβ(π + 1))βπ¦) β V |
82 | 80, 75, 81 | fvmpt 6952 |
. . . . . . . . . . . 12
β’ ((π + 1) β β β
((π β β β¦
((πβπ)βπ¦))β(π + 1)) = ((πβ(π + 1))βπ¦)) |
83 | 64, 82 | syl 17 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦ ((πβπ)βπ¦))β(π + 1)) = ((πβ(π + 1))βπ¦)) |
84 | 83 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π β β) β ((π β β β¦ ((πβπ)βπ¦))β(π + 1)) = ((πβ(π + 1))βπ¦)) |
85 | 74, 78, 84 | 3brtr4d 5141 |
. . . . . . . . 9
β’ (((π β§ π¦ β β) β§ π β β) β ((π β β β¦ ((πβπ)βπ¦))βπ) β€ ((π β β β¦ ((πβπ)βπ¦))β(π + 1))) |
86 | 77 | breq1d 5119 |
. . . . . . . . . . . 12
β’ (π β β β (((π β β β¦ ((πβπ)βπ¦))βπ) β€ π§ β ((πβπ)βπ¦) β€ π§)) |
87 | 86 | ralbiia 3091 |
. . . . . . . . . . 11
β’
(βπ β
β ((π β β
β¦ ((πβπ)βπ¦))βπ) β€ π§ β βπ β β ((πβπ)βπ¦) β€ π§) |
88 | 87 | rexbii 3094 |
. . . . . . . . . 10
β’
(βπ§ β
β βπ β
β ((π β β
β¦ ((πβπ)βπ¦))βπ) β€ π§ β βπ§ β β βπ β β ((πβπ)βπ¦) β€ π§) |
89 | 48, 88 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β βπ§ β β βπ β β ((π β β β¦ ((πβπ)βπ¦))βπ) β€ π§) |
90 | 59, 60, 63, 85, 89 | climsup 15563 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (π β β β¦ ((πβπ)βπ¦)) β sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < )) |
91 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β ((πβπ)βπ₯) = ((πβπ)βπ¦)) |
92 | 91 | mpteq2dv 5211 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ¦))) |
93 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
94 | 92, 93 | breq12d 5122 |
. . . . . . . . . 10
β’ (π₯ = π¦ β ((π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯) β (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦))) |
95 | 94 | rspccva 3582 |
. . . . . . . . 9
β’
((βπ₯ β
β (π β β
β¦ ((πβπ)βπ₯)) β (πΉβπ₯) β§ π¦ β β) β (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) |
96 | 32, 95 | sylan 581 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) |
97 | | climuni 15443 |
. . . . . . . 8
β’ (((π β β β¦ ((πβπ)βπ¦)) β sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < ) β§ (π β β β¦ ((πβπ)βπ¦)) β (πΉβπ¦)) β sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < ) = (πΉβπ¦)) |
98 | 90, 96, 97 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π¦ β β) β sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < ) = (πΉβπ¦)) |
99 | 58, 98 | eqtr3id 2787 |
. . . . . 6
β’ ((π β§ π¦ β β) β sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < ) = (πΉβπ¦)) |
100 | 99 | mpteq2dva 5209 |
. . . . 5
β’ (π β (π¦ β β β¦ sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < )) = (π¦ β β β¦ (πΉβπ¦))) |
101 | 54, 100 | eqtr4d 2776 |
. . . 4
β’ (π β πΉ = (π¦ β β β¦ sup(ran (π β β β¦ ((πβπ)βπ¦)), β, < ))) |
102 | 101, 9 | eqtr4di 2791 |
. . 3
β’ (π β πΉ = (π₯ β β β¦ sup(ran (π β β β¦ ((πβπ)βπ₯)), β, < ))) |
103 | 102 | fveq2d 6850 |
. 2
β’ (π β
(β«2βπΉ)
= (β«2β(π₯ β β β¦ sup(ran (π β β β¦ ((πβπ)βπ₯)), β, < )))) |
104 | | itg2i1fseq.6 |
. . . . . 6
β’ π = (π β β β¦
(β«1β(πβπ))) |
105 | | itg2itg1 25124 |
. . . . . . . 8
β’ (((πβπ) β dom β«1 β§
0π βr β€ (πβπ)) β (β«2β(πβπ)) = (β«1β(πβπ))) |
106 | 11, 23, 105 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β β) β
(β«2β(πβπ)) = (β«1β(πβπ))) |
107 | 106 | mpteq2dva 5209 |
. . . . . 6
β’ (π β (π β β β¦
(β«2β(πβπ))) = (π β β β¦
(β«1β(πβπ)))) |
108 | 104, 107 | eqtr4id 2792 |
. . . . 5
β’ (π β π = (π β β β¦
(β«2β(πβπ)))) |
109 | 108, 50 | eqtr4di 2791 |
. . . 4
β’ (π β π = (π β β β¦
(β«2β(πβπ)))) |
110 | 109 | rneqd 5897 |
. . 3
β’ (π β ran π = ran (π β β β¦
(β«2β(πβπ)))) |
111 | 110 | supeq1d 9390 |
. 2
β’ (π β sup(ran π, β*, < ) = sup(ran
(π β β β¦
(β«2β(πβπ))), β*, <
)) |
112 | 53, 103, 111 | 3eqtr4d 2783 |
1
β’ (π β
(β«2βπΉ)
= sup(ran π,
β*, < )) |