Metamath Proof Explorer

Theorem sge0rpcpnf

Description: The sum of an infinite number of a positive constant, is +oo (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0rpcpnf.a 
|- ( ph -> A e. V )
sge0rpcpnf.nfi 
|- ( ph -> -. A e. Fin )
sge0rpcpnf.b 
|- ( ph -> B e. RR+ )
Assertion sge0rpcpnf 
|- ( ph -> ( sum^ ` ( x e. A |-> B ) ) = +oo )

Proof

Step Hyp Ref Expression
1 sge0rpcpnf.a 
 |-  ( ph -> A e. V )
2 sge0rpcpnf.nfi 
 |-  ( ph -> -. A e. Fin )
3 sge0rpcpnf.b 
 |-  ( ph -> B e. RR+ )
4 1 adantr 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> A e. V )
5 0xr 
 |-  0 e. RR*
6 5 a1i 
 |-  ( ph -> 0 e. RR* )
7 pnfxr 
 |-  +oo e. RR*
8 7 a1i 
 |-  ( ph -> +oo e. RR* )
9 3 rpxrd 
 |-  ( ph -> B e. RR* )
10 3 rpge0d 
 |-  ( ph -> 0 <_ B )
11 3 rpred 
 |-  ( ph -> B e. RR )
12 ltpnf 
 |-  ( B e. RR -> B < +oo )
13 11 12 syl 
 |-  ( ph -> B < +oo )
14 9 8 13 xrltled 
 |-  ( ph -> B <_ +oo )
15 6 8 9 10 14 eliccxrd 
 |-  ( ph -> B e. ( 0 [,] +oo ) )
16 15 adantr 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
17 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
18 16 17 fmptd 
 |-  ( ph -> ( x e. A |-> B ) : A --> ( 0 [,] +oo ) )
19 18 adantr 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> ( x e. A |-> B ) : A --> ( 0 [,] +oo ) )
20 4 19 sge0xrcl 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> ( sum^ ` ( x e. A |-> B ) ) e. RR* )
21 7 a1i 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> +oo e. RR* )
22 simpr 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> ( sum^ ` ( x e. A |-> B ) ) < +oo )
23 20 21 22 xrgtned 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> +oo =/= ( sum^ ` ( x e. A |-> B ) ) )
24 23 necomd 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> ( sum^ ` ( x e. A |-> B ) ) =/= +oo )
25 24 neneqd 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> -. ( sum^ ` ( x e. A |-> B ) ) = +oo )
26 4 19 sge0repnf 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> ( ( sum^ ` ( x e. A |-> B ) ) e. RR <-> -. ( sum^ ` ( x e. A |-> B ) ) = +oo ) )
27 25 26 mpbird 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> ( sum^ ` ( x e. A |-> B ) ) e. RR )
28 11 adantr 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> B e. RR )
29 3 rpne0d 
 |-  ( ph -> B =/= 0 )
30 29 adantr 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> B =/= 0 )
31 27 28 30 redivcld 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> ( ( sum^ ` ( x e. A |-> B ) ) / B ) e. RR )
32 arch 
 |-  ( ( ( sum^ ` ( x e. A |-> B ) ) / B ) e. RR -> E. n e. NN ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n )
33 31 32 syl 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> E. n e. NN ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n )
34 ishashinf 
 |-  ( -. A e. Fin -> A. n e. NN E. y e. ~P A ( # ` y ) = n )
35 2 34 syl 
 |-  ( ph -> A. n e. NN E. y e. ~P A ( # ` y ) = n )
36 35 r19.21bi 
 |-  ( ( ph /\ n e. NN ) -> E. y e. ~P A ( # ` y ) = n )
37 df-rex 
 |-  ( E. y e. ~P A ( # ` y ) = n <-> E. y ( y e. ~P A /\ ( # ` y ) = n ) )
38 36 37 sylib 
 |-  ( ( ph /\ n e. NN ) -> E. y ( y e. ~P A /\ ( # ` y ) = n ) )
39 38 adantlr 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN ) -> E. y ( y e. ~P A /\ ( # ` y ) = n ) )
40 39 3adant3 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> E. y ( y e. ~P A /\ ( # ` y ) = n ) )
41 nfv 
 |-  F/ y ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n )
42 simprl 
 |-  ( ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> y e. ~P A )
43 simpr 
 |-  ( ( n e. NN /\ ( # ` y ) = n ) -> ( # ` y ) = n )
44 simpl 
 |-  ( ( n e. NN /\ ( # ` y ) = n ) -> n e. NN )
45 43 44 eqeltrd 
 |-  ( ( n e. NN /\ ( # ` y ) = n ) -> ( # ` y ) e. NN )
46 nnnn0 
 |-  ( ( # ` y ) e. NN -> ( # ` y ) e. NN0 )
47 vex 
 |-  y e. _V
48 47 a1i 
 |-  ( ( # ` y ) e. NN -> y e. _V )
49 hashclb 
 |-  ( y e. _V -> ( y e. Fin <-> ( # ` y ) e. NN0 ) )
50 48 49 syl 
 |-  ( ( # ` y ) e. NN -> ( y e. Fin <-> ( # ` y ) e. NN0 ) )
51 46 50 mpbird 
 |-  ( ( # ` y ) e. NN -> y e. Fin )
52 45 51 syl 
 |-  ( ( n e. NN /\ ( # ` y ) = n ) -> y e. Fin )
53 52 adantrl 
 |-  ( ( n e. NN /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> y e. Fin )
54 53 3ad2antl2 
 |-  ( ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> y e. Fin )
55 42 54 elind 
 |-  ( ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> y e. ( ~P A i^i Fin ) )
56 simp3 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n )
57 27 3ad2ant1 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> ( sum^ ` ( x e. A |-> B ) ) e. RR )
58 nnre 
 |-  ( n e. NN -> n e. RR )
59 58 3ad2ant2 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> n e. RR )
60 3 adantr 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> B e. RR+ )
61 60 3ad2ant1 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> B e. RR+ )
62 57 59 61 ltdivmul2d 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> ( ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n <-> ( sum^ ` ( x e. A |-> B ) ) < ( n x. B ) ) )
63 56 62 mpbid 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> ( sum^ ` ( x e. A |-> B ) ) < ( n x. B ) )
64 63 adantr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> ( sum^ ` ( x e. A |-> B ) ) < ( n x. B ) )
65 53 adantll 
 |-  ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> y e. Fin )
66 5 a1i 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) /\ x e. y ) -> 0 e. RR* )
67 7 a1i 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) /\ x e. y ) -> +oo e. RR* )
68 9 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) /\ x e. y ) -> B e. RR* )
69 10 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) /\ x e. y ) -> 0 <_ B )
70 13 ad3antrrr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) /\ x e. y ) -> B < +oo )
71 66 67 68 69 70 elicod 
 |-  ( ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) /\ x e. y ) -> B e. ( 0 [,) +oo ) )
72 65 71 sge0fsummpt 
 |-  ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> ( sum^ ` ( x e. y |-> B ) ) = sum_ x e. y B )
73 11 recnd 
 |-  ( ph -> B e. CC )
74 73 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> B e. CC )
75 fsumconst 
 |-  ( ( y e. Fin /\ B e. CC ) -> sum_ x e. y B = ( ( # ` y ) x. B ) )
76 65 74 75 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> sum_ x e. y B = ( ( # ` y ) x. B ) )
77 oveq1 
 |-  ( ( # ` y ) = n -> ( ( # ` y ) x. B ) = ( n x. B ) )
78 77 adantl 
 |-  ( ( y e. ~P A /\ ( # ` y ) = n ) -> ( ( # ` y ) x. B ) = ( n x. B ) )
79 78 adantl 
 |-  ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> ( ( # ` y ) x. B ) = ( n x. B ) )
80 72 76 79 3eqtrrd 
 |-  ( ( ( ph /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> ( n x. B ) = ( sum^ ` ( x e. y |-> B ) ) )
81 80 adantllr 
 |-  ( ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> ( n x. B ) = ( sum^ ` ( x e. y |-> B ) ) )
82 81 3adantl3 
 |-  ( ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> ( n x. B ) = ( sum^ ` ( x e. y |-> B ) ) )
83 64 82 breqtrd 
 |-  ( ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) )
84 55 83 jca 
 |-  ( ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) /\ ( y e. ~P A /\ ( # ` y ) = n ) ) -> ( y e. ( ~P A i^i Fin ) /\ ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) ) )
85 84 ex 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> ( ( y e. ~P A /\ ( # ` y ) = n ) -> ( y e. ( ~P A i^i Fin ) /\ ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) ) ) )
86 41 85 eximd 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> ( E. y ( y e. ~P A /\ ( # ` y ) = n ) -> E. y ( y e. ( ~P A i^i Fin ) /\ ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) ) ) )
87 40 86 mpd 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> E. y ( y e. ( ~P A i^i Fin ) /\ ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) ) )
88 df-rex 
 |-  ( E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) <-> E. y ( y e. ( ~P A i^i Fin ) /\ ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) ) )
89 87 88 sylibr 
 |-  ( ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) /\ n e. NN /\ ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n ) -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) )
90 89 3exp 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> ( n e. NN -> ( ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) ) ) )
91 90 rexlimdv 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> ( E. n e. NN ( ( sum^ ` ( x e. A |-> B ) ) / B ) < n -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) ) )
92 33 91 mpd 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) )
93 1 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> A e. V )
94 16 adantlr 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. A ) -> B e. ( 0 [,] +oo ) )
95 elpwinss 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
96 95 adantl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y C_ A )
97 93 94 96 sge0lessmpt 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( x e. y |-> B ) ) <_ ( sum^ ` ( x e. A |-> B ) ) )
98 simpr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y e. ( ~P A i^i Fin ) )
99 15 adantr 
 |-  ( ( ph /\ x e. y ) -> B e. ( 0 [,] +oo ) )
100 eqid 
 |-  ( x e. y |-> B ) = ( x e. y |-> B )
101 99 100 fmptd 
 |-  ( ph -> ( x e. y |-> B ) : y --> ( 0 [,] +oo ) )
102 101 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( x e. y |-> B ) : y --> ( 0 [,] +oo ) )
103 98 102 sge0xrcl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( x e. y |-> B ) ) e. RR* )
104 1 18 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( x e. A |-> B ) ) e. RR* )
105 104 adantr 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( sum^ ` ( x e. A |-> B ) ) e. RR* )
106 103 105 xrlenltd 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( ( sum^ ` ( x e. y |-> B ) ) <_ ( sum^ ` ( x e. A |-> B ) ) <-> -. ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) ) )
107 97 106 mpbid 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> -. ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) )
108 107 ralrimiva 
 |-  ( ph -> A. y e. ( ~P A i^i Fin ) -. ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) )
109 ralnex 
 |-  ( A. y e. ( ~P A i^i Fin ) -. ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) <-> -. E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) )
110 108 109 sylib 
 |-  ( ph -> -. E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) )
111 110 adantr 
 |-  ( ( ph /\ ( sum^ ` ( x e. A |-> B ) ) < +oo ) -> -. E. y e. ( ~P A i^i Fin ) ( sum^ ` ( x e. A |-> B ) ) < ( sum^ ` ( x e. y |-> B ) ) )
112 92 111 pm2.65da 
 |-  ( ph -> -. ( sum^ ` ( x e. A |-> B ) ) < +oo )
113 nltpnft 
 |-  ( ( sum^ ` ( x e. A |-> B ) ) e. RR* -> ( ( sum^ ` ( x e. A |-> B ) ) = +oo <-> -. ( sum^ ` ( x e. A |-> B ) ) < +oo ) )
114 104 113 syl 
 |-  ( ph -> ( ( sum^ ` ( x e. A |-> B ) ) = +oo <-> -. ( sum^ ` ( x e. A |-> B ) ) < +oo ) )
115 112 114 mpbird 
 |-  ( ph -> ( sum^ ` ( x e. A |-> B ) ) = +oo )