Metamath Proof Explorer


Theorem coeeq2

Description: Compute the coefficient function given a sum expression for the polynomial. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgrle.1 φ F Poly S
dgrle.2 φ N 0
dgrle.3 φ k 0 N A
dgrle.4 φ F = z k = 0 N A z k
Assertion coeeq2 φ coeff F = k 0 if k N A 0

Proof

Step Hyp Ref Expression
1 dgrle.1 φ F Poly S
2 dgrle.2 φ N 0
3 dgrle.3 φ k 0 N A
4 dgrle.4 φ F = z k = 0 N A z k
5 simpll φ k 0 k N φ
6 simpr φ k 0 k N k N
7 simplr φ k 0 k N k 0
8 nn0uz 0 = 0
9 7 8 eleqtrdi φ k 0 k N k 0
10 2 nn0zd φ N
11 10 ad2antrr φ k 0 k N N
12 elfz5 k 0 N k 0 N k N
13 9 11 12 syl2anc φ k 0 k N k 0 N k N
14 6 13 mpbird φ k 0 k N k 0 N
15 5 14 3 syl2anc φ k 0 k N A
16 0cnd φ k 0 ¬ k N 0
17 15 16 ifclda φ k 0 if k N A 0
18 17 fmpttd φ k 0 if k N A 0 : 0
19 simpr φ k 0 k 0
20 eqid k 0 if k N A 0 = k 0 if k N A 0
21 20 fvmpt2 k 0 if k N A 0 k 0 if k N A 0 k = if k N A 0
22 19 17 21 syl2anc φ k 0 k 0 if k N A 0 k = if k N A 0
23 22 neeq1d φ k 0 k 0 if k N A 0 k 0 if k N A 0 0
24 iffalse ¬ k N if k N A 0 = 0
25 24 necon1ai if k N A 0 0 k N
26 23 25 syl6bi φ k 0 k 0 if k N A 0 k 0 k N
27 26 ralrimiva φ k 0 k 0 if k N A 0 k 0 k N
28 nfv m k 0 if k N A 0 k 0 k N
29 nffvmpt1 _ k k 0 if k N A 0 m
30 nfcv _ k 0
31 29 30 nfne k k 0 if k N A 0 m 0
32 nfv k m N
33 31 32 nfim k k 0 if k N A 0 m 0 m N
34 fveq2 k = m k 0 if k N A 0 k = k 0 if k N A 0 m
35 34 neeq1d k = m k 0 if k N A 0 k 0 k 0 if k N A 0 m 0
36 breq1 k = m k N m N
37 35 36 imbi12d k = m k 0 if k N A 0 k 0 k N k 0 if k N A 0 m 0 m N
38 28 33 37 cbvralw k 0 k 0 if k N A 0 k 0 k N m 0 k 0 if k N A 0 m 0 m N
39 27 38 sylib φ m 0 k 0 if k N A 0 m 0 m N
40 plyco0 N 0 k 0 if k N A 0 : 0 k 0 if k N A 0 N + 1 = 0 m 0 k 0 if k N A 0 m 0 m N
41 2 18 40 syl2anc φ k 0 if k N A 0 N + 1 = 0 m 0 k 0 if k N A 0 m 0 m N
42 39 41 mpbird φ k 0 if k N A 0 N + 1 = 0
43 nfcv _ m k 0 if k N A 0 k z k
44 nfcv _ k ×
45 nfcv _ k z m
46 29 44 45 nfov _ k k 0 if k N A 0 m z m
47 oveq2 k = m z k = z m
48 34 47 oveq12d k = m k 0 if k N A 0 k z k = k 0 if k N A 0 m z m
49 43 46 48 cbvsumi k = 0 N k 0 if k N A 0 k z k = m = 0 N k 0 if k N A 0 m z m
50 elfznn0 k 0 N k 0
51 50 adantl φ z k 0 N k 0
52 elfzle2 k 0 N k N
53 52 adantl φ z k 0 N k N
54 53 iftrued φ z k 0 N if k N A 0 = A
55 3 adantlr φ z k 0 N A
56 54 55 eqeltrd φ z k 0 N if k N A 0
57 51 56 21 syl2anc φ z k 0 N k 0 if k N A 0 k = if k N A 0
58 57 54 eqtrd φ z k 0 N k 0 if k N A 0 k = A
59 58 oveq1d φ z k 0 N k 0 if k N A 0 k z k = A z k
60 59 sumeq2dv φ z k = 0 N k 0 if k N A 0 k z k = k = 0 N A z k
61 49 60 eqtr3id φ z m = 0 N k 0 if k N A 0 m z m = k = 0 N A z k
62 61 mpteq2dva φ z m = 0 N k 0 if k N A 0 m z m = z k = 0 N A z k
63 4 62 eqtr4d φ F = z m = 0 N k 0 if k N A 0 m z m
64 1 2 18 42 63 coeeq φ coeff F = k 0 if k N A 0