Theorem eulerpartlemv

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 19-Aug-2018)

	Ref	Expression
Hypothesis	eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
Assertion	eulerpartlemv	⊢ ( 𝐴 ∈ 𝑃 ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2	1	eulerpartleme	⊢ ( 𝐴 ∈ 𝑃 ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
3		cnvimass	⊢ ( ◡ 𝐴 “ ℕ ) ⊆ dom 𝐴
4		fdm	⊢ ( 𝐴 : ℕ ⟶ ℕ0 → dom 𝐴 = ℕ )
5	3 4	sseqtrid	⊢ ( 𝐴 : ℕ ⟶ ℕ0 → ( ◡ 𝐴 “ ℕ ) ⊆ ℕ )
6		simpl	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝐴 : ℕ ⟶ ℕ0 )
7	5	sselda	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝑘 ∈ ℕ )
8	6 7	ffvelcdmd	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 )
9	7	nnnn0d	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝑘 ∈ ℕ0 )
10	8 9	nn0mulcld	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 )
11	10	nn0cnd	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ∈ ℂ )
12		simpr	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) )
13	12	eldifad	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝑘 ∈ ℕ )
14	12	eldifbd	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ¬ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) )
15		simpl	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝐴 : ℕ ⟶ ℕ0 )
16		ffn	⊢ ( 𝐴 : ℕ ⟶ ℕ0 → 𝐴 Fn ℕ )
17		elpreima	⊢ ( 𝐴 Fn ℕ → ( 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) ) )
18	15 16 17	3syl	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) ) )
19	14 18	mtbid	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ¬ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) )
20		imnan	⊢ ( ( 𝑘 ∈ ℕ → ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) ↔ ¬ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) )
21	19 20	sylibr	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝑘 ∈ ℕ → ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) )
22	13 21	mpd	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ )
23	15 13	ffvelcdmd	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 )
24		elnn0	⊢ ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 ↔ ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑘 ) = 0 ) )
25	23 24	sylib	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑘 ) = 0 ) )
26		orel1	⊢ ( ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ → ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑘 ) = 0 ) → ( 𝐴 ‘ 𝑘 ) = 0 ) )
27	22 25 26	sylc	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
28	27	oveq1d	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = ( 0 · 𝑘 ) )
29	13	nncnd	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝑘 ∈ ℂ )
30	29	mul02d	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 0 · 𝑘 ) = 0 )
31	28 30	eqtrd	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 0 )
32		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
33	32	eqimssi	⊢ ℕ ⊆ ( ℤ≥ ‘ 1 )
34	33	a1i	⊢ ( 𝐴 : ℕ ⟶ ℕ0 → ℕ ⊆ ( ℤ≥ ‘ 1 ) )
35	5 11 31 34	sumss	⊢ ( 𝐴 : ℕ ⟶ ℕ0 → Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
36	35	eqcomd	⊢ ( 𝐴 : ℕ ⟶ ℕ0 → Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
37	36	adantr	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) → Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
38	37	eqeq1d	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) → ( Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ↔ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
39	38	pm5.32i	⊢ ( ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
40		df-3an	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
41		df-3an	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
42	39 40 41	3bitr4i	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
43	2 42	bitri	⊢ ( 𝐴 ∈ 𝑃 ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )