Metamath Proof Explorer

Theorem knoppndvlem6

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

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

Proof

Step Hyp Ref Expression
1 knoppndvlem6.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppndvlem6.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppndvlem6.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 knoppndvlem6.a 
 |-  A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M )
5 knoppndvlem6.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
6 knoppndvlem6.j 
 |-  ( ph -> J e. NN0 )
7 knoppndvlem6.m 
 |-  ( ph -> M e. ZZ )
8 knoppndvlem6.n 
 |-  ( ph -> N e. NN )
9 fveq2 
 |-  ( w = A -> ( F ` w ) = ( F ` A ) )
10 9 fveq1d 
 |-  ( w = A -> ( ( F ` w ) ` i ) = ( ( F ` A ) ` i ) )
11 10 sumeq2sdv 
 |-  ( w = A -> sum_ i e. NN0 ( ( F ` w ) ` i ) = sum_ i e. NN0 ( ( F ` A ) ` i ) )
12 4 a1i 
 |-  ( ph -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) )
13 6 nn0zd 
 |-  ( ph -> J e. ZZ )
14 8 13 7 knoppndvlem1 
 |-  ( ph -> ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) e. RR )
15 12 14 eqeltrd 
 |-  ( ph -> A e. RR )
16 sumex 
 |-  sum_ i e. NN0 ( ( F ` A ) ` i ) e. _V
17 16 a1i 
 |-  ( ph -> sum_ i e. NN0 ( ( F ` A ) ` i ) e. _V )
18 3 11 15 17 fvmptd3 
 |-  ( ph -> ( W ` A ) = sum_ i e. NN0 ( ( F ` A ) ` i ) )
19 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
20 eqid 
 |-  ( ZZ>= ` ( J + 1 ) ) = ( ZZ>= ` ( J + 1 ) )
21 peano2nn0 
 |-  ( J e. NN0 -> ( J + 1 ) e. NN0 )
22 6 21 syl 
 |-  ( ph -> ( J + 1 ) e. NN0 )
23 eqidd 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( F ` A ) ` i ) = ( ( F ` A ) ` i ) )
24 8 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> N e. NN )
25 5 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
26 25 simpld 
 |-  ( ph -> C e. RR )
27 26 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> C e. RR )
28 15 adantr 
 |-  ( ( ph /\ i e. NN0 ) -> A e. RR )
29 simpr 
 |-  ( ( ph /\ i e. NN0 ) -> i e. NN0 )
30 1 2 24 27 28 29 knoppcnlem3 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( F ` A ) ` i ) e. RR )
31 30 recnd 
 |-  ( ( ph /\ i e. NN0 ) -> ( ( F ` A ) ` i ) e. CC )
32 1 2 3 15 5 8 knoppndvlem4 
 |-  ( ph -> seq 0 ( + , ( F ` A ) ) ~~> ( W ` A ) )
33 seqex 
 |-  seq 0 ( + , ( F ` A ) ) e. _V
34 fvex 
 |-  ( W ` A ) e. _V
35 33 34 breldm 
 |-  ( seq 0 ( + , ( F ` A ) ) ~~> ( W ` A ) -> seq 0 ( + , ( F ` A ) ) e. dom ~~> )
36 32 35 syl 
 |-  ( ph -> seq 0 ( + , ( F ` A ) ) e. dom ~~> )
37 19 20 22 23 31 36 isumsplit 
 |-  ( ph -> sum_ i e. NN0 ( ( F ` A ) ` i ) = ( sum_ i e. ( 0 ... ( ( J + 1 ) - 1 ) ) ( ( F ` A ) ` i ) + sum_ i e. ( ZZ>= ` ( J + 1 ) ) ( ( F ` A ) ` i ) ) )
38 6 nn0cnd 
 |-  ( ph -> J e. CC )
39 1cnd 
 |-  ( ph -> 1 e. CC )
40 38 39 pncand 
 |-  ( ph -> ( ( J + 1 ) - 1 ) = J )
41 40 oveq2d 
 |-  ( ph -> ( 0 ... ( ( J + 1 ) - 1 ) ) = ( 0 ... J ) )
42 41 sumeq1d 
 |-  ( ph -> sum_ i e. ( 0 ... ( ( J + 1 ) - 1 ) ) ( ( F ` A ) ` i ) = sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) )
43 42 oveq1d 
 |-  ( ph -> ( sum_ i e. ( 0 ... ( ( J + 1 ) - 1 ) ) ( ( F ` A ) ` i ) + sum_ i e. ( ZZ>= ` ( J + 1 ) ) ( ( F ` A ) ` i ) ) = ( sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) + sum_ i e. ( ZZ>= ` ( J + 1 ) ) ( ( F ` A ) ` i ) ) )
44 18 37 43 3eqtrd 
 |-  ( ph -> ( W ` A ) = ( sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) + sum_ i e. ( ZZ>= ` ( J + 1 ) ) ( ( F ` A ) ` i ) ) )
45 15 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> A e. RR )
46 eluznn0 
 |-  ( ( ( J + 1 ) e. NN0 /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> i e. NN0 )
47 22 46 sylan 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> i e. NN0 )
48 2 45 47 knoppcnlem1 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( ( F ` A ) ` i ) = ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) )
49 4 a1i 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> A = ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) )
50 49 oveq2d 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( ( ( 2 x. N ) ^ i ) x. A ) = ( ( ( 2 x. N ) ^ i ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) )
51 8 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> N e. NN )
52 47 nn0zd 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> i e. ZZ )
53 13 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> J e. ZZ )
54 7 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> M e. ZZ )
55 eluzle 
 |-  ( i e. ( ZZ>= ` ( J + 1 ) ) -> ( J + 1 ) <_ i )
56 55 adantl 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( J + 1 ) <_ i )
57 53 52 jca 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( J e. ZZ /\ i e. ZZ ) )
58 zltp1le 
 |-  ( ( J e. ZZ /\ i e. ZZ ) -> ( J < i <-> ( J + 1 ) <_ i ) )
59 57 58 syl 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( J < i <-> ( J + 1 ) <_ i ) )
60 56 59 mpbird 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> J < i )
61 51 52 53 54 60 knoppndvlem2 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( ( ( 2 x. N ) ^ i ) x. ( ( ( ( 2 x. N ) ^ -u J ) / 2 ) x. M ) ) e. ZZ )
62 50 61 eqeltrd 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( ( ( 2 x. N ) ^ i ) x. A ) e. ZZ )
63 1 62 dnizeq0 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) = 0 )
64 63 oveq2d 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( ( C ^ i ) x. ( T ` ( ( ( 2 x. N ) ^ i ) x. A ) ) ) = ( ( C ^ i ) x. 0 ) )
65 26 recnd 
 |-  ( ph -> C e. CC )
66 65 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> C e. CC )
67 66 47 expcld 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( C ^ i ) e. CC )
68 67 mul01d 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( ( C ^ i ) x. 0 ) = 0 )
69 48 64 68 3eqtrd 
 |-  ( ( ph /\ i e. ( ZZ>= ` ( J + 1 ) ) ) -> ( ( F ` A ) ` i ) = 0 )
70 69 sumeq2dv 
 |-  ( ph -> sum_ i e. ( ZZ>= ` ( J + 1 ) ) ( ( F ` A ) ` i ) = sum_ i e. ( ZZ>= ` ( J + 1 ) ) 0 )
71 ssidd 
 |-  ( ph -> ( ZZ>= ` ( J + 1 ) ) C_ ( ZZ>= ` ( J + 1 ) ) )
72 71 orcd 
 |-  ( ph -> ( ( ZZ>= ` ( J + 1 ) ) C_ ( ZZ>= ` ( J + 1 ) ) \/ ( ZZ>= ` ( J + 1 ) ) e. Fin ) )
73 sumz 
 |-  ( ( ( ZZ>= ` ( J + 1 ) ) C_ ( ZZ>= ` ( J + 1 ) ) \/ ( ZZ>= ` ( J + 1 ) ) e. Fin ) -> sum_ i e. ( ZZ>= ` ( J + 1 ) ) 0 = 0 )
74 72 73 syl 
 |-  ( ph -> sum_ i e. ( ZZ>= ` ( J + 1 ) ) 0 = 0 )
75 70 74 eqtrd 
 |-  ( ph -> sum_ i e. ( ZZ>= ` ( J + 1 ) ) ( ( F ` A ) ` i ) = 0 )
76 75 oveq2d 
 |-  ( ph -> ( sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) + sum_ i e. ( ZZ>= ` ( J + 1 ) ) ( ( F ` A ) ` i ) ) = ( sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) + 0 ) )
77 1 2 15 26 8 knoppndvlem5 
 |-  ( ph -> sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) e. RR )
78 77 recnd 
 |-  ( ph -> sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) e. CC )
79 78 addridd 
 |-  ( ph -> ( sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) + 0 ) = sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) )
80 76 79 eqtrd 
 |-  ( ph -> ( sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) + sum_ i e. ( ZZ>= ` ( J + 1 ) ) ( ( F ` A ) ` i ) ) = sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) )
81 44 80 eqtrd 
 |-  ( ph -> ( W ` A ) = sum_ i e. ( 0 ... J ) ( ( F ` A ) ` i ) )