# Metamath Proof Explorer

## Theorem knoppcnlem1

Description: Lemma for knoppcn . (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypotheses knoppcnlem1.f ${⊢}{F}=\left({y}\in ℝ⟼\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)\right)$
knoppcnlem1.2 ${⊢}{\phi }\to {A}\in ℝ$
knoppcnlem1.3 ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
Assertion knoppcnlem1 ${⊢}{\phi }\to {F}\left({A}\right)\left({M}\right)={{C}}^{{M}}{T}\left({2\cdot {N}}^{{M}}{A}\right)$

### Proof

Step Hyp Ref Expression
1 knoppcnlem1.f ${⊢}{F}=\left({y}\in ℝ⟼\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)\right)$
2 knoppcnlem1.2 ${⊢}{\phi }\to {A}\in ℝ$
3 knoppcnlem1.3 ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
4 oveq2 ${⊢}{y}={A}\to {2\cdot {N}}^{{n}}{y}={2\cdot {N}}^{{n}}{A}$
5 4 fveq2d ${⊢}{y}={A}\to {T}\left({2\cdot {N}}^{{n}}{y}\right)={T}\left({2\cdot {N}}^{{n}}{A}\right)$
6 5 oveq2d ${⊢}{y}={A}\to {{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)={{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{A}\right)$
7 6 mpteq2dv ${⊢}{y}={A}\to \left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{y}\right)\right)=\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{A}\right)\right)$
8 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
9 8 mptex ${⊢}\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{A}\right)\right)\in \mathrm{V}$
10 9 a1i ${⊢}{\phi }\to \left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{A}\right)\right)\in \mathrm{V}$
11 1 7 2 10 fvmptd3 ${⊢}{\phi }\to {F}\left({A}\right)=\left({n}\in {ℕ}_{0}⟼{{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{A}\right)\right)$
12 oveq2 ${⊢}{n}={M}\to {{C}}^{{n}}={{C}}^{{M}}$
13 oveq2 ${⊢}{n}={M}\to {2\cdot {N}}^{{n}}={2\cdot {N}}^{{M}}$
14 13 fvoveq1d ${⊢}{n}={M}\to {T}\left({2\cdot {N}}^{{n}}{A}\right)={T}\left({2\cdot {N}}^{{M}}{A}\right)$
15 12 14 oveq12d ${⊢}{n}={M}\to {{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{A}\right)={{C}}^{{M}}{T}\left({2\cdot {N}}^{{M}}{A}\right)$
16 15 adantl ${⊢}\left({\phi }\wedge {n}={M}\right)\to {{C}}^{{n}}{T}\left({2\cdot {N}}^{{n}}{A}\right)={{C}}^{{M}}{T}\left({2\cdot {N}}^{{M}}{A}\right)$
17 ovexd ${⊢}{\phi }\to {{C}}^{{M}}{T}\left({2\cdot {N}}^{{M}}{A}\right)\in \mathrm{V}$
18 11 16 3 17 fvmptd ${⊢}{\phi }\to {F}\left({A}\right)\left({M}\right)={{C}}^{{M}}{T}\left({2\cdot {N}}^{{M}}{A}\right)$