Metamath Proof Explorer

Theorem eulerpartlemt0

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-Sep-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
Assertion eulerpartlemt0 ⊢ A ∈ T ∩ R ↔ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ∈ Fin ∧ A -1 ℕ ⊆ J

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 cnveq ⊢ f = A → f -1 = A -1
11 10 imaeq1d ⊢ f = A → f -1 ℕ = A -1 ℕ
12 11 sseq1d ⊢ f = A → f -1 ℕ ⊆ J ↔ A -1 ℕ ⊆ J
13 12 9 elrab2 ⊢ A ∈ T ↔ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ⊆ J
14 11 eleq1d ⊢ f = A → f -1 ℕ ∈ Fin ↔ A -1 ℕ ∈ Fin
15 14 8 elab4g ⊢ A ∈ R ↔ A ∈ V ∧ A -1 ℕ ∈ Fin
16 13 15 anbi12i ⊢ A ∈ T ∧ A ∈ R ↔ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ⊆ J ∧ A ∈ V ∧ A -1 ℕ ∈ Fin
17 elin ⊢ A ∈ T ∩ R ↔ A ∈ T ∧ A ∈ R
18 elex ⊢ A ∈ ℕ 0 ℕ → A ∈ V
19 18 pm4.71i ⊢ A ∈ ℕ 0 ℕ ↔ A ∈ ℕ 0 ℕ ∧ A ∈ V
20 19 anbi1i ⊢ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ∈ Fin ∧ A -1 ℕ ⊆ J ↔ A ∈ ℕ 0 ℕ ∧ A ∈ V ∧ A -1 ℕ ∈ Fin ∧ A -1 ℕ ⊆ J
21 3anass ⊢ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ∈ Fin ∧ A -1 ℕ ⊆ J ↔ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ∈ Fin ∧ A -1 ℕ ⊆ J
22 an42 ⊢ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ⊆ J ∧ A ∈ V ∧ A -1 ℕ ∈ Fin ↔ A ∈ ℕ 0 ℕ ∧ A ∈ V ∧ A -1 ℕ ∈ Fin ∧ A -1 ℕ ⊆ J
23 20 21 22 3bitr4i ⊢ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ∈ Fin ∧ A -1 ℕ ⊆ J ↔ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ⊆ J ∧ A ∈ V ∧ A -1 ℕ ∈ Fin
24 16 17 23 3bitr4i ⊢ A ∈ T ∩ R ↔ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ∈ Fin ∧ A -1 ℕ ⊆ J