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	$⊢ Ⅎ k φ$
	fprodaddrecnncnvlem.a	$⊢ φ \to A \in Fin$
	fprodaddrecnncnvlem.b	$⊢ (φ \land k \in A) \to B \in ℂ$
	fprodaddrecnncnvlem.s	$⊢ S = (n \in ℕ ⟼ \prod_{k \in A} (B + (\frac{1}{n})))$
	fprodaddrecnncnvlem.f	$⊢ F = (x \in ℂ ⟼ \prod_{k \in A} (B + x))$
	fprodaddrecnncnvlem.g	$⊢ G = (n \in ℕ ⟼ \frac{1}{n})$
Assertion	fprodaddrecnncnvlem	$⊢ φ \to S ⇝ \prod_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		fprodaddrecnncnvlem.k	$⊢ Ⅎ k φ$
2		fprodaddrecnncnvlem.a	$⊢ φ \to A \in Fin$
3		fprodaddrecnncnvlem.b	$⊢ (φ \land k \in A) \to B \in ℂ$
4		fprodaddrecnncnvlem.s	$⊢ S = (n \in ℕ ⟼ \prod_{k \in A} (B + (\frac{1}{n})))$
5		fprodaddrecnncnvlem.f	$⊢ F = (x \in ℂ ⟼ \prod_{k \in A} (B + x))$
6		fprodaddrecnncnvlem.g	$⊢ G = (n \in ℕ ⟼ \frac{1}{n})$
7		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
8		1zzd	$⊢ φ \to 1 \in ℤ$
9	1 2 3 5	fprodadd2cncf	$⊢ φ \to F : ℂ \underset{cn}{⟶} ℂ$
10		1rp	$⊢ 1 \in ℝ^{+}$
11	10	a1i	$⊢ n \in ℕ \to 1 \in ℝ^{+}$
12		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
13	11 12	rpdivcld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
14	13	rpcnd	$⊢ n \in ℕ \to \frac{1}{n} \in ℂ$
15	14	adantl	$⊢ (φ \land n \in ℕ) \to \frac{1}{n} \in ℂ$
16	15 6	fmptd	$⊢ φ \to G : ℕ ⟶ ℂ$
17		1cnd	$⊢ φ \to 1 \in ℂ$
18		divcnv	$⊢ 1 \in ℂ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
19	17 18	syl	$⊢ φ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
20	6	a1i	$⊢ φ \to G = (n \in ℕ ⟼ \frac{1}{n})$
21	20	breq1d	$⊢ φ \to (G ⇝ 0 \leftrightarrow (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0)$
22	19 21	mpbird	$⊢ φ \to G ⇝ 0$
23		0cnd	$⊢ φ \to 0 \in ℂ$
24	7 8 9 16 22 23	climcncf	$⊢ φ \to (F \circ G) ⇝ F (0)$
25		nfv	$⊢ Ⅎ k x \in ℂ$
26	1 25	nfan	$⊢ Ⅎ k (φ \land x \in ℂ)$
27	2	adantr	$⊢ (φ \land x \in ℂ) \to A \in Fin$
28	3	adantlr	$⊢ ((φ \land x \in ℂ) \land k \in A) \to B \in ℂ$
29		simplr	$⊢ ((φ \land x \in ℂ) \land k \in A) \to x \in ℂ$
30	28 29	addcld	$⊢ ((φ \land x \in ℂ) \land k \in A) \to B + x \in ℂ$
31	26 27 30	fprodclf	$⊢ (φ \land x \in ℂ) \to \prod_{k \in A} (B + x) \in ℂ$
32	31 5	fmptd	$⊢ φ \to F : ℂ ⟶ ℂ$
33		fcompt	$⊢ (F : ℂ ⟶ ℂ \land G : ℕ ⟶ ℂ) \to F \circ G = (n \in ℕ ⟼ F (G (n)))$
34	32 16 33	syl2anc	$⊢ φ \to F \circ G = (n \in ℕ ⟼ F (G (n)))$
35	4	a1i	$⊢ φ \to S = (n \in ℕ ⟼ \prod_{k \in A} (B + (\frac{1}{n})))$
36		id	$⊢ n \in ℕ \to n \in ℕ$
37	6	fvmpt2	$⊢ (n \in ℕ \land \frac{1}{n} \in ℂ) \to G (n) = \frac{1}{n}$
38	36 14 37	syl2anc	$⊢ n \in ℕ \to G (n) = \frac{1}{n}$
39	38	fveq2d	$⊢ n \in ℕ \to F (G (n)) = F (\frac{1}{n})$
40	39	adantl	$⊢ (φ \land n \in ℕ) \to F (G (n)) = F (\frac{1}{n})$
41		oveq2	$⊢ x = \frac{1}{n} \to B + x = B + (\frac{1}{n})$
42	41	prodeq2ad	$⊢ x = \frac{1}{n} \to \prod_{k \in A} (B + x) = \prod_{k \in A} (B + (\frac{1}{n}))$
43		prodex	$⊢ \prod_{k \in A} (B + (\frac{1}{n})) \in V$
44	43	a1i	$⊢ (φ \land n \in ℕ) \to \prod_{k \in A} (B + (\frac{1}{n})) \in V$
45	5 42 15 44	fvmptd3	$⊢ (φ \land n \in ℕ) \to F (\frac{1}{n}) = \prod_{k \in A} (B + (\frac{1}{n}))$
46	40 45	eqtr2d	$⊢ (φ \land n \in ℕ) \to \prod_{k \in A} (B + (\frac{1}{n})) = F (G (n))$
47	46	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ \prod_{k \in A} (B + (\frac{1}{n}))) = (n \in ℕ ⟼ F (G (n)))$
48	35 47	eqtrd	$⊢ φ \to S = (n \in ℕ ⟼ F (G (n)))$
49	34 48	eqtr4d	$⊢ φ \to F \circ G = S$
50	5	a1i	$⊢ φ \to F = (x \in ℂ ⟼ \prod_{k \in A} (B + x))$
51		nfv	$⊢ Ⅎ k x = 0$
52	1 51	nfan	$⊢ Ⅎ k (φ \land x = 0)$
53		oveq2	$⊢ x = 0 \to B + x = B + 0$
54	53	ad2antlr	$⊢ ((φ \land x = 0) \land k \in A) \to B + x = B + 0$
55	3	addid1d	$⊢ (φ \land k \in A) \to B + 0 = B$
56	55	adantlr	$⊢ ((φ \land x = 0) \land k \in A) \to B + 0 = B$
57	54 56	eqtrd	$⊢ ((φ \land x = 0) \land k \in A) \to B + x = B$
58	57	ex	$⊢ (φ \land x = 0) \to (k \in A \to B + x = B)$
59	52 58	ralrimi	$⊢ (φ \land x = 0) \to \forall k \in A B + x = B$
60	59	prodeq2d	$⊢ (φ \land x = 0) \to \prod_{k \in A} (B + x) = \prod_{k \in A} B$
61		prodex	$⊢ \prod_{k \in A} B \in V$
62	61	a1i	$⊢ φ \to \prod_{k \in A} B \in V$
63	50 60 23 62	fvmptd	$⊢ φ \to F (0) = \prod_{k \in A} B$
64	49 63	breq12d	$⊢ φ \to ((F \circ G) ⇝ F (0) \leftrightarrow S ⇝ \prod_{k \in A} B)$
65	24 64	mpbid	$⊢ φ \to S ⇝ \prod_{k \in A} B$

Metamath Proof Explorer

Theorem fprodaddrecnncnvlem

Proof