Theorem knoppcnlem3

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

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

Proof

Step	Hyp	Ref	Expression
1		knoppcnlem3.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		knoppcnlem3.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3		knoppcnlem3.n	|- ( ph -> N e. NN )
4		knoppcnlem3.1	|- ( ph -> C e. RR )
5		knoppcnlem3.2	|- ( ph -> A e. RR )
6		knoppcnlem3.3	|- ( ph -> M e. NN0 )
7	2 5 6	knoppcnlem1	|- ( ph -> ( ( F ` A ) ` M ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
8	1 3 4 5 6	knoppcnlem2	|- ( ph -> ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) e. RR )
9	7 8	eqeltrd	|- ( ph -> ( ( F ` A ) ` M ) e. RR )