Metamath Proof Explorer

Theorem 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∈ℕ⟼1+1nA1+An
Assertion faclim ⊢A∈ℕ0→seq1×F⇝A!

Proof

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