Description: Lemma for plymul . (Contributed by Mario Carneiro, 21-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | plyadd.1 | |
|
plyadd.2 | |
||
plyadd.3 | |
||
plyadd.m | |
||
plyadd.n | |
||
plyadd.a | |
||
plyadd.b | |
||
plyadd.a2 | |
||
plyadd.b2 | |
||
plyadd.f | |
||
plyadd.g | |
||
plymul.x | |
||
Assertion | plymullem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | plyadd.1 | |
|
2 | plyadd.2 | |
|
3 | plyadd.3 | |
|
4 | plyadd.m | |
|
5 | plyadd.n | |
|
6 | plyadd.a | |
|
7 | plyadd.b | |
|
8 | plyadd.a2 | |
|
9 | plyadd.b2 | |
|
10 | plyadd.f | |
|
11 | plyadd.g | |
|
12 | plymul.x | |
|
13 | plybss | |
|
14 | 1 13 | syl | |
15 | 0cnd | |
|
16 | 15 | snssd | |
17 | 14 16 | unssd | |
18 | cnex | |
|
19 | ssexg | |
|
20 | 17 18 19 | sylancl | |
21 | nn0ex | |
|
22 | elmapg | |
|
23 | 20 21 22 | sylancl | |
24 | 6 23 | mpbid | |
25 | 24 17 | fssd | |
26 | elmapg | |
|
27 | 20 21 26 | sylancl | |
28 | 7 27 | mpbid | |
29 | 28 17 | fssd | |
30 | 1 2 4 5 25 29 8 9 10 11 | plymullem1 | |
31 | 4 5 | nn0addcld | |
32 | eqid | |
|
33 | 14 32 3 | un0addcl | |
34 | fzfid | |
|
35 | elfznn0 | |
|
36 | ffvelrn | |
|
37 | 24 35 36 | syl2an | |
38 | fznn0sub | |
|
39 | ffvelrn | |
|
40 | 28 38 39 | syl2an | |
41 | 37 40 | jca | |
42 | 14 32 12 | un0mulcl | |
43 | 42 | caovclg | |
44 | 41 43 | syldan | |
45 | ssun2 | |
|
46 | c0ex | |
|
47 | 46 | snss | |
48 | 45 47 | mpbir | |
49 | 48 | a1i | |
50 | 17 33 34 44 49 | fsumcllem | |
51 | 50 | adantr | |
52 | 17 31 51 | elplyd | |
53 | 30 52 | eqeltrd | |
54 | plyun0 | |
|
55 | 53 54 | eleqtrdi | |