Metamath Proof Explorer


Theorem eulerpartlemgh

Description: Lemma for eulerpart : The F function is a bijection on the U subsets. (Contributed by Thierry Arnoux, 15-Aug-2018)

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
eulerpartlemgh.1 U = t A -1 J t × bits A t
Assertion eulerpartlemgh A T R F U : U 1-1 onto m | t n bits A t 2 n t = m

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 eulerpartlemgh.1 U = t A -1 J t × bits A t
12 4 5 oddpwdc F : J × 0 1-1 onto
13 f1of1 F : J × 0 1-1 onto F : J × 0 1-1
14 12 13 ax-mp F : J × 0 1-1
15 iunss t A -1 J t × bits A t J × 0 t A -1 J t × bits A t J × 0
16 inss2 A -1 J J
17 16 sseli t A -1 J t J
18 17 snssd t A -1 J t J
19 bitsss bits A t 0
20 xpss12 t J bits A t 0 t × bits A t J × 0
21 18 19 20 sylancl t A -1 J t × bits A t J × 0
22 15 21 mprgbir t A -1 J t × bits A t J × 0
23 11 22 eqsstri U J × 0
24 f1ores F : J × 0 1-1 U J × 0 F U : U 1-1 onto F U
25 14 23 24 mp2an F U : U 1-1 onto F U
26 simpr A T R t n bits A t 2 n t = p 2 n t = p
27 2nn 2
28 27 a1i A T R t n bits A t 2
29 19 sseli n bits A t n 0
30 29 adantl A T R t n bits A t n 0
31 28 30 nnexpcld A T R t n bits A t 2 n
32 simplr A T R t n bits A t t
33 31 32 nnmulcld A T R t n bits A t 2 n t
34 33 adantr A T R t n bits A t 2 n t = p 2 n t
35 26 34 eqeltrrd A T R t n bits A t 2 n t = p p
36 35 rexlimdva2 A T R t n bits A t 2 n t = p p
37 36 rexlimdva A T R t n bits A t 2 n t = p p
38 37 pm4.71rd A T R t n bits A t 2 n t = p p t n bits A t 2 n t = p
39 rex0 ¬ n 2 n t = p
40 simplr A T R t ¬ t A -1 t
41 simpr A T R t ¬ t A -1 ¬ t A -1
42 1 2 3 4 5 6 7 8 9 eulerpartlemt0 A T R A 0 A -1 Fin A -1 J
43 42 simp1bi A T R A 0
44 elmapi A 0 A : 0
45 43 44 syl A T R A : 0
46 45 ad2antrr A T R t ¬ t A -1 A : 0
47 ffn A : 0 A Fn
48 elpreima A Fn t A -1 t A t
49 46 47 48 3syl A T R t ¬ t A -1 t A -1 t A t
50 41 49 mtbid A T R t ¬ t A -1 ¬ t A t
51 imnan t ¬ A t ¬ t A t
52 50 51 sylibr A T R t ¬ t A -1 t ¬ A t
53 40 52 mpd A T R t ¬ t A -1 ¬ A t
54 46 40 ffvelrnd A T R t ¬ t A -1 A t 0
55 elnn0 A t 0 A t A t = 0
56 54 55 sylib A T R t ¬ t A -1 A t A t = 0
57 orel1 ¬ A t A t A t = 0 A t = 0
58 53 56 57 sylc A T R t ¬ t A -1 A t = 0
59 58 fveq2d A T R t ¬ t A -1 bits A t = bits 0
60 0bits bits 0 =
61 59 60 eqtrdi A T R t ¬ t A -1 bits A t =
62 61 rexeqdv A T R t ¬ t A -1 n bits A t 2 n t = p n 2 n t = p
63 39 62 mtbiri A T R t ¬ t A -1 ¬ n bits A t 2 n t = p
64 63 ex A T R t ¬ t A -1 ¬ n bits A t 2 n t = p
65 64 con4d A T R t n bits A t 2 n t = p t A -1
66 65 impr A T R t n bits A t 2 n t = p t A -1
67 eldif t J t ¬ t J
68 1 2 3 4 5 6 7 8 9 eulerpartlemf A T R t J A t = 0
69 67 68 sylan2br A T R t ¬ t J A t = 0
70 69 anassrs A T R t ¬ t J A t = 0
71 70 fveq2d A T R t ¬ t J bits A t = bits 0
72 71 60 eqtrdi A T R t ¬ t J bits A t =
73 72 rexeqdv A T R t ¬ t J n bits A t 2 n t = p n 2 n t = p
74 39 73 mtbiri A T R t ¬ t J ¬ n bits A t 2 n t = p
75 74 ex A T R t ¬ t J ¬ n bits A t 2 n t = p
76 75 con4d A T R t n bits A t 2 n t = p t J
77 76 impr A T R t n bits A t 2 n t = p t J
78 66 77 elind A T R t n bits A t 2 n t = p t A -1 J
79 simprr A T R t n bits A t 2 n t = p n bits A t 2 n t = p
80 78 79 jca A T R t n bits A t 2 n t = p t A -1 J n bits A t 2 n t = p
81 80 ex A T R t n bits A t 2 n t = p t A -1 J n bits A t 2 n t = p
82 81 reximdv2 A T R t n bits A t 2 n t = p t A -1 J n bits A t 2 n t = p
83 ssrab2 z | ¬ 2 z
84 4 83 eqsstri J
85 16 84 sstri A -1 J
86 ssrexv A -1 J t A -1 J n bits A t 2 n t = p t n bits A t 2 n t = p
87 85 86 mp1i A T R t A -1 J n bits A t 2 n t = p t n bits A t 2 n t = p
88 82 87 impbid A T R t n bits A t 2 n t = p t A -1 J n bits A t 2 n t = p
89 38 88 bitr3d A T R p t n bits A t 2 n t = p t A -1 J n bits A t 2 n t = p
90 eqeq2 m = p 2 n t = m 2 n t = p
91 90 2rexbidv m = p t n bits A t 2 n t = m t n bits A t 2 n t = p
92 91 elrab p m | t n bits A t 2 n t = m p t n bits A t 2 n t = p
93 92 a1i A T R p m | t n bits A t 2 n t = m p t n bits A t 2 n t = p
94 11 imaeq2i F U = F t A -1 J t × bits A t
95 imaiun F t A -1 J t × bits A t = t A -1 J F t × bits A t
96 94 95 eqtri F U = t A -1 J F t × bits A t
97 96 eleq2i p F U p t A -1 J F t × bits A t
98 eliun p t A -1 J F t × bits A t t A -1 J p F t × bits A t
99 f1ofn F : J × 0 1-1 onto F Fn J × 0
100 12 99 ax-mp F Fn J × 0
101 snssi t J t J
102 101 19 20 sylancl t J t × bits A t J × 0
103 ovelimab F Fn J × 0 t × bits A t J × 0 p F t × bits A t x t n bits A t p = x F n
104 100 102 103 sylancr t J p F t × bits A t x t n bits A t p = x F n
105 vex t V
106 oveq1 x = t x F n = t F n
107 106 eqeq2d x = t p = x F n p = t F n
108 107 rexbidv x = t n bits A t p = x F n n bits A t p = t F n
109 105 108 rexsn x t n bits A t p = x F n n bits A t p = t F n
110 104 109 bitrdi t J p F t × bits A t n bits A t p = t F n
111 df-ov t F n = F t n
112 111 eqeq1i t F n = p F t n = p
113 eqcom t F n = p p = t F n
114 112 113 bitr3i F t n = p p = t F n
115 opelxpi t J n 0 t n J × 0
116 4 5 oddpwdcv t n J × 0 F t n = 2 2 nd t n 1 st t n
117 vex n V
118 105 117 op2nd 2 nd t n = n
119 118 oveq2i 2 2 nd t n = 2 n
120 105 117 op1st 1 st t n = t
121 119 120 oveq12i 2 2 nd t n 1 st t n = 2 n t
122 116 121 eqtrdi t n J × 0 F t n = 2 n t
123 115 122 syl t J n 0 F t n = 2 n t
124 123 eqeq1d t J n 0 F t n = p 2 n t = p
125 114 124 bitr3id t J n 0 p = t F n 2 n t = p
126 29 125 sylan2 t J n bits A t p = t F n 2 n t = p
127 126 rexbidva t J n bits A t p = t F n n bits A t 2 n t = p
128 110 127 bitrd t J p F t × bits A t n bits A t 2 n t = p
129 17 128 syl t A -1 J p F t × bits A t n bits A t 2 n t = p
130 129 rexbiia t A -1 J p F t × bits A t t A -1 J n bits A t 2 n t = p
131 97 98 130 3bitri p F U t A -1 J n bits A t 2 n t = p
132 131 a1i A T R p F U t A -1 J n bits A t 2 n t = p
133 89 93 132 3bitr4rd A T R p F U p m | t n bits A t 2 n t = m
134 133 eqrdv A T R F U = m | t n bits A t 2 n t = m
135 f1oeq3 F U = m | t n bits A t 2 n t = m F U : U 1-1 onto F U F U : U 1-1 onto m | t n bits A t 2 n t = m
136 134 135 syl A T R F U : U 1-1 onto F U F U : U 1-1 onto m | t n bits A t 2 n t = m
137 25 136 mpbii A T R F U : U 1-1 onto m | t n bits A t 2 n t = m