# 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}=\left({x}\in ℝ⟼\left|⌊{x}+\left(\frac{1}{2}\right)⌋-{x}\right|\right)$
knoppndvlem7.f ${⊢}{F}=\left({y}\in ℝ⟼\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)\right)$
knoppndvlem7.a ${⊢}{A}=\left(\frac{{2\cdot {N}}^{-{J}}}{2}\right)\cdot {M}$
knoppndvlem7.j ${⊢}{\phi }\to {J}\in {ℕ}_{0}$
knoppndvlem7.m ${⊢}{\phi }\to {M}\in ℤ$
knoppndvlem7.n ${⊢}{\phi }\to {N}\in ℕ$
Assertion knoppndvlem7 ${⊢}{\phi }\to {F}\left({A}\right)\left({J}\right)={{C}}^{{J}}{T}\left(\frac{{M}}{2}\right)$

### Proof

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