Description: A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nmcfnex.1 | |
|
nmcfnex.2 | |
||
Assertion | nmcfnlbi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmcfnex.1 | |
|
2 | nmcfnex.2 | |
|
3 | fveq2 | |
|
4 | 1 | lnfn0i | |
5 | 3 4 | eqtrdi | |
6 | 5 | abs00bd | |
7 | 0le0 | |
|
8 | fveq2 | |
|
9 | norm0 | |
|
10 | 8 9 | eqtrdi | |
11 | 10 | oveq2d | |
12 | 1 2 | nmcfnexi | |
13 | 12 | recni | |
14 | 13 | mul01i | |
15 | 11 14 | eqtr2di | |
16 | 7 15 | breqtrid | |
17 | 6 16 | eqbrtrd | |
18 | 17 | adantl | |
19 | 1 | lnfnfi | |
20 | 19 | ffvelrni | |
21 | 20 | abscld | |
22 | 21 | adantr | |
23 | 22 | recnd | |
24 | normcl | |
|
25 | 24 | adantr | |
26 | 25 | recnd | |
27 | norm-i | |
|
28 | 27 | notbid | |
29 | 28 | biimpar | |
30 | 29 | neqned | |
31 | 23 26 30 | divrec2d | |
32 | 25 30 | rereccld | |
33 | 32 | recnd | |
34 | simpl | |
|
35 | 1 | lnfnmuli | |
36 | 33 34 35 | syl2anc | |
37 | 36 | fveq2d | |
38 | 20 | adantr | |
39 | 33 38 | absmuld | |
40 | df-ne | |
|
41 | normgt0 | |
|
42 | 40 41 | bitr3id | |
43 | 42 | biimpa | |
44 | 25 43 | recgt0d | |
45 | 0re | |
|
46 | ltle | |
|
47 | 45 46 | mpan | |
48 | 32 44 47 | sylc | |
49 | 32 48 | absidd | |
50 | 49 | oveq1d | |
51 | 37 39 50 | 3eqtrrd | |
52 | 31 51 | eqtrd | |
53 | hvmulcl | |
|
54 | 33 34 53 | syl2anc | |
55 | normcl | |
|
56 | 54 55 | syl | |
57 | norm1 | |
|
58 | 40 57 | sylan2br | |
59 | eqle | |
|
60 | 56 58 59 | syl2anc | |
61 | nmfnlb | |
|
62 | 19 61 | mp3an1 | |
63 | 54 60 62 | syl2anc | |
64 | 52 63 | eqbrtrd | |
65 | 12 | a1i | |
66 | ledivmul2 | |
|
67 | 22 65 25 43 66 | syl112anc | |
68 | 64 67 | mpbid | |
69 | 18 68 | pm2.61dan | |