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	bilani	$⊢ (m \in ℕ_{0} \land a \in ℕ) \to a \in ℤ_{\geq 1}$
70		1rp	$⊢ 1 \in ℝ^{+}$
71	70	a1i	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 \in ℝ^{+}$
72		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
73	72	rpreccld	$⊢ n \in ℕ \to \frac{1}{n} \in ℝ^{+}$
74	73	adantl	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{1}{n} \in ℝ^{+}$
75	71 74	rpaddcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 + (\frac{1}{n}) \in ℝ^{+}$
76		nn0z	$⊢ m \in ℕ_{0} \to m \in ℤ$
77	76	adantr	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to m \in ℤ$
78	75 77	rpexpcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to {(1 + (\frac{1}{n}))}^{m} \in ℝ^{+}$
79		1cnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 \in ℂ$
80		nn0nndivcl	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{m}{n} \in ℝ$
81	80	recnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{m}{n} \in ℂ$
82	79 81	addcomd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 + (\frac{m}{n}) = (\frac{m}{n}) + 1$
83		nn0ge0div	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 0 \leq \frac{m}{n}$
84	80 83	ge0p1rpd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to (\frac{m}{n}) + 1 \in ℝ^{+}$
85	82 84	eqeltrd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 + (\frac{m}{n}) \in ℝ^{+}$
86	78 85	rpdivcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})} \in ℝ^{+}$
87	86	rpcnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})} \in ℂ$
88	87	fmpttd	$⊢ m \in ℕ_{0} \to (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})}) : ℕ ⟶ ℂ$
89		elfznn	$⊢ b \in (1 \dots a) \to b \in ℕ$
90		ffvelcdm	$⊢ ((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 ℂ$
91	88 89 90	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 ℂ$
92	91	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 ℂ$
93		mulcl	$⊢ (b \in ℂ \land x \in ℂ) \to b x \in ℂ$
94	93	adantl	$⊢ ((m \in ℕ_{0} \land a \in ℕ) \land (b \in ℂ \land x \in ℂ)) \to b x \in ℂ$
95	69 92 94	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 ℂ$
96	95	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 ℂ$
97	85 75	rpmulcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to (1 + (\frac{m}{n})) (1 + (\frac{1}{n})) \in ℝ^{+}$
98		nn0p1nn	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ$
99	98	nnrpd	$⊢ m \in ℕ_{0} \to m + 1 \in ℝ^{+}$
100		rpdivcl	$⊢ (m + 1 \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{m + 1}{n} \in ℝ^{+}$
101	99 72 100	syl2an	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{m + 1}{n} \in ℝ^{+}$
102	71 101	rpaddcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to 1 + (\frac{m + 1}{n}) \in ℝ^{+}$
103	97 102	rpdivcld	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})} \in ℝ^{+}$
104	103	rpcnd	$⊢ (m \in ℕ_{0} \land n \in ℕ) \to \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})} \in ℂ$
105	104	fmpttd	$⊢ m \in ℕ_{0} \to (n \in ℕ ⟼ \frac{(1 + (\frac{m}{n})) (1 + (\frac{1}{n}))}{1 + (\frac{m + 1}{n})}) : ℕ ⟶ ℂ$
106		ffvelcdm	$⊢ ((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 ℂ$
107	105 89 106	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 ℂ$
108	107	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 ℂ$
109	69 108 94	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 ℂ$
110	109	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 ℂ$
111		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})})$
112		oveq2	$⊢ n = b \to \frac{1}{n} = \frac{1}{b}$
113	112	oveq2d	$⊢ n = b \to 1 + (\frac{1}{n}) = 1 + (\frac{1}{b})$
114	113	oveq1d	$⊢ n = b \to {(1 + (\frac{1}{n}))}^{m + 1} = {(1 + (\frac{1}{b}))}^{m + 1}$
115		oveq2	$⊢ n = b \to \frac{m + 1}{n} = \frac{m + 1}{b}$
116	115	oveq2d	$⊢ n = b \to 1 + (\frac{m + 1}{n}) = 1 + (\frac{m + 1}{b})$
117	114 116	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})}$
118		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})})$
119		ovex	$⊢ \frac{{(1 + (\frac{1}{b}))}^{m + 1}}{1 + (\frac{m + 1}{b})} \in V$
120	117 118 119	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})}$
121	120	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})}$
122	113	oveq1d	$⊢ n = b \to {(1 + (\frac{1}{n}))}^{m} = {(1 + (\frac{1}{b}))}^{m}$
123		oveq2	$⊢ n = b \to \frac{m}{n} = \frac{m}{b}$
124	123	oveq2d	$⊢ n = b \to 1 + (\frac{m}{n}) = 1 + (\frac{m}{b})$
125	122 124	oveq12d	$⊢ n = b \to \frac{{(1 + (\frac{1}{n}))}^{m}}{1 + (\frac{m}{n})} = \frac{{(1 + (\frac{1}{b}))}^{m}}{1 + (\frac{m}{b})}$
126		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})})$
127		ovex	$⊢ \frac{{(1 + (\frac{1}{b}))}^{m}}{1 + (\frac{m}{b})} \in V$
128	125 126 127	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})}$
129	124 113	oveq12d	$⊢ n = b \to (1 + (\frac{m}{n})) (1 + (\frac{1}{n})) = (1 + (\frac{m}{b})) (1 + (\frac{1}{b}))$
130	129 116	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})}$
131		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})})$
132		ovex	$⊢ \frac{(1 + (\frac{m}{b})) (1 + (\frac{1}{b}))}{1 + (\frac{m + 1}{b})} \in V$
133	130 131 132	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})}$
134	128 133	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})})$
135	134	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})})$
136	111 121 135	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)$
137	89 136	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)$
138	137	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)$
139	69 92 108 138	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)$
140	139	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)$
141	57 62 63 65 67 96 110 140	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)$
142		facp1	$⊢ m \in ℕ_{0} \to (m + 1)! = m! (m + 1)$
143	142	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)$
144	141 143	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)!$
145	144	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)!)$
146	13 21 29 37 61 145	nn0ind	$⊢ A \in ℕ_{0} \to seq 1 (\times (n \in ℕ ⟼ \frac{{(1 + (\frac{1}{n}))}^{A}}{1 + (\frac{A}{n})})) ⇝ A!$
147	3 146	eqbrtrid	$⊢ A \in ℕ_{0} \to seq 1 (\times F) ⇝ A!$

Metamath Proof Explorer

Theorem faclim

Proof