Metamath Proof Explorer

Theorem aks4d1p1p1

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

Ref Expression
Hypotheses aks4d1p1p1.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
aks4d1p1p1.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion aks4d1p1p1 ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 ↑𝑐 𝑘 ) = ( 𝐴 ↑𝑐 Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p1.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 aks4d1p1p1.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 1 rpcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5 1 rpne0d ⊢ ( 𝜑 → 𝐴 ≠ 0 )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ≠ 0 )
7 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℤ )
8 7 zcnd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
10 4 6 9 3jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑘 ∈ ℂ ) )
11 cxpef ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑘 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝑘 ) = ( exp ‘ ( 𝑘 · ( log ‘ 𝐴 ) ) ) )
12 10 11 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ↑𝑐 𝑘 ) = ( exp ‘ ( 𝑘 · ( log ‘ 𝐴 ) ) ) )
13 12 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 ↑𝑐 𝑘 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( exp ‘ ( 𝑘 · ( log ‘ 𝐴 ) ) ) )
14 eqid ⊢ ( ℤ≥ ‘ 1 ) = ( ℤ≥ ‘ 1 )
15 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
16 2 15 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
17 eluzelcn ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → 𝑘 ∈ ℂ )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑘 ∈ ℂ )
19 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 𝐴 ∈ ℂ )
20 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 𝐴 ≠ 0 )
21 19 20 logcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
22 18 21 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( 𝑘 · ( log ‘ 𝐴 ) ) ∈ ℂ )
23 14 16 22 fprodefsum ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( exp ‘ ( 𝑘 · ( log ‘ 𝐴 ) ) ) = ( exp ‘ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑘 · ( log ‘ 𝐴 ) ) ) )
24 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
25 3 5 logcld ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
26 24 25 9 fsummulc1 ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 · ( log ‘ 𝐴 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑘 · ( log ‘ 𝐴 ) ) )
27 26 eqcomd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑘 · ( log ‘ 𝐴 ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 · ( log ‘ 𝐴 ) ) )
28 27 fveq2d ⊢ ( 𝜑 → ( exp ‘ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑘 · ( log ‘ 𝐴 ) ) ) = ( exp ‘ ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 · ( log ‘ 𝐴 ) ) ) )
29 24 9 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ∈ ℂ )
30 3 5 29 cxpefd ⊢ ( 𝜑 → ( 𝐴 ↑𝑐 Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) = ( exp ‘ ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 · ( log ‘ 𝐴 ) ) ) )
31 30 eqcomd ⊢ ( 𝜑 → ( exp ‘ ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 · ( log ‘ 𝐴 ) ) ) = ( 𝐴 ↑𝑐 Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) )
32 28 31 eqtrd ⊢ ( 𝜑 → ( exp ‘ Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑘 · ( log ‘ 𝐴 ) ) ) = ( 𝐴 ↑𝑐 Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) )
33 23 32 eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( exp ‘ ( 𝑘 · ( log ‘ 𝐴 ) ) ) = ( 𝐴 ↑𝑐 Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) )
34 13 33 eqtrd ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 ↑𝑐 𝑘 ) = ( 𝐴 ↑𝑐 Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝑘 ) )