Metamath Proof Explorer

Theorem eulerpartlemr

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 13-Nov-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
eulerpart.j ⊢J=z∈ℕ|¬2∥z
eulerpart.f ⊢F=x∈J,y∈ℕ0⟼2y⁢x
eulerpart.h ⊢H=r∈𝒫ℕ0∩FinJ|rsupp∅∈Fin
eulerpart.m ⊢M=r∈H⟼xy|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⟼𝟙ℕ⁡FM⁡bits∘o↾J
Assertion eulerpartlemr ⊢O=T∩R∩P

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⟼2y⁢x
6 eulerpart.h ⊢H=r∈𝒫ℕ0∩FinJ|rsupp∅∈Fin
7 eulerpart.m ⊢M=r∈H⟼xy|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⟼𝟙ℕ⁡FM⁡bits∘o↾J
11 elin ⊢h∈T∩R↔h∈T∧h∈R
12 11 anbi1i ⊢h∈T∩R∧h∈P↔h∈T∧h∈R∧h∈P
13 elin ⊢h∈T∩R∩P↔h∈T∩R∧h∈P
14 1 2 3 eulerpartlemo ⊢h∈O↔h∈P∧∀n∈h-1ℕ¬2∥n
15 cnveq ⊢f=h→f-1=h-1
16 15 imaeq1d ⊢f=h→f-1ℕ=h-1ℕ
17 16 eleq1d ⊢f=h→f-1ℕ∈Fin↔h-1ℕ∈Fin
18 fveq1 ⊢f=h→f⁡k=h⁡k
19 18 oveq1d ⊢f=h→f⁡k⁢k=h⁡k⁢k
20 19 sumeq2sdv ⊢f=h→∑k∈ℕf⁡k⁢k=∑k∈ℕh⁡k⁢k
21 20 eqeq1d ⊢f=h→∑k∈ℕf⁡k⁢k=N↔∑k∈ℕh⁡k⁢k=N
22 17 21 anbi12d ⊢f=h→f-1ℕ∈Fin∧∑k∈ℕf⁡k⁢k=N↔h-1ℕ∈Fin∧∑k∈ℕh⁡k⁢k=N
23 22 1 elrab2 ⊢h∈P↔h∈ℕ0ℕ∧h-1ℕ∈Fin∧∑k∈ℕh⁡k⁢k=N
24 23 simplbi ⊢h∈P→h∈ℕ0ℕ
25 cnvimass ⊢h-1ℕ⊆dom⁡h
26 nn0ex ⊢ℕ0∈V
27 nnex ⊢ℕ∈V
28 26 27 elmap ⊢h∈ℕ0ℕ↔h:ℕ⟶ℕ0
29 fdm ⊢h:ℕ⟶ℕ0→dom⁡h=ℕ
30 28 29 sylbi ⊢h∈ℕ0ℕ→dom⁡h=ℕ
31 25 30 sseqtrid ⊢h∈ℕ0ℕ→h-1ℕ⊆ℕ
32 24 31 syl ⊢h∈P→h-1ℕ⊆ℕ
33 32 sselda ⊢h∈P∧n∈h-1ℕ→n∈ℕ
34 33 ralrimiva ⊢h∈P→∀n∈h-1ℕn∈ℕ
35 34 biantrurd ⊢h∈P→∀n∈h-1ℕ¬2∥n↔∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n
36 24 biantrurd ⊢h∈P→∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n↔h∈ℕ0ℕ∧∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n
37 23 simprbi ⊢h∈P→h-1ℕ∈Fin∧∑k∈ℕh⁡k⁢k=N
38 37 simpld ⊢h∈P→h-1ℕ∈Fin
39 38 biantrud ⊢h∈P→h∈ℕ0ℕ∧∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n↔h∈ℕ0ℕ∧∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n∧h-1ℕ∈Fin
40 35 36 39 3bitrd ⊢h∈P→∀n∈h-1ℕ¬2∥n↔h∈ℕ0ℕ∧∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n∧h-1ℕ∈Fin
41 dfss3 ⊢h-1ℕ⊆J↔∀n∈h-1ℕn∈J
42 breq2 ⊢z=n→2∥z↔2∥n
43 42 notbid ⊢z=n→¬2∥z↔¬2∥n
44 43 4 elrab2 ⊢n∈J↔n∈ℕ∧¬2∥n
45 44 ralbii ⊢∀n∈h-1ℕn∈J↔∀n∈h-1ℕn∈ℕ∧¬2∥n
46 r19.26 ⊢∀n∈h-1ℕn∈ℕ∧¬2∥n↔∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n
47 41 45 46 3bitri ⊢h-1ℕ⊆J↔∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n
48 47 anbi2i ⊢h∈ℕ0ℕ∧h-1ℕ⊆J↔h∈ℕ0ℕ∧∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n
49 48 anbi1i ⊢h∈ℕ0ℕ∧h-1ℕ⊆J∧h-1ℕ∈Fin↔h∈ℕ0ℕ∧∀n∈h-1ℕn∈ℕ∧∀n∈h-1ℕ¬2∥n∧h-1ℕ∈Fin
50 40 49 bitr4di ⊢h∈P→∀n∈h-1ℕ¬2∥n↔h∈ℕ0ℕ∧h-1ℕ⊆J∧h-1ℕ∈Fin
51 16 sseq1d ⊢f=h→f-1ℕ⊆J↔h-1ℕ⊆J
52 51 9 elrab2 ⊢h∈T↔h∈ℕ0ℕ∧h-1ℕ⊆J
53 vex ⊢h∈V
54 53 17 8 elab2 ⊢h∈R↔h-1ℕ∈Fin
55 52 54 anbi12i ⊢h∈T∧h∈R↔h∈ℕ0ℕ∧h-1ℕ⊆J∧h-1ℕ∈Fin
56 50 55 bitr4di ⊢h∈P→∀n∈h-1ℕ¬2∥n↔h∈T∧h∈R
57 56 pm5.32i ⊢h∈P∧∀n∈h-1ℕ¬2∥n↔h∈P∧h∈T∧h∈R
58 ancom ⊢h∈P∧h∈T∧h∈R↔h∈T∧h∈R∧h∈P
59 14 57 58 3bitri ⊢h∈O↔h∈T∧h∈R∧h∈P
60 12 13 59 3bitr4ri ⊢h∈O↔h∈T∩R∩P
61 60 eqriv ⊢O=T∩R∩P