Metamath Proof Explorer

Theorem fprodsubrecnncnvlem

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

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

Proof

Step Hyp Ref Expression
1 fprodsubrecnncnvlem.k ⊢ Ⅎ 𝑘 𝜑
2 fprodsubrecnncnvlem.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 fprodsubrecnncnvlem.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4 fprodsubrecnncnvlem.s ⊢ 𝑆 = ( 𝑛 ∈ ℕ ↦ ∏ 𝑘 ∈ 𝐴 ( 𝐵 − ( 1 / 𝑛 ) ) )
5 fprodsubrecnncnvlem.f ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ∏ 𝑘 ∈ 𝐴 ( 𝐵 − 𝑥 ) )
6 fprodsubrecnncnvlem.g ⊢ 𝐺 = ( 𝑛 ∈ ℕ ↦ ( 1 / 𝑛 ) )
7 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
8 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
9 1 2 3 5 fprodsub2cncf ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –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 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 − 𝑥 ) ∈ ℂ )
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 subid1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 − 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 ⊢ ( 𝜑 → 𝑆 ⇝ ∏ 𝑘 ∈ 𝐴 𝐵 )