Description: Value of the leading coefficient sequence function. (Contributed by Stefan O'Rear, 31-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hbtlem.p | |
|
hbtlem.u | |
||
hbtlem.s | |
||
hbtlem.d | |
||
Assertion | hbtlem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbtlem.p | |
|
2 | hbtlem.u | |
|
3 | hbtlem.s | |
|
4 | hbtlem.d | |
|
5 | elex | |
|
6 | fveq2 | |
|
7 | 6 1 | eqtr4di | |
8 | 7 | fveq2d | |
9 | 8 2 | eqtr4di | |
10 | fveq2 | |
|
11 | 10 4 | eqtr4di | |
12 | 11 | fveq1d | |
13 | 12 | breq1d | |
14 | 13 | anbi1d | |
15 | 14 | rexbidv | |
16 | 15 | abbidv | |
17 | 16 | mpteq2dv | |
18 | 9 17 | mpteq12dv | |
19 | df-ldgis | |
|
20 | 18 19 2 | mptfvmpt | |
21 | 5 20 | syl | |
22 | 3 21 | eqtrid | |
23 | 22 | fveq1d | |
24 | 23 | fveq1d | |
25 | 24 | 3ad2ant1 | |
26 | rexeq | |
|
27 | 26 | abbidv | |
28 | 27 | mpteq2dv | |
29 | eqid | |
|
30 | nn0ex | |
|
31 | 30 | mptex | |
32 | 28 29 31 | fvmpt | |
33 | 32 | fveq1d | |
34 | 33 | 3ad2ant2 | |
35 | eqid | |
|
36 | breq2 | |
|
37 | fveq2 | |
|
38 | 37 | eqeq2d | |
39 | 36 38 | anbi12d | |
40 | 39 | rexbidv | |
41 | 40 | abbidv | |
42 | simp3 | |
|
43 | simpr | |
|
44 | 43 | reximi | |
45 | 44 | ss2abi | |
46 | abrexexg | |
|
47 | 46 | 3ad2ant2 | |
48 | ssexg | |
|
49 | 45 47 48 | sylancr | |
50 | 35 41 42 49 | fvmptd3 | |
51 | 25 34 50 | 3eqtrd | |