Metamath Proof Explorer


Theorem fprodaddrecnncnvlem

Description: The sequence S of finite products, where every factor is added an "always smaller" amount, converges to the finite product of the factors. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses fprodaddrecnncnvlem.k 𝑘 𝜑
fprodaddrecnncnvlem.a ( 𝜑𝐴 ∈ Fin )
fprodaddrecnncnvlem.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
fprodaddrecnncnvlem.s 𝑆 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝐴 ( 𝐵 + ( 1 / 𝑛 ) ) )
fprodaddrecnncnvlem.f 𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘𝐴 ( 𝐵 + 𝑥 ) )
fprodaddrecnncnvlem.g 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
Assertion fprodaddrecnncnvlem ( 𝜑𝑆 ⇝ ∏ 𝑘𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 fprodaddrecnncnvlem.k 𝑘 𝜑
2 fprodaddrecnncnvlem.a ( 𝜑𝐴 ∈ Fin )
3 fprodaddrecnncnvlem.b ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℂ )
4 fprodaddrecnncnvlem.s 𝑆 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝐴 ( 𝐵 + ( 1 / 𝑛 ) ) )
5 fprodaddrecnncnvlem.f 𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘𝐴 ( 𝐵 + 𝑥 ) )
6 fprodaddrecnncnvlem.g 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
7 nnuz ℕ = ( ℤ ‘ 1 )
8 1zzd ( 𝜑 → 1 ∈ ℤ )
9 1 2 3 5 fprodadd2cncf ( 𝜑𝐹 ∈ ( ℂ –cn→ ℂ ) )
10 1rp 1 ∈ ℝ+
11 10 a1i ( 𝑛 ∈ ℕ → 1 ∈ ℝ+ )
12 nnrp ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
13 11 12 rpdivcld ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ+ )
14 13 rpcnd ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℂ )
15 14 adantl ( ( 𝜑𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℂ )
16 15 6 fmptd ( 𝜑𝐺 : ℕ ⟶ ℂ )
17 1cnd ( 𝜑 → 1 ∈ ℂ )
18 divcnv ( 1 ∈ ℂ → ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ⇝ 0 )
19 17 18 syl ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ⇝ 0 )
20 6 a1i ( 𝜑𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) )
21 20 breq1d ( 𝜑 → ( 𝐺 ⇝ 0 ↔ ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) ) ⇝ 0 ) )
22 19 21 mpbird ( 𝜑𝐺 ⇝ 0 )
23 0cnd ( 𝜑 → 0 ∈ ℂ )
24 7 8 9 16 22 23 climcncf ( 𝜑 → ( 𝐹𝐺 ) ⇝ ( 𝐹 ‘ 0 ) )
25 nfv 𝑘 𝑥 ∈ ℂ
26 1 25 nfan 𝑘 ( 𝜑𝑥 ∈ ℂ )
27 2 adantr ( ( 𝜑𝑥 ∈ ℂ ) → 𝐴 ∈ Fin )
28 3 adantlr ( ( ( 𝜑𝑥 ∈ ℂ ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ℂ )
29 simplr ( ( ( 𝜑𝑥 ∈ ℂ ) ∧ 𝑘𝐴 ) → 𝑥 ∈ ℂ )
30 28 29 addcld ( ( ( 𝜑𝑥 ∈ ℂ ) ∧ 𝑘𝐴 ) → ( 𝐵 + 𝑥 ) ∈ ℂ )
31 26 27 30 fprodclf ( ( 𝜑𝑥 ∈ ℂ ) → ∏ 𝑘𝐴 ( 𝐵 + 𝑥 ) ∈ ℂ )
32 31 5 fmptd ( 𝜑𝐹 : ℂ ⟶ ℂ )
33 fcompt ( ( 𝐹 : ℂ ⟶ ℂ ∧ 𝐺 : ℕ ⟶ ℂ ) → ( 𝐹𝐺 ) = ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ ( 𝐺𝑛 ) ) ) )
34 32 16 33 syl2anc ( 𝜑 → ( 𝐹𝐺 ) = ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ ( 𝐺𝑛 ) ) ) )
35 4 a1i ( 𝜑𝑆 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝐴 ( 𝐵 + ( 1 / 𝑛 ) ) ) )
36 id ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
37 6 fvmpt2 ( ( 𝑛 ∈ ℕ ∧ ( 1 / 𝑛 ) ∈ ℂ ) → ( 𝐺𝑛 ) = ( 1 / 𝑛 ) )
38 36 14 37 syl2anc ( 𝑛 ∈ ℕ → ( 𝐺𝑛 ) = ( 1 / 𝑛 ) )
39 38 fveq2d ( 𝑛 ∈ ℕ → ( 𝐹 ‘ ( 𝐺𝑛 ) ) = ( 𝐹 ‘ ( 1 / 𝑛 ) ) )
40 39 adantl ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺𝑛 ) ) = ( 𝐹 ‘ ( 1 / 𝑛 ) ) )
41 oveq2 ( 𝑥 = ( 1 / 𝑛 ) → ( 𝐵 + 𝑥 ) = ( 𝐵 + ( 1 / 𝑛 ) ) )
42 41 prodeq2ad ( 𝑥 = ( 1 / 𝑛 ) → ∏ 𝑘𝐴 ( 𝐵 + 𝑥 ) = ∏ 𝑘𝐴 ( 𝐵 + ( 1 / 𝑛 ) ) )
43 prodex 𝑘𝐴 ( 𝐵 + ( 1 / 𝑛 ) ) ∈ V
44 43 a1i ( ( 𝜑𝑛 ∈ ℕ ) → ∏ 𝑘𝐴 ( 𝐵 + ( 1 / 𝑛 ) ) ∈ V )
45 5 42 15 44 fvmptd3 ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝐹 ‘ ( 1 / 𝑛 ) ) = ∏ 𝑘𝐴 ( 𝐵 + ( 1 / 𝑛 ) ) )
46 40 45 eqtr2d ( ( 𝜑𝑛 ∈ ℕ ) → ∏ 𝑘𝐴 ( 𝐵 + ( 1 / 𝑛 ) ) = ( 𝐹 ‘ ( 𝐺𝑛 ) ) )
47 46 mpteq2dva ( 𝜑 → ( 𝑛 ∈ ℕ ↦ ∏ 𝑘𝐴 ( 𝐵 + ( 1 / 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ ( 𝐺𝑛 ) ) ) )
48 35 47 eqtrd ( 𝜑𝑆 = ( 𝑛 ∈ ℕ ↦ ( 𝐹 ‘ ( 𝐺𝑛 ) ) ) )
49 34 48 eqtr4d ( 𝜑 → ( 𝐹𝐺 ) = 𝑆 )
50 5 a1i ( 𝜑𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘𝐴 ( 𝐵 + 𝑥 ) ) )
51 nfv 𝑘 𝑥 = 0
52 1 51 nfan 𝑘 ( 𝜑𝑥 = 0 )
53 oveq2 ( 𝑥 = 0 → ( 𝐵 + 𝑥 ) = ( 𝐵 + 0 ) )
54 53 ad2antlr ( ( ( 𝜑𝑥 = 0 ) ∧ 𝑘𝐴 ) → ( 𝐵 + 𝑥 ) = ( 𝐵 + 0 ) )
55 3 addid1d ( ( 𝜑𝑘𝐴 ) → ( 𝐵 + 0 ) = 𝐵 )
56 55 adantlr ( ( ( 𝜑𝑥 = 0 ) ∧ 𝑘𝐴 ) → ( 𝐵 + 0 ) = 𝐵 )
57 54 56 eqtrd ( ( ( 𝜑𝑥 = 0 ) ∧ 𝑘𝐴 ) → ( 𝐵 + 𝑥 ) = 𝐵 )
58 57 ex ( ( 𝜑𝑥 = 0 ) → ( 𝑘𝐴 → ( 𝐵 + 𝑥 ) = 𝐵 ) )
59 52 58 ralrimi ( ( 𝜑𝑥 = 0 ) → ∀ 𝑘𝐴 ( 𝐵 + 𝑥 ) = 𝐵 )
60 59 prodeq2d ( ( 𝜑𝑥 = 0 ) → ∏ 𝑘𝐴 ( 𝐵 + 𝑥 ) = ∏ 𝑘𝐴 𝐵 )
61 prodex 𝑘𝐴 𝐵 ∈ V
62 61 a1i ( 𝜑 → ∏ 𝑘𝐴 𝐵 ∈ V )
63 50 60 23 62 fvmptd ( 𝜑 → ( 𝐹 ‘ 0 ) = ∏ 𝑘𝐴 𝐵 )
64 49 63 breq12d ( 𝜑 → ( ( 𝐹𝐺 ) ⇝ ( 𝐹 ‘ 0 ) ↔ 𝑆 ⇝ ∏ 𝑘𝐴 𝐵 ) )
65 24 64 mpbid ( 𝜑𝑆 ⇝ ∏ 𝑘𝐴 𝐵 )