Metamath Proof Explorer

Theorem faclimlem1

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

Ref Expression
Assertion faclimlem1 ⊢M∈ℕ0→seq1×n∈ℕ⟼1+Mn⁢1+1n1+M+1n=x∈ℕ⟼M+1⁢x+1x+M+1

Proof

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