Theorem efaddlem

Description: Lemma for efadd (exponential function addition law). (Contributed by Mario Carneiro, 29-Apr-2014)

	Ref	Expression
Hypotheses	efadd.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
	efadd.2	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐵 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
	efadd.3	⊢ 𝐻 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
	efadd.4	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	efadd.5	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	efaddlem	⊢ ( 𝜑 → ( exp ‘ ( 𝐴 + 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		efadd.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2		efadd.2	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐵 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
3		efadd.3	⊢ 𝐻 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
4		efadd.4	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
5		efadd.5	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
6	4 5	addcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
7	3	efcvg	⊢ ( ( 𝐴 + 𝐵 ) ∈ ℂ → seq 0 ( + , 𝐻 ) ⇝ ( exp ‘ ( 𝐴 + 𝐵 ) ) )
8	6 7	syl	⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( exp ‘ ( 𝐴 + 𝐵 ) ) )
9	1	eftval	⊢ ( 𝑗 ∈ ℕ0 → ( 𝐹 ‘ 𝑗 ) = ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑗 ) = ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
11		absexp	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) )
12	4 11	sylan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) = ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) )
13		faccl	⊢ ( 𝑗 ∈ ℕ0 → ( ! ‘ 𝑗 ) ∈ ℕ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ! ‘ 𝑗 ) ∈ ℕ )
15		nnre	⊢ ( ( ! ‘ 𝑗 ) ∈ ℕ → ( ! ‘ 𝑗 ) ∈ ℝ )
16		nnnn0	⊢ ( ( ! ‘ 𝑗 ) ∈ ℕ → ( ! ‘ 𝑗 ) ∈ ℕ0 )
17	16	nn0ge0d	⊢ ( ( ! ‘ 𝑗 ) ∈ ℕ → 0 ≤ ( ! ‘ 𝑗 ) )
18	15 17	absidd	⊢ ( ( ! ‘ 𝑗 ) ∈ ℕ → ( abs ‘ ( ! ‘ 𝑗 ) ) = ( ! ‘ 𝑗 ) )
19	14 18	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ ( ! ‘ 𝑗 ) ) = ( ! ‘ 𝑗 ) )
20	12 19	oveq12d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) / ( abs ‘ ( ! ‘ 𝑗 ) ) ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
21		expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
22	4 21	sylan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
23	14	nncnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ! ‘ 𝑗 ) ∈ ℂ )
24	14	nnne0d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ! ‘ 𝑗 ) ≠ 0 )
25	22 23 24	absdivd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) = ( ( abs ‘ ( 𝐴 ↑ 𝑗 ) ) / ( abs ‘ ( ! ‘ 𝑗 ) ) ) )
26		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
27	26	eftval	⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ( ( ( abs ‘ 𝐴 ) ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
29	20 25 28	3eqtr4rd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑗 ) = ( abs ‘ ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) )
30		eftcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ∈ ℂ )
31	4 30	sylan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ∈ ℂ )
32	2	eftval	⊢ ( 𝑘 ∈ ℕ0 → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐵 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐺 ‘ 𝑘 ) = ( ( 𝐵 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
34		eftcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
35	5 34	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
36	3	eftval	⊢ ( 𝑘 ∈ ℕ0 → ( 𝐻 ‘ 𝑘 ) = ( ( ( 𝐴 + 𝐵 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
37	36	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = ( ( ( 𝐴 + 𝐵 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
38	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
39	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
40		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
41		binom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) )
42	38 39 40 41	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) )
43	42	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) )
44		fzfid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 0 ... 𝑘 ) ∈ Fin )
45		faccl	⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
46	45	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℕ )
47	46	nncnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℂ )
48		bccl2	⊢ ( 𝑗 ∈ ( 0 ... 𝑘 ) → ( 𝑘 C 𝑗 ) ∈ ℕ )
49	48	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 C 𝑗 ) ∈ ℕ )
50	49	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 C 𝑗 ) ∈ ℂ )
51	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝐴 ∈ ℂ )
52		fznn0sub	⊢ ( 𝑗 ∈ ( 0 ... 𝑘 ) → ( 𝑘 − 𝑗 ) ∈ ℕ0 )
53	52	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − 𝑗 ) ∈ ℕ0 )
54	51 53	expcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) ∈ ℂ )
55	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝐵 ∈ ℂ )
56		elfznn0	⊢ ( 𝑗 ∈ ( 0 ... 𝑘 ) → 𝑗 ∈ ℕ0 )
57	56	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑗 ∈ ℕ0 )
58	55 57	expcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐵 ↑ 𝑗 ) ∈ ℂ )
59	54 58	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ∈ ℂ )
60	50 59	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) ∈ ℂ )
61	46	nnne0d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ≠ 0 )
62	44 47 60 61	fsumdivc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) )
63	51 57	expcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
64	57 13	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ! ‘ 𝑗 ) ∈ ℕ )
65	64	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ! ‘ 𝑗 ) ∈ ℂ )
66	64	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ! ‘ 𝑗 ) ≠ 0 )
67	63 65 66	divcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ∈ ℂ )
68	2	eftval	⊢ ( ( 𝑘 − 𝑗 ) ∈ ℕ0 → ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) = ( ( 𝐵 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) )
69	53 68	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) = ( ( 𝐵 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) )
70	55 53	expcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐵 ↑ ( 𝑘 − 𝑗 ) ) ∈ ℂ )
71		faccl	⊢ ( ( 𝑘 − 𝑗 ) ∈ ℕ0 → ( ! ‘ ( 𝑘 − 𝑗 ) ) ∈ ℕ )
72	53 71	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ! ‘ ( 𝑘 − 𝑗 ) ) ∈ ℕ )
73	72	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ! ‘ ( 𝑘 − 𝑗 ) ) ∈ ℂ )
74	72	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ! ‘ ( 𝑘 − 𝑗 ) ) ≠ 0 )
75	70 73 74	divcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐵 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) ∈ ℂ )
76	69 75	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ∈ ℂ )
77	67 76	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) ∈ ℂ )
78		oveq2	⊢ ( 𝑗 = ( ( 0 + 𝑘 ) − 𝑚 ) → ( 𝐴 ↑ 𝑗 ) = ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑚 ) ) )
79		fveq2	⊢ ( 𝑗 = ( ( 0 + 𝑘 ) − 𝑚 ) → ( ! ‘ 𝑗 ) = ( ! ‘ ( ( 0 + 𝑘 ) − 𝑚 ) ) )
80	78 79	oveq12d	⊢ ( 𝑗 = ( ( 0 + 𝑘 ) − 𝑚 ) → ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) = ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑚 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑚 ) ) ) )
81		oveq2	⊢ ( 𝑗 = ( ( 0 + 𝑘 ) − 𝑚 ) → ( 𝑘 − 𝑗 ) = ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑚 ) ) )
82	81	fveq2d	⊢ ( 𝑗 = ( ( 0 + 𝑘 ) − 𝑚 ) → ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) = ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑚 ) ) ) )
83	80 82	oveq12d	⊢ ( 𝑗 = ( ( 0 + 𝑘 ) − 𝑚 ) → ( ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) = ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑚 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑚 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑚 ) ) ) ) )
84	77 83	fsumrev2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) = Σ 𝑚 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑚 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑚 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑚 ) ) ) ) )
85	2	eftval	⊢ ( 𝑗 ∈ ℕ0 → ( 𝐺 ‘ 𝑗 ) = ( ( 𝐵 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
86	57 85	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐺 ‘ 𝑗 ) = ( ( 𝐵 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
87	86	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) · ( 𝐺 ‘ 𝑗 ) ) = ( ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) · ( ( 𝐵 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) )
88	72 64	nnmulcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ∈ ℕ )
89	88	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ∈ ℂ )
90	88	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ≠ 0 )
91	59 89 90	divrec2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) = ( ( 1 / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) )
92	54 73 58 65 74 66	divmuldivd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) · ( ( 𝐵 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) = ( ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) )
93		bcval2	⊢ ( 𝑗 ∈ ( 0 ... 𝑘 ) → ( 𝑘 C 𝑗 ) = ( ( ! ‘ 𝑘 ) / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) )
94	93	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 C 𝑗 ) = ( ( ! ‘ 𝑘 ) / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) )
95	94	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝑘 C 𝑗 ) / ( ! ‘ 𝑘 ) ) = ( ( ( ! ‘ 𝑘 ) / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) )
96	47	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
97	61	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
98	96 89 96 90 97	divdiv32d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( ! ‘ 𝑘 ) / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) = ( ( ( ! ‘ 𝑘 ) / ( ! ‘ 𝑘 ) ) / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) )
99	96 97	dividd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ! ‘ 𝑘 ) / ( ! ‘ 𝑘 ) ) = 1 )
100	99	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( ! ‘ 𝑘 ) / ( ! ‘ 𝑘 ) ) / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) = ( 1 / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) )
101	98 100	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( ! ‘ 𝑘 ) / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) = ( 1 / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) )
102	95 101	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝑘 C 𝑗 ) / ( ! ‘ 𝑘 ) ) = ( 1 / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) )
103	102	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝑘 C 𝑗 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) = ( ( 1 / ( ( ! ‘ ( 𝑘 − 𝑗 ) ) · ( ! ‘ 𝑗 ) ) ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) )
104	91 92 103	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝑘 C 𝑗 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) = ( ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) · ( ( 𝐵 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) ) )
105	87 104	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) · ( 𝐺 ‘ 𝑗 ) ) = ( ( ( 𝑘 C 𝑗 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) )
106		nn0cn	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
107	106	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑘 ∈ ℂ )
108	107	addlidd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 0 + 𝑘 ) = 𝑘 )
109	108	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( 0 + 𝑘 ) − 𝑗 ) = ( 𝑘 − 𝑗 ) )
110	109	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑗 ) ) = ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) )
111	109	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ! ‘ ( ( 0 + 𝑘 ) − 𝑗 ) ) = ( ! ‘ ( 𝑘 − 𝑗 ) ) )
112	110 111	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑗 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑗 ) ) ) = ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) )
113	109	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) = ( 𝑘 − ( 𝑘 − 𝑗 ) ) )
114		nn0cn	⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℂ )
115	57 114	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑗 ∈ ℂ )
116	107 115	nncand	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − ( 𝑘 − 𝑗 ) ) = 𝑗 )
117	113 116	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) = 𝑗 )
118	117	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) ) = ( 𝐺 ‘ 𝑗 ) )
119	112 118	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑗 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑗 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) ) ) = ( ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) / ( ! ‘ ( 𝑘 − 𝑗 ) ) ) · ( 𝐺 ‘ 𝑗 ) ) )
120	50 59 96 97	div23d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) = ( ( ( 𝑘 C 𝑗 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) )
121	105 119 120	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) = ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑗 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑗 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) ) ) )
122	121	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑗 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑗 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) ) ) )
123		oveq2	⊢ ( 𝑗 = 𝑚 → ( ( 0 + 𝑘 ) − 𝑗 ) = ( ( 0 + 𝑘 ) − 𝑚 ) )
124	123	oveq2d	⊢ ( 𝑗 = 𝑚 → ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑗 ) ) = ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑚 ) ) )
125	123	fveq2d	⊢ ( 𝑗 = 𝑚 → ( ! ‘ ( ( 0 + 𝑘 ) − 𝑗 ) ) = ( ! ‘ ( ( 0 + 𝑘 ) − 𝑚 ) ) )
126	124 125	oveq12d	⊢ ( 𝑗 = 𝑚 → ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑗 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑗 ) ) ) = ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑚 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑚 ) ) ) )
127	123	oveq2d	⊢ ( 𝑗 = 𝑚 → ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) = ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑚 ) ) )
128	127	fveq2d	⊢ ( 𝑗 = 𝑚 → ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) ) = ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑚 ) ) ) )
129	126 128	oveq12d	⊢ ( 𝑗 = 𝑚 → ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑗 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑗 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) ) ) = ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑚 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑚 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑚 ) ) ) ) )
130	129	cbvsumv	⊢ Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑗 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑗 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑗 ) ) ) ) = Σ 𝑚 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑚 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑚 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑚 ) ) ) )
131	122 130	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) = Σ 𝑚 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ ( ( 0 + 𝑘 ) − 𝑚 ) ) / ( ! ‘ ( ( 0 + 𝑘 ) − 𝑚 ) ) ) · ( 𝐺 ‘ ( 𝑘 − ( ( 0 + 𝑘 ) − 𝑚 ) ) ) ) )
132	84 131	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) )
133	62 132	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( 𝑘 C 𝑗 ) · ( ( 𝐴 ↑ ( 𝑘 − 𝑗 ) ) · ( 𝐵 ↑ 𝑗 ) ) ) / ( ! ‘ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
134	43 133	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
135	37 134	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐻 ‘ 𝑘 ) = Σ 𝑗 ∈ ( 0 ... 𝑘 ) ( ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · ( 𝐺 ‘ ( 𝑘 − 𝑗 ) ) ) )
136	4	abscld	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ )
137	136	recnd	⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℂ )
138	26	efcllem	⊢ ( ( abs ‘ 𝐴 ) ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ dom ⇝ )
139	137 138	syl	⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ dom ⇝ )
140	2	efcllem	⊢ ( 𝐵 ∈ ℂ → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
141	5 140	syl	⊢ ( 𝜑 → seq 0 ( + , 𝐺 ) ∈ dom ⇝ )
142	10 29 31 33 35 135 139 141	mertens	⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( Σ 𝑗 ∈ ℕ0 ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝐵 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )
143		efval	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = Σ 𝑗 ∈ ℕ0 ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
144	4 143	syl	⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = Σ 𝑗 ∈ ℕ0 ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) )
145		efval	⊢ ( 𝐵 ∈ ℂ → ( exp ‘ 𝐵 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐵 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
146	5 145	syl	⊢ ( 𝜑 → ( exp ‘ 𝐵 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐵 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
147	144 146	oveq12d	⊢ ( 𝜑 → ( ( exp ‘ 𝐴 ) · ( exp ‘ 𝐵 ) ) = ( Σ 𝑗 ∈ ℕ0 ( ( 𝐴 ↑ 𝑗 ) / ( ! ‘ 𝑗 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝐵 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ) )
148	142 147	breqtrrd	⊢ ( 𝜑 → seq 0 ( + , 𝐻 ) ⇝ ( ( exp ‘ 𝐴 ) · ( exp ‘ 𝐵 ) ) )
149		climuni	⊢ ( ( seq 0 ( + , 𝐻 ) ⇝ ( exp ‘ ( 𝐴 + 𝐵 ) ) ∧ seq 0 ( + , 𝐻 ) ⇝ ( ( exp ‘ 𝐴 ) · ( exp ‘ 𝐵 ) ) ) → ( exp ‘ ( 𝐴 + 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ 𝐵 ) ) )
150	8 148 149	syl2anc	⊢ ( 𝜑 → ( exp ‘ ( 𝐴 + 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ 𝐵 ) ) )