Metamath Proof Explorer

Theorem cnndvlem1

Description: Lemma for cnndv . (Contributed by Asger C. Ipsen, 25-Aug-2021)

Ref Expression
Hypotheses cnndvlem1.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
cnndvlem1.f 
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( ( 1 / 2 ) ^ n ) x. ( T ` ( ( ( 2 x. 3 ) ^ n ) x. y ) ) ) ) )
cnndvlem1.w 
|- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
Assertion cnndvlem1 
|- ( W e. ( RR -cn-> RR ) /\ dom ( RR _D W ) = (/) )

Proof

Step Hyp Ref Expression
1 cnndvlem1.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 cnndvlem1.f 
 |-  F = ( y e. RR |-> ( n e. NN0 |-> ( ( ( 1 / 2 ) ^ n ) x. ( T ` ( ( ( 2 x. 3 ) ^ n ) x. y ) ) ) ) )
3 cnndvlem1.w 
 |-  W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )
4 3nn 
 |-  3 e. NN
5 4 a1i 
 |-  ( T. -> 3 e. NN )
6 neg1rr 
 |-  -u 1 e. RR
7 6 rexri 
 |-  -u 1 e. RR*
8 1re 
 |-  1 e. RR
9 8 rexri 
 |-  1 e. RR*
10 halfre 
 |-  ( 1 / 2 ) e. RR
11 10 rexri 
 |-  ( 1 / 2 ) e. RR*
12 7 9 11 3pm3.2i 
 |-  ( -u 1 e. RR* /\ 1 e. RR* /\ ( 1 / 2 ) e. RR* )
13 neg1lt0 
 |-  -u 1 < 0
14 halfgt0 
 |-  0 < ( 1 / 2 )
15 13 14 pm3.2i 
 |-  ( -u 1 < 0 /\ 0 < ( 1 / 2 ) )
16 0re 
 |-  0 e. RR
17 6 16 10 lttri 
 |-  ( ( -u 1 < 0 /\ 0 < ( 1 / 2 ) ) -> -u 1 < ( 1 / 2 ) )
18 15 17 ax-mp 
 |-  -u 1 < ( 1 / 2 )
19 halflt1 
 |-  ( 1 / 2 ) < 1
20 18 19 pm3.2i 
 |-  ( -u 1 < ( 1 / 2 ) /\ ( 1 / 2 ) < 1 )
21 12 20 pm3.2i 
 |-  ( ( -u 1 e. RR* /\ 1 e. RR* /\ ( 1 / 2 ) e. RR* ) /\ ( -u 1 < ( 1 / 2 ) /\ ( 1 / 2 ) < 1 ) )
22 elioo3g 
 |-  ( ( 1 / 2 ) e. ( -u 1 (,) 1 ) <-> ( ( -u 1 e. RR* /\ 1 e. RR* /\ ( 1 / 2 ) e. RR* ) /\ ( -u 1 < ( 1 / 2 ) /\ ( 1 / 2 ) < 1 ) ) )
23 21 22 mpbir 
 |-  ( 1 / 2 ) e. ( -u 1 (,) 1 )
24 23 a1i 
 |-  ( T. -> ( 1 / 2 ) e. ( -u 1 (,) 1 ) )
25 1 2 3 5 24 knoppcn2 
 |-  ( T. -> W e. ( RR -cn-> RR ) )
26 25 mptru 
 |-  W e. ( RR -cn-> RR )
27 2cn 
 |-  2 e. CC
28 27 mullidi 
 |-  ( 1 x. 2 ) = 2
29 2lt3 
 |-  2 < 3
30 28 29 eqbrtri 
 |-  ( 1 x. 2 ) < 3
31 2pos 
 |-  0 < 2
32 4 nnrei 
 |-  3 e. RR
33 2re 
 |-  2 e. RR
34 8 32 33 ltmuldivi 
 |-  ( 0 < 2 -> ( ( 1 x. 2 ) < 3 <-> 1 < ( 3 / 2 ) ) )
35 31 34 ax-mp 
 |-  ( ( 1 x. 2 ) < 3 <-> 1 < ( 3 / 2 ) )
36 30 35 mpbi 
 |-  1 < ( 3 / 2 )
37 16 10 14 ltleii 
 |-  0 <_ ( 1 / 2 )
38 10 absidi 
 |-  ( 0 <_ ( 1 / 2 ) -> ( abs ` ( 1 / 2 ) ) = ( 1 / 2 ) )
39 37 38 ax-mp 
 |-  ( abs ` ( 1 / 2 ) ) = ( 1 / 2 )
40 39 oveq2i 
 |-  ( 3 x. ( abs ` ( 1 / 2 ) ) ) = ( 3 x. ( 1 / 2 ) )
41 4 nncni 
 |-  3 e. CC
42 2ne0 
 |-  2 =/= 0
43 41 27 42 divreci 
 |-  ( 3 / 2 ) = ( 3 x. ( 1 / 2 ) )
44 43 eqcomi 
 |-  ( 3 x. ( 1 / 2 ) ) = ( 3 / 2 )
45 40 44 eqtri 
 |-  ( 3 x. ( abs ` ( 1 / 2 ) ) ) = ( 3 / 2 )
46 36 45 breqtrri 
 |-  1 < ( 3 x. ( abs ` ( 1 / 2 ) ) )
47 46 a1i 
 |-  ( T. -> 1 < ( 3 x. ( abs ` ( 1 / 2 ) ) ) )
48 1 2 3 24 5 47 knoppndv 
 |-  ( T. -> dom ( RR _D W ) = (/) )
49 48 mptru 
 |-  dom ( RR _D W ) = (/)
50 26 49 pm3.2i 
 |-  ( W e. ( RR -cn-> RR ) /\ dom ( RR _D W ) = (/) )