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	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
	eulerpart.o	⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
	eulerpart.d	⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
Assertion	eulerpartlemd	⊢ ( 𝐴 ∈ 𝐷 ↔ ( 𝐴 ∈ 𝑃 ∧ ( 𝐴 “ ℕ ) ⊆ { 0 , 1 } ) )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2		eulerpart.o	⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3		eulerpart.d	⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
4		fveq1	⊢ ( 𝑔 = 𝐴 → ( 𝑔 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑛 ) )
5	4	breq1d	⊢ ( 𝑔 = 𝐴 → ( ( 𝑔 ‘ 𝑛 ) ≤ 1 ↔ ( 𝐴 ‘ 𝑛 ) ≤ 1 ) )
6	5	ralbidv	⊢ ( 𝑔 = 𝐴 → ( ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ≤ 1 ) )
7	6 3	elrab2	⊢ ( 𝐴 ∈ 𝐷 ↔ ( 𝐴 ∈ 𝑃 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ≤ 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	⊢ ( ( 𝐴 ‘ 𝑛 ) ∈ { 0 , 1 } ↔ ( 𝐴 ‘ 𝑛 ) ∈ ( 0 ... 1 ) )
16	1	eulerpartleme	⊢ ( 𝐴 ∈ 𝑃 ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
17	16	simp1bi	⊢ ( 𝐴 ∈ 𝑃 → 𝐴 : ℕ ⟶ ℕ0 )
18	17	ffvelrnda	⊢ ( ( 𝐴 ∈ 𝑃 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ‘ 𝑛 ) ∈ ℕ0 )
19		1nn0	⊢ 1 ∈ ℕ0
20		elfz2nn0	⊢ ( ( 𝐴 ‘ 𝑛 ) ∈ ( 0 ... 1 ) ↔ ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑛 ) ≤ 1 ) )
21		df-3an	⊢ ( ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑛 ) ≤ 1 ) ↔ ( ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑛 ) ≤ 1 ) )
22	20 21	bitri	⊢ ( ( 𝐴 ‘ 𝑛 ) ∈ ( 0 ... 1 ) ↔ ( ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑛 ) ≤ 1 ) )
23	22	baib	⊢ ( ( ( 𝐴 ‘ 𝑛 ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑛 ) ∈ ( 0 ... 1 ) ↔ ( 𝐴 ‘ 𝑛 ) ≤ 1 ) )
24	18 19 23	sylancl	⊢ ( ( 𝐴 ∈ 𝑃 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑛 ) ∈ ( 0 ... 1 ) ↔ ( 𝐴 ‘ 𝑛 ) ≤ 1 ) )
25	15 24	bitr2id	⊢ ( ( 𝐴 ∈ 𝑃 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 ‘ 𝑛 ) ≤ 1 ↔ ( 𝐴 ‘ 𝑛 ) ∈ { 0 , 1 } ) )
26	25	ralbidva	⊢ ( 𝐴 ∈ 𝑃 → ( ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ≤ 1 ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ∈ { 0 , 1 } ) )
27	17	ffund	⊢ ( 𝐴 ∈ 𝑃 → Fun 𝐴 )
28		fdm	⊢ ( 𝐴 : ℕ ⟶ ℕ0 → dom 𝐴 = ℕ )
29		eqimss2	⊢ ( dom 𝐴 = ℕ → ℕ ⊆ dom 𝐴 )
30	17 28 29	3syl	⊢ ( 𝐴 ∈ 𝑃 → ℕ ⊆ dom 𝐴 )
31		funimass4	⊢ ( ( Fun 𝐴 ∧ ℕ ⊆ dom 𝐴 ) → ( ( 𝐴 “ ℕ ) ⊆ { 0 , 1 } ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ∈ { 0 , 1 } ) )
32	27 30 31	syl2anc	⊢ ( 𝐴 ∈ 𝑃 → ( ( 𝐴 “ ℕ ) ⊆ { 0 , 1 } ↔ ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ∈ { 0 , 1 } ) )
33	26 32	bitr4d	⊢ ( 𝐴 ∈ 𝑃 → ( ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ≤ 1 ↔ ( 𝐴 “ ℕ ) ⊆ { 0 , 1 } ) )
34	33	pm5.32i	⊢ ( ( 𝐴 ∈ 𝑃 ∧ ∀ 𝑛 ∈ ℕ ( 𝐴 ‘ 𝑛 ) ≤ 1 ) ↔ ( 𝐴 ∈ 𝑃 ∧ ( 𝐴 “ ℕ ) ⊆ { 0 , 1 } ) )
35	7 34	bitri	⊢ ( 𝐴 ∈ 𝐷 ↔ ( 𝐴 ∈ 𝑃 ∧ ( 𝐴 “ ℕ ) ⊆ { 0 , 1 } ) )