faclimlem1

Description: Lemma for faclim . Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017)

		Ref	Expression
	Assertion	faclimlem1	$⊢ M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) = (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1}))$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ a = 1 \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (1)$
2		1z	$⊢ 1 \in ℤ$
3		seq1	$⊢ 1 \in ℤ \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (1) = (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (1)$
4	2 3	ax-mp	$⊢ seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (1) = (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (1)$
5	1 4	eqtrdi	$⊢ a = 1 \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (1)$
6		oveq1	$⊢ a = 1 \to a + 1 = 1 + 1$
7		oveq1	$⊢ a = 1 \to a + M + 1 = 1 + M + 1$
8	6 7	oveq12d	$⊢ a = 1 \to \frac{a + 1}{a + M + 1} = \frac{1 + 1}{1 + M + 1}$
9	8	oveq2d	$⊢ a = 1 \to (M + 1) (\frac{a + 1}{a + M + 1}) = (M + 1) (\frac{1 + 1}{1 + M + 1})$
10	5 9	eqeq12d	$⊢ a = 1 \to (seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = (M + 1) (\frac{a + 1}{a + M + 1}) \leftrightarrow (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (1) = (M + 1) (\frac{1 + 1}{1 + M + 1}))$
11	10	imbi2d	$⊢ a = 1 \to ((M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = (M + 1) (\frac{a + 1}{a + M + 1})) \leftrightarrow (M \in ℕ_{0} \to (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (1) = (M + 1) (\frac{1 + 1}{1 + M + 1})))$
12		fveq2	$⊢ a = k \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k)$
13		oveq1	$⊢ a = k \to a + 1 = k + 1$
14		oveq1	$⊢ a = k \to a + M + 1 = k + M + 1$
15	13 14	oveq12d	$⊢ a = k \to \frac{a + 1}{a + M + 1} = \frac{k + 1}{k + M + 1}$
16	15	oveq2d	$⊢ a = k \to (M + 1) (\frac{a + 1}{a + M + 1}) = (M + 1) (\frac{k + 1}{k + M + 1})$
17	12 16	eqeq12d	$⊢ a = k \to (seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = (M + 1) (\frac{a + 1}{a + M + 1}) \leftrightarrow seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) = (M + 1) (\frac{k + 1}{k + M + 1}))$
18	17	imbi2d	$⊢ a = k \to ((M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = (M + 1) (\frac{a + 1}{a + M + 1})) \leftrightarrow (M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) = (M + 1) (\frac{k + 1}{k + M + 1})))$
19		fveq2	$⊢ a = k + 1 \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1)$
20		oveq1	$⊢ a = k + 1 \to a + 1 = k + 1 + 1$
21		oveq1	$⊢ a = k + 1 \to a + M + 1 = k + 1 + M + 1$
22	20 21	oveq12d	$⊢ a = k + 1 \to \frac{a + 1}{a + M + 1} = \frac{k + 1 + 1}{k + 1 + M + 1}$
23	22	oveq2d	$⊢ a = k + 1 \to (M + 1) (\frac{a + 1}{a + M + 1}) = (M + 1) (\frac{k + 1 + 1}{k + 1 + M + 1})$
24	19 23	eqeq12d	$⊢ a = k + 1 \to (seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = (M + 1) (\frac{a + 1}{a + M + 1}) \leftrightarrow seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1) = (M + 1) (\frac{k + 1 + 1}{k + 1 + M + 1}))$
25	24	imbi2d	$⊢ a = k + 1 \to ((M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = (M + 1) (\frac{a + 1}{a + M + 1})) \leftrightarrow (M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1) = (M + 1) (\frac{k + 1 + 1}{k + 1 + M + 1})))$
26		fveq2	$⊢ a = b \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (b)$
27		oveq1	$⊢ a = b \to a + 1 = b + 1$
28		oveq1	$⊢ a = b \to a + M + 1 = b + M + 1$
29	27 28	oveq12d	$⊢ a = b \to \frac{a + 1}{a + M + 1} = \frac{b + 1}{b + M + 1}$
30	29	oveq2d	$⊢ a = b \to (M + 1) (\frac{a + 1}{a + M + 1}) = (M + 1) (\frac{b + 1}{b + M + 1})$
31	26 30	eqeq12d	$⊢ a = b \to (seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = (M + 1) (\frac{a + 1}{a + M + 1}) \leftrightarrow seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (b) = (M + 1) (\frac{b + 1}{b + M + 1}))$
32	31	imbi2d	$⊢ a = b \to ((M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (a) = (M + 1) (\frac{a + 1}{a + M + 1})) \leftrightarrow (M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (b) = (M + 1) (\frac{b + 1}{b + M + 1})))$
33		1nn	$⊢ 1 \in ℕ$
34		oveq2	$⊢ n = 1 \to \frac{M}{n} = \frac{M}{1}$
35	34	oveq2d	$⊢ n = 1 \to 1 + (\frac{M}{n}) = 1 + (\frac{M}{1})$
36		oveq2	$⊢ n = 1 \to \frac{1}{n} = \frac{1}{1}$
37	36	oveq2d	$⊢ n = 1 \to 1 + (\frac{1}{n}) = 1 + (\frac{1}{1})$
38	35 37	oveq12d	$⊢ n = 1 \to (1 + (\frac{M}{n})) (1 + (\frac{1}{n})) = (1 + (\frac{M}{1})) (1 + (\frac{1}{1}))$
39		oveq2	$⊢ n = 1 \to \frac{M + 1}{n} = \frac{M + 1}{1}$
40	39	oveq2d	$⊢ n = 1 \to 1 + (\frac{M + 1}{n}) = 1 + (\frac{M + 1}{1})$
41	38 40	oveq12d	$⊢ n = 1 \to \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})} = \frac{(1 + (\frac{M}{1})) (1 + (\frac{1}{1}))}{1 + (\frac{M + 1}{1})}$
42		eqid	$⊢ (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) = (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})$
43		ovex	$⊢ \frac{(1 + (\frac{M}{1})) (1 + (\frac{1}{1}))}{1 + (\frac{M + 1}{1})} \in V$
44	41 42 43	fvmpt	$⊢ 1 \in ℕ \to (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (1) = \frac{(1 + (\frac{M}{1})) (1 + (\frac{1}{1}))}{1 + (\frac{M + 1}{1})}$
45	33 44	ax-mp	$⊢ (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (1) = \frac{(1 + (\frac{M}{1})) (1 + (\frac{1}{1}))}{1 + (\frac{M + 1}{1})}$
46		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
47	46	div1d	$⊢ M \in ℕ_{0} \to \frac{M}{1} = M$
48	47	oveq2d	$⊢ M \in ℕ_{0} \to 1 + (\frac{M}{1}) = 1 + M$
49		1div1e1	$⊢ \frac{1}{1} = 1$
50	49	oveq2i	$⊢ 1 + (\frac{1}{1}) = 1 + 1$
51	50	a1i	$⊢ M \in ℕ_{0} \to 1 + (\frac{1}{1}) = 1 + 1$
52	48 51	oveq12d	$⊢ M \in ℕ_{0} \to (1 + (\frac{M}{1})) (1 + (\frac{1}{1})) = (1 + M) (1 + 1)$
53		nn0p1nn	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ$
54	53	nncnd	$⊢ M \in ℕ_{0} \to M + 1 \in ℂ$
55	54	div1d	$⊢ M \in ℕ_{0} \to \frac{M + 1}{1} = M + 1$
56	55	oveq2d	$⊢ M \in ℕ_{0} \to 1 + (\frac{M + 1}{1}) = 1 + M + 1$
57	52 56	oveq12d	$⊢ M \in ℕ_{0} \to \frac{(1 + (\frac{M}{1})) (1 + (\frac{1}{1}))}{1 + (\frac{M + 1}{1})} = \frac{(1 + M) (1 + 1)}{1 + M + 1}$
58		1cnd	$⊢ M \in ℕ_{0} \to 1 \in ℂ$
59	58 46	addcomd	$⊢ M \in ℕ_{0} \to 1 + M = M + 1$
60	59	oveq1d	$⊢ M \in ℕ_{0} \to (1 + M) (1 + 1) = (M + 1) (1 + 1)$
61	60	oveq1d	$⊢ M \in ℕ_{0} \to \frac{(1 + M) (1 + 1)}{1 + M + 1} = \frac{(M + 1) (1 + 1)}{1 + M + 1}$
62		ax-1cn	$⊢ 1 \in ℂ$
63	62 62	addcli	$⊢ 1 + 1 \in ℂ$
64	63	a1i	$⊢ M \in ℕ_{0} \to 1 + 1 \in ℂ$
65	33	a1i	$⊢ M \in ℕ_{0} \to 1 \in ℕ$
66	65 53	nnaddcld	$⊢ M \in ℕ_{0} \to 1 + M + 1 \in ℕ$
67	66	nncnd	$⊢ M \in ℕ_{0} \to 1 + M + 1 \in ℂ$
68	66	nnne0d	$⊢ M \in ℕ_{0} \to 1 + M + 1 \neq 0$
69	54 64 67 68	divassd	$⊢ M \in ℕ_{0} \to \frac{(M + 1) (1 + 1)}{1 + M + 1} = (M + 1) (\frac{1 + 1}{1 + M + 1})$
70	57 61 69	3eqtrd	$⊢ M \in ℕ_{0} \to \frac{(1 + (\frac{M}{1})) (1 + (\frac{1}{1}))}{1 + (\frac{M + 1}{1})} = (M + 1) (\frac{1 + 1}{1 + M + 1})$
71	45 70	syl5eq	$⊢ M \in ℕ_{0} \to (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (1) = (M + 1) (\frac{1 + 1}{1 + M + 1})$
72		seqp1	$⊢ k \in ℤ_{\geq 1} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1) = seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1)$
73		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
74	72 73	eleq2s	$⊢ k \in ℕ \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1) = seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1)$
75	74	adantr	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1) = seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1)$
76	75	adantr	$⊢ ((k \in ℕ \land M \in ℕ_{0}) \land seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) = (M + 1) (\frac{k + 1}{k + M + 1})) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1) = seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1)$
77		oveq1	$⊢ seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) = (M + 1) (\frac{k + 1}{k + M + 1}) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1) = (M + 1) (\frac{k + 1}{k + M + 1}) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1)$
78	77	adantl	$⊢ ((k \in ℕ \land M \in ℕ_{0}) \land seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) = (M + 1) (\frac{k + 1}{k + M + 1})) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1) = (M + 1) (\frac{k + 1}{k + M + 1}) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1)$
79		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
80		oveq2	$⊢ n = k + 1 \to \frac{M}{n} = \frac{M}{k + 1}$
81	80	oveq2d	$⊢ n = k + 1 \to 1 + (\frac{M}{n}) = 1 + (\frac{M}{k + 1})$
82		oveq2	$⊢ n = k + 1 \to \frac{1}{n} = \frac{1}{k + 1}$
83	82	oveq2d	$⊢ n = k + 1 \to 1 + (\frac{1}{n}) = 1 + (\frac{1}{k + 1})$
84	81 83	oveq12d	$⊢ n = k + 1 \to (1 + (\frac{M}{n})) (1 + (\frac{1}{n})) = (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))$
85		oveq2	$⊢ n = k + 1 \to \frac{M + 1}{n} = \frac{M + 1}{k + 1}$
86	85	oveq2d	$⊢ n = k + 1 \to 1 + (\frac{M + 1}{n}) = 1 + (\frac{M + 1}{k + 1})$
87	84 86	oveq12d	$⊢ n = k + 1 \to \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})} = \frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})}$
88		ovex	$⊢ \frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})} \in V$
89	87 42 88	fvmpt	$⊢ k + 1 \in ℕ \to (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1) = \frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})}$
90	79 89	syl	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1) = \frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})}$
91	90	oveq2d	$⊢ k \in ℕ \to (M + 1) (\frac{k + 1}{k + M + 1}) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1) = (M + 1) (\frac{k + 1}{k + M + 1}) (\frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})})$
92	91	adantr	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (M + 1) (\frac{k + 1}{k + M + 1}) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1) = (M + 1) (\frac{k + 1}{k + M + 1}) (\frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})})$
93	53	adantl	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to M + 1 \in ℕ$
94	93	nncnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to M + 1 \in ℂ$
95	79	adantr	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + 1 \in ℕ$
96	95	nnrpd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + 1 \in ℝ^{+}$
97		simpl	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k \in ℕ$
98	97	nnrpd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k \in ℝ^{+}$
99	93	nnrpd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to M + 1 \in ℝ^{+}$
100	98 99	rpaddcld	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + M + 1 \in ℝ^{+}$
101	96 100	rpdivcld	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{k + 1}{k + M + 1} \in ℝ^{+}$
102	101	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{k + 1}{k + M + 1} \in ℂ$
103		1cnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 \in ℂ$
104		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
105	104	adantl	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to M \in ℝ$
106	105 95	nndivred	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{M}{k + 1} \in ℝ$
107	106	recnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{M}{k + 1} \in ℂ$
108	103 107	addcomd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 + (\frac{M}{k + 1}) = (\frac{M}{k + 1}) + 1$
109		nn0ge0	$⊢ M \in ℕ_{0} \to 0 \leq M$
110	109	adantl	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 0 \leq M$
111	105 96 110	divge0d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 0 \leq \frac{M}{k + 1}$
112	106 111	ge0p1rpd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{M}{k + 1}) + 1 \in ℝ^{+}$
113	108 112	eqeltrd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 + (\frac{M}{k + 1}) \in ℝ^{+}$
114		1rp	$⊢ 1 \in ℝ^{+}$
115	114	a1i	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 \in ℝ^{+}$
116	96	rpreccld	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{1}{k + 1} \in ℝ^{+}$
117	115 116	rpaddcld	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 + (\frac{1}{k + 1}) \in ℝ^{+}$
118	113 117	rpmulcld	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) \in ℝ^{+}$
119	99 96	rpdivcld	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{M + 1}{k + 1} \in ℝ^{+}$
120	115 119	rpaddcld	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 + (\frac{M + 1}{k + 1}) \in ℝ^{+}$
121	118 120	rpdivcld	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})} \in ℝ^{+}$
122	121	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})} \in ℂ$
123	94 102 122	mulassd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (M + 1) (\frac{k + 1}{k + M + 1}) (\frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})}) = (M + 1) (\frac{k + 1}{k + M + 1}) (\frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})})$
124	101 118	rpmulcld	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{k + 1}{k + M + 1}) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) \in ℝ^{+}$
125	124	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{k + 1}{k + M + 1}) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) \in ℂ$
126	120	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 + (\frac{M + 1}{k + 1}) \in ℂ$
127	95	nncnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + 1 \in ℂ$
128	120	rpne0d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 + (\frac{M + 1}{k + 1}) \neq 0$
129	95	nnne0d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + 1 \neq 0$
130	125 126 127 128 129	divcan5d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{(k + 1) (\frac{k + 1}{k + M + 1}) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{(k + 1) (1 + (\frac{M + 1}{k + 1}))} = \frac{(\frac{k + 1}{k + M + 1}) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})}$
131	118	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) \in ℂ$
132	127 102 131	mul12d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (\frac{k + 1}{k + M + 1}) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) = (\frac{k + 1}{k + M + 1}) (k + 1) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))$
133	113	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 + (\frac{M}{k + 1}) \in ℂ$
134	117	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 + (\frac{1}{k + 1}) \in ℂ$
135	127 133 134	mulassd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) = (k + 1) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))$
136	127 103 107	adddid	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (1 + (\frac{M}{k + 1})) = (k + 1) \cdot 1 + (k + 1) (\frac{M}{k + 1})$
137	127	mulid1d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) \cdot 1 = k + 1$
138		simpr	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to M \in ℕ_{0}$
139	138	nn0cnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to M \in ℂ$
140	139 127 129	divcan2d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (\frac{M}{k + 1}) = M$
141	137 140	oveq12d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) \cdot 1 + (k + 1) (\frac{M}{k + 1}) = k + 1 + M$
142	97	nncnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k \in ℂ$
143	142 103 139	addassd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + 1 + M = k + 1 + M$
144	103 139	addcomd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to 1 + M = M + 1$
145	144	oveq2d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + 1 + M = k + M + 1$
146	143 145	eqtrd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + 1 + M = k + M + 1$
147	136 141 146	3eqtrd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (1 + (\frac{M}{k + 1})) = k + M + 1$
148	147	oveq1d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) = (k + M + 1) (1 + (\frac{1}{k + 1}))$
149	135 148	eqtr3d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) = (k + M + 1) (1 + (\frac{1}{k + 1}))$
150	149	oveq2d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{k + 1}{k + M + 1}) (k + 1) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) = (\frac{k + 1}{k + M + 1}) (k + M + 1) (1 + (\frac{1}{k + 1}))$
151	100	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + M + 1 \in ℂ$
152	102 151 134	mulassd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{k + 1}{k + M + 1}) (k + M + 1) (1 + (\frac{1}{k + 1})) = (\frac{k + 1}{k + M + 1}) (k + M + 1) (1 + (\frac{1}{k + 1}))$
153	100	rpne0d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to k + M + 1 \neq 0$
154	127 151 153	divcan1d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{k + 1}{k + M + 1}) (k + M + 1) = k + 1$
155	154	oveq1d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{k + 1}{k + M + 1}) (k + M + 1) (1 + (\frac{1}{k + 1})) = (k + 1) (1 + (\frac{1}{k + 1}))$
156	116	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{1}{k + 1} \in ℂ$
157	127 103 156	adddid	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (1 + (\frac{1}{k + 1})) = (k + 1) \cdot 1 + (k + 1) (\frac{1}{k + 1})$
158	103 127 129	divcan2d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (\frac{1}{k + 1}) = 1$
159	137 158	oveq12d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) \cdot 1 + (k + 1) (\frac{1}{k + 1}) = k + 1 + 1$
160	155 157 159	3eqtrd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{k + 1}{k + M + 1}) (k + M + 1) (1 + (\frac{1}{k + 1})) = k + 1 + 1$
161	152 160	eqtr3d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{k + 1}{k + M + 1}) (k + M + 1) (1 + (\frac{1}{k + 1})) = k + 1 + 1$
162	132 150 161	3eqtrd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (\frac{k + 1}{k + M + 1}) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1})) = k + 1 + 1$
163	119	rpcnd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{M + 1}{k + 1} \in ℂ$
164	127 103 163	adddid	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (1 + (\frac{M + 1}{k + 1})) = (k + 1) \cdot 1 + (k + 1) (\frac{M + 1}{k + 1})$
165	94 127 129	divcan2d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (\frac{M + 1}{k + 1}) = M + 1$
166	137 165	oveq12d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) \cdot 1 + (k + 1) (\frac{M + 1}{k + 1}) = k + 1 + M + 1$
167	164 166	eqtrd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (k + 1) (1 + (\frac{M + 1}{k + 1})) = k + 1 + M + 1$
168	162 167	oveq12d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{(k + 1) (\frac{k + 1}{k + M + 1}) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{(k + 1) (1 + (\frac{M + 1}{k + 1}))} = \frac{k + 1 + 1}{k + 1 + M + 1}$
169	102 131 126 128	divassd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to \frac{(\frac{k + 1}{k + M + 1}) (1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})} = (\frac{k + 1}{k + M + 1}) (\frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})})$
170	130 168 169	3eqtr3rd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (\frac{k + 1}{k + M + 1}) (\frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})}) = \frac{k + 1 + 1}{k + 1 + M + 1}$
171	170	oveq2d	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (M + 1) (\frac{k + 1}{k + M + 1}) (\frac{(1 + (\frac{M}{k + 1})) (1 + (\frac{1}{k + 1}))}{1 + (\frac{M + 1}{k + 1})}) = (M + 1) (\frac{k + 1 + 1}{k + 1 + M + 1})$
172	92 123 171	3eqtrd	$⊢ (k \in ℕ \land M \in ℕ_{0}) \to (M + 1) (\frac{k + 1}{k + M + 1}) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1) = (M + 1) (\frac{k + 1 + 1}{k + 1 + M + 1})$
173	172	adantr	$⊢ ((k \in ℕ \land M \in ℕ_{0}) \land seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) = (M + 1) (\frac{k + 1}{k + M + 1})) \to (M + 1) (\frac{k + 1}{k + M + 1}) (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})}) (k + 1) = (M + 1) (\frac{k + 1 + 1}{k + 1 + M + 1})$
174	76 78 173	3eqtrd	$⊢ ((k \in ℕ \land M \in ℕ_{0}) \land seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) = (M + 1) (\frac{k + 1}{k + M + 1})) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1) = (M + 1) (\frac{k + 1 + 1}{k + 1 + M + 1})$
175	174	exp31	$⊢ k \in ℕ \to (M \in ℕ_{0} \to (seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) = (M + 1) (\frac{k + 1}{k + M + 1}) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1) = (M + 1) (\frac{k + 1 + 1}{k + 1 + M + 1})))$
176	175	a2d	$⊢ k \in ℕ \to ((M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k) = (M + 1) (\frac{k + 1}{k + M + 1})) \to (M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (k + 1) = (M + 1) (\frac{k + 1 + 1}{k + 1 + M + 1})))$
177	11 18 25 32 71 176	nnind	$⊢ b \in ℕ \to (M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (b) = (M + 1) (\frac{b + 1}{b + M + 1}))$
178	177	impcom	$⊢ (M \in ℕ_{0} \land b \in ℕ) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (b) = (M + 1) (\frac{b + 1}{b + M + 1})$
179		oveq1	$⊢ x = b \to x + 1 = b + 1$
180		oveq1	$⊢ x = b \to x + M + 1 = b + M + 1$
181	179 180	oveq12d	$⊢ x = b \to \frac{x + 1}{x + M + 1} = \frac{b + 1}{b + M + 1}$
182	181	oveq2d	$⊢ x = b \to (M + 1) (\frac{x + 1}{x + M + 1}) = (M + 1) (\frac{b + 1}{b + M + 1})$
183		eqid	$⊢ (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) = (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1}))$
184		ovex	$⊢ (M + 1) (\frac{b + 1}{b + M + 1}) \in V$
185	182 183 184	fvmpt	$⊢ b \in ℕ \to (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) (b) = (M + 1) (\frac{b + 1}{b + M + 1})$
186	185	adantl	$⊢ (M \in ℕ_{0} \land b \in ℕ) \to (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) (b) = (M + 1) (\frac{b + 1}{b + M + 1})$
187	178 186	eqtr4d	$⊢ (M \in ℕ_{0} \land b \in ℕ) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (b) = (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) (b)$
188	187	ralrimiva	$⊢ M \in ℕ_{0} \to \forall b \in ℕ seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (b) = (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) (b)$
189		seqfn	$⊢ 1 \in ℤ \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) Fn ℤ_{\geq 1}$
190	2 189	ax-mp	$⊢ seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) Fn ℤ_{\geq 1}$
191	73	fneq2i	$⊢ seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) Fn ℕ \leftrightarrow seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) Fn ℤ_{\geq 1}$
192	190 191	mpbir	$⊢ seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) Fn ℕ$
193		ovex	$⊢ (M + 1) (\frac{x + 1}{x + M + 1}) \in V$
194	193 183	fnmpti	$⊢ (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) Fn ℕ$
195		eqfnfv	$⊢ (seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) Fn ℕ \land (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) Fn ℕ) \to (seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) = (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) \leftrightarrow \forall b \in ℕ seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (b) = (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) (b))$
196	192 194 195	mp2an	$⊢ seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) = (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) \leftrightarrow \forall b \in ℕ seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) (b) = (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1})) (b)$
197	188 196	sylibr	$⊢ M \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{M}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{M + 1}{n})})) = (x \in ℕ ⟼ (M + 1) (\frac{x + 1}{x + M + 1}))$

Metamath Proof Explorer

Theorem faclimlem1

Proof