Theorem knoppndvlem5

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

	Ref	Expression
Hypotheses	knoppndvlem5.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
	knoppndvlem5.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
	knoppndvlem5.a	|- ( ph -> A e. RR )
	knoppndvlem5.c	|- ( ph -> C e. RR )
	knoppndvlem5.n	|- ( ph -> N e. NN )
Assertion	knoppndvlem5	|- ( ph -> sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem5.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		knoppndvlem5.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3		knoppndvlem5.a	|- ( ph -> A e. RR )
4		knoppndvlem5.c	|- ( ph -> C e. RR )
5		knoppndvlem5.n	|- ( ph -> N e. NN )
6		fzfid	|- ( ph -> ( 0 ... J ) e. Fin )
7	5	adantr	|- ( ( ph /\ i e. ( 0 ... J ) ) -> N e. NN )
8	4	adantr	|- ( ( ph /\ i e. ( 0 ... J ) ) -> C e. RR )
9	3	adantr	|- ( ( ph /\ i e. ( 0 ... J ) ) -> A e. RR )
10		elfznn0	|- ( i e. ( 0 ... J ) -> i e. NN0 )
11	10	adantl	|- ( ( ph /\ i e. ( 0 ... J ) ) -> i e. NN0 )
12	1 2 7 8 9 11	knoppcnlem3	|- ( ( ph /\ i e. ( 0 ... J ) ) -> ( ( F ` A ) ` i ) e. RR )
13	6 12	fsumrecl	|- ( ph -> sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) e. RR )