Metamath Proof Explorer

Theorem eulerpartlemr

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 13-Nov-2017)

Ref Expression
Hypotheses eulerpart.p ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
eulerpart.o ⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
eulerpart.d ⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
eulerpart.j ⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
eulerpart.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
eulerpart.h ⊢ 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
eulerpart.m ⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
eulerpart.r ⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
eulerpart.t ⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
eulerpart.g ⊢ 𝐺 = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
Assertion eulerpartlemr 𝑂 = ( ( 𝑇 ∩ 𝑅 ) ∩ 𝑃 )

Proof

Step Hyp Ref Expression
1 eulerpart.p ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2 eulerpart.o ⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3 eulerpart.d ⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
4 eulerpart.j ⊢ 𝐽 = { 𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧 }
5 eulerpart.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ ℕ0 ↦ ( ( 2 ↑ 𝑦 ) · 𝑥 ) )
6 eulerpart.h ⊢ 𝐻 = { 𝑟 ∈ ( ( 𝒫 ℕ0 ∩ Fin ) ↑m 𝐽 ) ∣ ( 𝑟 supp ∅ ) ∈ Fin }
7 eulerpart.m ⊢ 𝑀 = ( 𝑟 ∈ 𝐻 ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ ( 𝑟 ‘ 𝑥 ) ) } )
8 eulerpart.r ⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
9 eulerpart.t ⊢ 𝑇 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 }
10 eulerpart.g ⊢ 𝐺 = ( 𝑜 ∈ ( 𝑇 ∩ 𝑅 ) ↦ ( ( 𝟭 ‘ ℕ ) ‘ ( 𝐹 “ ( 𝑀 ‘ ( bits ∘ ( 𝑜 ↾ 𝐽 ) ) ) ) ) )
11 elin ⊢ ( ℎ ∈ ( 𝑇 ∩ 𝑅 ) ↔ ( ℎ ∈ 𝑇 ∧ ℎ ∈ 𝑅 ) )
12 11 anbi1i ⊢ ( ( ℎ ∈ ( 𝑇 ∩ 𝑅 ) ∧ ℎ ∈ 𝑃 ) ↔ ( ( ℎ ∈ 𝑇 ∧ ℎ ∈ 𝑅 ) ∧ ℎ ∈ 𝑃 ) )
13 elin ⊢ ( ℎ ∈ ( ( 𝑇 ∩ 𝑅 ) ∩ 𝑃 ) ↔ ( ℎ ∈ ( 𝑇 ∩ 𝑅 ) ∧ ℎ ∈ 𝑃 ) )
14 1 2 3 eulerpartlemo ⊢ ( ℎ ∈ 𝑂 ↔ ( ℎ ∈ 𝑃 ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) )
15 cnveq ⊢ ( 𝑓 = ℎ → ◡ 𝑓 = ◡ ℎ )
16 15 imaeq1d ⊢ ( 𝑓 = ℎ → ( ◡ 𝑓 “ ℕ ) = ( ◡ ℎ “ ℕ ) )
17 16 eleq1d ⊢ ( 𝑓 = ℎ → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ ℎ “ ℕ ) ∈ Fin ) )
18 fveq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ‘ 𝑘 ) = ( ℎ ‘ 𝑘 ) )
19 18 oveq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = ( ( ℎ ‘ 𝑘 ) · 𝑘 ) )
20 19 sumeq2sdv ⊢ ( 𝑓 = ℎ → Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( ℎ ‘ 𝑘 ) · 𝑘 ) )
21 20 eqeq1d ⊢ ( 𝑓 = ℎ → ( Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ↔ Σ 𝑘 ∈ ℕ ( ( ℎ ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
22 17 21 anbi12d ⊢ ( 𝑓 = ℎ → ( ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( ◡ ℎ “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( ℎ ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ) )
23 22 1 elrab2 ⊢ ( ℎ ∈ 𝑃 ↔ ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ( ◡ ℎ “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( ℎ ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ) )
24 23 simplbi ⊢ ( ℎ ∈ 𝑃 → ℎ ∈ ( ℕ0 ↑m ℕ ) )
25 cnvimass ⊢ ( ◡ ℎ “ ℕ ) ⊆ dom ℎ
26 nn0ex ⊢ ℕ0 ∈ V
27 nnex ⊢ ℕ ∈ V
28 26 27 elmap ⊢ ( ℎ ∈ ( ℕ0 ↑m ℕ ) ↔ ℎ : ℕ ⟶ ℕ0 )
29 fdm ⊢ ( ℎ : ℕ ⟶ ℕ0 → dom ℎ = ℕ )
30 28 29 sylbi ⊢ ( ℎ ∈ ( ℕ0 ↑m ℕ ) → dom ℎ = ℕ )
31 25 30 sseqtrid ⊢ ( ℎ ∈ ( ℕ0 ↑m ℕ ) → ( ◡ ℎ “ ℕ ) ⊆ ℕ )
32 24 31 syl ⊢ ( ℎ ∈ 𝑃 → ( ◡ ℎ “ ℕ ) ⊆ ℕ )
33 32 sselda ⊢ ( ( ℎ ∈ 𝑃 ∧ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ) → 𝑛 ∈ ℕ )
34 33 ralrimiva ⊢ ( ℎ ∈ 𝑃 → ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ )
35 34 biantrurd ⊢ ( ℎ ∈ 𝑃 → ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ↔ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) ) )
36 24 biantrurd ⊢ ( ℎ ∈ 𝑃 → ( ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) ↔ ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) ) ) )
37 23 simprbi ⊢ ( ℎ ∈ 𝑃 → ( ( ◡ ℎ “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( ℎ ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
38 37 simpld ⊢ ( ℎ ∈ 𝑃 → ( ◡ ℎ “ ℕ ) ∈ Fin )
39 38 biantrud ⊢ ( ℎ ∈ 𝑃 → ( ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) ) ↔ ( ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) ) ∧ ( ◡ ℎ “ ℕ ) ∈ Fin ) ) )
40 35 36 39 3bitrd ⊢ ( ℎ ∈ 𝑃 → ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ↔ ( ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) ) ∧ ( ◡ ℎ “ ℕ ) ∈ Fin ) ) )
41 dfss3 ⊢ ( ( ◡ ℎ “ ℕ ) ⊆ 𝐽 ↔ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ 𝐽 )
42 breq2 ⊢ ( 𝑧 = 𝑛 → ( 2 ∥ 𝑧 ↔ 2 ∥ 𝑛 ) )
43 42 notbid ⊢ ( 𝑧 = 𝑛 → ( ¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥ 𝑛 ) )
44 43 4 elrab2 ⊢ ( 𝑛 ∈ 𝐽 ↔ ( 𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛 ) )
45 44 ralbii ⊢ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ 𝐽 ↔ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ( 𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛 ) )
46 r19.26 ⊢ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ( 𝑛 ∈ ℕ ∧ ¬ 2 ∥ 𝑛 ) ↔ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) )
47 41 45 46 3bitri ⊢ ( ( ◡ ℎ “ ℕ ) ⊆ 𝐽 ↔ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) )
48 47 anbi2i ⊢ ( ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ ℎ “ ℕ ) ⊆ 𝐽 ) ↔ ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) ) )
49 48 anbi1i ⊢ ( ( ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ ℎ “ ℕ ) ⊆ 𝐽 ) ∧ ( ◡ ℎ “ ℕ ) ∈ Fin ) ↔ ( ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) 𝑛 ∈ ℕ ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) ) ∧ ( ◡ ℎ “ ℕ ) ∈ Fin ) )
50 40 49 bitr4di ⊢ ( ℎ ∈ 𝑃 → ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ↔ ( ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ ℎ “ ℕ ) ⊆ 𝐽 ) ∧ ( ◡ ℎ “ ℕ ) ∈ Fin ) ) )
51 16 sseq1d ⊢ ( 𝑓 = ℎ → ( ( ◡ 𝑓 “ ℕ ) ⊆ 𝐽 ↔ ( ◡ ℎ “ ℕ ) ⊆ 𝐽 ) )
52 51 9 elrab2 ⊢ ( ℎ ∈ 𝑇 ↔ ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ ℎ “ ℕ ) ⊆ 𝐽 ) )
53 vex ⊢ ℎ ∈ V
54 53 17 8 elab2 ⊢ ( ℎ ∈ 𝑅 ↔ ( ◡ ℎ “ ℕ ) ∈ Fin )
55 52 54 anbi12i ⊢ ( ( ℎ ∈ 𝑇 ∧ ℎ ∈ 𝑅 ) ↔ ( ( ℎ ∈ ( ℕ0 ↑m ℕ ) ∧ ( ◡ ℎ “ ℕ ) ⊆ 𝐽 ) ∧ ( ◡ ℎ “ ℕ ) ∈ Fin ) )
56 50 55 bitr4di ⊢ ( ℎ ∈ 𝑃 → ( ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ↔ ( ℎ ∈ 𝑇 ∧ ℎ ∈ 𝑅 ) ) )
57 56 pm5.32i ⊢ ( ( ℎ ∈ 𝑃 ∧ ∀ 𝑛 ∈ ( ◡ ℎ “ ℕ ) ¬ 2 ∥ 𝑛 ) ↔ ( ℎ ∈ 𝑃 ∧ ( ℎ ∈ 𝑇 ∧ ℎ ∈ 𝑅 ) ) )
58 ancom ⊢ ( ( ℎ ∈ 𝑃 ∧ ( ℎ ∈ 𝑇 ∧ ℎ ∈ 𝑅 ) ) ↔ ( ( ℎ ∈ 𝑇 ∧ ℎ ∈ 𝑅 ) ∧ ℎ ∈ 𝑃 ) )
59 14 57 58 3bitri ⊢ ( ℎ ∈ 𝑂 ↔ ( ( ℎ ∈ 𝑇 ∧ ℎ ∈ 𝑅 ) ∧ ℎ ∈ 𝑃 ) )
60 12 13 59 3bitr4ri ⊢ ( ℎ ∈ 𝑂 ↔ ℎ ∈ ( ( 𝑇 ∩ 𝑅 ) ∩ 𝑃 ) )
61 60 eqriv ⊢ 𝑂 = ( ( 𝑇 ∩ 𝑅 ) ∩ 𝑃 )