iprodefisumlem

	Ref	Expression
Hypotheses	iprodefisumlem.1	$⊢ Z = ℤ_{\geq M}$
	iprodefisumlem.2	$⊢ φ \to M \in ℤ$
	iprodefisumlem.3	$⊢ φ \to F : Z ⟶ ℂ$
Assertion	iprodefisumlem	$⊢ φ \to seq M (\times (\exp \circ F)) = \exp \circ seq M (+ F)$

Proof

Step	Hyp	Ref	Expression
1		iprodefisumlem.1	$⊢ Z = ℤ_{\geq M}$
2		iprodefisumlem.2	$⊢ φ \to M \in ℤ$
3		iprodefisumlem.3	$⊢ φ \to F : Z ⟶ ℂ$
4		fvco3	$⊢ (F : Z ⟶ ℂ \land k \in Z) \to (\exp \circ F) (k) = e^{F (k)}$
5	3 4	sylan	$⊢ (φ \land k \in Z) \to (\exp \circ F) (k) = e^{F (k)}$
6	3	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
7		efcl	$⊢ F (k) \in ℂ \to e^{F (k)} \in ℂ$
8	6 7	syl	$⊢ (φ \land k \in Z) \to e^{F (k)} \in ℂ$
9	5 8	eqeltrd	$⊢ (φ \land k \in Z) \to (\exp \circ F) (k) \in ℂ$
10	1 2 9	prodf	$⊢ φ \to seq M (\times (\exp \circ F)) : Z ⟶ ℂ$
11	10	ffnd	$⊢ φ \to seq M (\times (\exp \circ F)) Fn Z$
12		eff	$⊢ \exp : ℂ ⟶ ℂ$
13		ffn	$⊢ \exp : ℂ ⟶ ℂ \to \exp Fn ℂ$
14	12 13	ax-mp	$⊢ \exp Fn ℂ$
15	1 2 6	serf	$⊢ φ \to seq M (+ F) : Z ⟶ ℂ$
16		fnfco	$⊢ (\exp Fn ℂ \land seq M (+ F) : Z ⟶ ℂ) \to (\exp \circ seq M (+ F)) Fn Z$
17	14 15 16	sylancr	$⊢ φ \to (\exp \circ seq M (+ F)) Fn Z$
18		fveq2	$⊢ j = M \to seq M (\times (\exp \circ F)) (j) = seq M (\times (\exp \circ F)) (M)$
19		2fveq3	$⊢ j = M \to e^{seq M (+ F) (j)} = e^{seq M (+ F) (M)}$
20	18 19	eqeq12d	$⊢ j = M \to (seq M (\times (\exp \circ F)) (j) = e^{seq M (+ F) (j)} \leftrightarrow seq M (\times (\exp \circ F)) (M) = e^{seq M (+ F) (M)})$
21	20	imbi2d	$⊢ j = M \to ((φ \to seq M (\times (\exp \circ F)) (j) = e^{seq M (+ F) (j)}) \leftrightarrow (φ \to seq M (\times (\exp \circ F)) (M) = e^{seq M (+ F) (M)}))$
22		fveq2	$⊢ j = n \to seq M (\times (\exp \circ F)) (j) = seq M (\times (\exp \circ F)) (n)$
23		2fveq3	$⊢ j = n \to e^{seq M (+ F) (j)} = e^{seq M (+ F) (n)}$
24	22 23	eqeq12d	$⊢ j = n \to (seq M (\times (\exp \circ F)) (j) = e^{seq M (+ F) (j)} \leftrightarrow seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)})$
25	24	imbi2d	$⊢ j = n \to ((φ \to seq M (\times (\exp \circ F)) (j) = e^{seq M (+ F) (j)}) \leftrightarrow (φ \to seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)}))$
26		fveq2	$⊢ j = n + 1 \to seq M (\times (\exp \circ F)) (j) = seq M (\times (\exp \circ F)) (n + 1)$
27		2fveq3	$⊢ j = n + 1 \to e^{seq M (+ F) (j)} = e^{seq M (+ F) (n + 1)}$
28	26 27	eqeq12d	$⊢ j = n + 1 \to (seq M (\times (\exp \circ F)) (j) = e^{seq M (+ F) (j)} \leftrightarrow seq M (\times (\exp \circ F)) (n + 1) = e^{seq M (+ F) (n + 1)})$
29	28	imbi2d	$⊢ j = n + 1 \to ((φ \to seq M (\times (\exp \circ F)) (j) = e^{seq M (+ F) (j)}) \leftrightarrow (φ \to seq M (\times (\exp \circ F)) (n + 1) = e^{seq M (+ F) (n + 1)}))$
30		fveq2	$⊢ j = k \to seq M (\times (\exp \circ F)) (j) = seq M (\times (\exp \circ F)) (k)$
31		2fveq3	$⊢ j = k \to e^{seq M (+ F) (j)} = e^{seq M (+ F) (k)}$
32	30 31	eqeq12d	$⊢ j = k \to (seq M (\times (\exp \circ F)) (j) = e^{seq M (+ F) (j)} \leftrightarrow seq M (\times (\exp \circ F)) (k) = e^{seq M (+ F) (k)})$
33	32	imbi2d	$⊢ j = k \to ((φ \to seq M (\times (\exp \circ F)) (j) = e^{seq M (+ F) (j)}) \leftrightarrow (φ \to seq M (\times (\exp \circ F)) (k) = e^{seq M (+ F) (k)}))$
34		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
35	2 34	syl	$⊢ φ \to M \in ℤ_{\geq M}$
36	35 1	eleqtrrdi	$⊢ φ \to M \in Z$
37		fvco3	$⊢ (F : Z ⟶ ℂ \land M \in Z) \to (\exp \circ F) (M) = e^{F (M)}$
38	3 36 37	syl2anc	$⊢ φ \to (\exp \circ F) (M) = e^{F (M)}$
39		seq1	$⊢ M \in ℤ \to seq M (\times (\exp \circ F)) (M) = (\exp \circ F) (M)$
40	2 39	syl	$⊢ φ \to seq M (\times (\exp \circ F)) (M) = (\exp \circ F) (M)$
41		seq1	$⊢ M \in ℤ \to seq M (+ F) (M) = F (M)$
42	2 41	syl	$⊢ φ \to seq M (+ F) (M) = F (M)$
43	42	fveq2d	$⊢ φ \to e^{seq M (+ F) (M)} = e^{F (M)}$
44	38 40 43	3eqtr4d	$⊢ φ \to seq M (\times (\exp \circ F)) (M) = e^{seq M (+ F) (M)}$
45	44	a1i	$⊢ M \in ℤ \to (φ \to seq M (\times (\exp \circ F)) (M) = e^{seq M (+ F) (M)})$
46		oveq1	$⊢ seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)} \to seq M (\times (\exp \circ F)) (n) (\exp \circ F) (n + 1) = e^{seq M (+ F) (n)} (\exp \circ F) (n + 1)$
47	46	3ad2ant3	$⊢ (n \in ℤ_{\geq M} \land φ \land seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)}) \to seq M (\times (\exp \circ F)) (n) (\exp \circ F) (n + 1) = e^{seq M (+ F) (n)} (\exp \circ F) (n + 1)$
48	3	adantl	$⊢ (n \in ℤ_{\geq M} \land φ) \to F : Z ⟶ ℂ$
49		peano2uz	$⊢ n \in ℤ_{\geq M} \to n + 1 \in ℤ_{\geq M}$
50	49 1	eleqtrrdi	$⊢ n \in ℤ_{\geq M} \to n + 1 \in Z$
51	50	adantr	$⊢ (n \in ℤ_{\geq M} \land φ) \to n + 1 \in Z$
52		fvco3	$⊢ (F : Z ⟶ ℂ \land n + 1 \in Z) \to (\exp \circ F) (n + 1) = e^{F (n + 1)}$
53	48 51 52	syl2anc	$⊢ (n \in ℤ_{\geq M} \land φ) \to (\exp \circ F) (n + 1) = e^{F (n + 1)}$
54	53	oveq2d	$⊢ (n \in ℤ_{\geq M} \land φ) \to e^{seq M (+ F) (n)} (\exp \circ F) (n + 1) = e^{seq M (+ F) (n)} e^{F (n + 1)}$
55	15	ffvelrnda	$⊢ (φ \land n \in Z) \to seq M (+ F) (n) \in ℂ$
56	55	expcom	$⊢ n \in Z \to (φ \to seq M (+ F) (n) \in ℂ)$
57	1	eqcomi	$⊢ ℤ_{\geq M} = Z$
58	56 57	eleq2s	$⊢ n \in ℤ_{\geq M} \to (φ \to seq M (+ F) (n) \in ℂ)$
59	58	imp	$⊢ (n \in ℤ_{\geq M} \land φ) \to seq M (+ F) (n) \in ℂ$
60	48 51	ffvelrnd	$⊢ (n \in ℤ_{\geq M} \land φ) \to F (n + 1) \in ℂ$
61		efadd	$⊢ (seq M (+ F) (n) \in ℂ \land F (n + 1) \in ℂ) \to e^{seq M (+ F) (n) + F (n + 1)} = e^{seq M (+ F) (n)} e^{F (n + 1)}$
62	59 60 61	syl2anc	$⊢ (n \in ℤ_{\geq M} \land φ) \to e^{seq M (+ F) (n) + F (n + 1)} = e^{seq M (+ F) (n)} e^{F (n + 1)}$
63	54 62	eqtr4d	$⊢ (n \in ℤ_{\geq M} \land φ) \to e^{seq M (+ F) (n)} (\exp \circ F) (n + 1) = e^{seq M (+ F) (n) + F (n + 1)}$
64	63	3adant3	$⊢ (n \in ℤ_{\geq M} \land φ \land seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)}) \to e^{seq M (+ F) (n)} (\exp \circ F) (n + 1) = e^{seq M (+ F) (n) + F (n + 1)}$
65	47 64	eqtrd	$⊢ (n \in ℤ_{\geq M} \land φ \land seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)}) \to seq M (\times (\exp \circ F)) (n) (\exp \circ F) (n + 1) = e^{seq M (+ F) (n) + F (n + 1)}$
66		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\times (\exp \circ F)) (n + 1) = seq M (\times (\exp \circ F)) (n) (\exp \circ F) (n + 1)$
67	66	adantr	$⊢ (n \in ℤ_{\geq M} \land φ) \to seq M (\times (\exp \circ F)) (n + 1) = seq M (\times (\exp \circ F)) (n) (\exp \circ F) (n + 1)$
68	67	3adant3	$⊢ (n \in ℤ_{\geq M} \land φ \land seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)}) \to seq M (\times (\exp \circ F)) (n + 1) = seq M (\times (\exp \circ F)) (n) (\exp \circ F) (n + 1)$
69		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (+ F) (n + 1) = seq M (+ F) (n) + F (n + 1)$
70	69	adantr	$⊢ (n \in ℤ_{\geq M} \land φ) \to seq M (+ F) (n + 1) = seq M (+ F) (n) + F (n + 1)$
71	70	fveq2d	$⊢ (n \in ℤ_{\geq M} \land φ) \to e^{seq M (+ F) (n + 1)} = e^{seq M (+ F) (n) + F (n + 1)}$
72	71	3adant3	$⊢ (n \in ℤ_{\geq M} \land φ \land seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)}) \to e^{seq M (+ F) (n + 1)} = e^{seq M (+ F) (n) + F (n + 1)}$
73	65 68 72	3eqtr4d	$⊢ (n \in ℤ_{\geq M} \land φ \land seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)}) \to seq M (\times (\exp \circ F)) (n + 1) = e^{seq M (+ F) (n + 1)}$
74	73	3exp	$⊢ n \in ℤ_{\geq M} \to (φ \to (seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)} \to seq M (\times (\exp \circ F)) (n + 1) = e^{seq M (+ F) (n + 1)}))$
75	74	a2d	$⊢ n \in ℤ_{\geq M} \to ((φ \to seq M (\times (\exp \circ F)) (n) = e^{seq M (+ F) (n)}) \to (φ \to seq M (\times (\exp \circ F)) (n + 1) = e^{seq M (+ F) (n + 1)}))$
76	21 25 29 33 45 75	uzind4	$⊢ k \in ℤ_{\geq M} \to (φ \to seq M (\times (\exp \circ F)) (k) = e^{seq M (+ F) (k)})$
77	76 1	eleq2s	$⊢ k \in Z \to (φ \to seq M (\times (\exp \circ F)) (k) = e^{seq M (+ F) (k)})$
78	77	impcom	$⊢ (φ \land k \in Z) \to seq M (\times (\exp \circ F)) (k) = e^{seq M (+ F) (k)}$
79		fvco3	$⊢ (seq M (+ F) : Z ⟶ ℂ \land k \in Z) \to (\exp \circ seq M (+ F)) (k) = e^{seq M (+ F) (k)}$
80	15 79	sylan	$⊢ (φ \land k \in Z) \to (\exp \circ seq M (+ F)) (k) = e^{seq M (+ F) (k)}$
81	78 80	eqtr4d	$⊢ (φ \land k \in Z) \to seq M (\times (\exp \circ F)) (k) = (\exp \circ seq M (+ F)) (k)$
82	11 17 81	eqfnfvd	$⊢ φ \to seq M (\times (\exp \circ F)) = \exp \circ seq M (+ F)$

Metamath Proof Explorer

Theorem iprodefisumlem

Proof