Metamath Proof Explorer


Theorem eulerpartlemd

Description: Lemma for eulerpart : D is the set of distinct part. of N . (Contributed by Thierry Arnoux, 11-Aug-2017)

Ref Expression
Hypotheses eulerpart.p P = f 0 | f -1 Fin k f k k = N
eulerpart.o O = g P | n g -1 ¬ 2 n
eulerpart.d D = g P | n g n 1
Assertion eulerpartlemd A D A P A 0 1

Proof

Step Hyp Ref Expression
1 eulerpart.p P = f 0 | f -1 Fin k f k k = N
2 eulerpart.o O = g P | n g -1 ¬ 2 n
3 eulerpart.d D = g P | n g n 1
4 fveq1 g = A g n = A n
5 4 breq1d g = A g n 1 A n 1
6 5 ralbidv g = A n g n 1 n A n 1
7 6 3 elrab2 A D A P n A n 1
8 2z 2
9 fzoval 2 0 ..^ 2 = 0 2 1
10 8 9 ax-mp 0 ..^ 2 = 0 2 1
11 fzo0to2pr 0 ..^ 2 = 0 1
12 2m1e1 2 1 = 1
13 12 oveq2i 0 2 1 = 0 1
14 10 11 13 3eqtr3i 0 1 = 0 1
15 14 eleq2i A n 0 1 A n 0 1
16 1 eulerpartleme A P A : 0 A -1 Fin k A k k = N
17 16 simp1bi A P A : 0
18 17 ffvelrnda A P n A n 0
19 1nn0 1 0
20 elfz2nn0 A n 0 1 A n 0 1 0 A n 1
21 df-3an A n 0 1 0 A n 1 A n 0 1 0 A n 1
22 20 21 bitri A n 0 1 A n 0 1 0 A n 1
23 22 baib A n 0 1 0 A n 0 1 A n 1
24 18 19 23 sylancl A P n A n 0 1 A n 1
25 15 24 bitr2id A P n A n 1 A n 0 1
26 25 ralbidva A P n A n 1 n A n 0 1
27 17 ffund A P Fun A
28 fdm A : 0 dom A =
29 eqimss2 dom A = dom A
30 17 28 29 3syl A P dom A
31 funimass4 Fun A dom A A 0 1 n A n 0 1
32 27 30 31 syl2anc A P A 0 1 n A n 0 1
33 26 32 bitr4d A P n A n 1 A 0 1
34 33 pm5.32i A P n A n 1 A P A 0 1
35 7 34 bitri A D A P A 0 1