Metamath Proof Explorer

Theorem sge0pnffsumgt

Description: If the sum of nonnegative extended reals is +oo , then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses sge0pnffsumgt.k 
|- F/ k ph
sge0pnffsumgt.a 
|- ( ph -> A e. V )
sge0pnffsumgt.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
sge0pnffsumgt.p 
|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = +oo )
sge0pnffsumgt.y 
|- ( ph -> Y e. RR )
Assertion sge0pnffsumgt 
|- ( ph -> E. x e. ( ~P A i^i Fin ) Y < sum_ k e. x B )

Proof

Step Hyp Ref Expression
1 sge0pnffsumgt.k 
 |-  F/ k ph
2 sge0pnffsumgt.a 
 |-  ( ph -> A e. V )
3 sge0pnffsumgt.b 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
4 sge0pnffsumgt.p 
 |-  ( ph -> ( sum^ ` ( k e. A |-> B ) ) = +oo )
5 sge0pnffsumgt.y 
 |-  ( ph -> Y e. RR )
6 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
7 6 3 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
8 1 2 7 4 5 sge0pnffigtmpt 
 |-  ( ph -> E. x e. ( ~P A i^i Fin ) Y < ( sum^ ` ( k e. x |-> B ) ) )
9 simpr 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ Y < ( sum^ ` ( k e. x |-> B ) ) ) -> Y < ( sum^ ` ( k e. x |-> B ) ) )
10 nfv 
 |-  F/ k x e. ( ~P A i^i Fin )
11 1 10 nfan 
 |-  F/ k ( ph /\ x e. ( ~P A i^i Fin ) )
12 elinel2 
 |-  ( x e. ( ~P A i^i Fin ) -> x e. Fin )
13 12 adantl 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> x e. Fin )
14 simpll 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> ph )
15 elpwinss 
 |-  ( x e. ( ~P A i^i Fin ) -> x C_ A )
16 15 sselda 
 |-  ( ( x e. ( ~P A i^i Fin ) /\ k e. x ) -> k e. A )
17 16 adantll 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> k e. A )
18 14 17 3 syl2anc 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ k e. x ) -> B e. ( 0 [,) +oo ) )
19 11 13 18 sge0fsummptf 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( k e. x |-> B ) ) = sum_ k e. x B )
20 19 adantr 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ Y < ( sum^ ` ( k e. x |-> B ) ) ) -> ( sum^ ` ( k e. x |-> B ) ) = sum_ k e. x B )
21 9 20 breqtrd 
 |-  ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ Y < ( sum^ ` ( k e. x |-> B ) ) ) -> Y < sum_ k e. x B )
22 21 ex 
 |-  ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> ( Y < ( sum^ ` ( k e. x |-> B ) ) -> Y < sum_ k e. x B ) )
23 22 reximdva 
 |-  ( ph -> ( E. x e. ( ~P A i^i Fin ) Y < ( sum^ ` ( k e. x |-> B ) ) -> E. x e. ( ~P A i^i Fin ) Y < sum_ k e. x B ) )
24 8 23 mpd 
 |-  ( ph -> E. x e. ( ~P A i^i Fin ) Y < sum_ k e. x B )