Theorem efnnfsumcl

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

	Ref	Expression
Hypotheses	efnnfsumcl.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	efnnfsumcl.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	efnnfsumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( exp ‘ 𝐵 ) ∈ ℕ )
Assertion	efnnfsumcl	⊢ ( 𝜑 → ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		efnnfsumcl.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		efnnfsumcl.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3		efnnfsumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( exp ‘ 𝐵 ) ∈ ℕ )
4		ssrab2	⊢ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ⊆ ℝ
5		ax-resscn	⊢ ℝ ⊆ ℂ
6	4 5	sstri	⊢ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ⊆ ℂ
7	6	a1i	⊢ ( 𝜑 → { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ⊆ ℂ )
8		fveq2	⊢ ( 𝑥 = 𝑦 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝑦 ) )
9	8	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ 𝑦 ) ∈ ℕ ) )
10	9	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) )
11		fveq2	⊢ ( 𝑥 = 𝑧 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝑧 ) )
12	11	eleq1d	⊢ ( 𝑥 = 𝑧 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ 𝑧 ) ∈ ℕ ) )
13	12	elrab	⊢ ( 𝑧 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) )
14		fveq2	⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( exp ‘ 𝑥 ) = ( exp ‘ ( 𝑦 + 𝑧 ) ) )
15	14	eleq1d	⊢ ( 𝑥 = ( 𝑦 + 𝑧 ) → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ ( 𝑦 + 𝑧 ) ) ∈ ℕ ) )
16		simpll	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑦 ∈ ℝ )
17		simprl	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑧 ∈ ℝ )
18	16 17	readdcld	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( 𝑦 + 𝑧 ) ∈ ℝ )
19	16	recnd	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑦 ∈ ℂ )
20	17	recnd	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → 𝑧 ∈ ℂ )
21		efadd	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( exp ‘ ( 𝑦 + 𝑧 ) ) = ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) )
22	19 20 21	syl2anc	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( exp ‘ ( 𝑦 + 𝑧 ) ) = ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) )
23		nnmulcl	⊢ ( ( ( exp ‘ 𝑦 ) ∈ ℕ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) → ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) ∈ ℕ )
24	23	ad2ant2l	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( ( exp ‘ 𝑦 ) · ( exp ‘ 𝑧 ) ) ∈ ℕ )
25	22 24	eqeltrd	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( exp ‘ ( 𝑦 + 𝑧 ) ) ∈ ℕ )
26	15 18 25	elrabd	⊢ ( ( ( 𝑦 ∈ ℝ ∧ ( exp ‘ 𝑦 ) ∈ ℕ ) ∧ ( 𝑧 ∈ ℝ ∧ ( exp ‘ 𝑧 ) ∈ ℕ ) ) → ( 𝑦 + 𝑧 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
27	10 13 26	syl2anb	⊢ ( ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ∧ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ) → ( 𝑦 + 𝑧 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
28	27	adantl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ∧ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ) ) → ( 𝑦 + 𝑧 ) ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
29		fveq2	⊢ ( 𝑥 = 𝐵 → ( exp ‘ 𝑥 ) = ( exp ‘ 𝐵 ) )
30	29	eleq1d	⊢ ( 𝑥 = 𝐵 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ 𝐵 ) ∈ ℕ ) )
31	30 2 3	elrabd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
32		0re	⊢ 0 ∈ ℝ
33		1nn	⊢ 1 ∈ ℕ
34		fveq2	⊢ ( 𝑥 = 0 → ( exp ‘ 𝑥 ) = ( exp ‘ 0 ) )
35		ef0	⊢ ( exp ‘ 0 ) = 1
36	34 35	eqtrdi	⊢ ( 𝑥 = 0 → ( exp ‘ 𝑥 ) = 1 )
37	36	eleq1d	⊢ ( 𝑥 = 0 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ 1 ∈ ℕ ) )
38	37	elrab	⊢ ( 0 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( 0 ∈ ℝ ∧ 1 ∈ ℕ ) )
39	32 33 38	mpbir2an	⊢ 0 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ }
40	39	a1i	⊢ ( 𝜑 → 0 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
41	7 28 1 31 40	fsumcllem	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } )
42		fveq2	⊢ ( 𝑥 = Σ 𝑘 ∈ 𝐴 𝐵 → ( exp ‘ 𝑥 ) = ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) )
43	42	eleq1d	⊢ ( 𝑥 = Σ 𝑘 ∈ 𝐴 𝐵 → ( ( exp ‘ 𝑥 ) ∈ ℕ ↔ ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ ) )
44	43	elrab	⊢ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } ↔ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ ∧ ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ ) )
45	44	simprbi	⊢ ( Σ 𝑘 ∈ 𝐴 𝐵 ∈ { 𝑥 ∈ ℝ ∣ ( exp ‘ 𝑥 ) ∈ ℕ } → ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ )
46	41 45	syl	⊢ ( 𝜑 → ( exp ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) ∈ ℕ )