Theorem knoppcnlem2

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

	Ref	Expression
Hypotheses	knoppcnlem2.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
	knoppcnlem2.n	|- ( ph -> N e. NN )
	knoppcnlem2.1	|- ( ph -> C e. RR )
	knoppcnlem2.2	|- ( ph -> A e. RR )
	knoppcnlem2.3	|- ( ph -> M e. NN0 )
Assertion	knoppcnlem2	|- ( ph -> ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem2.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		knoppcnlem2.n	|- ( ph -> N e. NN )
3		knoppcnlem2.1	|- ( ph -> C e. RR )
4		knoppcnlem2.2	|- ( ph -> A e. RR )
5		knoppcnlem2.3	|- ( ph -> M e. NN0 )
6	3 5	reexpcld	|- ( ph -> ( C ^ M ) e. RR )
7		2re	|- 2 e. RR
8	7	a1i	|- ( ph -> 2 e. RR )
9		nnre	|- ( N e. NN -> N e. RR )
10	2 9	syl	|- ( ph -> N e. RR )
11	8 10	remulcld	|- ( ph -> ( 2 x. N ) e. RR )
12	11 5	reexpcld	|- ( ph -> ( ( 2 x. N ) ^ M ) e. RR )
13	12 4	remulcld	|- ( ph -> ( ( ( 2 x. N ) ^ M ) x. A ) e. RR )
14	1 13	dnicld2	|- ( ph -> ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) e. RR )
15	6 14	remulcld	|- ( ph -> ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) e. RR )