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 sseldi
 |-  ( ( 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 )