Metamath Proof Explorer

Theorem iprodefisum

Description: Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018)

Ref Expression
Hypotheses iprodefisum.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
iprodefisum.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
iprodefisum.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
iprodefisum.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
iprodefisum.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion iprodefisum ( 𝜑 → ∏ 𝑘 ∈ 𝑍 ( exp ‘ 𝐵 ) = ( exp ‘ Σ 𝑘 ∈ 𝑍 𝐵 ) )

Proof

Step Hyp Ref Expression
1 iprodefisum.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 iprodefisum.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 iprodefisum.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐵 )
4 iprodefisum.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
5 iprodefisum.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6 1 2 3 4 5 isumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐵 ∈ ℂ )
7 efne0 ⊢ ( Σ 𝑘 ∈ 𝑍 𝐵 ∈ ℂ → ( exp ‘ Σ 𝑘 ∈ 𝑍 𝐵 ) ≠ 0 )
8 6 7 syl ⊢ ( 𝜑 → ( exp ‘ Σ 𝑘 ∈ 𝑍 𝐵 ) ≠ 0 )
9 efcn ⊢ exp ∈ ( ℂ –cn→ ℂ )
10 9 a1i ⊢ ( 𝜑 → exp ∈ ( ℂ –cn→ ℂ ) )
11 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑘 ) )
12 eqid ⊢ ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) = ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) )
13 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
14 11 12 13 fvmpt ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
16 3 4 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
17 15 16 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑘 ) ∈ ℂ )
18 1 2 17 serf ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) : 𝑍 ⟶ ℂ )
19 1 eqcomi ⊢ ( ℤ≥ ‘ 𝑀 ) = 𝑍
20 14 19 eleq2s ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
22 2 21 seqfeq ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) = seq 𝑀 ( + , 𝐹 ) )
23 climdm ⊢ ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
24 5 23 sylib ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
25 22 24 eqbrtrd ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
26 climcl ⊢ ( seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) ∈ ℂ )
27 24 26 syl ⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) ∈ ℂ )
28 1 2 10 18 25 27 climcncf ⊢ ( 𝜑 → ( exp ∘ seq 𝑀 ( + , ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) ) ⇝ ( exp ‘ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) ) )
29 11 cbvmptv ⊢ ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
30 16 29 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) : 𝑍 ⟶ ℂ )
31 1 2 30 iprodefisumlem ⊢ ( 𝜑 → seq 𝑀 ( · , ( exp ∘ ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) ) = ( exp ∘ seq 𝑀 ( + , ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) ) )
32 1 2 3 4 isum ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐵 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
33 32 fveq2d ⊢ ( 𝜑 → ( exp ‘ Σ 𝑘 ∈ 𝑍 𝐵 ) = ( exp ‘ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) ) )
34 28 31 33 3brtr4d ⊢ ( 𝜑 → seq 𝑀 ( · , ( exp ∘ ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) ) ⇝ ( exp ‘ Σ 𝑘 ∈ 𝑍 𝐵 ) )
35 fvco3 ⊢ ( ( ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) : 𝑍 ⟶ ℂ ∧ 𝑘 ∈ 𝑍 ) → ( ( exp ∘ ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) ‘ 𝑘 ) = ( exp ‘ ( ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
36 30 35 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( exp ∘ ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) ‘ 𝑘 ) = ( exp ‘ ( ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑘 ) ) )
37 15 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( exp ‘ ( ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑘 ) ) = ( exp ‘ ( 𝐹 ‘ 𝑘 ) ) )
38 3 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( exp ‘ ( 𝐹 ‘ 𝑘 ) ) = ( exp ‘ 𝐵 ) )
39 36 37 38 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( exp ∘ ( 𝑗 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑗 ) ) ) ‘ 𝑘 ) = ( exp ‘ 𝐵 ) )
40 efcl ⊢ ( 𝐵 ∈ ℂ → ( exp ‘ 𝐵 ) ∈ ℂ )
41 4 40 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( exp ‘ 𝐵 ) ∈ ℂ )
42 1 2 8 34 39 41 iprodn0 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝑍 ( exp ‘ 𝐵 ) = ( exp ‘ Σ 𝑘 ∈ 𝑍 𝐵 ) )