faclim

Description: An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017)

		Ref	Expression
	Hypothesis	faclim.1	$⊢ F = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})})$
	Assertion	faclim	$⊢ A \in ℕ_{0} \to seq 1 (\times F) ⇝ A!$

Proof

Step	Hyp	Ref	Expression
1		faclim.1	$⊢ F = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})})$
2		seqeq3	$⊢ F = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})}) \to seq 1 (\times F) = seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})}))$
3	1 2	ax-mp	$⊢ seq 1 (\times F) = seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})}))$
4		oveq2	$⊢ a = 0 \to {(1 + (\frac{1}{n}))}^{a} = {(1 + (\frac{1}{n}))}^{0}$
5		oveq1	$⊢ a = 0 \to \frac{a}{n} = \frac{0}{n}$
6	5	oveq2d	$⊢ a = 0 \to 1 + (\frac{a}{n}) = 1 + (\frac{0}{n})$
7	4 6	oveq12d	$⊢ a = 0 \to \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})} = \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})}$
8	7	mpteq2dv	$⊢ a = 0 \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})}) = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})})$
9	8	seqeq3d	$⊢ a = 0 \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})})) = seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})}))$
10		fveq2	$⊢ a = 0 \to a! = 0!$
11		fac0	$⊢ 0! = 1$
12	10 11	eqtrdi	$⊢ a = 0 \to a! = 1$
13	9 12	breq12d	$⊢ a = 0 \to (seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})})) ⇝ a! \leftrightarrow seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})})) ⇝ 1)$
14		oveq2	$⊢ a = m \to {(1 + (\frac{1}{n}))}^{a} = {(1 + (\frac{1}{n}))}^{m}$
15		oveq1	$⊢ a = m \to \frac{a}{n} = \frac{m}{n}$
16	15	oveq2d	$⊢ a = m \to 1 + (\frac{a}{n}) = 1 + (\frac{m}{n})$
17	14 16	oveq12d	$⊢ a = m \to \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})} = \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}$
18	17	mpteq2dv	$⊢ a = m \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})}) = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})$
19	18	seqeq3d	$⊢ a = m \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})})) = seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}))$
20		fveq2	$⊢ a = m \to a! = m!$
21	19 20	breq12d	$⊢ a = m \to (seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})})) ⇝ a! \leftrightarrow seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!)$
22		oveq2	$⊢ a = m + 1 \to {(1 + (\frac{1}{n}))}^{a} = {(1 + (\frac{1}{n}))}^{m + 1}$
23		oveq1	$⊢ a = m + 1 \to \frac{a}{n} = \frac{m + 1}{n}$
24	23	oveq2d	$⊢ a = m + 1 \to 1 + (\frac{a}{n}) = 1 + (\frac{m + 1}{n})$
25	22 24	oveq12d	$⊢ a = m + 1 \to \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})} = \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})}$
26	25	mpteq2dv	$⊢ a = m + 1 \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})}) = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})$
27	26	seqeq3d	$⊢ a = m + 1 \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})})) = seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})}))$
28		fveq2	$⊢ a = m + 1 \to a! = (m + 1)!$
29	27 28	breq12d	$⊢ a = m + 1 \to (seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})})) ⇝ a! \leftrightarrow seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})) ⇝ (m + 1)!)$
30		oveq2	$⊢ a = A \to {(1 + (\frac{1}{n}))}^{a} = {(1 + (\frac{1}{n}))}^{A}$
31		oveq1	$⊢ a = A \to \frac{a}{n} = \frac{A}{n}$
32	31	oveq2d	$⊢ a = A \to 1 + (\frac{a}{n}) = 1 + (\frac{A}{n})$
33	30 32	oveq12d	$⊢ a = A \to \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})} = \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})}$
34	33	mpteq2dv	$⊢ a = A \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})}) = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})})$
35	34	seqeq3d	$⊢ a = A \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})})) = seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})}))$
36		fveq2	$⊢ a = A \to a! = A!$
37	35 36	breq12d	$⊢ a = A \to (seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{a}}{1 + (\frac{a}{n})})) ⇝ a! \leftrightarrow seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})})) ⇝ A!)$
38		1red	$⊢ n \in ℕ \to 1 \in ℝ$
39		nnrecre	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ$
40	38 39	readdcld	$⊢ n \in ℕ \to 1 + (\frac{1}{n}) \in ℝ$
41	40	recnd	$⊢ n \in ℕ \to 1 + (\frac{1}{n}) \in ℂ$
42	41	exp0d	$⊢ n \in ℕ \to {(1 + (\frac{1}{n}))}^{0} = 1$
43		nncn	$⊢ n \in ℕ \to n \in ℂ$
44		nnne0	$⊢ n \in ℕ \to n \neq 0$
45	43 44	div0d	$⊢ n \in ℕ \to \frac{0}{n} = 0$
46	45	oveq2d	$⊢ n \in ℕ \to 1 + (\frac{0}{n}) = 1 + 0$
47		1p0e1	$⊢ 1 + 0 = 1$
48	46 47	eqtrdi	$⊢ n \in ℕ \to 1 + (\frac{0}{n}) = 1$
49	42 48	oveq12d	$⊢ n \in ℕ \to \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})} = \frac{1}{1}$
50		1div1e1	$⊢ \frac{1}{1} = 1$
51	49 50	eqtrdi	$⊢ n \in ℕ \to \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})} = 1$
52	51	mpteq2ia	$⊢ (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})}) = (n \in ℕ ⟼ 1)$
53		fconstmpt	$⊢ ℕ \times \{1\} = (n \in ℕ ⟼ 1)$
54	52 53	eqtr4i	$⊢ (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})}) = ℕ \times \{1\}$
55		seqeq3	$⊢ (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})}) = ℕ \times \{1\} \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})})) = seq 1 (\times (ℕ \times \{1\}))$
56	54 55	ax-mp	$⊢ seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})})) = seq 1 (\times (ℕ \times \{1\}))$
57		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
58		1zzd	$⊢ ⊤ \to 1 \in ℤ$
59	57 58	climprod1	$⊢ ⊤ \to seq 1 (\times (ℕ \times \{1\})) ⇝ 1$
60	59	mptru	$⊢ seq 1 (\times (ℕ \times \{1\})) ⇝ 1$
61	56 60	eqbrtri	$⊢ seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{0}}{1 + (\frac{0}{n})})) ⇝ 1$
62		1zzd	$⊢ (m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \to 1 \in ℤ$
63		simpr	$⊢ (m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!$
64		seqex	$⊢ seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})) \in V$
65	64	a1i	$⊢ (m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})) \in V$
66		faclimlem2	$⊢ m \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})})) ⇝ (m + 1)$
67	66	adantr	$⊢ (m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})})) ⇝ (m + 1)$
68		elnnuz	$⊢ a \in ℕ \leftrightarrow a \in ℤ_{\geq 1}$
69	68	biimpi	$⊢ a \in ℕ \to a \in ℤ_{\geq 1}$
70	69	adantl	$⊢ (m \in ℕ_{0} \land a \in ℕ) \to a \in ℤ_{\geq 1}$
71		1rp	$⊢ 1 \in ℝ^{+}$
72	71	a1i	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 \in ℝ^{+}$
73		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
74	73	rpreccld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
75	74	adantl	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
76	72 75	rpaddcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 + (\frac{1}{n}) \in ℝ^{+}$
77		nn0z	$⊢ m \in ℕ_{0} \to m \in ℤ$
78	77	adantr	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to m \in ℤ$
79	76 78	rpexpcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to {(1 + (\frac{1}{n}))}^{m} \in ℝ^{+}$
80		1cnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 \in ℂ$
81		nn0nndivcl	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{m}{n} \in ℝ$
82	81	recnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{m}{n} \in ℂ$
83	80 82	addcomd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 + (\frac{m}{n}) = (\frac{m}{n}) + 1$
84		nn0ge0div	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 0 \leq \frac{m}{n}$
85	81 84	ge0p1rpd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to (\frac{m}{n}) + 1 \in ℝ^{+}$
86	83 85	eqeltrd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 + (\frac{m}{n}) \in ℝ^{+}$
87	79 86	rpdivcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})} \in ℝ^{+}$
88	87	rpcnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})} \in ℂ$
89	88	fmpttd	$⊢ m \in ℕ_{0} \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) : ℕ ⟶ ℂ$
90		elfznn	$⊢ b \in (1 \dots a) \to b \in ℕ$
91		ffvelrn	$⊢ ((n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) : ℕ ⟶ ℂ \land b \in ℕ) \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) (b) \in ℂ$
92	89 90 91	syl2an	$⊢ (m \in ℕ_{0} \land b \in (1 \dots a)) \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) (b) \in ℂ$
93	92	adantlr	$⊢ ((m \in ℕ_{0} \land a \in ℕ) \land b \in (1 \dots a)) \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) (b) \in ℂ$
94		mulcl	$⊢ (b \in ℂ \land x \in ℂ) \to b x \in ℂ$
95	94	adantl	$⊢ ((m \in ℕ_{0} \land a \in ℕ) \land (b \in ℂ \land x \in ℂ)) \to b x \in ℂ$
96	70 93 95	seqcl	$⊢ (m \in ℕ_{0} \land a \in ℕ) \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) (a) \in ℂ$
97	96	adantlr	$⊢ ((m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \land a \in ℕ) \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) (a) \in ℂ$
98	86 76	rpmulcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to (1 + (\frac{m}{n})) (1 + (\frac{1}{n})) \in ℝ^{+}$
99		nn0p1nn	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ$
100	99	nnrpd	$⊢ m \in ℕ_{0} \to m + 1 \in ℝ^{+}$
101		rpdivcl	$⊢ (m + 1 \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{m + 1}{n} \in ℝ^{+}$
102	100 73 101	syl2an	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{m + 1}{n} \in ℝ^{+}$
103	72 102	rpaddcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 + (\frac{m + 1}{n}) \in ℝ^{+}$
104	98 103	rpdivcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})} \in ℝ^{+}$
105	104	rpcnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})} \in ℂ$
106	105	fmpttd	$⊢ m \in ℕ_{0} \to (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) : ℕ ⟶ ℂ$
107		ffvelrn	$⊢ ((n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) : ℕ ⟶ ℂ \land b \in ℕ) \to (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) (b) \in ℂ$
108	106 90 107	syl2an	$⊢ (m \in ℕ_{0} \land b \in (1 \dots a)) \to (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) (b) \in ℂ$
109	108	adantlr	$⊢ ((m \in ℕ_{0} \land a \in ℕ) \land b \in (1 \dots a)) \to (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) (b) \in ℂ$
110	70 109 95	seqcl	$⊢ (m \in ℕ_{0} \land a \in ℕ) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})})) (a) \in ℂ$
111	110	adantlr	$⊢ ((m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \land a \in ℕ) \to seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})})) (a) \in ℂ$
112		faclimlem3	$⊢ (m \in ℕ_{0} \land b \in ℕ) \to \frac{{(1 + (\frac{1}{b}))}^{m + 1}}{1 + (\frac{m + 1}{b})} = (\frac{{(1 + (\frac{1}{b}))}^{m}}{1 + (\frac{m}{b})}) (\frac{(1 + (\frac{m}{b})) (1 + (\frac{1}{b}))}{1 + (\frac{m + 1}{b})})$
113		oveq2	$⊢ n = b \to \frac{1}{n} = \frac{1}{b}$
114	113	oveq2d	$⊢ n = b \to 1 + (\frac{1}{n}) = 1 + (\frac{1}{b})$
115	114	oveq1d	$⊢ n = b \to {(1 + (\frac{1}{n}))}^{m + 1} = {(1 + (\frac{1}{b}))}^{m + 1}$
116		oveq2	$⊢ n = b \to \frac{m + 1}{n} = \frac{m + 1}{b}$
117	116	oveq2d	$⊢ n = b \to 1 + (\frac{m + 1}{n}) = 1 + (\frac{m + 1}{b})$
118	115 117	oveq12d	$⊢ n = b \to \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})} = \frac{{(1 + (\frac{1}{b}))}^{m + 1}}{1 + (\frac{m + 1}{b})}$
119		eqid	$⊢ (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})}) = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})$
120		ovex	$⊢ \frac{{(1 + (\frac{1}{b}))}^{m + 1}}{1 + (\frac{m + 1}{b})} \in V$
121	118 119 120	fvmpt	$⊢ b \in ℕ \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})}) (b) = \frac{{(1 + (\frac{1}{b}))}^{m + 1}}{1 + (\frac{m + 1}{b})}$
122	121	adantl	$⊢ (m \in ℕ_{0} \land b \in ℕ) \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})}) (b) = \frac{{(1 + (\frac{1}{b}))}^{m + 1}}{1 + (\frac{m + 1}{b})}$
123	114	oveq1d	$⊢ n = b \to {(1 + (\frac{1}{n}))}^{m} = {(1 + (\frac{1}{b}))}^{m}$
124		oveq2	$⊢ n = b \to \frac{m}{n} = \frac{m}{b}$
125	124	oveq2d	$⊢ n = b \to 1 + (\frac{m}{n}) = 1 + (\frac{m}{b})$
126	123 125	oveq12d	$⊢ n = b \to \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})} = \frac{{(1 + (\frac{1}{b}))}^{m}}{1 + (\frac{m}{b})}$
127		eqid	$⊢ (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})$
128		ovex	$⊢ \frac{{(1 + (\frac{1}{b}))}^{m}}{1 + (\frac{m}{b})} \in V$
129	126 127 128	fvmpt	$⊢ b \in ℕ \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) (b) = \frac{{(1 + (\frac{1}{b}))}^{m}}{1 + (\frac{m}{b})}$
130	125 114	oveq12d	$⊢ n = b \to (1 + (\frac{m}{n})) (1 + (\frac{1}{n})) = (1 + (\frac{m}{b})) (1 + (\frac{1}{b}))$
131	130 117	oveq12d	$⊢ n = b \to \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})} = \frac{(1 + (\frac{m}{b})) (1 + (\frac{1}{b}))}{1 + (\frac{m + 1}{b})}$
132		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})})$
133		ovex	$⊢ \frac{(1 + (\frac{m}{b})) (1 + (\frac{1}{b}))}{1 + (\frac{m + 1}{b})} \in V$
134	131 132 133	fvmpt	$⊢ b \in ℕ \to (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) (b) = \frac{(1 + (\frac{m}{b})) (1 + (\frac{1}{b}))}{1 + (\frac{m + 1}{b})}$
135	129 134	oveq12d	$⊢ b \in ℕ \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) (b) (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) (b) = (\frac{{(1 + (\frac{1}{b}))}^{m}}{1 + (\frac{m}{b})}) (\frac{(1 + (\frac{m}{b})) (1 + (\frac{1}{b}))}{1 + (\frac{m + 1}{b})})$
136	135	adantl	$⊢ (m \in ℕ_{0} \land b \in ℕ) \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) (b) (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) (b) = (\frac{{(1 + (\frac{1}{b}))}^{m}}{1 + (\frac{m}{b})}) (\frac{(1 + (\frac{m}{b})) (1 + (\frac{1}{b}))}{1 + (\frac{m + 1}{b})})$
137	112 122 136	3eqtr4d	$⊢ (m \in ℕ_{0} \land b \in ℕ) \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})}) (b) = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) (b) (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) (b)$
138	90 137	sylan2	$⊢ (m \in ℕ_{0} \land b \in (1 \dots a)) \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})}) (b) = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) (b) (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) (b)$
139	138	adantlr	$⊢ ((m \in ℕ_{0} \land a \in ℕ) \land b \in (1 \dots a)) \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})}) (b) = (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) (b) (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) (b)$
140	70 93 109 139	prodfmul	$⊢ (m \in ℕ_{0} \land a \in ℕ) \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})) (a) = seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) (a) seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})})) (a)$
141	140	adantlr	$⊢ ((m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \land a \in ℕ) \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})) (a) = seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) (a) seq 1 (\times (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})})) (a)$
142	57 62 63 65 67 97 111 141	climmul	$⊢ (m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})) ⇝ m! (m + 1)$
143		facp1	$⊢ m \in ℕ_{0} \to (m + 1)! = m! (m + 1)$
144	143	adantr	$⊢ (m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \to (m + 1)! = m! (m + 1)$
145	142 144	breqtrrd	$⊢ (m \in ℕ_{0} \land seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m!) \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})) ⇝ (m + 1)!$
146	145	ex	$⊢ m \in ℕ_{0} \to (seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})})) ⇝ m! \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m + 1}}{1 + (\frac{m + 1}{n})})) ⇝ (m + 1)!)$
147	13 21 29 37 61 146	nn0ind	$⊢ A \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})})) ⇝ A!$
148	3 147	eqbrtrid	$⊢ A \in ℕ_{0} \to seq 1 (\times F) ⇝ A!$

Metamath Proof Explorer

Theorem faclim

Proof