Step | Hyp | Ref
| Expression |
1 | | sge0isum.z |
. . . . . 6
β’ π =
(β€β₯βπ) |
2 | 1 | fvexi 6905 |
. . . . 5
β’ π β V |
3 | 2 | a1i 11 |
. . . 4
β’ (π β π β V) |
4 | | sge0isum.f |
. . . . 5
β’ (π β πΉ:πβΆ(0[,)+β)) |
5 | | icossicc 13412 |
. . . . . 6
β’
(0[,)+β) β (0[,]+β) |
6 | 5 | a1i 11 |
. . . . 5
β’ (π β (0[,)+β) β
(0[,]+β)) |
7 | 4, 6 | fssd 6735 |
. . . 4
β’ (π β πΉ:πβΆ(0[,]+β)) |
8 | 3, 7 | sge0xrcl 45091 |
. . 3
β’ (π β
(Ξ£^βπΉ) β
β*) |
9 | | sge0isum.m |
. . . . 5
β’ (π β π β β€) |
10 | | sge0isum.g |
. . . . . 6
β’ πΊ = seqπ( + , πΉ) |
11 | | eqidd 2733 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) = (πΉβπ)) |
12 | | rge0ssre 13432 |
. . . . . . 7
β’
(0[,)+β) β β |
13 | 4 | ffvelcdmda 7086 |
. . . . . . 7
β’ ((π β§ π β π) β (πΉβπ) β (0[,)+β)) |
14 | 12, 13 | sselid 3980 |
. . . . . 6
β’ ((π β§ π β π) β (πΉβπ) β β) |
15 | | 0xr 11260 |
. . . . . . . 8
β’ 0 β
β* |
16 | 15 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π) β 0 β
β*) |
17 | | pnfxr 11267 |
. . . . . . . 8
β’ +β
β β* |
18 | 17 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β π) β +β β
β*) |
19 | | icogelb 13374 |
. . . . . . 7
β’ ((0
β β* β§ +β β β* β§
(πΉβπ) β (0[,)+β)) β 0 β€ (πΉβπ)) |
20 | 16, 18, 13, 19 | syl3anc 1371 |
. . . . . 6
β’ ((π β§ π β π) β 0 β€ (πΉβπ)) |
21 | | seqex 13967 |
. . . . . . . . . . 11
β’ seqπ( + , πΉ) β V |
22 | 10, 21 | eqeltri 2829 |
. . . . . . . . . 10
β’ πΊ β V |
23 | 22 | a1i 11 |
. . . . . . . . 9
β’ (π β πΊ β V) |
24 | | sge0isum.gcnv |
. . . . . . . . . 10
β’ (π β πΊ β π΅) |
25 | | climcl 15442 |
. . . . . . . . . 10
β’ (πΊ β π΅ β π΅ β β) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
β’ (π β π΅ β β) |
27 | | breldmg 5909 |
. . . . . . . . 9
β’ ((πΊ β V β§ π΅ β β β§ πΊ β π΅) β πΊ β dom β ) |
28 | 23, 26, 24, 27 | syl3anc 1371 |
. . . . . . . 8
β’ (π β πΊ β dom β ) |
29 | 10 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β πΊ = seqπ( + , πΉ)) |
30 | 29 | fveq1d 6893 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΊβπ) = (seqπ( + , πΉ)βπ)) |
31 | 1 | eleq2i 2825 |
. . . . . . . . . . . . . 14
β’ (π β π β π β (β€β₯βπ)) |
32 | 31 | biimpi 215 |
. . . . . . . . . . . . 13
β’ (π β π β π β (β€β₯βπ)) |
33 | 32 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
34 | | simpll 765 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β (π...π)) β π) |
35 | | elfzuz 13496 |
. . . . . . . . . . . . . . 15
β’ (π β (π...π) β π β (β€β₯βπ)) |
36 | 35, 1 | eleqtrrdi 2844 |
. . . . . . . . . . . . . 14
β’ (π β (π...π) β π β π) |
37 | 36 | adantl 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π) β§ π β (π...π)) β π β π) |
38 | 34, 37, 14 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ π β (π...π)) β (πΉβπ) β β) |
39 | | readdcl 11192 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β) β (π + π) β β) |
40 | 39 | adantl 482 |
. . . . . . . . . . . 12
β’ (((π β§ π β π) β§ (π β β β§ π β β)) β (π + π) β β) |
41 | 33, 38, 40 | seqcl 13987 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
42 | 30, 41 | eqeltrd 2833 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (πΊβπ) β β) |
43 | 42 | recnd 11241 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΊβπ) β β) |
44 | 43 | ralrimiva 3146 |
. . . . . . . 8
β’ (π β βπ β π (πΊβπ) β β) |
45 | 1 | climbdd 15617 |
. . . . . . . 8
β’ ((π β β€ β§ πΊ β dom β β§
βπ β π (πΊβπ) β β) β βπ₯ β β βπ β π (absβ(πΊβπ)) β€ π₯) |
46 | 9, 28, 44, 45 | syl3anc 1371 |
. . . . . . 7
β’ (π β βπ₯ β β βπ β π (absβ(πΊβπ)) β€ π₯) |
47 | 42 | ad4ant13 749 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π β π) β§ (absβ(πΊβπ)) β€ π₯) β (πΊβπ) β β) |
48 | 43 | ad4ant13 749 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π β π) β§ (absβ(πΊβπ)) β€ π₯) β (πΊβπ) β β) |
49 | 48 | abscld 15382 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π β π) β§ (absβ(πΊβπ)) β€ π₯) β (absβ(πΊβπ)) β β) |
50 | | simpllr 774 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π β π) β§ (absβ(πΊβπ)) β€ π₯) β π₯ β β) |
51 | 47 | leabsd 15360 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π β π) β§ (absβ(πΊβπ)) β€ π₯) β (πΊβπ) β€ (absβ(πΊβπ))) |
52 | | simpr 485 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π β π) β§ (absβ(πΊβπ)) β€ π₯) β (absβ(πΊβπ)) β€ π₯) |
53 | 47, 49, 50, 51, 52 | letrd 11370 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β) β§ π β π) β§ (absβ(πΊβπ)) β€ π₯) β (πΊβπ) β€ π₯) |
54 | 53 | ex 413 |
. . . . . . . . 9
β’ (((π β§ π₯ β β) β§ π β π) β ((absβ(πΊβπ)) β€ π₯ β (πΊβπ) β€ π₯)) |
55 | 54 | ralimdva 3167 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β (βπ β π (absβ(πΊβπ)) β€ π₯ β βπ β π (πΊβπ) β€ π₯)) |
56 | 55 | reximdva 3168 |
. . . . . . 7
β’ (π β (βπ₯ β β βπ β π (absβ(πΊβπ)) β€ π₯ β βπ₯ β β βπ β π (πΊβπ) β€ π₯)) |
57 | 46, 56 | mpd 15 |
. . . . . 6
β’ (π β βπ₯ β β βπ β π (πΊβπ) β€ π₯) |
58 | 1, 10, 9, 11, 14, 20, 57 | isumsup2 15791 |
. . . . 5
β’ (π β πΊ β sup(ran πΊ, β, < )) |
59 | 1, 9, 58, 42 | climrecl 15526 |
. . . 4
β’ (π β sup(ran πΊ, β, < ) β
β) |
60 | 59 | rexrd 11263 |
. . 3
β’ (π β sup(ran πΊ, β, < ) β
β*) |
61 | 4 | feqmptd 6960 |
. . . . 5
β’ (π β πΉ = (π β π β¦ (πΉβπ))) |
62 | 61 | fveq2d 6895 |
. . . 4
β’ (π β
(Ξ£^βπΉ) =
(Ξ£^β(π β π β¦ (πΉβπ)))) |
63 | | mpteq1 5241 |
. . . . . . . . . . 11
β’ (π¦ = β
β (π β π¦ β¦ (πΉβπ)) = (π β β
β¦ (πΉβπ))) |
64 | 63 | fveq2d 6895 |
. . . . . . . . . 10
β’ (π¦ = β
β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) =
(Ξ£^β(π β β
β¦ (πΉβπ)))) |
65 | | mpt0 6692 |
. . . . . . . . . . . . 13
β’ (π β β
β¦ (πΉβπ)) = β
|
66 | 65 | fveq2i 6894 |
. . . . . . . . . . . 12
β’
(Ξ£^β(π β β
β¦ (πΉβπ))) =
(Ξ£^ββ
) |
67 | | sge00 45082 |
. . . . . . . . . . . 12
β’
(Ξ£^ββ
) = 0 |
68 | 66, 67 | eqtri 2760 |
. . . . . . . . . . 11
β’
(Ξ£^β(π β β
β¦ (πΉβπ))) = 0 |
69 | 68 | a1i 11 |
. . . . . . . . . 10
β’ (π¦ = β
β
(Ξ£^β(π β β
β¦ (πΉβπ))) = 0) |
70 | 64, 69 | eqtrd 2772 |
. . . . . . . . 9
β’ (π¦ = β
β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) = 0) |
71 | 70 | adantl 482 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π¦ = β
) β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) = 0) |
72 | | 0red 11216 |
. . . . . . . . . 10
β’ (π β 0 β
β) |
73 | 39 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β β β§ π β β)) β (π + π) β β) |
74 | 1, 9, 14, 73 | seqf 13988 |
. . . . . . . . . . . . 13
β’ (π β seqπ( + , πΉ):πβΆβ) |
75 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β πΊ = seqπ( + , πΉ)) |
76 | 75 | feq1d 6702 |
. . . . . . . . . . . . 13
β’ (π β (πΊ:πβΆβ β seqπ( + , πΉ):πβΆβ)) |
77 | 74, 76 | mpbird 256 |
. . . . . . . . . . . 12
β’ (π β πΊ:πβΆβ) |
78 | 77 | frnd 6725 |
. . . . . . . . . . 11
β’ (π β ran πΊ β β) |
79 | 77 | ffund 6721 |
. . . . . . . . . . . 12
β’ (π β Fun πΊ) |
80 | | uzid 12836 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β π β
(β€β₯βπ)) |
81 | 9, 80 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π β (β€β₯βπ)) |
82 | 1 | eqcomi 2741 |
. . . . . . . . . . . . . 14
β’
(β€β₯βπ) = π |
83 | 81, 82 | eleqtrdi 2843 |
. . . . . . . . . . . . 13
β’ (π β π β π) |
84 | 77 | fdmd 6728 |
. . . . . . . . . . . . . 14
β’ (π β dom πΊ = π) |
85 | 84 | eqcomd 2738 |
. . . . . . . . . . . . 13
β’ (π β π = dom πΊ) |
86 | 83, 85 | eleqtrd 2835 |
. . . . . . . . . . . 12
β’ (π β π β dom πΊ) |
87 | | fvelrn 7078 |
. . . . . . . . . . . 12
β’ ((Fun
πΊ β§ π β dom πΊ) β (πΊβπ) β ran πΊ) |
88 | 79, 86, 87 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β (πΊβπ) β ran πΊ) |
89 | 78, 88 | sseldd 3983 |
. . . . . . . . . 10
β’ (π β (πΊβπ) β β) |
90 | 15 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 0 β
β*) |
91 | 17 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β +β β
β*) |
92 | 4, 83 | ffvelcdmd 7087 |
. . . . . . . . . . . 12
β’ (π β (πΉβπ) β (0[,)+β)) |
93 | | icogelb 13374 |
. . . . . . . . . . . 12
β’ ((0
β β* β§ +β β β* β§
(πΉβπ) β (0[,)+β)) β 0 β€
(πΉβπ)) |
94 | 90, 91, 92, 93 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (π β 0 β€ (πΉβπ)) |
95 | 10 | fveq1i 6892 |
. . . . . . . . . . . . 13
β’ (πΊβπ) = (seqπ( + , πΉ)βπ) |
96 | 95 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (πΊβπ) = (seqπ( + , πΉ)βπ)) |
97 | | seq1 13978 |
. . . . . . . . . . . . 13
β’ (π β β€ β (seqπ( + , πΉ)βπ) = (πΉβπ)) |
98 | 9, 97 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (seqπ( + , πΉ)βπ) = (πΉβπ)) |
99 | 96, 98 | eqtr2d 2773 |
. . . . . . . . . . 11
β’ (π β (πΉβπ) = (πΊβπ)) |
100 | 94, 99 | breqtrd 5174 |
. . . . . . . . . 10
β’ (π β 0 β€ (πΊβπ)) |
101 | 88 | ne0d 4335 |
. . . . . . . . . . 11
β’ (π β ran πΊ β β
) |
102 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β ran πΊ) β π§ β ran πΊ) |
103 | 77 | ffnd 6718 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΊ Fn π) |
104 | | fvelrnb 6952 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΊ Fn π β (π§ β ran πΊ β βπ β π (πΊβπ) = π§)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π§ β ran πΊ β βπ β π (πΊβπ) = π§)) |
106 | 105 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β ran πΊ) β (π§ β ran πΊ β βπ β π (πΊβπ) = π§)) |
107 | 102, 106 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β ran πΊ) β βπ β π (πΊβπ) = π§) |
108 | 107 | adantlr 713 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ βπ β π (πΊβπ) β€ π₯) β§ π§ β ran πΊ) β βπ β π (πΊβπ) = π§) |
109 | | nfv 1917 |
. . . . . . . . . . . . . . . . . . 19
β’
β²ππ |
110 | | nfra1 3281 |
. . . . . . . . . . . . . . . . . . 19
β’
β²πβπ β π (πΊβπ) β€ π₯ |
111 | 109, 110 | nfan 1902 |
. . . . . . . . . . . . . . . . . 18
β’
β²π(π β§ βπ β π (πΊβπ) β€ π₯) |
112 | | nfv 1917 |
. . . . . . . . . . . . . . . . . 18
β’
β²π π§ β ran πΊ |
113 | 111, 112 | nfan 1902 |
. . . . . . . . . . . . . . . . 17
β’
β²π((π β§ βπ β π (πΊβπ) β€ π₯) β§ π§ β ran πΊ) |
114 | | nfv 1917 |
. . . . . . . . . . . . . . . . 17
β’
β²π π§ β€ π₯ |
115 | | rspa 3245 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((βπ β
π (πΊβπ) β€ π₯ β§ π β π) β (πΊβπ) β€ π₯) |
116 | 115 | 3adant3 1132 |
. . . . . . . . . . . . . . . . . . . 20
β’
((βπ β
π (πΊβπ) β€ π₯ β§ π β π β§ (πΊβπ) = π§) β (πΊβπ) β€ π₯) |
117 | | simp3 1138 |
. . . . . . . . . . . . . . . . . . . 20
β’
((βπ β
π (πΊβπ) β€ π₯ β§ π β π β§ (πΊβπ) = π§) β (πΊβπ) = π§) |
118 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΊβπ) = π§ β (πΊβπ) = π§) |
119 | 118 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΊβπ) = π§ β π§ = (πΊβπ)) |
120 | 119 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΊβπ) β€ π₯ β§ (πΊβπ) = π§) β π§ = (πΊβπ)) |
121 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΊβπ) β€ π₯ β§ (πΊβπ) = π§) β (πΊβπ) β€ π₯) |
122 | 120, 121 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πΊβπ) β€ π₯ β§ (πΊβπ) = π§) β π§ β€ π₯) |
123 | 116, 117,
122 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
β’
((βπ β
π (πΊβπ) β€ π₯ β§ π β π β§ (πΊβπ) = π§) β π§ β€ π₯) |
124 | 123 | 3exp 1119 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
π (πΊβπ) β€ π₯ β (π β π β ((πΊβπ) = π§ β π§ β€ π₯))) |
125 | 124 | ad2antlr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ βπ β π (πΊβπ) β€ π₯) β§ π§ β ran πΊ) β (π β π β ((πΊβπ) = π§ β π§ β€ π₯))) |
126 | 113, 114,
125 | rexlimd 3263 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ βπ β π (πΊβπ) β€ π₯) β§ π§ β ran πΊ) β (βπ β π (πΊβπ) = π§ β π§ β€ π₯)) |
127 | 108, 126 | mpd 15 |
. . . . . . . . . . . . . . 15
β’ (((π β§ βπ β π (πΊβπ) β€ π₯) β§ π§ β ran πΊ) β π§ β€ π₯) |
128 | 127 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
β’ ((π β§ βπ β π (πΊβπ) β€ π₯) β βπ§ β ran πΊ π§ β€ π₯) |
129 | 128 | ex 413 |
. . . . . . . . . . . . 13
β’ (π β (βπ β π (πΊβπ) β€ π₯ β βπ§ β ran πΊ π§ β€ π₯)) |
130 | 129 | reximdv 3170 |
. . . . . . . . . . . 12
β’ (π β (βπ₯ β β βπ β π (πΊβπ) β€ π₯ β βπ₯ β β βπ§ β ran πΊ π§ β€ π₯)) |
131 | 57, 130 | mpd 15 |
. . . . . . . . . . 11
β’ (π β βπ₯ β β βπ§ β ran πΊ π§ β€ π₯) |
132 | | suprub 12174 |
. . . . . . . . . . 11
β’ (((ran
πΊ β β β§ ran
πΊ β β
β§
βπ₯ β β
βπ§ β ran πΊ π§ β€ π₯) β§ (πΊβπ) β ran πΊ) β (πΊβπ) β€ sup(ran πΊ, β, < )) |
133 | 78, 101, 131, 88, 132 | syl31anc 1373 |
. . . . . . . . . 10
β’ (π β (πΊβπ) β€ sup(ran πΊ, β, < )) |
134 | 72, 89, 59, 100, 133 | letrd 11370 |
. . . . . . . . 9
β’ (π β 0 β€ sup(ran πΊ, β, <
)) |
135 | 134 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π¦ = β
) β 0 β€ sup(ran πΊ, β, <
)) |
136 | 71, 135 | eqbrtrd 5170 |
. . . . . . 7
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π¦ = β
) β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) β€ sup(ran πΊ, β, < )) |
137 | | simpr 485 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π β© Fin)) β π¦ β (π« π β© Fin)) |
138 | | simpll 765 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π β π¦) β π) |
139 | | elpwinss 43726 |
. . . . . . . . . . . . . 14
β’ (π¦ β (π« π β© Fin) β π¦ β π) |
140 | 139 | sselda 3982 |
. . . . . . . . . . . . 13
β’ ((π¦ β (π« π β© Fin) β§ π β π¦) β π β π) |
141 | 140 | adantll 712 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π β π¦) β π β π) |
142 | 5, 13 | sselid 3980 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ) β (0[,]+β)) |
143 | 138, 141,
142 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π β π¦) β (πΉβπ) β (0[,]+β)) |
144 | | eqid 2732 |
. . . . . . . . . . 11
β’ (π β π¦ β¦ (πΉβπ)) = (π β π¦ β¦ (πΉβπ)) |
145 | 143, 144 | fmptd 7113 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π β© Fin)) β (π β π¦ β¦ (πΉβπ)):π¦βΆ(0[,]+β)) |
146 | 137, 145 | sge0xrcl 45091 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π« π β© Fin)) β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) β
β*) |
147 | 146 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) β
β*) |
148 | | fzfid 13937 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π β© Fin)) β (π...sup(π¦, β, < )) β
Fin) |
149 | | elfzuz 13496 |
. . . . . . . . . . . . . 14
β’ (π β (π...sup(π¦, β, < )) β π β (β€β₯βπ)) |
150 | 149, 82 | eleqtrdi 2843 |
. . . . . . . . . . . . 13
β’ (π β (π...sup(π¦, β, < )) β π β π) |
151 | 150, 142 | sylan2 593 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π...sup(π¦, β, < ))) β (πΉβπ) β (0[,]+β)) |
152 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (π β (π...sup(π¦, β, < )) β¦ (πΉβπ)) = (π β (π...sup(π¦, β, < )) β¦ (πΉβπ)) |
153 | 151, 152 | fmptd 7113 |
. . . . . . . . . . 11
β’ (π β (π β (π...sup(π¦, β, < )) β¦ (πΉβπ)):(π...sup(π¦, β, <
))βΆ(0[,]+β)) |
154 | 153 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π β© Fin)) β (π β (π...sup(π¦, β, < )) β¦ (πΉβπ)):(π...sup(π¦, β, <
))βΆ(0[,]+β)) |
155 | 148, 154 | sge0xrcl 45091 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π« π β© Fin)) β
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ))) β
β*) |
156 | 155 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ))) β
β*) |
157 | 60 | adantr 481 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π« π β© Fin)) β sup(ran πΊ, β, < ) β
β*) |
158 | 157 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β sup(ran πΊ, β, < ) β
β*) |
159 | | simpll 765 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π β (π...sup(π¦, β, < ))) β π) |
160 | 150 | adantl 482 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π β (π...sup(π¦, β, < ))) β π β π) |
161 | 159, 160,
142 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π β (π...sup(π¦, β, < ))) β (πΉβπ) β (0[,]+β)) |
162 | | elinel2 4196 |
. . . . . . . . . . . 12
β’ (π¦ β (π« π β© Fin) β π¦ β Fin) |
163 | 1, 139, 162 | ssuzfz 44049 |
. . . . . . . . . . 11
β’ (π¦ β (π« π β© Fin) β π¦ β (π...sup(π¦, β, < ))) |
164 | 163 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π β© Fin)) β π¦ β (π...sup(π¦, β, < ))) |
165 | 148, 161,
164 | sge0lessmpt 45105 |
. . . . . . . . 9
β’ ((π β§ π¦ β (π« π β© Fin)) β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) β€
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ)))) |
166 | 165 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) β€
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ)))) |
167 | 78 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π β© Fin)) β ran πΊ β β) |
168 | 167 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β ran πΊ β β) |
169 | 101 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π β© Fin)) β ran πΊ β β
) |
170 | 169 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β ran πΊ β β
) |
171 | 131 | adantr 481 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« π β© Fin)) β βπ₯ β β βπ§ β ran πΊ π§ β€ π₯) |
172 | 171 | adantr 481 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β βπ₯ β β βπ§ β ran πΊ π§ β€ π₯) |
173 | 159, 160,
13 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π β (π...sup(π¦, β, < ))) β (πΉβπ) β (0[,)+β)) |
174 | 148, 173 | sge0fsummpt 45096 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π« π β© Fin)) β
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ))) = Ξ£π β (π...sup(π¦, β, < ))(πΉβπ)) |
175 | 174 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ))) = Ξ£π β (π...sup(π¦, β, < ))(πΉβπ)) |
176 | | eqidd 2733 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β§ π β (π...sup(π¦, β, < ))) β (πΉβπ) = (πΉβπ)) |
177 | 139, 1 | sseqtrdi 4032 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (π« π β© Fin) β π¦ β
(β€β₯βπ)) |
178 | 177 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π¦ β (π« π β© Fin) β§ Β¬ π¦ = β
) β π¦ β
(β€β₯βπ)) |
179 | | uzssz 12842 |
. . . . . . . . . . . . . . . . . 18
β’
(β€β₯βπ) β β€ |
180 | 1, 179 | eqsstri 4016 |
. . . . . . . . . . . . . . . . 17
β’ π β
β€ |
181 | 139, 180 | sstrdi 3994 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (π« π β© Fin) β π¦ β
β€) |
182 | 181 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β (π« π β© Fin) β§ Β¬ π¦ = β
) β π¦ β
β€) |
183 | | neqne 2948 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π¦ = β
β π¦ β β
) |
184 | 183 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β (π« π β© Fin) β§ Β¬ π¦ = β
) β π¦ β β
) |
185 | 162 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β (π« π β© Fin) β§ Β¬ π¦ = β
) β π¦ β Fin) |
186 | | suprfinzcl 12675 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β β€ β§ π¦ β β
β§ π¦ β Fin) β sup(π¦, β, < ) β π¦) |
187 | 182, 184,
185, 186 | syl3anc 1371 |
. . . . . . . . . . . . . 14
β’ ((π¦ β (π« π β© Fin) β§ Β¬ π¦ = β
) β sup(π¦, β, < ) β π¦) |
188 | 178, 187 | sseldd 3983 |
. . . . . . . . . . . . 13
β’ ((π¦ β (π« π β© Fin) β§ Β¬ π¦ = β
) β sup(π¦, β, < ) β
(β€β₯βπ)) |
189 | 188 | adantll 712 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β sup(π¦, β, < ) β
(β€β₯βπ)) |
190 | 14 | recnd 11241 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β (πΉβπ) β β) |
191 | 159, 160,
190 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π« π β© Fin)) β§ π β (π...sup(π¦, β, < ))) β (πΉβπ) β β) |
192 | 191 | adantlr 713 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β§ π β (π...sup(π¦, β, < ))) β (πΉβπ) β β) |
193 | 176, 189,
192 | fsumser 15675 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β Ξ£π β (π...sup(π¦, β, < ))(πΉβπ) = (seqπ( + , πΉ)βsup(π¦, β, < ))) |
194 | 10 | eqcomi 2741 |
. . . . . . . . . . . . 13
β’ seqπ( + , πΉ) = πΊ |
195 | 194 | fveq1i 6892 |
. . . . . . . . . . . 12
β’ (seqπ( + , πΉ)βsup(π¦, β, < )) = (πΊβsup(π¦, β, < )) |
196 | 195 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β (seqπ( + , πΉ)βsup(π¦, β, < )) = (πΊβsup(π¦, β, < ))) |
197 | 175, 193,
196 | 3eqtrd 2776 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ))) = (πΊβsup(π¦, β, < ))) |
198 | 79 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (π« π β© Fin)) β Fun πΊ) |
199 | 198 | adantr 481 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β Fun πΊ) |
200 | 189, 82 | eleqtrdi 2843 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β sup(π¦, β, < ) β π) |
201 | 85 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β π = dom πΊ) |
202 | 200, 201 | eleqtrd 2835 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β sup(π¦, β, < ) β dom πΊ) |
203 | | fvelrn 7078 |
. . . . . . . . . . 11
β’ ((Fun
πΊ β§ sup(π¦, β, < ) β dom
πΊ) β (πΊβsup(π¦, β, < )) β ran πΊ) |
204 | 199, 202,
203 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β (πΊβsup(π¦, β, < )) β ran πΊ) |
205 | 197, 204 | eqeltrd 2833 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ))) β ran πΊ) |
206 | | suprub 12174 |
. . . . . . . . 9
β’ (((ran
πΊ β β β§ ran
πΊ β β
β§
βπ₯ β β
βπ§ β ran πΊ π§ β€ π₯) β§
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ))) β ran πΊ) β
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ))) β€ sup(ran πΊ, β, < )) |
207 | 168, 170,
172, 205, 206 | syl31anc 1373 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β
(Ξ£^β(π β (π...sup(π¦, β, < )) β¦ (πΉβπ))) β€ sup(ran πΊ, β, < )) |
208 | 147, 156,
158, 166, 207 | xrletrd 13140 |
. . . . . . 7
β’ (((π β§ π¦ β (π« π β© Fin)) β§ Β¬ π¦ = β
) β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) β€ sup(ran πΊ, β, < )) |
209 | 136, 208 | pm2.61dan 811 |
. . . . . 6
β’ ((π β§ π¦ β (π« π β© Fin)) β
(Ξ£^β(π β π¦ β¦ (πΉβπ))) β€ sup(ran πΊ, β, < )) |
210 | 209 | ralrimiva 3146 |
. . . . 5
β’ (π β βπ¦ β (π« π β©
Fin)(Ξ£^β(π β π¦ β¦ (πΉβπ))) β€ sup(ran πΊ, β, < )) |
211 | | nfv 1917 |
. . . . . 6
β’
β²ππ |
212 | 211, 3, 142, 60 | sge0lefimpt 45129 |
. . . . 5
β’ (π β
((Ξ£^β(π β π β¦ (πΉβπ))) β€ sup(ran πΊ, β, < ) β βπ¦ β (π« π β©
Fin)(Ξ£^β(π β π¦ β¦ (πΉβπ))) β€ sup(ran πΊ, β, < ))) |
213 | 210, 212 | mpbird 256 |
. . . 4
β’ (π β
(Ξ£^β(π β π β¦ (πΉβπ))) β€ sup(ran πΊ, β, < )) |
214 | 62, 213 | eqbrtrd 5170 |
. . 3
β’ (π β
(Ξ£^βπΉ) β€ sup(ran πΊ, β, < )) |
215 | 36 | ssriv 3986 |
. . . . . . . . . . . . 13
β’ (π...π) β π |
216 | 215 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (π...π) β π) |
217 | 3, 142, 216 | sge0lessmpt 45105 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) β€
(Ξ£^β(π β π β¦ (πΉβπ)))) |
218 | 217 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (πΊβπ) = π§) β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) β€
(Ξ£^β(π β π β¦ (πΉβπ)))) |
219 | | fzfid 13937 |
. . . . . . . . . . . . . . 15
β’ (π β (π...π) β Fin) |
220 | 36, 13 | sylan2 593 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (π...π)) β (πΉβπ) β (0[,)+β)) |
221 | 219, 220 | sge0fsummpt 45096 |
. . . . . . . . . . . . . 14
β’ (π β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) = Ξ£π β (π...π)(πΉβπ)) |
222 | 221 | 3ad2ant1 1133 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ (πΊβπ) = π§) β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) = Ξ£π β (π...π)(πΉβπ)) |
223 | 34, 37, 11 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β (π...π)) β (πΉβπ) = (πΉβπ)) |
224 | 34, 37, 190 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π) β§ π β (π...π)) β (πΉβπ) β β) |
225 | 223, 33, 224 | fsumser 15675 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β Ξ£π β (π...π)(πΉβπ) = (seqπ( + , πΉ)βπ)) |
226 | 225 | 3adant3 1132 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ (πΊβπ) = π§) β Ξ£π β (π...π)(πΉβπ) = (seqπ( + , πΉ)βπ)) |
227 | 222, 226 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ (πΊβπ) = π§) β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) = (seqπ( + , πΉ)βπ)) |
228 | 194 | fveq1i 6892 |
. . . . . . . . . . . . 13
β’ (seqπ( + , πΉ)βπ) = (πΊβπ) |
229 | 228 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ (πΊβπ) = π§) β (seqπ( + , πΉ)βπ) = (πΊβπ)) |
230 | | simp3 1138 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ (πΊβπ) = π§) β (πΊβπ) = π§) |
231 | 227, 229,
230 | 3eqtrrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ (πΊβπ) = π§) β π§ =
(Ξ£^β(π β (π...π) β¦ (πΉβπ)))) |
232 | 62 | 3ad2ant1 1133 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ (πΊβπ) = π§) β
(Ξ£^βπΉ) =
(Ξ£^β(π β π β¦ (πΉβπ)))) |
233 | 231, 232 | breq12d 5161 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ (πΊβπ) = π§) β (π§ β€
(Ξ£^βπΉ) β
(Ξ£^β(π β (π...π) β¦ (πΉβπ))) β€
(Ξ£^β(π β π β¦ (πΉβπ))))) |
234 | 218, 233 | mpbird 256 |
. . . . . . . . 9
β’ ((π β§ π β π β§ (πΊβπ) = π§) β π§ β€
(Ξ£^βπΉ)) |
235 | 234 | 3exp 1119 |
. . . . . . . 8
β’ (π β (π β π β ((πΊβπ) = π§ β π§ β€
(Ξ£^βπΉ)))) |
236 | 235 | adantr 481 |
. . . . . . 7
β’ ((π β§ π§ β ran πΊ) β (π β π β ((πΊβπ) = π§ β π§ β€
(Ξ£^βπΉ)))) |
237 | 236 | rexlimdv 3153 |
. . . . . 6
β’ ((π β§ π§ β ran πΊ) β (βπ β π (πΊβπ) = π§ β π§ β€
(Ξ£^βπΉ))) |
238 | 107, 237 | mpd 15 |
. . . . 5
β’ ((π β§ π§ β ran πΊ) β π§ β€
(Ξ£^βπΉ)) |
239 | 238 | ralrimiva 3146 |
. . . 4
β’ (π β βπ§ β ran πΊ π§ β€
(Ξ£^βπΉ)) |
240 | 3, 7 | sge0cl 45087 |
. . . . . 6
β’ (π β
(Ξ£^βπΉ) β (0[,]+β)) |
241 | 59 | ltpnfd 13100 |
. . . . . . . . 9
β’ (π β sup(ran πΊ, β, < ) <
+β) |
242 | 8, 60, 91, 214, 241 | xrlelttrd 13138 |
. . . . . . . 8
β’ (π β
(Ξ£^βπΉ) < +β) |
243 | 8, 91, 242 | xrgtned 44022 |
. . . . . . 7
β’ (π β +β β
(Ξ£^βπΉ)) |
244 | 243 | necomd 2996 |
. . . . . 6
β’ (π β
(Ξ£^βπΉ) β +β) |
245 | | ge0xrre 44234 |
. . . . . 6
β’
(((Ξ£^βπΉ) β (0[,]+β) β§
(Ξ£^βπΉ) β +β) β
(Ξ£^βπΉ) β β) |
246 | 240, 244,
245 | syl2anc 584 |
. . . . 5
β’ (π β
(Ξ£^βπΉ) β β) |
247 | | suprleub 12179 |
. . . . 5
β’ (((ran
πΊ β β β§ ran
πΊ β β
β§
βπ₯ β β
βπ§ β ran πΊ π§ β€ π₯) β§
(Ξ£^βπΉ) β β) β (sup(ran πΊ, β, < ) β€
(Ξ£^βπΉ) β βπ§ β ran πΊ π§ β€
(Ξ£^βπΉ))) |
248 | 78, 101, 131, 246, 247 | syl31anc 1373 |
. . . 4
β’ (π β (sup(ran πΊ, β, < ) β€
(Ξ£^βπΉ) β βπ§ β ran πΊ π§ β€
(Ξ£^βπΉ))) |
249 | 239, 248 | mpbird 256 |
. . 3
β’ (π β sup(ran πΊ, β, < ) β€
(Ξ£^βπΉ)) |
250 | 8, 60, 214, 249 | xrletrid 13133 |
. 2
β’ (π β
(Ξ£^βπΉ) = sup(ran πΊ, β, < )) |
251 | | climuni 15495 |
. . 3
β’ ((πΊ β π΅ β§ πΊ β sup(ran πΊ, β, < )) β π΅ = sup(ran πΊ, β, < )) |
252 | 24, 58, 251 | syl2anc 584 |
. 2
β’ (π β π΅ = sup(ran πΊ, β, < )) |
253 | 250, 252 | eqtr4d 2775 |
1
β’ (π β
(Ξ£^βπΉ) = π΅) |