Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | normlem7t.1 | |
|
normlem7t.2 | |
||
Assertion | normlem7tALT | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | normlem7t.1 | |
|
2 | normlem7t.2 | |
|
3 | fveq2 | |
|
4 | 3 | oveq1d | |
5 | oveq1 | |
|
6 | 4 5 | oveq12d | |
7 | 6 | breq1d | |
8 | eleq1 | |
|
9 | fveq2 | |
|
10 | 9 | eqeq1d | |
11 | 8 10 | anbi12d | |
12 | eleq1 | |
|
13 | fveq2 | |
|
14 | 13 | eqeq1d | |
15 | 12 14 | anbi12d | |
16 | ax-1cn | |
|
17 | abs1 | |
|
18 | 16 17 | pm3.2i | |
19 | 11 15 18 | elimhyp | |
20 | 19 | simpli | |
21 | 19 | simpri | |
22 | 20 1 2 21 | normlem7 | |
23 | 7 22 | dedth | |