Metamath Proof Explorer


Theorem knoppndvlem7

Description: Lemma for knoppndv . (Contributed by Asger C. Ipsen, 15-Jun-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

Ref Expression
Hypotheses knoppndvlem7.t T = x x + 1 2 x
knoppndvlem7.f F = y n 0 C n T 2 N n y
knoppndvlem7.a A = 2 N J 2 M
knoppndvlem7.j φ J 0
knoppndvlem7.m φ M
knoppndvlem7.n φ N
Assertion knoppndvlem7 φ F A J = C J T M 2

Proof

Step Hyp Ref Expression
1 knoppndvlem7.t T = x x + 1 2 x
2 knoppndvlem7.f F = y n 0 C n T 2 N n y
3 knoppndvlem7.a A = 2 N J 2 M
4 knoppndvlem7.j φ J 0
5 knoppndvlem7.m φ M
6 knoppndvlem7.n φ N
7 3 a1i φ A = 2 N J 2 M
8 4 nn0zd φ J
9 6 8 5 knoppndvlem1 φ 2 N J 2 M
10 7 9 eqeltrd φ A
11 2 10 4 knoppcnlem1 φ F A J = C J T 2 N J A
12 3 oveq2i 2 N J A = 2 N J 2 N J 2 M
13 12 a1i φ 2 N J A = 2 N J 2 N J 2 M
14 2cnd φ 2
15 nnz N N
16 6 15 syl φ N
17 16 zcnd φ N
18 14 17 mulcld φ 2 N
19 18 4 expcld φ 2 N J
20 2ne0 2 0
21 20 a1i φ 2 0
22 0red φ 0
23 1red φ 1
24 16 zred φ N
25 0lt1 0 < 1
26 25 a1i φ 0 < 1
27 nnge1 N 1 N
28 6 27 syl φ 1 N
29 22 23 24 26 28 ltletrd φ 0 < N
30 22 29 ltned φ 0 N
31 30 necomd φ N 0
32 14 17 21 31 mulne0d φ 2 N 0
33 8 znegcld φ J
34 18 32 33 expclzd φ 2 N J
35 34 14 21 divcld φ 2 N J 2
36 5 zcnd φ M
37 19 35 36 mulassd φ 2 N J 2 N J 2 M = 2 N J 2 N J 2 M
38 37 eqcomd φ 2 N J 2 N J 2 M = 2 N J 2 N J 2 M
39 19 34 14 21 divassd φ 2 N J 2 N J 2 = 2 N J 2 N J 2
40 39 eqcomd φ 2 N J 2 N J 2 = 2 N J 2 N J 2
41 18 32 8 expnegd φ 2 N J = 1 2 N J
42 41 oveq2d φ 2 N J 2 N J = 2 N J 1 2 N J
43 18 32 8 expne0d φ 2 N J 0
44 19 43 recidd φ 2 N J 1 2 N J = 1
45 42 44 eqtrd φ 2 N J 2 N J = 1
46 45 oveq1d φ 2 N J 2 N J 2 = 1 2
47 40 46 eqtrd φ 2 N J 2 N J 2 = 1 2
48 47 oveq1d φ 2 N J 2 N J 2 M = 1 2 M
49 36 14 21 divrec2d φ M 2 = 1 2 M
50 49 eqcomd φ 1 2 M = M 2
51 38 48 50 3eqtrd φ 2 N J 2 N J 2 M = M 2
52 13 51 eqtrd φ 2 N J A = M 2
53 52 fveq2d φ T 2 N J A = T M 2
54 53 oveq2d φ C J T 2 N J A = C J T M 2
55 11 54 eqtrd φ F A J = C J T M 2