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ℕ⊆01

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=01
12 2m1e1 ⊢2−1=1
13 12 oveq2i ⊢0…2−1=0…1
14 10 11 13 3eqtr3i ⊢01=0…1
15 14 eleq2i ⊢A⁡n∈01↔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 ffvelcdmda ⊢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∈01
26 25 ralbidva ⊢A∈P→∀n∈ℕA⁡n≤1↔∀n∈ℕA⁡n∈01
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ℕ⊆01↔∀n∈ℕA⁡n∈01
32 27 30 31 syl2anc ⊢A∈P→Aℕ⊆01↔∀n∈ℕA⁡n∈01
33 26 32 bitr4d ⊢A∈P→∀n∈ℕA⁡n≤1↔Aℕ⊆01
34 33 pm5.32i ⊢A∈P∧∀n∈ℕA⁡n≤1↔A∈P∧Aℕ⊆01
35 7 34 bitri ⊢A∈D↔A∈P∧Aℕ⊆01