iprodefisum

Description: Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018)

	Ref	Expression
Hypotheses	iprodefisum.1	$⊢ Z = ℤ_{\geq M}$
	iprodefisum.2	$⊢ φ \to M \in ℤ$
	iprodefisum.3	$⊢ (φ \land k \in Z) \to F (k) = B$
	iprodefisum.4	$⊢ (φ \land k \in Z) \to B \in ℂ$
	iprodefisum.5	$⊢ φ \to seq M (+ F) \in dom ⇝$
Assertion	iprodefisum	$⊢ φ \to \prod_{k \in Z} e^{B} = e^{\sum_{k \in Z} B}$

Proof

Step	Hyp	Ref	Expression
1		iprodefisum.1	$⊢ Z = ℤ_{\geq M}$
2		iprodefisum.2	$⊢ φ \to M \in ℤ$
3		iprodefisum.3	$⊢ (φ \land k \in Z) \to F (k) = B$
4		iprodefisum.4	$⊢ (φ \land k \in Z) \to B \in ℂ$
5		iprodefisum.5	$⊢ φ \to seq M (+ F) \in dom ⇝$
6	1 2 3 4 5	isumcl	$⊢ φ \to \sum_{k \in Z} B \in ℂ$
7		efne0	$⊢ \sum_{k \in Z} B \in ℂ \to e^{\sum_{k \in Z} B} \neq 0$
8	6 7	syl	$⊢ φ \to e^{\sum_{k \in Z} B} \neq 0$
9		efcn	$⊢ \exp : ℂ \underset{cn}{⟶} ℂ$
10	9	a1i	$⊢ φ \to \exp : ℂ \underset{cn}{⟶} ℂ$
11		fveq2	$⊢ j = k \to F (j) = F (k)$
12		eqid	$⊢ (j \in Z ⟼ F (j)) = (j \in Z ⟼ F (j))$
13		fvex	$⊢ F (k) \in V$
14	11 12 13	fvmpt	$⊢ k \in Z \to (j \in Z ⟼ F (j)) (k) = F (k)$
15	14	adantl	$⊢ (φ \land k \in Z) \to (j \in Z ⟼ F (j)) (k) = F (k)$
16	3 4	eqeltrd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
17	15 16	eqeltrd	$⊢ (φ \land k \in Z) \to (j \in Z ⟼ F (j)) (k) \in ℂ$
18	1 2 17	serf	$⊢ φ \to seq M (+ (j \in Z ⟼ F (j))) : Z ⟶ ℂ$
19	1	eqcomi	$⊢ ℤ_{\geq M} = Z$
20	14 19	eleq2s	$⊢ k \in ℤ_{\geq M} \to (j \in Z ⟼ F (j)) (k) = F (k)$
21	20	adantl	$⊢ (φ \land k \in ℤ_{\geq M}) \to (j \in Z ⟼ F (j)) (k) = F (k)$
22	2 21	seqfeq	$⊢ φ \to seq M (+ (j \in Z ⟼ F (j))) = seq M (+ F)$
23		climdm	$⊢ seq M (+ F) \in dom ⇝ \leftrightarrow seq M (+ F) ⇝ ⇝ (seq M (+ F))$
24	5 23	sylib	$⊢ φ \to seq M (+ F) ⇝ ⇝ (seq M (+ F))$
25	22 24	eqbrtrd	$⊢ φ \to seq M (+ (j \in Z ⟼ F (j))) ⇝ ⇝ (seq M (+ F))$
26		climcl	$⊢ seq M (+ F) ⇝ ⇝ (seq M (+ F)) \to ⇝ (seq M (+ F)) \in ℂ$
27	24 26	syl	$⊢ φ \to ⇝ (seq M (+ F)) \in ℂ$
28	1 2 10 18 25 27	climcncf	$⊢ φ \to (\exp \circ seq M (+ (j \in Z ⟼ F (j)))) ⇝ e^{⇝ (seq M (+ F))}$
29	11	cbvmptv	$⊢ (j \in Z ⟼ F (j)) = (k \in Z ⟼ F (k))$
30	16 29	fmptd	$⊢ φ \to (j \in Z ⟼ F (j)) : Z ⟶ ℂ$
31	1 2 30	iprodefisumlem	$⊢ φ \to seq M (\times (\exp \circ (j \in Z ⟼ F (j)))) = \exp \circ seq M (+ (j \in Z ⟼ F (j)))$
32	1 2 3 4	isum	$⊢ φ \to \sum_{k \in Z} B = ⇝ (seq M (+ F))$
33	32	fveq2d	$⊢ φ \to e^{\sum_{k \in Z} B} = e^{⇝ (seq M (+ F))}$
34	28 31 33	3brtr4d	$⊢ φ \to seq M (\times (\exp \circ (j \in Z ⟼ F (j)))) ⇝ e^{\sum_{k \in Z} B}$
35		fvco3	$⊢ ((j \in Z ⟼ F (j)) : Z ⟶ ℂ \land k \in Z) \to (\exp \circ (j \in Z ⟼ F (j))) (k) = e^{(j \in Z ⟼ F (j)) (k)}$
36	30 35	sylan	$⊢ (φ \land k \in Z) \to (\exp \circ (j \in Z ⟼ F (j))) (k) = e^{(j \in Z ⟼ F (j)) (k)}$
37	15	fveq2d	$⊢ (φ \land k \in Z) \to e^{(j \in Z ⟼ F (j)) (k)} = e^{F (k)}$
38	3	fveq2d	$⊢ (φ \land k \in Z) \to e^{F (k)} = e^{B}$
39	36 37 38	3eqtrd	$⊢ (φ \land k \in Z) \to (\exp \circ (j \in Z ⟼ F (j))) (k) = e^{B}$
40		efcl	$⊢ B \in ℂ \to e^{B} \in ℂ$
41	4 40	syl	$⊢ (φ \land k \in Z) \to e^{B} \in ℂ$
42	1 2 8 34 39 41	iprodn0	$⊢ φ \to \prod_{k \in Z} e^{B} = e^{\sum_{k \in Z} B}$

Metamath Proof Explorer

Theorem iprodefisum

Proof