Step |
Hyp |
Ref |
Expression |
1 |
|
esumpcvgval.1 |
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,) +oo ) ) |
2 |
|
esumpcvgval.2 |
|- ( k = l -> A = B ) |
3 |
|
esumpcvgval.3 |
|- ( ph -> ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) e. dom ~~> ) |
4 |
|
xrltso |
|- < Or RR* |
5 |
4
|
a1i |
|- ( ph -> < Or RR* ) |
6 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
7 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
8 |
|
eqcom |
|- ( k = l <-> l = k ) |
9 |
|
eqcom |
|- ( A = B <-> B = A ) |
10 |
2 8 9
|
3imtr3i |
|- ( l = k -> B = A ) |
11 |
10
|
cbvmptv |
|- ( l e. NN |-> B ) = ( k e. NN |-> A ) |
12 |
1 11
|
fmptd |
|- ( ph -> ( l e. NN |-> B ) : NN --> ( 0 [,) +oo ) ) |
13 |
12
|
ffvelrnda |
|- ( ( ph /\ x e. NN ) -> ( ( l e. NN |-> B ) ` x ) e. ( 0 [,) +oo ) ) |
14 |
|
elrege0 |
|- ( ( ( l e. NN |-> B ) ` x ) e. ( 0 [,) +oo ) <-> ( ( ( l e. NN |-> B ) ` x ) e. RR /\ 0 <_ ( ( l e. NN |-> B ) ` x ) ) ) |
15 |
14
|
simplbi |
|- ( ( ( l e. NN |-> B ) ` x ) e. ( 0 [,) +oo ) -> ( ( l e. NN |-> B ) ` x ) e. RR ) |
16 |
13 15
|
syl |
|- ( ( ph /\ x e. NN ) -> ( ( l e. NN |-> B ) ` x ) e. RR ) |
17 |
6 7 16
|
serfre |
|- ( ph -> seq 1 ( + , ( l e. NN |-> B ) ) : NN --> RR ) |
18 |
12
|
adantr |
|- ( ( ph /\ n e. NN ) -> ( l e. NN |-> B ) : NN --> ( 0 [,) +oo ) ) |
19 |
|
simpr |
|- ( ( ph /\ n e. NN ) -> n e. NN ) |
20 |
19
|
peano2nnd |
|- ( ( ph /\ n e. NN ) -> ( n + 1 ) e. NN ) |
21 |
18 20
|
ffvelrnd |
|- ( ( ph /\ n e. NN ) -> ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. ( 0 [,) +oo ) ) |
22 |
|
elrege0 |
|- ( ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. ( 0 [,) +oo ) <-> ( ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. RR /\ 0 <_ ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) ) |
23 |
22
|
simprbi |
|- ( ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. ( 0 [,) +oo ) -> 0 <_ ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) |
24 |
21 23
|
syl |
|- ( ( ph /\ n e. NN ) -> 0 <_ ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) |
25 |
17
|
ffvelrnda |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) e. RR ) |
26 |
22
|
simplbi |
|- ( ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. ( 0 [,) +oo ) -> ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. RR ) |
27 |
21 26
|
syl |
|- ( ( ph /\ n e. NN ) -> ( ( l e. NN |-> B ) ` ( n + 1 ) ) e. RR ) |
28 |
25 27
|
addge01d |
|- ( ( ph /\ n e. NN ) -> ( 0 <_ ( ( l e. NN |-> B ) ` ( n + 1 ) ) <-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) + ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) ) ) |
29 |
24 28
|
mpbid |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) + ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) ) |
30 |
19 6
|
eleqtrdi |
|- ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) ) |
31 |
|
seqp1 |
|- ( n e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` ( n + 1 ) ) = ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) + ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) ) |
32 |
30 31
|
syl |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` ( n + 1 ) ) = ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) + ( ( l e. NN |-> B ) ` ( n + 1 ) ) ) ) |
33 |
29 32
|
breqtrrd |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ ( seq 1 ( + , ( l e. NN |-> B ) ) ` ( n + 1 ) ) ) |
34 |
|
simpr |
|- ( ( ph /\ k e. NN ) -> k e. NN ) |
35 |
11
|
fvmpt2 |
|- ( ( k e. NN /\ A e. ( 0 [,) +oo ) ) -> ( ( l e. NN |-> B ) ` k ) = A ) |
36 |
34 1 35
|
syl2anc |
|- ( ( ph /\ k e. NN ) -> ( ( l e. NN |-> B ) ` k ) = A ) |
37 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
38 |
37 1
|
sseldi |
|- ( ( ph /\ k e. NN ) -> A e. RR ) |
39 |
17
|
feqmptd |
|- ( ph -> seq 1 ( + , ( l e. NN |-> B ) ) = ( n e. NN |-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) ) |
40 |
|
simpll |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ph ) |
41 |
|
elfznn |
|- ( k e. ( 1 ... n ) -> k e. NN ) |
42 |
41
|
adantl |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> k e. NN ) |
43 |
40 42 36
|
syl2anc |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> ( ( l e. NN |-> B ) ` k ) = A ) |
44 |
38
|
recnd |
|- ( ( ph /\ k e. NN ) -> A e. CC ) |
45 |
40 42 44
|
syl2anc |
|- ( ( ( ph /\ n e. NN ) /\ k e. ( 1 ... n ) ) -> A e. CC ) |
46 |
43 30 45
|
fsumser |
|- ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) |
47 |
46
|
eqcomd |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) = sum_ k e. ( 1 ... n ) A ) |
48 |
47
|
mpteq2dva |
|- ( ph -> ( n e. NN |-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) = ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) ) |
49 |
39 48
|
eqtr2d |
|- ( ph -> ( n e. NN |-> sum_ k e. ( 1 ... n ) A ) = seq 1 ( + , ( l e. NN |-> B ) ) ) |
50 |
49 3
|
eqeltrrd |
|- ( ph -> seq 1 ( + , ( l e. NN |-> B ) ) e. dom ~~> ) |
51 |
6 7 36 38 50
|
isumrecl |
|- ( ph -> sum_ k e. NN A e. RR ) |
52 |
|
1zzd |
|- ( ( ph /\ n e. NN ) -> 1 e. ZZ ) |
53 |
|
fzfid |
|- ( ( ph /\ n e. NN ) -> ( 1 ... n ) e. Fin ) |
54 |
|
fzssuz |
|- ( 1 ... n ) C_ ( ZZ>= ` 1 ) |
55 |
54 6
|
sseqtrri |
|- ( 1 ... n ) C_ NN |
56 |
55
|
a1i |
|- ( ( ph /\ n e. NN ) -> ( 1 ... n ) C_ NN ) |
57 |
36
|
adantlr |
|- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> ( ( l e. NN |-> B ) ` k ) = A ) |
58 |
38
|
adantlr |
|- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> A e. RR ) |
59 |
1
|
adantlr |
|- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> A e. ( 0 [,) +oo ) ) |
60 |
|
elrege0 |
|- ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) ) |
61 |
60
|
simprbi |
|- ( A e. ( 0 [,) +oo ) -> 0 <_ A ) |
62 |
59 61
|
syl |
|- ( ( ( ph /\ n e. NN ) /\ k e. NN ) -> 0 <_ A ) |
63 |
50
|
adantr |
|- ( ( ph /\ n e. NN ) -> seq 1 ( + , ( l e. NN |-> B ) ) e. dom ~~> ) |
64 |
6 52 53 56 57 58 62 63
|
isumless |
|- ( ( ph /\ n e. NN ) -> sum_ k e. ( 1 ... n ) A <_ sum_ k e. NN A ) |
65 |
46 64
|
eqbrtrrd |
|- ( ( ph /\ n e. NN ) -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ sum_ k e. NN A ) |
66 |
65
|
ralrimiva |
|- ( ph -> A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ sum_ k e. NN A ) |
67 |
|
brralrspcev |
|- ( ( sum_ k e. NN A e. RR /\ A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ sum_ k e. NN A ) -> E. s e. RR A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s ) |
68 |
51 66 67
|
syl2anc |
|- ( ph -> E. s e. RR A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s ) |
69 |
6 7 17 33 68
|
climsup |
|- ( ph -> seq 1 ( + , ( l e. NN |-> B ) ) ~~> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
70 |
6 7 69 25
|
climrecl |
|- ( ph -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR ) |
71 |
70
|
rexrd |
|- ( ph -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR* ) |
72 |
|
eqid |
|- ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) = ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) |
73 |
|
sumex |
|- sum_ k e. b A e. _V |
74 |
72 73
|
elrnmpti |
|- ( x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) <-> E. b e. ( ~P NN i^i Fin ) x = sum_ k e. b A ) |
75 |
|
ssnnssfz |
|- ( b e. ( ~P NN i^i Fin ) -> E. m e. NN b C_ ( 1 ... m ) ) |
76 |
|
fzfid |
|- ( ( ph /\ b C_ ( 1 ... m ) ) -> ( 1 ... m ) e. Fin ) |
77 |
|
elfznn |
|- ( k e. ( 1 ... m ) -> k e. NN ) |
78 |
77 1
|
sylan2 |
|- ( ( ph /\ k e. ( 1 ... m ) ) -> A e. ( 0 [,) +oo ) ) |
79 |
60
|
simplbi |
|- ( A e. ( 0 [,) +oo ) -> A e. RR ) |
80 |
78 79
|
syl |
|- ( ( ph /\ k e. ( 1 ... m ) ) -> A e. RR ) |
81 |
80
|
adantlr |
|- ( ( ( ph /\ b C_ ( 1 ... m ) ) /\ k e. ( 1 ... m ) ) -> A e. RR ) |
82 |
78 61
|
syl |
|- ( ( ph /\ k e. ( 1 ... m ) ) -> 0 <_ A ) |
83 |
82
|
adantlr |
|- ( ( ( ph /\ b C_ ( 1 ... m ) ) /\ k e. ( 1 ... m ) ) -> 0 <_ A ) |
84 |
|
simpr |
|- ( ( ph /\ b C_ ( 1 ... m ) ) -> b C_ ( 1 ... m ) ) |
85 |
76 81 83 84
|
fsumless |
|- ( ( ph /\ b C_ ( 1 ... m ) ) -> sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) |
86 |
85
|
ex |
|- ( ph -> ( b C_ ( 1 ... m ) -> sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) ) |
87 |
86
|
reximdv |
|- ( ph -> ( E. m e. NN b C_ ( 1 ... m ) -> E. m e. NN sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) ) |
88 |
87
|
imp |
|- ( ( ph /\ E. m e. NN b C_ ( 1 ... m ) ) -> E. m e. NN sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) |
89 |
75 88
|
sylan2 |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> E. m e. NN sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) |
90 |
|
breq1 |
|- ( x = sum_ k e. b A -> ( x <_ sum_ k e. ( 1 ... m ) A <-> sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) ) |
91 |
90
|
rexbidv |
|- ( x = sum_ k e. b A -> ( E. m e. NN x <_ sum_ k e. ( 1 ... m ) A <-> E. m e. NN sum_ k e. b A <_ sum_ k e. ( 1 ... m ) A ) ) |
92 |
89 91
|
syl5ibrcom |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( x = sum_ k e. b A -> E. m e. NN x <_ sum_ k e. ( 1 ... m ) A ) ) |
93 |
92
|
rexlimdva |
|- ( ph -> ( E. b e. ( ~P NN i^i Fin ) x = sum_ k e. b A -> E. m e. NN x <_ sum_ k e. ( 1 ... m ) A ) ) |
94 |
93
|
imp |
|- ( ( ph /\ E. b e. ( ~P NN i^i Fin ) x = sum_ k e. b A ) -> E. m e. NN x <_ sum_ k e. ( 1 ... m ) A ) |
95 |
74 94
|
sylan2b |
|- ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> E. m e. NN x <_ sum_ k e. ( 1 ... m ) A ) |
96 |
|
simpr |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ x = sum_ k e. b A ) -> x = sum_ k e. b A ) |
97 |
|
inss2 |
|- ( ~P NN i^i Fin ) C_ Fin |
98 |
|
simpr |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> b e. ( ~P NN i^i Fin ) ) |
99 |
97 98
|
sseldi |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> b e. Fin ) |
100 |
|
simpll |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> ph ) |
101 |
|
inss1 |
|- ( ~P NN i^i Fin ) C_ ~P NN |
102 |
|
simplr |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> b e. ( ~P NN i^i Fin ) ) |
103 |
101 102
|
sseldi |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> b e. ~P NN ) |
104 |
103
|
elpwid |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> b C_ NN ) |
105 |
|
simpr |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> k e. b ) |
106 |
104 105
|
sseldd |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> k e. NN ) |
107 |
100 106 1
|
syl2anc |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> A e. ( 0 [,) +oo ) ) |
108 |
107 79
|
syl |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> A e. RR ) |
109 |
99 108
|
fsumrecl |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> sum_ k e. b A e. RR ) |
110 |
109
|
adantr |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ x = sum_ k e. b A ) -> sum_ k e. b A e. RR ) |
111 |
96 110
|
eqeltrd |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ x = sum_ k e. b A ) -> x e. RR ) |
112 |
111
|
r19.29an |
|- ( ( ph /\ E. b e. ( ~P NN i^i Fin ) x = sum_ k e. b A ) -> x e. RR ) |
113 |
74 112
|
sylan2b |
|- ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> x e. RR ) |
114 |
113
|
adantr |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> x e. RR ) |
115 |
|
fzfid |
|- ( ph -> ( 1 ... m ) e. Fin ) |
116 |
115 80
|
fsumrecl |
|- ( ph -> sum_ k e. ( 1 ... m ) A e. RR ) |
117 |
116
|
ad2antrr |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> sum_ k e. ( 1 ... m ) A e. RR ) |
118 |
70
|
ad2antrr |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR ) |
119 |
|
simprr |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> x <_ sum_ k e. ( 1 ... m ) A ) |
120 |
17
|
frnd |
|- ( ph -> ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR ) |
121 |
120
|
ad2antrr |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR ) |
122 |
|
1nn |
|- 1 e. NN |
123 |
122
|
ne0ii |
|- NN =/= (/) |
124 |
|
dm0rn0 |
|- ( dom seq 1 ( + , ( l e. NN |-> B ) ) = (/) <-> ran seq 1 ( + , ( l e. NN |-> B ) ) = (/) ) |
125 |
17
|
fdmd |
|- ( ph -> dom seq 1 ( + , ( l e. NN |-> B ) ) = NN ) |
126 |
125
|
eqeq1d |
|- ( ph -> ( dom seq 1 ( + , ( l e. NN |-> B ) ) = (/) <-> NN = (/) ) ) |
127 |
124 126
|
bitr3id |
|- ( ph -> ( ran seq 1 ( + , ( l e. NN |-> B ) ) = (/) <-> NN = (/) ) ) |
128 |
127
|
necon3bid |
|- ( ph -> ( ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) <-> NN =/= (/) ) ) |
129 |
123 128
|
mpbiri |
|- ( ph -> ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) ) |
130 |
129
|
ad2antrr |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) ) |
131 |
|
1z |
|- 1 e. ZZ |
132 |
|
seqfn |
|- ( 1 e. ZZ -> seq 1 ( + , ( l e. NN |-> B ) ) Fn ( ZZ>= ` 1 ) ) |
133 |
131 132
|
ax-mp |
|- seq 1 ( + , ( l e. NN |-> B ) ) Fn ( ZZ>= ` 1 ) |
134 |
6
|
fneq2i |
|- ( seq 1 ( + , ( l e. NN |-> B ) ) Fn NN <-> seq 1 ( + , ( l e. NN |-> B ) ) Fn ( ZZ>= ` 1 ) ) |
135 |
133 134
|
mpbir |
|- seq 1 ( + , ( l e. NN |-> B ) ) Fn NN |
136 |
|
dffn5 |
|- ( seq 1 ( + , ( l e. NN |-> B ) ) Fn NN <-> seq 1 ( + , ( l e. NN |-> B ) ) = ( n e. NN |-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) ) |
137 |
135 136
|
mpbi |
|- seq 1 ( + , ( l e. NN |-> B ) ) = ( n e. NN |-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) |
138 |
|
fvex |
|- ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) e. _V |
139 |
137 138
|
elrnmpti |
|- ( z e. ran seq 1 ( + , ( l e. NN |-> B ) ) <-> E. n e. NN z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) |
140 |
|
r19.29 |
|- ( ( A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ E. n e. NN z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> E. n e. NN ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) ) |
141 |
|
breq1 |
|- ( z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) -> ( z <_ s <-> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s ) ) |
142 |
141
|
biimparc |
|- ( ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> z <_ s ) |
143 |
142
|
rexlimivw |
|- ( E. n e. NN ( ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> z <_ s ) |
144 |
140 143
|
syl |
|- ( ( A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ E. n e. NN z = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> z <_ s ) |
145 |
139 144
|
sylan2b |
|- ( ( A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s /\ z e. ran seq 1 ( + , ( l e. NN |-> B ) ) ) -> z <_ s ) |
146 |
145
|
ralrimiva |
|- ( A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s -> A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) |
147 |
146
|
reximi |
|- ( E. s e. RR A. n e. NN ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) <_ s -> E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) |
148 |
68 147
|
syl |
|- ( ph -> E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) |
149 |
148
|
ad2antrr |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) |
150 |
|
simpr |
|- ( ( ph /\ m e. NN ) -> m e. NN ) |
151 |
|
simpll |
|- ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> ph ) |
152 |
77
|
adantl |
|- ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> k e. NN ) |
153 |
151 152 36
|
syl2anc |
|- ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> ( ( l e. NN |-> B ) ` k ) = A ) |
154 |
150 6
|
eleqtrdi |
|- ( ( ph /\ m e. NN ) -> m e. ( ZZ>= ` 1 ) ) |
155 |
151 152 1
|
syl2anc |
|- ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> A e. ( 0 [,) +oo ) ) |
156 |
155 79
|
syl |
|- ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> A e. RR ) |
157 |
156
|
recnd |
|- ( ( ( ph /\ m e. NN ) /\ k e. ( 1 ... m ) ) -> A e. CC ) |
158 |
153 154 157
|
fsumser |
|- ( ( ph /\ m e. NN ) -> sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` m ) ) |
159 |
|
fveq2 |
|- ( n = m -> ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) = ( seq 1 ( + , ( l e. NN |-> B ) ) ` m ) ) |
160 |
159
|
rspceeqv |
|- ( ( m e. NN /\ sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` m ) ) -> E. n e. NN sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) |
161 |
150 158 160
|
syl2anc |
|- ( ( ph /\ m e. NN ) -> E. n e. NN sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) |
162 |
137 138
|
elrnmpti |
|- ( sum_ k e. ( 1 ... m ) A e. ran seq 1 ( + , ( l e. NN |-> B ) ) <-> E. n e. NN sum_ k e. ( 1 ... m ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) |
163 |
161 162
|
sylibr |
|- ( ( ph /\ m e. NN ) -> sum_ k e. ( 1 ... m ) A e. ran seq 1 ( + , ( l e. NN |-> B ) ) ) |
164 |
163
|
ad2ant2r |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> sum_ k e. ( 1 ... m ) A e. ran seq 1 ( + , ( l e. NN |-> B ) ) ) |
165 |
|
suprub |
|- ( ( ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR /\ ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) /\ E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) /\ sum_ k e. ( 1 ... m ) A e. ran seq 1 ( + , ( l e. NN |-> B ) ) ) -> sum_ k e. ( 1 ... m ) A <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
166 |
121 130 149 164 165
|
syl31anc |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> sum_ k e. ( 1 ... m ) A <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
167 |
114 117 118 119 166
|
letrd |
|- ( ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) /\ ( m e. NN /\ x <_ sum_ k e. ( 1 ... m ) A ) ) -> x <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
168 |
95 167
|
rexlimddv |
|- ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> x <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
169 |
70
|
adantr |
|- ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR ) |
170 |
113 169
|
lenltd |
|- ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> ( x <_ sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> -. sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) < x ) ) |
171 |
168 170
|
mpbid |
|- ( ( ph /\ x e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) -> -. sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) < x ) |
172 |
|
simpr1r |
|- ( ( ph /\ ( ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) /\ 0 <_ x /\ x = +oo ) ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
173 |
172
|
3anassrs |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
174 |
71
|
ad3antrrr |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR* ) |
175 |
|
pnfnlt |
|- ( sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) e. RR* -> -. +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
176 |
174 175
|
syl |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> -. +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
177 |
|
breq1 |
|- ( x = +oo -> ( x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) |
178 |
177
|
notbid |
|- ( x = +oo -> ( -. x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> -. +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) |
179 |
178
|
adantl |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> ( -. x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> -. +oo < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) |
180 |
176 179
|
mpbird |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> -. x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
181 |
173 180
|
pm2.21dd |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x = +oo ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) |
182 |
|
simplll |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> ph ) |
183 |
|
simpr1l |
|- ( ( ph /\ ( ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) /\ 0 <_ x /\ x < +oo ) ) -> x e. RR* ) |
184 |
183
|
3anassrs |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> x e. RR* ) |
185 |
|
simplr |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> 0 <_ x ) |
186 |
|
simpr |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> x < +oo ) |
187 |
|
0xr |
|- 0 e. RR* |
188 |
|
pnfxr |
|- +oo e. RR* |
189 |
|
elico1 |
|- ( ( 0 e. RR* /\ +oo e. RR* ) -> ( x e. ( 0 [,) +oo ) <-> ( x e. RR* /\ 0 <_ x /\ x < +oo ) ) ) |
190 |
187 188 189
|
mp2an |
|- ( x e. ( 0 [,) +oo ) <-> ( x e. RR* /\ 0 <_ x /\ x < +oo ) ) |
191 |
184 185 186 190
|
syl3anbrc |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> x e. ( 0 [,) +oo ) ) |
192 |
|
simpr1r |
|- ( ( ph /\ ( ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) /\ 0 <_ x /\ x < +oo ) ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
193 |
192
|
3anassrs |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
194 |
120
|
adantr |
|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR ) |
195 |
129
|
adantr |
|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) ) |
196 |
148
|
adantr |
|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) |
197 |
194 195 196
|
3jca |
|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR /\ ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) /\ E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) ) |
198 |
|
simprl |
|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> x e. ( 0 [,) +oo ) ) |
199 |
37 198
|
sseldi |
|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> x e. RR ) |
200 |
|
simprr |
|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
201 |
|
suprlub |
|- ( ( ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR /\ ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) /\ E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) /\ x e. RR ) -> ( x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) <-> E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y ) ) |
202 |
201
|
biimpa |
|- ( ( ( ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ RR /\ ran seq 1 ( + , ( l e. NN |-> B ) ) =/= (/) /\ E. s e. RR A. z e. ran seq 1 ( + , ( l e. NN |-> B ) ) z <_ s ) /\ x e. RR ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) -> E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y ) |
203 |
197 199 200 202
|
syl21anc |
|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y ) |
204 |
41
|
ssriv |
|- ( 1 ... n ) C_ NN |
205 |
|
ovex |
|- ( 1 ... n ) e. _V |
206 |
205
|
elpw |
|- ( ( 1 ... n ) e. ~P NN <-> ( 1 ... n ) C_ NN ) |
207 |
204 206
|
mpbir |
|- ( 1 ... n ) e. ~P NN |
208 |
|
fzfi |
|- ( 1 ... n ) e. Fin |
209 |
|
elin |
|- ( ( 1 ... n ) e. ( ~P NN i^i Fin ) <-> ( ( 1 ... n ) e. ~P NN /\ ( 1 ... n ) e. Fin ) ) |
210 |
207 208 209
|
mpbir2an |
|- ( 1 ... n ) e. ( ~P NN i^i Fin ) |
211 |
210
|
a1i |
|- ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> ( 1 ... n ) e. ( ~P NN i^i Fin ) ) |
212 |
|
simpr |
|- ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) |
213 |
46
|
adantr |
|- ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> sum_ k e. ( 1 ... n ) A = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) |
214 |
212 213
|
eqtr4d |
|- ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> y = sum_ k e. ( 1 ... n ) A ) |
215 |
|
sumeq1 |
|- ( b = ( 1 ... n ) -> sum_ k e. b A = sum_ k e. ( 1 ... n ) A ) |
216 |
215
|
rspceeqv |
|- ( ( ( 1 ... n ) e. ( ~P NN i^i Fin ) /\ y = sum_ k e. ( 1 ... n ) A ) -> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A ) |
217 |
211 214 216
|
syl2anc |
|- ( ( ( ph /\ n e. NN ) /\ y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) -> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A ) |
218 |
217
|
ex |
|- ( ( ph /\ n e. NN ) -> ( y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) -> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A ) ) |
219 |
218
|
rexlimdva |
|- ( ph -> ( E. n e. NN y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) -> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A ) ) |
220 |
137 138
|
elrnmpti |
|- ( y e. ran seq 1 ( + , ( l e. NN |-> B ) ) <-> E. n e. NN y = ( seq 1 ( + , ( l e. NN |-> B ) ) ` n ) ) |
221 |
72 73
|
elrnmpti |
|- ( y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) <-> E. b e. ( ~P NN i^i Fin ) y = sum_ k e. b A ) |
222 |
219 220 221
|
3imtr4g |
|- ( ph -> ( y e. ran seq 1 ( + , ( l e. NN |-> B ) ) -> y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) ) |
223 |
222
|
ssrdv |
|- ( ph -> ran seq 1 ( + , ( l e. NN |-> B ) ) C_ ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) ) |
224 |
|
ssrexv |
|- ( ran seq 1 ( + , ( l e. NN |-> B ) ) C_ ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) -> ( E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) ) |
225 |
223 224
|
syl |
|- ( ph -> ( E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) ) |
226 |
225
|
imp |
|- ( ( ph /\ E. y e. ran seq 1 ( + , ( l e. NN |-> B ) ) x < y ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) |
227 |
203 226
|
syldan |
|- ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) |
228 |
182 191 193 227
|
syl12anc |
|- ( ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) /\ x < +oo ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) |
229 |
|
simplrl |
|- ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) -> x e. RR* ) |
230 |
|
xrlelttric |
|- ( ( +oo e. RR* /\ x e. RR* ) -> ( +oo <_ x \/ x < +oo ) ) |
231 |
188 230
|
mpan |
|- ( x e. RR* -> ( +oo <_ x \/ x < +oo ) ) |
232 |
|
xgepnf |
|- ( x e. RR* -> ( +oo <_ x <-> x = +oo ) ) |
233 |
232
|
orbi1d |
|- ( x e. RR* -> ( ( +oo <_ x \/ x < +oo ) <-> ( x = +oo \/ x < +oo ) ) ) |
234 |
231 233
|
mpbid |
|- ( x e. RR* -> ( x = +oo \/ x < +oo ) ) |
235 |
229 234
|
syl |
|- ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) -> ( x = +oo \/ x < +oo ) ) |
236 |
181 228 235
|
mpjaodan |
|- ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ 0 <_ x ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) |
237 |
|
0elpw |
|- (/) e. ~P NN |
238 |
|
0fin |
|- (/) e. Fin |
239 |
|
elin |
|- ( (/) e. ( ~P NN i^i Fin ) <-> ( (/) e. ~P NN /\ (/) e. Fin ) ) |
240 |
237 238 239
|
mpbir2an |
|- (/) e. ( ~P NN i^i Fin ) |
241 |
|
sum0 |
|- sum_ k e. (/) A = 0 |
242 |
241
|
eqcomi |
|- 0 = sum_ k e. (/) A |
243 |
|
sumeq1 |
|- ( b = (/) -> sum_ k e. b A = sum_ k e. (/) A ) |
244 |
243
|
rspceeqv |
|- ( ( (/) e. ( ~P NN i^i Fin ) /\ 0 = sum_ k e. (/) A ) -> E. b e. ( ~P NN i^i Fin ) 0 = sum_ k e. b A ) |
245 |
240 242 244
|
mp2an |
|- E. b e. ( ~P NN i^i Fin ) 0 = sum_ k e. b A |
246 |
72 73
|
elrnmpti |
|- ( 0 e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) <-> E. b e. ( ~P NN i^i Fin ) 0 = sum_ k e. b A ) |
247 |
245 246
|
mpbir |
|- 0 e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) |
248 |
|
breq2 |
|- ( y = 0 -> ( x < y <-> x < 0 ) ) |
249 |
248
|
rspcev |
|- ( ( 0 e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) /\ x < 0 ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) |
250 |
247 249
|
mpan |
|- ( x < 0 -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) |
251 |
250
|
adantl |
|- ( ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) /\ x < 0 ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) |
252 |
|
xrlelttric |
|- ( ( 0 e. RR* /\ x e. RR* ) -> ( 0 <_ x \/ x < 0 ) ) |
253 |
187 252
|
mpan |
|- ( x e. RR* -> ( 0 <_ x \/ x < 0 ) ) |
254 |
253
|
ad2antrl |
|- ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> ( 0 <_ x \/ x < 0 ) ) |
255 |
236 251 254
|
mpjaodan |
|- ( ( ph /\ ( x e. RR* /\ x < sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) ) -> E. y e. ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) x < y ) |
256 |
5 71 171 255
|
eqsupd |
|- ( ph -> sup ( ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) , RR* , < ) = sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
257 |
|
nfv |
|- F/ k ph |
258 |
|
nfcv |
|- F/_ k NN |
259 |
|
nnex |
|- NN e. _V |
260 |
259
|
a1i |
|- ( ph -> NN e. _V ) |
261 |
|
icossicc |
|- ( 0 [,) +oo ) C_ ( 0 [,] +oo ) |
262 |
261 1
|
sseldi |
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) ) |
263 |
|
elex |
|- ( b e. ( ~P NN i^i Fin ) -> b e. _V ) |
264 |
263
|
adantl |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> b e. _V ) |
265 |
107
|
fmpttd |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( k e. b |-> A ) : b --> ( 0 [,) +oo ) ) |
266 |
|
esumpfinvallem |
|- ( ( b e. _V /\ ( k e. b |-> A ) : b --> ( 0 [,) +oo ) ) -> ( CCfld gsum ( k e. b |-> A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. b |-> A ) ) ) |
267 |
264 265 266
|
syl2anc |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( CCfld gsum ( k e. b |-> A ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. b |-> A ) ) ) |
268 |
108
|
recnd |
|- ( ( ( ph /\ b e. ( ~P NN i^i Fin ) ) /\ k e. b ) -> A e. CC ) |
269 |
99 268
|
gsumfsum |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( CCfld gsum ( k e. b |-> A ) ) = sum_ k e. b A ) |
270 |
267 269
|
eqtr3d |
|- ( ( ph /\ b e. ( ~P NN i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. b |-> A ) ) = sum_ k e. b A ) |
271 |
257 258 260 262 270
|
esumval |
|- ( ph -> sum* k e. NN A = sup ( ran ( b e. ( ~P NN i^i Fin ) |-> sum_ k e. b A ) , RR* , < ) ) |
272 |
6 7 36 44 69
|
isumclim |
|- ( ph -> sum_ k e. NN A = sup ( ran seq 1 ( + , ( l e. NN |-> B ) ) , RR , < ) ) |
273 |
256 271 272
|
3eqtr4d |
|- ( ph -> sum* k e. NN A = sum_ k e. NN A ) |