Metamath Proof Explorer


Theorem ply1termlem

Description: Lemma for ply1term . (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis ply1term.1 F = z A z N
Assertion ply1termlem A N 0 F = z k = 0 N if k = N A 0 z k

Proof

Step Hyp Ref Expression
1 ply1term.1 F = z A z N
2 simplr A N 0 z N 0
3 nn0uz 0 = 0
4 2 3 eleqtrdi A N 0 z N 0
5 fzss1 N 0 N N 0 N
6 4 5 syl A N 0 z N N 0 N
7 elfz1eq k N N k = N
8 7 adantl A N 0 z k N N k = N
9 iftrue k = N if k = N A 0 = A
10 8 9 syl A N 0 z k N N if k = N A 0 = A
11 simpll A N 0 z A
12 11 adantr A N 0 z k N N A
13 10 12 eqeltrd A N 0 z k N N if k = N A 0
14 simplr A N 0 z k N N z
15 2 adantr A N 0 z k N N N 0
16 8 15 eqeltrd A N 0 z k N N k 0
17 14 16 expcld A N 0 z k N N z k
18 13 17 mulcld A N 0 z k N N if k = N A 0 z k
19 eldifn k 0 N N N ¬ k N N
20 19 adantl A N 0 z k 0 N N N ¬ k N N
21 2 adantr A N 0 z k 0 N N N N 0
22 21 nn0zd A N 0 z k 0 N N N N
23 fzsn N N N = N
24 23 eleq2d N k N N k N
25 elsn2g N k N k = N
26 24 25 bitrd N k N N k = N
27 22 26 syl A N 0 z k 0 N N N k N N k = N
28 20 27 mtbid A N 0 z k 0 N N N ¬ k = N
29 28 iffalsed A N 0 z k 0 N N N if k = N A 0 = 0
30 29 oveq1d A N 0 z k 0 N N N if k = N A 0 z k = 0 z k
31 simpr A N 0 z z
32 eldifi k 0 N N N k 0 N
33 elfznn0 k 0 N k 0
34 32 33 syl k 0 N N N k 0
35 expcl z k 0 z k
36 31 34 35 syl2an A N 0 z k 0 N N N z k
37 36 mul02d A N 0 z k 0 N N N 0 z k = 0
38 30 37 eqtrd A N 0 z k 0 N N N if k = N A 0 z k = 0
39 fzfid A N 0 z 0 N Fin
40 6 18 38 39 fsumss A N 0 z k = N N if k = N A 0 z k = k = 0 N if k = N A 0 z k
41 2 nn0zd A N 0 z N
42 31 2 expcld A N 0 z z N
43 11 42 mulcld A N 0 z A z N
44 oveq2 k = N z k = z N
45 9 44 oveq12d k = N if k = N A 0 z k = A z N
46 45 fsum1 N A z N k = N N if k = N A 0 z k = A z N
47 41 43 46 syl2anc A N 0 z k = N N if k = N A 0 z k = A z N
48 40 47 eqtr3d A N 0 z k = 0 N if k = N A 0 z k = A z N
49 48 mpteq2dva A N 0 z k = 0 N if k = N A 0 z k = z A z N
50 1 49 eqtr4id A N 0 F = z k = 0 N if k = N A 0 z k