Theorem aks4d1p1p1

Description: Exponential law for finite products, special case. (Contributed by metakunt, 22-Jul-2024)

	Ref	Expression
Hypotheses	aks4d1p1p1.1	$$⊢\phi \to A\in {ℝ}^{+}$$
	aks4d1p1p1.2	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	aks4d1p1p1	$$⊢\phi \to \prod _{k=1}^N{A}^k=A^{\sum _{k=1}^{N}k}$$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p1p1.1	$$⊢\phi \to A\in {ℝ}^{+}$$
2		aks4d1p1p1.2	$$⊢\phi \to N\in \mathbb{N}$$
3	1	rpcnd	$$⊢\phi \to A\in ℂ$$
4	3	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots N\right)\right)\to A\in ℂ$$
5	1	rpne0d	$$⊢\phi \to A\ne 0$$
6	5	adantr	$$⊢\left(\phi \wedge k\in \left(1\dots N\right)\right)\to A\ne 0$$
7		elfzelz	$$⊢k\in \left(1\dots N\right)\to k\in \mathbb{Z}$$
8	7	zcnd	$$⊢k\in \left(1\dots N\right)\to k\in ℂ$$
9	8	adantl	$$⊢\left(\phi \wedge k\in \left(1\dots N\right)\right)\to k\in ℂ$$
10	4 6 9	3jca	$$⊢\left(\phi \wedge k\in \left(1\dots N\right)\right)\to \left(A\in ℂ\wedge A\ne 0\wedge k\in ℂ\right)$$
11		cxpef	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge k\in ℂ\right)\to A^k={\mathrm{e}}^{k\log A}$$
12	10 11	syl	$$⊢\left(\phi \wedge k\in \left(1\dots N\right)\right)\to A^k={\mathrm{e}}^{k\log A}$$
13	12	prodeq2dv	$$⊢\phi \to \prod _{k=1}^N{A}^k=\prod _{k=1}^N{\mathrm{e}}^{k\log A}$$
14		eqid	$$⊢{\mathbb{Z}}_{\ge 1}={\mathbb{Z}}_{\ge 1}$$
15		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
16	2 15	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge 1}$$
17		eluzelcn	$$⊢k\in {\mathbb{Z}}_{\ge 1}\to k\in ℂ$$
18	17	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to k\in ℂ$$
19	3	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to A\in ℂ$$
20	5	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to A\ne 0$$
21	19 20	logcld	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to \log A\in ℂ$$
22	18 21	mulcld	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to k\log A\in ℂ$$
23	14 16 22	fprodefsum	$$⊢\phi \to \prod _{k=1}^N{\mathrm{e}}^{k\log A}={\mathrm{e}}^{\sum _{k=1}^{N}k\log A}$$
24		fzfid	$$⊢\phi \to \left(1\dots N\right)\in \mathrm{Fin}$$
25	3 5	logcld	$$⊢\phi \to \log A\in ℂ$$
26	24 25 9	fsummulc1	$$⊢\phi \to \sum _{k=1}^{N}k\log A=\sum _{k=1}^{N}k\log A$$
27	26	eqcomd	$$⊢\phi \to \sum _{k=1}^{N}k\log A=\sum _{k=1}^{N}k\log A$$
28	27	fveq2d	$$⊢\phi \to {\mathrm{e}}^{\sum _{k=1}^{N}k\log A}={\mathrm{e}}^{\sum _{k=1}^{N}k\log A}$$
29	24 9	fsumcl	$$⊢\phi \to \sum _{k=1}^{N}k\in ℂ$$
30	3 5 29	cxpefd	$$⊢\phi \to A^{\sum _{k=1}^{N}k}={\mathrm{e}}^{\sum _{k=1}^{N}k\log A}$$
31	30	eqcomd	$$⊢\phi \to {\mathrm{e}}^{\sum _{k=1}^{N}k\log A}=A^{\sum _{k=1}^{N}k}$$
32	28 31	eqtrd	$$⊢\phi \to {\mathrm{e}}^{\sum _{k=1}^{N}k\log A}=A^{\sum _{k=1}^{N}k}$$
33	23 32	eqtrd	$$⊢\phi \to \prod _{k=1}^N{\mathrm{e}}^{k\log A}=A^{\sum _{k=1}^{N}k}$$
34	13 33	eqtrd	$$⊢\phi \to \prod _{k=1}^N{A}^k=A^{\sum _{k=1}^{N}k}$$