Metamath Proof Explorer

Theorem fsumnncl

Description: Closure of a nonempty, finite sum of positive integers. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fsumnncl.an0 
|- ( ph -> A =/= (/) )
fsumnncl.afi 
|- ( ph -> A e. Fin )
fsumnncl.b 
|- ( ( ph /\ k e. A ) -> B e. NN )
Assertion fsumnncl 
|- ( ph -> sum_ k e. A B e. NN )

Proof

Step Hyp Ref Expression
1 fsumnncl.an0 
 |-  ( ph -> A =/= (/) )
2 fsumnncl.afi 
 |-  ( ph -> A e. Fin )
3 fsumnncl.b 
 |-  ( ( ph /\ k e. A ) -> B e. NN )
4 3 nnnn0d 
 |-  ( ( ph /\ k e. A ) -> B e. NN0 )
5 2 4 fsumnn0cl 
 |-  ( ph -> sum_ k e. A B e. NN0 )
6 n0 
 |-  ( A =/= (/) <-> E. j j e. A )
7 1 6 sylib 
 |-  ( ph -> E. j j e. A )
8 0red 
 |-  ( ( ph /\ j e. A ) -> 0 e. RR )
9 nfv 
 |-  F/ k ( ph /\ j e. A )
10 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
11 10 nfel1 
 |-  F/ k [_ j / k ]_ B e. NN
12 9 11 nfim 
 |-  F/ k ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. NN )
13 eleq1w 
 |-  ( k = j -> ( k e. A <-> j e. A ) )
14 13 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. A ) <-> ( ph /\ j e. A ) ) )
15 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
16 15 eleq1d 
 |-  ( k = j -> ( B e. NN <-> [_ j / k ]_ B e. NN ) )
17 14 16 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. A ) -> B e. NN ) <-> ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. NN ) ) )
18 12 17 3 chvarfv 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. NN )
19 18 nnred 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. RR )
20 8 19 readdcld 
 |-  ( ( ph /\ j e. A ) -> ( 0 + [_ j / k ]_ B ) e. RR )
21 diffi 
 |-  ( A e. Fin -> ( A \ { j } ) e. Fin )
22 2 21 syl 
 |-  ( ph -> ( A \ { j } ) e. Fin )
23 eldifi 
 |-  ( k e. ( A \ { j } ) -> k e. A )
24 23 adantl 
 |-  ( ( ph /\ k e. ( A \ { j } ) ) -> k e. A )
25 24 4 syldan 
 |-  ( ( ph /\ k e. ( A \ { j } ) ) -> B e. NN0 )
26 22 25 fsumnn0cl 
 |-  ( ph -> sum_ k e. ( A \ { j } ) B e. NN0 )
27 26 nn0red 
 |-  ( ph -> sum_ k e. ( A \ { j } ) B e. RR )
28 27 adantr 
 |-  ( ( ph /\ j e. A ) -> sum_ k e. ( A \ { j } ) B e. RR )
29 28 19 readdcld 
 |-  ( ( ph /\ j e. A ) -> ( sum_ k e. ( A \ { j } ) B + [_ j / k ]_ B ) e. RR )
30 18 nnrpd 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. RR+ )
31 8 30 ltaddrpd 
 |-  ( ( ph /\ j e. A ) -> 0 < ( 0 + [_ j / k ]_ B ) )
32 26 nn0ge0d 
 |-  ( ph -> 0 <_ sum_ k e. ( A \ { j } ) B )
33 32 adantr 
 |-  ( ( ph /\ j e. A ) -> 0 <_ sum_ k e. ( A \ { j } ) B )
34 8 28 19 33 leadd1dd 
 |-  ( ( ph /\ j e. A ) -> ( 0 + [_ j / k ]_ B ) <_ ( sum_ k e. ( A \ { j } ) B + [_ j / k ]_ B ) )
35 8 20 29 31 34 ltletrd 
 |-  ( ( ph /\ j e. A ) -> 0 < ( sum_ k e. ( A \ { j } ) B + [_ j / k ]_ B ) )
36 difsnid 
 |-  ( j e. A -> ( ( A \ { j } ) u. { j } ) = A )
37 36 adantl 
 |-  ( ( ph /\ j e. A ) -> ( ( A \ { j } ) u. { j } ) = A )
38 37 eqcomd 
 |-  ( ( ph /\ j e. A ) -> A = ( ( A \ { j } ) u. { j } ) )
39 38 sumeq1d 
 |-  ( ( ph /\ j e. A ) -> sum_ k e. A B = sum_ k e. ( ( A \ { j } ) u. { j } ) B )
40 22 adantr 
 |-  ( ( ph /\ j e. A ) -> ( A \ { j } ) e. Fin )
41 simpr 
 |-  ( ( ph /\ j e. A ) -> j e. A )
42 neldifsnd 
 |-  ( ( ph /\ j e. A ) -> -. j e. ( A \ { j } ) )
43 simpl 
 |-  ( ( ph /\ k e. ( A \ { j } ) ) -> ph )
44 43 24 3 syl2anc 
 |-  ( ( ph /\ k e. ( A \ { j } ) ) -> B e. NN )
45 44 nncnd 
 |-  ( ( ph /\ k e. ( A \ { j } ) ) -> B e. CC )
46 45 adantlr 
 |-  ( ( ( ph /\ j e. A ) /\ k e. ( A \ { j } ) ) -> B e. CC )
47 nnsscn 
 |-  NN C_ CC
48 47 a1i 
 |-  ( ( ph /\ j e. A ) -> NN C_ CC )
49 48 18 sseldd 
 |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )
50 9 10 40 41 42 46 15 49 fsumsplitsn 
 |-  ( ( ph /\ j e. A ) -> sum_ k e. ( ( A \ { j } ) u. { j } ) B = ( sum_ k e. ( A \ { j } ) B + [_ j / k ]_ B ) )
51 39 50 eqtr2d 
 |-  ( ( ph /\ j e. A ) -> ( sum_ k e. ( A \ { j } ) B + [_ j / k ]_ B ) = sum_ k e. A B )
52 35 51 breqtrd 
 |-  ( ( ph /\ j e. A ) -> 0 < sum_ k e. A B )
53 52 ex 
 |-  ( ph -> ( j e. A -> 0 < sum_ k e. A B ) )
54 53 exlimdv 
 |-  ( ph -> ( E. j j e. A -> 0 < sum_ k e. A B ) )
55 7 54 mpd 
 |-  ( ph -> 0 < sum_ k e. A B )
56 5 55 jca 
 |-  ( ph -> ( sum_ k e. A B e. NN0 /\ 0 < sum_ k e. A B ) )
57 elnnnn0b 
 |-  ( sum_ k e. A B e. NN <-> ( sum_ k e. A B e. NN0 /\ 0 < sum_ k e. A B ) )
58 56 57 sylibr 
 |-  ( ph -> sum_ k e. A B e. NN )