Metamath Proof Explorer

Theorem eulerpartlemd

Description: Lemma for eulerpart : D is the set of distinct part. of N . (Contributed by Thierry Arnoux, 11-Aug-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
Assertion eulerpartlemd ⊢ A ∈ D ↔ A ∈ P ∧ A ℕ ⊆ 0 1

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 fveq1 ⊢ g = A → g ⁡ n = A ⁡ n
5 4 breq1d ⊢ g = A → g ⁡ n ≤ 1 ↔ A ⁡ n ≤ 1
6 5 ralbidv ⊢ g = A → ∀ n ∈ ℕ g ⁡ n ≤ 1 ↔ ∀ n ∈ ℕ A ⁡ n ≤ 1
7 6 3 elrab2 ⊢ A ∈ D ↔ A ∈ P ∧ ∀ n ∈ ℕ A ⁡ n ≤ 1
8 2z ⊢ 2 ∈ ℤ
9 fzoval ⊢ 2 ∈ ℤ → 0 ..^ 2 = 0 … 2 − 1
10 8 9 ax-mp ⊢ 0 ..^ 2 = 0 … 2 − 1
11 fzo0to2pr ⊢ 0 ..^ 2 = 0 1
12 2m1e1 ⊢ 2 − 1 = 1
13 12 oveq2i ⊢ 0 … 2 − 1 = 0 … 1
14 10 11 13 3eqtr3i ⊢ 0 1 = 0 … 1
15 14 eleq2i ⊢ A ⁡ n ∈ 0 1 ↔ A ⁡ n ∈ 0 … 1
16 1 eulerpartleme ⊢ A ∈ P ↔ A : ℕ ⟶ ℕ 0 ∧ A -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ A ⁡ k ⁢ k = N
17 16 simp1bi ⊢ A ∈ P → A : ℕ ⟶ ℕ 0
18 17 ffvelrnda ⊢ A ∈ P ∧ n ∈ ℕ → A ⁡ n ∈ ℕ 0
19 1nn0 ⊢ 1 ∈ ℕ 0
20 elfz2nn0 ⊢ A ⁡ n ∈ 0 … 1 ↔ A ⁡ n ∈ ℕ 0 ∧ 1 ∈ ℕ 0 ∧ A ⁡ n ≤ 1
21 df-3an ⊢ A ⁡ n ∈ ℕ 0 ∧ 1 ∈ ℕ 0 ∧ A ⁡ n ≤ 1 ↔ A ⁡ n ∈ ℕ 0 ∧ 1 ∈ ℕ 0 ∧ A ⁡ n ≤ 1
22 20 21 bitri ⊢ A ⁡ n ∈ 0 … 1 ↔ A ⁡ n ∈ ℕ 0 ∧ 1 ∈ ℕ 0 ∧ A ⁡ n ≤ 1
23 22 baib ⊢ A ⁡ n ∈ ℕ 0 ∧ 1 ∈ ℕ 0 → A ⁡ n ∈ 0 … 1 ↔ A ⁡ n ≤ 1
24 18 19 23 sylancl ⊢ A ∈ P ∧ n ∈ ℕ → A ⁡ n ∈ 0 … 1 ↔ A ⁡ n ≤ 1
25 15 24 bitr2id ⊢ A ∈ P ∧ n ∈ ℕ → A ⁡ n ≤ 1 ↔ A ⁡ n ∈ 0 1
26 25 ralbidva ⊢ A ∈ P → ∀ n ∈ ℕ A ⁡ n ≤ 1 ↔ ∀ n ∈ ℕ A ⁡ n ∈ 0 1
27 17 ffund ⊢ A ∈ P → Fun ⁡ A
28 fdm ⊢ A : ℕ ⟶ ℕ 0 → dom ⁡ A = ℕ
29 eqimss2 ⊢ dom ⁡ A = ℕ → ℕ ⊆ dom ⁡ A
30 17 28 29 3syl ⊢ A ∈ P → ℕ ⊆ dom ⁡ A
31 funimass4 ⊢ Fun ⁡ A ∧ ℕ ⊆ dom ⁡ A → A ℕ ⊆ 0 1 ↔ ∀ n ∈ ℕ A ⁡ n ∈ 0 1
32 27 30 31 syl2anc ⊢ A ∈ P → A ℕ ⊆ 0 1 ↔ ∀ n ∈ ℕ A ⁡ n ∈ 0 1
33 26 32 bitr4d ⊢ A ∈ P → ∀ n ∈ ℕ A ⁡ n ≤ 1 ↔ A ℕ ⊆ 0 1
34 33 pm5.32i ⊢ A ∈ P ∧ ∀ n ∈ ℕ A ⁡ n ≤ 1 ↔ A ∈ P ∧ A ℕ ⊆ 0 1
35 7 34 bitri ⊢ A ∈ D ↔ A ∈ P ∧ A ℕ ⊆ 0 1