Metamath Proof Explorer

Theorem efnnfsumcl

Description: Finite sum closure in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Hypotheses efnnfsumcl.1 
|- ( ph -> A e. Fin )
efnnfsumcl.2 
|- ( ( ph /\ k e. A ) -> B e. RR )
efnnfsumcl.3 
|- ( ( ph /\ k e. A ) -> ( exp ` B ) e. NN )
Assertion efnnfsumcl 
|- ( ph -> ( exp ` sum_ k e. A B ) e. NN )

Proof

Step Hyp Ref Expression
1 efnnfsumcl.1 
 |-  ( ph -> A e. Fin )
2 efnnfsumcl.2 
 |-  ( ( ph /\ k e. A ) -> B e. RR )
3 efnnfsumcl.3 
 |-  ( ( ph /\ k e. A ) -> ( exp ` B ) e. NN )
4 ssrab2 
 |-  { x e. RR | ( exp ` x ) e. NN } C_ RR
5 ax-resscn 
 |-  RR C_ CC
6 4 5 sstri 
 |-  { x e. RR | ( exp ` x ) e. NN } C_ CC
7 6 a1i 
 |-  ( ph -> { x e. RR | ( exp ` x ) e. NN } C_ CC )
8 fveq2 
 |-  ( x = y -> ( exp ` x ) = ( exp ` y ) )
9 8 eleq1d 
 |-  ( x = y -> ( ( exp ` x ) e. NN <-> ( exp ` y ) e. NN ) )
10 9 elrab 
 |-  ( y e. { x e. RR | ( exp ` x ) e. NN } <-> ( y e. RR /\ ( exp ` y ) e. NN ) )
11 fveq2 
 |-  ( x = z -> ( exp ` x ) = ( exp ` z ) )
12 11 eleq1d 
 |-  ( x = z -> ( ( exp ` x ) e. NN <-> ( exp ` z ) e. NN ) )
13 12 elrab 
 |-  ( z e. { x e. RR | ( exp ` x ) e. NN } <-> ( z e. RR /\ ( exp ` z ) e. NN ) )
14 fveq2 
 |-  ( x = ( y + z ) -> ( exp ` x ) = ( exp ` ( y + z ) ) )
15 14 eleq1d 
 |-  ( x = ( y + z ) -> ( ( exp ` x ) e. NN <-> ( exp ` ( y + z ) ) e. NN ) )
16 simpll 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> y e. RR )
17 simprl 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> z e. RR )
18 16 17 readdcld 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( y + z ) e. RR )
19 16 recnd 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> y e. CC )
20 17 recnd 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> z e. CC )
21 efadd 
 |-  ( ( y e. CC /\ z e. CC ) -> ( exp ` ( y + z ) ) = ( ( exp ` y ) x. ( exp ` z ) ) )
22 19 20 21 syl2anc 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( exp ` ( y + z ) ) = ( ( exp ` y ) x. ( exp ` z ) ) )
23 nnmulcl 
 |-  ( ( ( exp ` y ) e. NN /\ ( exp ` z ) e. NN ) -> ( ( exp ` y ) x. ( exp ` z ) ) e. NN )
24 23 ad2ant2l 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( ( exp ` y ) x. ( exp ` z ) ) e. NN )
25 22 24 eqeltrd 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( exp ` ( y + z ) ) e. NN )
26 15 18 25 elrabd 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( y + z ) e. { x e. RR | ( exp ` x ) e. NN } )
27 10 13 26 syl2anb 
 |-  ( ( y e. { x e. RR | ( exp ` x ) e. NN } /\ z e. { x e. RR | ( exp ` x ) e. NN } ) -> ( y + z ) e. { x e. RR | ( exp ` x ) e. NN } )
28 27 adantl 
 |-  ( ( ph /\ ( y e. { x e. RR | ( exp ` x ) e. NN } /\ z e. { x e. RR | ( exp ` x ) e. NN } ) ) -> ( y + z ) e. { x e. RR | ( exp ` x ) e. NN } )
29 fveq2 
 |-  ( x = B -> ( exp ` x ) = ( exp ` B ) )
30 29 eleq1d 
 |-  ( x = B -> ( ( exp ` x ) e. NN <-> ( exp ` B ) e. NN ) )
31 30 2 3 elrabd 
 |-  ( ( ph /\ k e. A ) -> B e. { x e. RR | ( exp ` x ) e. NN } )
32 0re 
 |-  0 e. RR
33 1nn 
 |-  1 e. NN
34 fveq2 
 |-  ( x = 0 -> ( exp ` x ) = ( exp ` 0 ) )
35 ef0 
 |-  ( exp ` 0 ) = 1
36 34 35 eqtrdi 
 |-  ( x = 0 -> ( exp ` x ) = 1 )
37 36 eleq1d 
 |-  ( x = 0 -> ( ( exp ` x ) e. NN <-> 1 e. NN ) )
38 37 elrab 
 |-  ( 0 e. { x e. RR | ( exp ` x ) e. NN } <-> ( 0 e. RR /\ 1 e. NN ) )
39 32 33 38 mpbir2an 
 |-  0 e. { x e. RR | ( exp ` x ) e. NN }
40 39 a1i 
 |-  ( ph -> 0 e. { x e. RR | ( exp ` x ) e. NN } )
41 7 28 1 31 40 fsumcllem 
 |-  ( ph -> sum_ k e. A B e. { x e. RR | ( exp ` x ) e. NN } )
42 fveq2 
 |-  ( x = sum_ k e. A B -> ( exp ` x ) = ( exp ` sum_ k e. A B ) )
43 42 eleq1d 
 |-  ( x = sum_ k e. A B -> ( ( exp ` x ) e. NN <-> ( exp ` sum_ k e. A B ) e. NN ) )
44 43 elrab 
 |-  ( sum_ k e. A B e. { x e. RR | ( exp ` x ) e. NN } <-> ( sum_ k e. A B e. RR /\ ( exp ` sum_ k e. A B ) e. NN ) )
45 44 simprbi 
 |-  ( sum_ k e. A B e. { x e. RR | ( exp ` x ) e. NN } -> ( exp ` sum_ k e. A B ) e. NN )
46 41 45 syl 
 |-  ( ph -> ( exp ` sum_ k e. A B ) e. NN )