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 addid1d
 |-  ( 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 ) )