Theorem knoppndvlem8

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

	Ref	Expression
Hypotheses	knoppndvlem8.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
	knoppndvlem8.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
	knoppndvlem8.a	|- A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
	knoppndvlem8.c	|- ( ph -> C e. ( -u 1 (,) 1 ) )
	knoppndvlem8.j	|- ( ph -> J e. NN0 )
	knoppndvlem8.m	|- ( ph -> M e. ZZ )
	knoppndvlem8.n	|- ( ph -> N e. NN )
	knoppndvlem8.1	|- ( ph -> 2 || M )
Assertion	knoppndvlem8	|- ( ph -> ( ( F ` A ) ` J ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		knoppndvlem8.t	|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2		knoppndvlem8.f	|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3		knoppndvlem8.a	|- A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
4		knoppndvlem8.c	|- ( ph -> C e. ( -u 1 (,) 1 ) )
5		knoppndvlem8.j	|- ( ph -> J e. NN0 )
6		knoppndvlem8.m	|- ( ph -> M e. ZZ )
7		knoppndvlem8.n	|- ( ph -> N e. NN )
8		knoppndvlem8.1	|- ( ph -> 2 || M )
9	1 2 3 5 6 7	knoppndvlem7	|- ( ph -> ( ( F ` A ) ` J ) = ( ( C ^ J ) x. ( T ` ( M / 2 ) ) ) )
10		2z	|- 2 e. ZZ
11	10	a1i	|- ( ph -> 2 e. ZZ )
12		2ne0	|- 2 =/= 0
13	12	a1i	|- ( ph -> 2 =/= 0 )
14	11 13 6	3jca	|- ( ph -> ( 2 e. ZZ /\ 2 =/= 0 /\ M e. ZZ ) )
15		dvdsval2	|- ( ( 2 e. ZZ /\ 2 =/= 0 /\ M e. ZZ ) -> ( 2 || M <-> ( M / 2 ) e. ZZ ) )
16	14 15	syl	|- ( ph -> ( 2 || M <-> ( M / 2 ) e. ZZ ) )
17	8 16	mpbid	|- ( ph -> ( M / 2 ) e. ZZ )
18	1 17	dnizeq0	|- ( ph -> ( T ` ( M / 2 ) ) = 0 )
19	18	oveq2d	|- ( ph -> ( ( C ^ J ) x. ( T ` ( M / 2 ) ) ) = ( ( C ^ J ) x. 0 ) )
20	4	knoppndvlem3	|- ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
21	20	simpld	|- ( ph -> C e. RR )
22	21	recnd	|- ( ph -> C e. CC )
23	22 5	expcld	|- ( ph -> ( C ^ J ) e. CC )
24	23	mul01d	|- ( ph -> ( ( C ^ J ) x. 0 ) = 0 )
25	9 19 24	3eqtrd	|- ( ph -> ( ( F ` A ) ` J ) = 0 )