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	⊢ ( 𝜑 → 𝑆 ⇝ ∏ 𝑘 ∈ 𝐴 𝐵 )