Description: A lower bound for a functional norm. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | nmfnlb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmfnsetre | |
|
2 | ressxr | |
|
3 | 1 2 | sstrdi | |
4 | 3 | 3ad2ant1 | |
5 | fveq2 | |
|
6 | 5 | breq1d | |
7 | 2fveq3 | |
|
8 | 7 | eqeq2d | |
9 | 6 8 | anbi12d | |
10 | eqid | |
|
11 | 10 | biantru | |
12 | 9 11 | bitr4di | |
13 | 12 | rspcev | |
14 | fvex | |
|
15 | eqeq1 | |
|
16 | 15 | anbi2d | |
17 | 16 | rexbidv | |
18 | 14 17 | elab | |
19 | 13 18 | sylibr | |
20 | 19 | 3adant1 | |
21 | supxrub | |
|
22 | 4 20 21 | syl2anc | |
23 | nmfnval | |
|
24 | 23 | 3ad2ant1 | |
25 | 22 24 | breqtrrd | |