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 ⟼ 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 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 ⟼ 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 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