Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-Aug-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | eulerpart.p | |
|
Assertion | eulerpartlemv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eulerpart.p | |
|
2 | 1 | eulerpartleme | |
3 | cnvimass | |
|
4 | fdm | |
|
5 | 3 4 | sseqtrid | |
6 | simpl | |
|
7 | 5 | sselda | |
8 | 6 7 | ffvelrnd | |
9 | 7 | nnnn0d | |
10 | 8 9 | nn0mulcld | |
11 | 10 | nn0cnd | |
12 | simpr | |
|
13 | 12 | eldifad | |
14 | 12 | eldifbd | |
15 | simpl | |
|
16 | ffn | |
|
17 | elpreima | |
|
18 | 15 16 17 | 3syl | |
19 | 14 18 | mtbid | |
20 | imnan | |
|
21 | 19 20 | sylibr | |
22 | 13 21 | mpd | |
23 | 15 13 | ffvelrnd | |
24 | elnn0 | |
|
25 | 23 24 | sylib | |
26 | orel1 | |
|
27 | 22 25 26 | sylc | |
28 | 27 | oveq1d | |
29 | 13 | nncnd | |
30 | 29 | mul02d | |
31 | 28 30 | eqtrd | |
32 | nnuz | |
|
33 | 32 | eqimssi | |
34 | 33 | a1i | |
35 | 5 11 31 34 | sumss | |
36 | 35 | eqcomd | |
37 | 36 | adantr | |
38 | 37 | eqeq1d | |
39 | 38 | pm5.32i | |
40 | df-3an | |
|
41 | df-3an | |
|
42 | 39 40 41 | 3bitr4i | |
43 | 2 42 | bitri | |