Metamath Proof Explorer

Theorem knoppf

Description: Knopp's function is a function. (Contributed by Asger C. Ipsen, 25-Aug-2021)

Ref Expression
Hypotheses knoppf.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
knoppf.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
knoppf.w 
|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
knoppf.c 
|- ( ph -> C e. ( -u 1 (,) 1 ) )
knoppf.n 
|- ( ph -> N e. NN )
Assertion knoppf 
|- ( ph -> W : RR --> RR )

Proof

Step Hyp Ref Expression
1 knoppf.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 knoppf.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )
3 knoppf.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 knoppf.c 
 |-  ( ph -> C e. ( -u 1 (,) 1 ) )
5 knoppf.n 
 |-  ( ph -> N e. NN )
6 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
7 0zd 
 |-  ( ( ph /\ w e. RR ) -> 0 e. ZZ )
8 eqidd 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> ( ( F ` w ) ` i ) = ( ( F ` w ) ` i ) )
9 5 adantr 
 |-  ( ( ph /\ w e. RR ) -> N e. NN )
10 9 adantr 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> N e. NN )
11 4 knoppndvlem3 
 |-  ( ph -> ( C e. RR /\ ( abs ` C ) < 1 ) )
12 11 simpld 
 |-  ( ph -> C e. RR )
13 12 adantr 
 |-  ( ( ph /\ w e. RR ) -> C e. RR )
14 13 adantr 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> C e. RR )
15 simpr 
 |-  ( ( ph /\ w e. RR ) -> w e. RR )
16 15 adantr 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> w e. RR )
17 simpr 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> i e. NN0 )
18 1 2 10 14 16 17 knoppcnlem3 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. NN0 ) -> ( ( F ` w ) ` i ) e. RR )
19 fveq2 
 |-  ( w = z -> ( F ` w ) = ( F ` z ) )
20 19 fveq1d 
 |-  ( w = z -> ( ( F ` w ) ` i ) = ( ( F ` z ) ` i ) )
21 20 sumeq2sdv 
 |-  ( w = z -> sum_ i e. NN0 ( ( F ` w ) ` i ) = sum_ i e. NN0 ( ( F ` z ) ` i ) )
22 21 cbvmptv 
 |-  ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) ) = ( z e. RR |-> sum_ i e. NN0 ( ( F ` z ) ` i ) )
23 3 22 eqtri 
 |-  W = ( z e. RR |-> sum_ i e. NN0 ( ( F ` z ) ` i ) )
24 4 adantr 
 |-  ( ( ph /\ w e. RR ) -> C e. ( -u 1 (,) 1 ) )
25 1 2 23 15 24 9 knoppndvlem4 
 |-  ( ( ph /\ w e. RR ) -> seq 0 ( + , ( F ` w ) ) ~~> ( W ` w ) )
26 seqex 
 |-  seq 0 ( + , ( F ` w ) ) e. _V
27 fvex 
 |-  ( W ` w ) e. _V
28 26 27 breldm 
 |-  ( seq 0 ( + , ( F ` w ) ) ~~> ( W ` w ) -> seq 0 ( + , ( F ` w ) ) e. dom ~~> )
29 25 28 syl 
 |-  ( ( ph /\ w e. RR ) -> seq 0 ( + , ( F ` w ) ) e. dom ~~> )
30 6 7 8 18 29 isumrecl 
 |-  ( ( ph /\ w e. RR ) -> sum_ i e. NN0 ( ( F ` w ) ` i ) e. RR )
31 30 3 fmptd 
 |-  ( ph -> W : RR --> RR )