Metamath Proof Explorer


Theorem eulerpartlemv

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-Aug-2018)

Ref Expression
Hypothesis eulerpart.p P=f0|f-1Finkfkk=N
Assertion eulerpartlemv APA:0A-1FinkA-1Akk=N

Proof

Step Hyp Ref Expression
1 eulerpart.p P=f0|f-1Finkfkk=N
2 1 eulerpartleme APA:0A-1FinkAkk=N
3 cnvimass A-1domA
4 fdm A:0domA=
5 3 4 sseqtrid A:0A-1
6 simpl A:0kA-1A:0
7 5 sselda A:0kA-1k
8 6 7 ffvelrnd A:0kA-1Ak0
9 7 nnnn0d A:0kA-1k0
10 8 9 nn0mulcld A:0kA-1Akk0
11 10 nn0cnd A:0kA-1Akk
12 simpr A:0kA-1kA-1
13 12 eldifad A:0kA-1k
14 12 eldifbd A:0kA-1¬kA-1
15 simpl A:0kA-1A:0
16 ffn A:0AFn
17 elpreima AFnkA-1kAk
18 15 16 17 3syl A:0kA-1kA-1kAk
19 14 18 mtbid A:0kA-1¬kAk
20 imnan k¬Ak¬kAk
21 19 20 sylibr A:0kA-1k¬Ak
22 13 21 mpd A:0kA-1¬Ak
23 15 13 ffvelrnd A:0kA-1Ak0
24 elnn0 Ak0AkAk=0
25 23 24 sylib A:0kA-1AkAk=0
26 orel1 ¬AkAkAk=0Ak=0
27 22 25 26 sylc A:0kA-1Ak=0
28 27 oveq1d A:0kA-1Akk=0k
29 13 nncnd A:0kA-1k
30 29 mul02d A:0kA-10k=0
31 28 30 eqtrd A:0kA-1Akk=0
32 nnuz =1
33 32 eqimssi 1
34 33 a1i A:01
35 5 11 31 34 sumss A:0kA-1Akk=kAkk
36 35 eqcomd A:0kAkk=kA-1Akk
37 36 adantr A:0A-1FinkAkk=kA-1Akk
38 37 eqeq1d A:0A-1FinkAkk=NkA-1Akk=N
39 38 pm5.32i A:0A-1FinkAkk=NA:0A-1FinkA-1Akk=N
40 df-3an A:0A-1FinkAkk=NA:0A-1FinkAkk=N
41 df-3an A:0A-1FinkA-1Akk=NA:0A-1FinkA-1Akk=N
42 39 40 41 3bitr4i A:0A-1FinkAkk=NA:0A-1FinkA-1Akk=N
43 2 42 bitri APA:0A-1FinkA-1Akk=N