fprodefsum

Description: Move the exponential function from inside a finite product to outside a finite sum. (Contributed by Scott Fenton, 26-Dec-2017)

	Ref	Expression
Hypotheses	fprodefsum.1	$⊢ Z = ℤ_{\geq M}$
	fprodefsum.2	$⊢ φ \to N \in Z$
	fprodefsum.3	$⊢ (φ \land k \in Z) \to A \in ℂ$
Assertion	fprodefsum	$⊢ φ \to \prod_{k = M}^{N} e^{A} = e^{\sum_{k = M}^{N} A}$

Proof

Step	Hyp	Ref	Expression
1		fprodefsum.1	$⊢ Z = ℤ_{\geq M}$
2		fprodefsum.2	$⊢ φ \to N \in Z$
3		fprodefsum.3	$⊢ (φ \land k \in Z) \to A \in ℂ$
4	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
5		oveq2	$⊢ a = M \to (M \dots a) = (M \dots M)$
6	5	prodeq1d	$⊢ a = M \to \prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = \prod_{m = M}^{M} (k \in Z ⟼ e^{A}) (m)$
7	5	sumeq1d	$⊢ a = M \to \sum_{m = M}^{a} (k \in Z ⟼ A) (m) = \sum_{m = M}^{M} (k \in Z ⟼ A) (m)$
8	7	fveq2d	$⊢ a = M \to e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)} = e^{\sum_{m = M}^{M} (k \in Z ⟼ A) (m)}$
9	6 8	eqeq12d	$⊢ a = M \to (\prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)} \leftrightarrow \prod_{m = M}^{M} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{M} (k \in Z ⟼ A) (m)})$
10	9	imbi2d	$⊢ a = M \to ((φ \to \prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)}) \leftrightarrow (φ \to \prod_{m = M}^{M} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{M} (k \in Z ⟼ A) (m)}))$
11		oveq2	$⊢ a = n \to (M \dots a) = (M \dots n)$
12	11	prodeq1d	$⊢ a = n \to \prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m)$
13	11	sumeq1d	$⊢ a = n \to \sum_{m = M}^{a} (k \in Z ⟼ A) (m) = \sum_{m = M}^{n} (k \in Z ⟼ A) (m)$
14	13	fveq2d	$⊢ a = n \to e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)} = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}$
15	12 14	eqeq12d	$⊢ a = n \to (\prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)} \leftrightarrow \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)})$
16	15	imbi2d	$⊢ a = n \to ((φ \to \prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)}) \leftrightarrow (φ \to \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}))$
17		oveq2	$⊢ a = n + 1 \to (M \dots a) = (M \dots n + 1)$
18	17	prodeq1d	$⊢ a = n + 1 \to \prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m)$
19	17	sumeq1d	$⊢ a = n + 1 \to \sum_{m = M}^{a} (k \in Z ⟼ A) (m) = \sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)$
20	19	fveq2d	$⊢ a = n + 1 \to e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)} = e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)}$
21	18 20	eqeq12d	$⊢ a = n + 1 \to (\prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)} \leftrightarrow \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)})$
22	21	imbi2d	$⊢ a = n + 1 \to ((φ \to \prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)}) \leftrightarrow (φ \to \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)}))$
23		oveq2	$⊢ a = N \to (M \dots a) = (M \dots N)$
24	23	prodeq1d	$⊢ a = N \to \prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = \prod_{m = M}^{N} (k \in Z ⟼ e^{A}) (m)$
25	23	sumeq1d	$⊢ a = N \to \sum_{m = M}^{a} (k \in Z ⟼ A) (m) = \sum_{m = M}^{N} (k \in Z ⟼ A) (m)$
26	25	fveq2d	$⊢ a = N \to e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)} = e^{\sum_{m = M}^{N} (k \in Z ⟼ A) (m)}$
27	24 26	eqeq12d	$⊢ a = N \to (\prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)} \leftrightarrow \prod_{m = M}^{N} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{N} (k \in Z ⟼ A) (m)})$
28	27	imbi2d	$⊢ a = N \to ((φ \to \prod_{m = M}^{a} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{a} (k \in Z ⟼ A) (m)}) \leftrightarrow (φ \to \prod_{m = M}^{N} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{N} (k \in Z ⟼ A) (m)}))$
29		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
30	29	adantl	$⊢ (φ \land M \in ℤ) \to (M \dots M) = \{M\}$
31	30	prodeq1d	$⊢ (φ \land M \in ℤ) \to \prod_{m = M}^{M} (k \in Z ⟼ e^{A}) (m) = \prod_{m \in \{M\}} (k \in Z ⟼ e^{A}) (m)$
32		simpr	$⊢ (φ \land M \in ℤ) \to M \in ℤ$
33		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
34	33 1	eleqtrrdi	$⊢ M \in ℤ \to M \in Z$
35		efcl	$⊢ A \in ℂ \to e^{A} \in ℂ$
36	3 35	syl	$⊢ (φ \land k \in Z) \to e^{A} \in ℂ$
37	36	fmpttd	$⊢ φ \to (k \in Z ⟼ e^{A}) : Z ⟶ ℂ$
38	37	ffvelrnda	$⊢ (φ \land M \in Z) \to (k \in Z ⟼ e^{A}) (M) \in ℂ$
39	34 38	sylan2	$⊢ (φ \land M \in ℤ) \to (k \in Z ⟼ e^{A}) (M) \in ℂ$
40		fveq2	$⊢ m = M \to (k \in Z ⟼ e^{A}) (m) = (k \in Z ⟼ e^{A}) (M)$
41	40	prodsn	$⊢ (M \in ℤ \land (k \in Z ⟼ e^{A}) (M) \in ℂ) \to \prod_{m \in \{M\}} (k \in Z ⟼ e^{A}) (m) = (k \in Z ⟼ e^{A}) (M)$
42	32 39 41	syl2anc	$⊢ (φ \land M \in ℤ) \to \prod_{m \in \{M\}} (k \in Z ⟼ e^{A}) (m) = (k \in Z ⟼ e^{A}) (M)$
43	34	adantl	$⊢ (φ \land M \in ℤ) \to M \in Z$
44		fvex	$⊢ e^{⦋ M / k ⦌ A} \in V$
45		nfcv	$⊢ \underline{Ⅎ} k M$
46		nfcv	$⊢ \underline{Ⅎ} k \exp$
47		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ M / k ⦌ A$
48	46 47	nffv	$⊢ \underline{Ⅎ} k e^{⦋ M / k ⦌ A}$
49		csbeq1a	$⊢ k = M \to A = ⦋ M / k ⦌ A$
50	49	fveq2d	$⊢ k = M \to e^{A} = e^{⦋ M / k ⦌ A}$
51		eqid	$⊢ (k \in Z ⟼ e^{A}) = (k \in Z ⟼ e^{A})$
52	45 48 50 51	fvmptf	$⊢ (M \in Z \land e^{⦋ M / k ⦌ A} \in V) \to (k \in Z ⟼ e^{A}) (M) = e^{⦋ M / k ⦌ A}$
53	43 44 52	sylancl	$⊢ (φ \land M \in ℤ) \to (k \in Z ⟼ e^{A}) (M) = e^{⦋ M / k ⦌ A}$
54	31 42 53	3eqtrd	$⊢ (φ \land M \in ℤ) \to \prod_{m = M}^{M} (k \in Z ⟼ e^{A}) (m) = e^{⦋ M / k ⦌ A}$
55	30	sumeq1d	$⊢ (φ \land M \in ℤ) \to \sum_{m = M}^{M} (k \in Z ⟼ A) (m) = \sum_{m \in \{M\}} (k \in Z ⟼ A) (m)$
56	3	fmpttd	$⊢ φ \to (k \in Z ⟼ A) : Z ⟶ ℂ$
57	56	ffvelrnda	$⊢ (φ \land M \in Z) \to (k \in Z ⟼ A) (M) \in ℂ$
58	34 57	sylan2	$⊢ (φ \land M \in ℤ) \to (k \in Z ⟼ A) (M) \in ℂ$
59		fveq2	$⊢ m = M \to (k \in Z ⟼ A) (m) = (k \in Z ⟼ A) (M)$
60	59	sumsn	$⊢ (M \in ℤ \land (k \in Z ⟼ A) (M) \in ℂ) \to \sum_{m \in \{M\}} (k \in Z ⟼ A) (m) = (k \in Z ⟼ A) (M)$
61	32 58 60	syl2anc	$⊢ (φ \land M \in ℤ) \to \sum_{m \in \{M\}} (k \in Z ⟼ A) (m) = (k \in Z ⟼ A) (M)$
62	3	ralrimiva	$⊢ φ \to \forall k \in Z A \in ℂ$
63	47	nfel1	$⊢ Ⅎ k ⦋ M / k ⦌ A \in ℂ$
64	49	eleq1d	$⊢ k = M \to (A \in ℂ \leftrightarrow ⦋ M / k ⦌ A \in ℂ)$
65	63 64	rspc	$⊢ M \in Z \to (\forall k \in Z A \in ℂ \to ⦋ M / k ⦌ A \in ℂ)$
66	65	impcom	$⊢ (\forall k \in Z A \in ℂ \land M \in Z) \to ⦋ M / k ⦌ A \in ℂ$
67	62 34 66	syl2an	$⊢ (φ \land M \in ℤ) \to ⦋ M / k ⦌ A \in ℂ$
68		eqid	$⊢ (k \in Z ⟼ A) = (k \in Z ⟼ A)$
69	68	fvmpts	$⊢ (M \in Z \land ⦋ M / k ⦌ A \in ℂ) \to (k \in Z ⟼ A) (M) = ⦋ M / k ⦌ A$
70	43 67 69	syl2anc	$⊢ (φ \land M \in ℤ) \to (k \in Z ⟼ A) (M) = ⦋ M / k ⦌ A$
71	55 61 70	3eqtrd	$⊢ (φ \land M \in ℤ) \to \sum_{m = M}^{M} (k \in Z ⟼ A) (m) = ⦋ M / k ⦌ A$
72	71	fveq2d	$⊢ (φ \land M \in ℤ) \to e^{\sum_{m = M}^{M} (k \in Z ⟼ A) (m)} = e^{⦋ M / k ⦌ A}$
73	54 72	eqtr4d	$⊢ (φ \land M \in ℤ) \to \prod_{m = M}^{M} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{M} (k \in Z ⟼ A) (m)}$
74	73	expcom	$⊢ M \in ℤ \to (φ \to \prod_{m = M}^{M} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{M} (k \in Z ⟼ A) (m)})$
75		simp3	$⊢ (φ \land n \in Z \land \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}) \to \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}$
76	1	peano2uzs	$⊢ n \in Z \to n + 1 \in Z$
77		simpr	$⊢ (φ \land n + 1 \in Z) \to n + 1 \in Z$
78		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ (n + 1) / k ⦌ A$
79	78	nfel1	$⊢ Ⅎ k ⦋ (n + 1) / k ⦌ A \in ℂ$
80		csbeq1a	$⊢ k = n + 1 \to A = ⦋ (n + 1) / k ⦌ A$
81	80	eleq1d	$⊢ k = n + 1 \to (A \in ℂ \leftrightarrow ⦋ (n + 1) / k ⦌ A \in ℂ)$
82	79 81	rspc	$⊢ n + 1 \in Z \to (\forall k \in Z A \in ℂ \to ⦋ (n + 1) / k ⦌ A \in ℂ)$
83	62 82	mpan9	$⊢ (φ \land n + 1 \in Z) \to ⦋ (n + 1) / k ⦌ A \in ℂ$
84		efcl	$⊢ ⦋ (n + 1) / k ⦌ A \in ℂ \to e^{⦋ (n + 1) / k ⦌ A} \in ℂ$
85	83 84	syl	$⊢ (φ \land n + 1 \in Z) \to e^{⦋ (n + 1) / k ⦌ A} \in ℂ$
86		nfcv	$⊢ \underline{Ⅎ} k (n + 1)$
87	46 78	nffv	$⊢ \underline{Ⅎ} k e^{⦋ (n + 1) / k ⦌ A}$
88	80	fveq2d	$⊢ k = n + 1 \to e^{A} = e^{⦋ (n + 1) / k ⦌ A}$
89	86 87 88 51	fvmptf	$⊢ (n + 1 \in Z \land e^{⦋ (n + 1) / k ⦌ A} \in ℂ) \to (k \in Z ⟼ e^{A}) (n + 1) = e^{⦋ (n + 1) / k ⦌ A}$
90	77 85 89	syl2anc	$⊢ (φ \land n + 1 \in Z) \to (k \in Z ⟼ e^{A}) (n + 1) = e^{⦋ (n + 1) / k ⦌ A}$
91	68	fvmpts	$⊢ (n + 1 \in Z \land ⦋ (n + 1) / k ⦌ A \in ℂ) \to (k \in Z ⟼ A) (n + 1) = ⦋ (n + 1) / k ⦌ A$
92	77 83 91	syl2anc	$⊢ (φ \land n + 1 \in Z) \to (k \in Z ⟼ A) (n + 1) = ⦋ (n + 1) / k ⦌ A$
93	92	fveq2d	$⊢ (φ \land n + 1 \in Z) \to e^{(k \in Z ⟼ A) (n + 1)} = e^{⦋ (n + 1) / k ⦌ A}$
94	90 93	eqtr4d	$⊢ (φ \land n + 1 \in Z) \to (k \in Z ⟼ e^{A}) (n + 1) = e^{(k \in Z ⟼ A) (n + 1)}$
95	76 94	sylan2	$⊢ (φ \land n \in Z) \to (k \in Z ⟼ e^{A}) (n + 1) = e^{(k \in Z ⟼ A) (n + 1)}$
96	95	3adant3	$⊢ (φ \land n \in Z \land \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}) \to (k \in Z ⟼ e^{A}) (n + 1) = e^{(k \in Z ⟼ A) (n + 1)}$
97	75 96	oveq12d	$⊢ (φ \land n \in Z \land \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}) \to \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) (k \in Z ⟼ e^{A}) (n + 1) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)} e^{(k \in Z ⟼ A) (n + 1)}$
98		simpr	$⊢ (φ \land n \in Z) \to n \in Z$
99	98 1	eleqtrdi	$⊢ (φ \land n \in Z) \to n \in ℤ_{\geq M}$
100		elfzuz	$⊢ m \in (M \dots n + 1) \to m \in ℤ_{\geq M}$
101	100 1	eleqtrrdi	$⊢ m \in (M \dots n + 1) \to m \in Z$
102	37	ffvelrnda	$⊢ (φ \land m \in Z) \to (k \in Z ⟼ e^{A}) (m) \in ℂ$
103	101 102	sylan2	$⊢ (φ \land m \in (M \dots n + 1)) \to (k \in Z ⟼ e^{A}) (m) \in ℂ$
104	103	adantlr	$⊢ ((φ \land n \in Z) \land m \in (M \dots n + 1)) \to (k \in Z ⟼ e^{A}) (m) \in ℂ$
105		fveq2	$⊢ m = n + 1 \to (k \in Z ⟼ e^{A}) (m) = (k \in Z ⟼ e^{A}) (n + 1)$
106	99 104 105	fprodp1	$⊢ (φ \land n \in Z) \to \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m) = \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) (k \in Z ⟼ e^{A}) (n + 1)$
107	106	3adant3	$⊢ (φ \land n \in Z \land \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}) \to \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m) = \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) (k \in Z ⟼ e^{A}) (n + 1)$
108	56	ffvelrnda	$⊢ (φ \land m \in Z) \to (k \in Z ⟼ A) (m) \in ℂ$
109	101 108	sylan2	$⊢ (φ \land m \in (M \dots n + 1)) \to (k \in Z ⟼ A) (m) \in ℂ$
110	109	adantlr	$⊢ ((φ \land n \in Z) \land m \in (M \dots n + 1)) \to (k \in Z ⟼ A) (m) \in ℂ$
111		fveq2	$⊢ m = n + 1 \to (k \in Z ⟼ A) (m) = (k \in Z ⟼ A) (n + 1)$
112	99 110 111	fsump1	$⊢ (φ \land n \in Z) \to \sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m) = \sum_{m = M}^{n} (k \in Z ⟼ A) (m) + (k \in Z ⟼ A) (n + 1)$
113	112	fveq2d	$⊢ (φ \land n \in Z) \to e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)} = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m) + (k \in Z ⟼ A) (n + 1)}$
114		fzfid	$⊢ (φ \land n \in Z) \to (M \dots n) \in Fin$
115		elfzuz	$⊢ m \in (M \dots n) \to m \in ℤ_{\geq M}$
116	115 1	eleqtrrdi	$⊢ m \in (M \dots n) \to m \in Z$
117	116 108	sylan2	$⊢ (φ \land m \in (M \dots n)) \to (k \in Z ⟼ A) (m) \in ℂ$
118	117	adantlr	$⊢ ((φ \land n \in Z) \land m \in (M \dots n)) \to (k \in Z ⟼ A) (m) \in ℂ$
119	114 118	fsumcl	$⊢ (φ \land n \in Z) \to \sum_{m = M}^{n} (k \in Z ⟼ A) (m) \in ℂ$
120	56	ffvelrnda	$⊢ (φ \land n + 1 \in Z) \to (k \in Z ⟼ A) (n + 1) \in ℂ$
121	76 120	sylan2	$⊢ (φ \land n \in Z) \to (k \in Z ⟼ A) (n + 1) \in ℂ$
122		efadd	$⊢ (\sum_{m = M}^{n} (k \in Z ⟼ A) (m) \in ℂ \land (k \in Z ⟼ A) (n + 1) \in ℂ) \to e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m) + (k \in Z ⟼ A) (n + 1)} = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)} e^{(k \in Z ⟼ A) (n + 1)}$
123	119 121 122	syl2anc	$⊢ (φ \land n \in Z) \to e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m) + (k \in Z ⟼ A) (n + 1)} = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)} e^{(k \in Z ⟼ A) (n + 1)}$
124	113 123	eqtrd	$⊢ (φ \land n \in Z) \to e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)} = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)} e^{(k \in Z ⟼ A) (n + 1)}$
125	124	3adant3	$⊢ (φ \land n \in Z \land \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}) \to e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)} = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)} e^{(k \in Z ⟼ A) (n + 1)}$
126	97 107 125	3eqtr4d	$⊢ (φ \land n \in Z \land \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}) \to \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)}$
127	126	3exp	$⊢ φ \to (n \in Z \to (\prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)} \to \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)}))$
128	127	com12	$⊢ n \in Z \to (φ \to (\prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)} \to \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)}))$
129	128	a2d	$⊢ n \in Z \to ((φ \to \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}) \to (φ \to \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)}))$
130	1	eqcomi	$⊢ ℤ_{\geq M} = Z$
131	129 130	eleq2s	$⊢ n \in ℤ_{\geq M} \to ((φ \to \prod_{m = M}^{n} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n} (k \in Z ⟼ A) (m)}) \to (φ \to \prod_{m = M}^{n + 1} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{n + 1} (k \in Z ⟼ A) (m)}))$
132	10 16 22 28 74 131	uzind4	$⊢ N \in ℤ_{\geq M} \to (φ \to \prod_{m = M}^{N} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{N} (k \in Z ⟼ A) (m)})$
133	4 132	mpcom	$⊢ φ \to \prod_{m = M}^{N} (k \in Z ⟼ e^{A}) (m) = e^{\sum_{m = M}^{N} (k \in Z ⟼ A) (m)}$
134		fvres	$⊢ m \in (M \dots N) \to ({(k \in Z ⟼ e^{A}) ↾}_{(M \dots N)}) (m) = (k \in Z ⟼ e^{A}) (m)$
135		fzssuz	$⊢ (M \dots N) \subseteq ℤ_{\geq M}$
136	135 1	sseqtrri	$⊢ (M \dots N) \subseteq Z$
137		resmpt	$⊢ (M \dots N) \subseteq Z \to {(k \in Z ⟼ e^{A}) ↾}_{(M \dots N)} = (k \in (M \dots N) ⟼ e^{A})$
138	136 137	ax-mp	$⊢ {(k \in Z ⟼ e^{A}) ↾}_{(M \dots N)} = (k \in (M \dots N) ⟼ e^{A})$
139	138	fveq1i	$⊢ ({(k \in Z ⟼ e^{A}) ↾}_{(M \dots N)}) (m) = (k \in (M \dots N) ⟼ e^{A}) (m)$
140	134 139	eqtr3di	$⊢ m \in (M \dots N) \to (k \in Z ⟼ e^{A}) (m) = (k \in (M \dots N) ⟼ e^{A}) (m)$
141	140	prodeq2i	$⊢ \prod_{m = M}^{N} (k \in Z ⟼ e^{A}) (m) = \prod_{m = M}^{N} (k \in (M \dots N) ⟼ e^{A}) (m)$
142		prodfc	$⊢ \prod_{m = M}^{N} (k \in (M \dots N) ⟼ e^{A}) (m) = \prod_{k = M}^{N} e^{A}$
143	141 142	eqtri	$⊢ \prod_{m = M}^{N} (k \in Z ⟼ e^{A}) (m) = \prod_{k = M}^{N} e^{A}$
144		fvres	$⊢ m \in (M \dots N) \to ({(k \in Z ⟼ A) ↾}_{(M \dots N)}) (m) = (k \in Z ⟼ A) (m)$
145		resmpt	$⊢ (M \dots N) \subseteq Z \to {(k \in Z ⟼ A) ↾}_{(M \dots N)} = (k \in (M \dots N) ⟼ A)$
146	136 145	ax-mp	$⊢ {(k \in Z ⟼ A) ↾}_{(M \dots N)} = (k \in (M \dots N) ⟼ A)$
147	146	fveq1i	$⊢ ({(k \in Z ⟼ A) ↾}_{(M \dots N)}) (m) = (k \in (M \dots N) ⟼ A) (m)$
148	144 147	eqtr3di	$⊢ m \in (M \dots N) \to (k \in Z ⟼ A) (m) = (k \in (M \dots N) ⟼ A) (m)$
149	148	sumeq2i	$⊢ \sum_{m = M}^{N} (k \in Z ⟼ A) (m) = \sum_{m = M}^{N} (k \in (M \dots N) ⟼ A) (m)$
150		sumfc	$⊢ \sum_{m = M}^{N} (k \in (M \dots N) ⟼ A) (m) = \sum_{k = M}^{N} A$
151	149 150	eqtri	$⊢ \sum_{m = M}^{N} (k \in Z ⟼ A) (m) = \sum_{k = M}^{N} A$
152	151	fveq2i	$⊢ e^{\sum_{m = M}^{N} (k \in Z ⟼ A) (m)} = e^{\sum_{k = M}^{N} A}$
153	133 143 152	3eqtr3g	$⊢ φ \to \prod_{k = M}^{N} e^{A} = e^{\sum_{k = M}^{N} A}$

Metamath Proof Explorer

Theorem fprodefsum

Proof