Metamath Proof Explorer


Theorem knoppndvlem14

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 1-Jul-2021) (Revised by Asger C. Ipsen, 7-Jul-2021)

Ref Expression
Hypotheses knoppndvlem14.t T = x x + 1 2 x
knoppndvlem14.f F = y n 0 C n T 2 N n y
knoppndvlem14.a A = 2 N J 2 M
knoppndvlem14.b B = 2 N J 2 M + 1
knoppndvlem14.c φ C 1 1
knoppndvlem14.j φ J 0
knoppndvlem14.m φ M
knoppndvlem14.n φ N
knoppndvlem14.1 φ 1 < N C
Assertion knoppndvlem14 φ i = 0 J 1 F B i i = 0 J 1 F A i C J 2 1 2 N C 1

Proof

Step Hyp Ref Expression
1 knoppndvlem14.t T = x x + 1 2 x
2 knoppndvlem14.f F = y n 0 C n T 2 N n y
3 knoppndvlem14.a A = 2 N J 2 M
4 knoppndvlem14.b B = 2 N J 2 M + 1
5 knoppndvlem14.c φ C 1 1
6 knoppndvlem14.j φ J 0
7 knoppndvlem14.m φ M
8 knoppndvlem14.n φ N
9 knoppndvlem14.1 φ 1 < N C
10 4 a1i φ B = 2 N J 2 M + 1
11 6 nn0zd φ J
12 7 peano2zd φ M + 1
13 8 11 12 knoppndvlem1 φ 2 N J 2 M + 1
14 10 13 eqeltrd φ B
15 5 knoppndvlem3 φ C C < 1
16 15 simpld φ C
17 1 2 14 16 8 knoppndvlem5 φ i = 0 J 1 F B i
18 3 a1i φ A = 2 N J 2 M
19 8 11 7 knoppndvlem1 φ 2 N J 2 M
20 18 19 eqeltrd φ A
21 1 2 20 16 8 knoppndvlem5 φ i = 0 J 1 F A i
22 17 21 resubcld φ i = 0 J 1 F B i i = 0 J 1 F A i
23 22 recnd φ i = 0 J 1 F B i i = 0 J 1 F A i
24 23 abscld φ i = 0 J 1 F B i i = 0 J 1 F A i
25 14 20 resubcld φ B A
26 25 recnd φ B A
27 26 abscld φ B A
28 fzfid φ 0 J 1 Fin
29 2re 2
30 29 a1i φ 2
31 nnre N N
32 8 31 syl φ N
33 30 32 remulcld φ 2 N
34 16 recnd φ C
35 34 abscld φ C
36 33 35 remulcld φ 2 N C
37 36 adantr φ i 0 J 1 2 N C
38 elfznn0 i 0 J 1 i 0
39 38 adantl φ i 0 J 1 i 0
40 37 39 reexpcld φ i 0 J 1 2 N C i
41 28 40 fsumrecl φ i = 0 J 1 2 N C i
42 27 41 remulcld φ B A i = 0 J 1 2 N C i
43 35 6 reexpcld φ C J
44 2ne0 2 0
45 44 a1i φ 2 0
46 43 30 45 redivcld φ C J 2
47 1red φ 1
48 36 47 resubcld φ 2 N C 1
49 0red φ 0
50 0lt1 0 < 1
51 50 a1i φ 0 < 1
52 5 8 9 knoppndvlem12 φ 2 N C 1 1 < 2 N C 1
53 52 simprd φ 1 < 2 N C 1
54 49 47 48 51 53 lttrd φ 0 < 2 N C 1
55 49 54 jca φ 0 0 < 2 N C 1
56 ltne 0 0 < 2 N C 1 2 N C 1 0
57 55 56 syl φ 2 N C 1 0
58 47 48 57 redivcld φ 1 2 N C 1
59 46 58 remulcld φ C J 2 1 2 N C 1
60 1 2 20 14 5 6 8 knoppndvlem11 φ i = 0 J 1 F B i i = 0 J 1 F A i B A i = 0 J 1 2 N C i
61 10 18 oveq12d φ B A = 2 N J 2 M + 1 2 N J 2 M
62 30 recnd φ 2
63 32 recnd φ N
64 nnge1 N 1 N
65 8 64 syl φ 1 N
66 49 47 32 51 65 ltletrd φ 0 < N
67 49 66 jca φ 0 0 < N
68 ltne 0 0 < N N 0
69 67 68 syl φ N 0
70 62 63 45 69 mulne0d φ 2 N 0
71 11 znegcld φ J
72 33 70 71 reexpclzd φ 2 N J
73 72 30 45 redivcld φ 2 N J 2
74 73 recnd φ 2 N J 2
75 12 zcnd φ M + 1
76 7 zcnd φ M
77 74 75 76 subdid φ 2 N J 2 M + 1 - M = 2 N J 2 M + 1 2 N J 2 M
78 77 eqcomd φ 2 N J 2 M + 1 2 N J 2 M = 2 N J 2 M + 1 - M
79 1cnd φ 1
80 76 79 pncan2d φ M + 1 - M = 1
81 80 oveq2d φ 2 N J 2 M + 1 - M = 2 N J 2 1
82 74 mulid1d φ 2 N J 2 1 = 2 N J 2
83 78 81 82 3eqtrd φ 2 N J 2 M + 1 2 N J 2 M = 2 N J 2
84 61 83 eqtrd φ B A = 2 N J 2
85 84 fveq2d φ B A = 2 N J 2
86 72 recnd φ 2 N J
87 86 62 45 absdivd φ 2 N J 2 = 2 N J 2
88 62 63 mulcld φ 2 N
89 88 70 71 3jca φ 2 N 2 N 0 J
90 absexpz 2 N 2 N 0 J 2 N J = 2 N J
91 89 90 syl φ 2 N J = 2 N J
92 62 63 absmuld φ 2 N = 2 N
93 0le2 0 2
94 29 93 pm3.2i 2 0 2
95 absid 2 0 2 2 = 2
96 94 95 ax-mp 2 = 2
97 96 a1i φ 2 = 2
98 49 32 66 ltled φ 0 N
99 32 98 absidd φ N = N
100 97 99 oveq12d φ 2 N = 2 N
101 92 100 eqtrd φ 2 N = 2 N
102 101 oveq1d φ 2 N J = 2 N J
103 91 102 eqtrd φ 2 N J = 2 N J
104 103 97 oveq12d φ 2 N J 2 = 2 N J 2
105 87 104 eqtrd φ 2 N J 2 = 2 N J 2
106 85 105 eqtrd φ B A = 2 N J 2
107 36 recnd φ 2 N C
108 52 simpld φ 2 N C 1
109 107 108 6 geoser φ i = 0 J 1 2 N C i = 1 2 N C J 1 2 N C
110 107 6 expcld φ 2 N C J
111 108 necomd φ 1 2 N C
112 79 110 79 107 111 div2subd φ 1 2 N C J 1 2 N C = 2 N C J 1 2 N C 1
113 109 112 eqtrd φ i = 0 J 1 2 N C i = 2 N C J 1 2 N C 1
114 106 113 oveq12d φ B A i = 0 J 1 2 N C i = 2 N J 2 2 N C J 1 2 N C 1
115 113 41 eqeltrrd φ 2 N C J 1 2 N C 1
116 36 6 reexpcld φ 2 N C J
117 116 48 57 redivcld φ 2 N C J 2 N C 1
118 2rp 2 +
119 118 a1i φ 2 +
120 119 rpgt0d φ 0 < 2
121 30 32 120 66 mulgt0d φ 0 < 2 N
122 33 71 121 3jca φ 2 N J 0 < 2 N
123 expgt0 2 N J 0 < 2 N 0 < 2 N J
124 122 123 syl φ 0 < 2 N J
125 49 72 124 ltled φ 0 2 N J
126 72 119 125 divge0d φ 0 2 N J 2
127 116 47 resubcld φ 2 N C J 1
128 48 54 elrpd φ 2 N C 1 +
129 116 lem1d φ 2 N C J 1 2 N C J
130 127 116 128 129 lediv1dd φ 2 N C J 1 2 N C 1 2 N C J 2 N C 1
131 115 117 73 126 130 lemul2ad φ 2 N J 2 2 N C J 1 2 N C 1 2 N J 2 2 N C J 2 N C 1
132 48 recnd φ 2 N C 1
133 110 132 57 divrecd φ 2 N C J 2 N C 1 = 2 N C J 1 2 N C 1
134 133 oveq2d φ 2 N J 2 2 N C J 2 N C 1 = 2 N J 2 2 N C J 1 2 N C 1
135 58 recnd φ 1 2 N C 1
136 74 110 135 mulassd φ 2 N J 2 2 N C J 1 2 N C 1 = 2 N J 2 2 N C J 1 2 N C 1
137 136 eqcomd φ 2 N J 2 2 N C J 1 2 N C 1 = 2 N J 2 2 N C J 1 2 N C 1
138 86 110 62 45 div23d φ 2 N J 2 N C J 2 = 2 N J 2 2 N C J
139 138 eqcomd φ 2 N J 2 2 N C J = 2 N J 2 N C J 2
140 88 70 jca φ 2 N 2 N 0
141 35 recnd φ C
142 5 8 9 knoppndvlem13 φ C 0
143 34 142 absne0d φ C 0
144 141 143 jca φ C C 0
145 140 144 11 3jca φ 2 N 2 N 0 C C 0 J
146 mulexpz 2 N 2 N 0 C C 0 J 2 N C J = 2 N J C J
147 145 146 syl φ 2 N C J = 2 N J C J
148 147 oveq2d φ 2 N J 2 N C J = 2 N J 2 N J C J
149 88 6 expcld φ 2 N J
150 43 recnd φ C J
151 86 149 150 mulassd φ 2 N J 2 N J C J = 2 N J 2 N J C J
152 151 eqcomd φ 2 N J 2 N J C J = 2 N J 2 N J C J
153 140 71 11 jca32 φ 2 N 2 N 0 J J
154 expaddz 2 N 2 N 0 J J 2 N - J + J = 2 N J 2 N J
155 153 154 syl φ 2 N - J + J = 2 N J 2 N J
156 155 eqcomd φ 2 N J 2 N J = 2 N - J + J
157 71 zcnd φ J
158 6 nn0cnd φ J
159 157 158 addcomd φ - J + J = J + -J
160 158 negidd φ J + -J = 0
161 159 160 eqtrd φ - J + J = 0
162 161 oveq2d φ 2 N - J + J = 2 N 0
163 88 exp0d φ 2 N 0 = 1
164 156 162 163 3eqtrd φ 2 N J 2 N J = 1
165 164 oveq1d φ 2 N J 2 N J C J = 1 C J
166 150 mulid2d φ 1 C J = C J
167 165 166 eqtrd φ 2 N J 2 N J C J = C J
168 148 152 167 3eqtrd φ 2 N J 2 N C J = C J
169 168 oveq1d φ 2 N J 2 N C J 2 = C J 2
170 139 169 eqtrd φ 2 N J 2 2 N C J = C J 2
171 170 oveq1d φ 2 N J 2 2 N C J 1 2 N C 1 = C J 2 1 2 N C 1
172 134 137 171 3eqtrd φ 2 N J 2 2 N C J 2 N C 1 = C J 2 1 2 N C 1
173 131 172 breqtrd φ 2 N J 2 2 N C J 1 2 N C 1 C J 2 1 2 N C 1
174 114 173 eqbrtrd φ B A i = 0 J 1 2 N C i C J 2 1 2 N C 1
175 24 42 59 60 174 letrd φ i = 0 J 1 F B i i = 0 J 1 F A i C J 2 1 2 N C 1