Description: Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | elplyd.1 | |
|
elplyd.2 | |
||
elplyd.3 | |
||
Assertion | elplyd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elplyd.1 | |
|
2 | elplyd.2 | |
|
3 | elplyd.3 | |
|
4 | nffvmpt1 | |
|
5 | nfcv | |
|
6 | nfcv | |
|
7 | 4 5 6 | nfov | |
8 | nfcv | |
|
9 | fveq2 | |
|
10 | oveq2 | |
|
11 | 9 10 | oveq12d | |
12 | 7 8 11 | cbvsumi | |
13 | elfznn0 | |
|
14 | iftrue | |
|
15 | 14 | adantl | |
16 | 15 3 | eqeltrd | |
17 | eqid | |
|
18 | 17 | fvmpt2 | |
19 | 13 16 18 | syl2an2 | |
20 | 19 15 | eqtrd | |
21 | 20 | oveq1d | |
22 | 21 | sumeq2dv | |
23 | 12 22 | eqtrid | |
24 | 23 | mpteq2dv | |
25 | 0cnd | |
|
26 | 25 | snssd | |
27 | 1 26 | unssd | |
28 | elun1 | |
|
29 | 3 28 | syl | |
30 | 29 | adantlr | |
31 | ssun2 | |
|
32 | c0ex | |
|
33 | 32 | snss | |
34 | 31 33 | mpbir | |
35 | 34 | a1i | |
36 | 30 35 | ifclda | |
37 | 36 | fmpttd | |
38 | elplyr | |
|
39 | 27 2 37 38 | syl3anc | |
40 | 24 39 | eqeltrrd | |
41 | plyun0 | |
|
42 | 40 41 | eleqtrdi | |