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
|
mulid2i |
|- ( 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 ) = (/) ) |