Metamath Proof Explorer


Theorem eulerpartlemmf

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 30-Aug-2018) (Revised by Thierry Arnoux, 1-Sep-2019)

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
eulerpart.j J = z | ¬ 2 z
eulerpart.f F = x J , y 0 2 y x
eulerpart.h H = r 𝒫 0 Fin J | r supp Fin
eulerpart.m M = r H x y | x J y r x
eulerpart.r R = f | f -1 Fin
eulerpart.t T = f 0 | f -1 J
eulerpart.g G = o T R 𝟙 F M bits o J
Assertion eulerpartlemmf A T R bits A J H

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 eulerpart.j J = z | ¬ 2 z
5 eulerpart.f F = x J , y 0 2 y x
6 eulerpart.h H = r 𝒫 0 Fin J | r supp Fin
7 eulerpart.m M = r H x y | x J y r x
8 eulerpart.r R = f | f -1 Fin
9 eulerpart.t T = f 0 | f -1 J
10 eulerpart.g G = o T R 𝟙 F M bits o J
11 bitsf1o bits 0 : 0 1-1 onto 𝒫 0 Fin
12 f1of bits 0 : 0 1-1 onto 𝒫 0 Fin bits 0 : 0 𝒫 0 Fin
13 11 12 ax-mp bits 0 : 0 𝒫 0 Fin
14 1 2 3 4 5 6 7 8 9 eulerpartlemt0 A T R A 0 A -1 Fin A -1 J
15 14 biimpi A T R A 0 A -1 Fin A -1 J
16 15 simp1d A T R A 0
17 nn0ex 0 V
18 nnex V
19 17 18 elmap A 0 A : 0
20 16 19 sylib A T R A : 0
21 ssrab2 z | ¬ 2 z
22 4 21 eqsstri J
23 fssres A : 0 J A J : J 0
24 20 22 23 sylancl A T R A J : J 0
25 fco2 bits 0 : 0 𝒫 0 Fin A J : J 0 bits A J : J 𝒫 0 Fin
26 13 24 25 sylancr A T R bits A J : J 𝒫 0 Fin
27 17 pwex 𝒫 0 V
28 27 inex1 𝒫 0 Fin V
29 18 22 ssexi J V
30 28 29 elmap bits A J 𝒫 0 Fin J bits A J : J 𝒫 0 Fin
31 26 30 sylibr A T R bits A J 𝒫 0 Fin J
32 15 simp2d A T R A -1 Fin
33 0nn0 0 0
34 suppimacnv A T R 0 0 A supp 0 = A -1 V 0
35 33 34 mpan2 A T R A supp 0 = A -1 V 0
36 frnsuppeq V 0 0 A : 0 A supp 0 = A -1 0 0
37 18 33 36 mp2an A : 0 A supp 0 = A -1 0 0
38 20 37 syl A T R A supp 0 = A -1 0 0
39 35 38 eqtr3d A T R A -1 V 0 = A -1 0 0
40 39 eleq1d A T R A -1 V 0 Fin A -1 0 0 Fin
41 dfn2 = 0 0
42 41 imaeq2i A -1 = A -1 0 0
43 42 eleq1i A -1 Fin A -1 0 0 Fin
44 40 43 bitr4di A T R A -1 V 0 Fin A -1 Fin
45 32 44 mpbird A T R A -1 V 0 Fin
46 resss A J A
47 cnvss A J A A J -1 A -1
48 imass1 A J -1 A -1 A J -1 V 0 A -1 V 0
49 46 47 48 mp2b A J -1 V 0 A -1 V 0
50 ssfi A -1 V 0 Fin A J -1 V 0 A -1 V 0 A J -1 V 0 Fin
51 45 49 50 sylancl A T R A J -1 V 0 Fin
52 cnvco bits A J -1 = A J -1 bits -1
53 52 imaeq1i bits A J -1 V = A J -1 bits -1 V
54 imaco A J -1 bits -1 V = A J -1 bits -1 V
55 53 54 eqtri bits A J -1 V = A J -1 bits -1 V
56 ffun A : 0 Fun A
57 funres Fun A Fun A J
58 20 56 57 3syl A T R Fun A J
59 ssv bits -1 V V
60 ssdif bits -1 V V bits -1 V bits -1 V bits -1
61 59 60 ax-mp bits -1 V bits -1 V bits -1
62 bitsf bits : 𝒫 0
63 ffun bits : 𝒫 0 Fun bits
64 difpreima Fun bits bits -1 V = bits -1 V bits -1
65 62 63 64 mp2b bits -1 V = bits -1 V bits -1
66 bitsf1 bits : 1-1 𝒫 0
67 0z 0
68 snssi 0 0
69 67 68 ax-mp 0
70 f1imacnv bits : 1-1 𝒫 0 0 bits -1 bits 0 = 0
71 66 69 70 mp2an bits -1 bits 0 = 0
72 ffn bits : 𝒫 0 bits Fn
73 62 72 ax-mp bits Fn
74 fnsnfv bits Fn 0 bits 0 = bits 0
75 73 67 74 mp2an bits 0 = bits 0
76 0bits bits 0 =
77 76 sneqi bits 0 =
78 75 77 eqtr3i bits 0 =
79 78 imaeq2i bits -1 bits 0 = bits -1
80 71 79 eqtr3i 0 = bits -1
81 80 difeq2i V 0 = V bits -1
82 61 65 81 3sstr4i bits -1 V V 0
83 sspreima Fun A J bits -1 V V 0 A J -1 bits -1 V A J -1 V 0
84 58 82 83 sylancl A T R A J -1 bits -1 V A J -1 V 0
85 55 84 eqsstrid A T R bits A J -1 V A J -1 V 0
86 ssfi A J -1 V 0 Fin bits A J -1 V A J -1 V 0 bits A J -1 V Fin
87 51 85 86 syl2anc A T R bits A J -1 V Fin
88 oveq1 r = bits A J r supp = bits A J supp
89 88 eleq1d r = bits A J r supp Fin bits A J supp Fin
90 89 6 elrab2 bits A J H bits A J 𝒫 0 Fin J bits A J supp Fin
91 zex V
92 fex bits : 𝒫 0 V bits V
93 62 91 92 mp2an bits V
94 resexg A T R A J V
95 coexg bits V A J V bits A J V
96 93 94 95 sylancr A T R bits A J V
97 0ex V
98 suppimacnv bits A J V V bits A J supp = bits A J -1 V
99 97 98 mpan2 bits A J V bits A J supp = bits A J -1 V
100 99 eleq1d bits A J V bits A J supp Fin bits A J -1 V Fin
101 100 anbi2d bits A J V bits A J 𝒫 0 Fin J bits A J supp Fin bits A J 𝒫 0 Fin J bits A J -1 V Fin
102 96 101 syl A T R bits A J 𝒫 0 Fin J bits A J supp Fin bits A J 𝒫 0 Fin J bits A J -1 V Fin
103 90 102 syl5bb A T R bits A J H bits A J 𝒫 0 Fin J bits A J -1 V Fin
104 31 87 103 mpbir2and A T R bits A J H