efnnfsumcl

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

	Ref	Expression
Hypotheses	efnnfsumcl.1	$⊢ φ \to A \in Fin$
	efnnfsumcl.2	$⊢ (φ \land k \in A) \to B \in ℝ$
	efnnfsumcl.3	$⊢ (φ \land k \in A) \to e^{B} \in ℕ$
Assertion	efnnfsumcl	$⊢ φ \to e^{\sum_{k \in A} B} \in ℕ$

Proof

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

Metamath Proof Explorer

Theorem efnnfsumcl

Proof