fsumvma

Description: Rewrite a sum over the von Mangoldt function as a sum over prime powers. (Contributed by Mario Carneiro, 15-Apr-2016)

	Ref	Expression
Hypotheses	fsumvma.1	⊢ ( 𝑥 = ( 𝑝 ↑ 𝑘 ) → 𝐵 = 𝐶 )
	fsumvma.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumvma.3	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
	fsumvma.4	⊢ ( 𝜑 → 𝑃 ∈ Fin )
	fsumvma.5	⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 ) ) )
	fsumvma.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fsumvma.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( Λ ‘ 𝑥 ) = 0 ) ) → 𝐵 = 0 )
Assertion	fsumvma	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 𝐵 = Σ 𝑝 ∈ 𝑃 Σ 𝑘 ∈ 𝐾 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fsumvma.1	⊢ ( 𝑥 = ( 𝑝 ↑ 𝑘 ) → 𝐵 = 𝐶 )
2		fsumvma.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fsumvma.3	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
4		fsumvma.4	⊢ ( 𝜑 → 𝑃 ∈ Fin )
5		fsumvma.5	⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 ) ) )
6		fsumvma.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
7		fsumvma.7	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ ( Λ ‘ 𝑥 ) = 0 ) ) → 𝐵 = 0 )
8		fvexd	⊢ ( 𝑧 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑧 ) ∈ V )
9		fveq2	⊢ ( 𝑧 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑧 ) = ( ↑ ‘ ⟨ 𝑝 , 𝑘 ⟩ ) )
10		df-ov	⊢ ( 𝑝 ↑ 𝑘 ) = ( ↑ ‘ ⟨ 𝑝 , 𝑘 ⟩ )
11	9 10	eqtr4di	⊢ ( 𝑧 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑧 ) = ( 𝑝 ↑ 𝑘 ) )
12	11	eqeq2d	⊢ ( 𝑧 = ⟨ 𝑝 , 𝑘 ⟩ → ( 𝑥 = ( ↑ ‘ 𝑧 ) ↔ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) )
13	12	biimpa	⊢ ( ( 𝑧 = ⟨ 𝑝 , 𝑘 ⟩ ∧ 𝑥 = ( ↑ ‘ 𝑧 ) ) → 𝑥 = ( 𝑝 ↑ 𝑘 ) )
14	13 1	syl	⊢ ( ( 𝑧 = ⟨ 𝑝 , 𝑘 ⟩ ∧ 𝑥 = ( ↑ ‘ 𝑧 ) ) → 𝐵 = 𝐶 )
15	8 14	csbied	⊢ ( 𝑧 = ⟨ 𝑝 , 𝑘 ⟩ → ⦋ ( ↑ ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 = 𝐶 )
16	2	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐴 ∈ Fin )
17	5	biimpd	⊢ ( 𝜑 → ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) → ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 ) ) )
18	17	impl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝐾 ) → ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 ) )
19	18	simprd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 )
20	19	ex	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑘 ∈ 𝐾 → ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 ) )
21	18	simpld	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝐾 ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) )
22	21	simpld	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑝 ∈ ℙ )
23	22	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑝 ∈ ℙ )
24	21	simprd	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝐾 ) → 𝑘 ∈ ℕ )
25	24	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑘 ∈ ℕ )
26	24	ex	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑘 ∈ 𝐾 → 𝑘 ∈ ℕ ) )
27	26	ssrdv	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐾 ⊆ ℕ )
28	27	sselda	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝐾 ) → 𝑧 ∈ ℕ )
29	28	adantrl	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → 𝑧 ∈ ℕ )
30		eqid	⊢ 𝑝 = 𝑝
31		prmexpb	⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → ( ( 𝑝 ↑ 𝑘 ) = ( 𝑝 ↑ 𝑧 ) ↔ ( 𝑝 = 𝑝 ∧ 𝑘 = 𝑧 ) ) )
32	31	baibd	⊢ ( ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) ∧ 𝑝 = 𝑝 ) → ( ( 𝑝 ↑ 𝑘 ) = ( 𝑝 ↑ 𝑧 ) ↔ 𝑘 = 𝑧 ) )
33	30 32	mpan2	⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ) → ( ( 𝑝 ↑ 𝑘 ) = ( 𝑝 ↑ 𝑧 ) ↔ 𝑘 = 𝑧 ) )
34	23 23 25 29 33	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) ) → ( ( 𝑝 ↑ 𝑘 ) = ( 𝑝 ↑ 𝑧 ) ↔ 𝑘 = 𝑧 ) )
35	34	ex	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( 𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾 ) → ( ( 𝑝 ↑ 𝑘 ) = ( 𝑝 ↑ 𝑧 ) ↔ 𝑘 = 𝑧 ) ) )
36	20 35	dom2lem	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( 𝑘 ∈ 𝐾 ↦ ( 𝑝 ↑ 𝑘 ) ) : 𝐾 –1-1→ 𝐴 )
37		f1fi	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝑘 ∈ 𝐾 ↦ ( 𝑝 ↑ 𝑘 ) ) : 𝐾 –1-1→ 𝐴 ) → 𝐾 ∈ Fin )
38	16 36 37	syl2anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → 𝐾 ∈ Fin )
39	1	eleq1d	⊢ ( 𝑥 = ( 𝑝 ↑ 𝑘 ) → ( 𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
40	6	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℂ )
41	40	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℂ )
42	5	simplbda	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 )
43	39 41 42	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → 𝐶 ∈ ℂ )
44	15 4 38 43	fsum2d	⊢ ( 𝜑 → Σ 𝑝 ∈ 𝑃 Σ 𝑘 ∈ 𝐾 𝐶 = Σ 𝑧 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ⦋ ( ↑ ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
45		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
46		nfcv	⊢ Ⅎ 𝑦 𝐵
47		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
48	45 46 47	cbvsum	⊢ Σ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) 𝐵 = Σ 𝑦 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ⦋ 𝑦 / 𝑥 ⦌ 𝐵
49		csbeq1	⊢ ( 𝑦 = ( ↑ ‘ 𝑧 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ ( ↑ ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
50		snfi	⊢ { 𝑝 } ∈ Fin
51		xpfi	⊢ ( ( { 𝑝 } ∈ Fin ∧ 𝐾 ∈ Fin ) → ( { 𝑝 } × 𝐾 ) ∈ Fin )
52	50 38 51	sylancr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( { 𝑝 } × 𝐾 ) ∈ Fin )
53	52	ralrimiva	⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ∈ Fin )
54		iunfi	⊢ ( ( 𝑃 ∈ Fin ∧ ∀ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ∈ Fin ) → ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ∈ Fin )
55	4 53 54	syl2anc	⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ∈ Fin )
56		fvex	⊢ ( ↑ ‘ 𝑎 ) ∈ V
57	56	2a1i	⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) → ( ↑ ‘ 𝑎 ) ∈ V ) )
58		eliunxp	⊢ ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↔ ∃ 𝑝 ∃ 𝑘 ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) )
59	5	simprbda	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) )
60		opelxp	⊢ ( ⟨ 𝑝 , 𝑘 ⟩ ∈ ( ℙ × ℕ ) ↔ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) )
61	59 60	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ⟨ 𝑝 , 𝑘 ⟩ ∈ ( ℙ × ℕ ) )
62		eleq1	⊢ ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( 𝑎 ∈ ( ℙ × ℕ ) ↔ ⟨ 𝑝 , 𝑘 ⟩ ∈ ( ℙ × ℕ ) ) )
63	61 62	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → 𝑎 ∈ ( ℙ × ℕ ) ) )
64	63	impancom	⊢ ( ( 𝜑 ∧ 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ) → ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) → 𝑎 ∈ ( ℙ × ℕ ) ) )
65	64	expimpd	⊢ ( 𝜑 → ( ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → 𝑎 ∈ ( ℙ × ℕ ) ) )
66	65	exlimdvv	⊢ ( 𝜑 → ( ∃ 𝑝 ∃ 𝑘 ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → 𝑎 ∈ ( ℙ × ℕ ) ) )
67	58 66	biimtrid	⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) → 𝑎 ∈ ( ℙ × ℕ ) ) )
68	67	ssrdv	⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ⊆ ( ℙ × ℕ ) )
69	68	sseld	⊢ ( 𝜑 → ( 𝑏 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) → 𝑏 ∈ ( ℙ × ℕ ) ) )
70	67 69	anim12d	⊢ ( 𝜑 → ( ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ∧ 𝑏 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ) → ( 𝑎 ∈ ( ℙ × ℕ ) ∧ 𝑏 ∈ ( ℙ × ℕ ) ) ) )
71		1st2nd2	⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → 𝑎 = ⟨ ( 1^st ‘ 𝑎 ) , ( 2^nd ‘ 𝑎 ) ⟩ )
72	71	fveq2d	⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑎 ) = ( ↑ ‘ ⟨ ( 1^st ‘ 𝑎 ) , ( 2^nd ‘ 𝑎 ) ⟩ ) )
73		df-ov	⊢ ( ( 1^st ‘ 𝑎 ) ↑ ( 2^nd ‘ 𝑎 ) ) = ( ↑ ‘ ⟨ ( 1^st ‘ 𝑎 ) , ( 2^nd ‘ 𝑎 ) ⟩ )
74	72 73	eqtr4di	⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑎 ) = ( ( 1^st ‘ 𝑎 ) ↑ ( 2^nd ‘ 𝑎 ) ) )
75		1st2nd2	⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → 𝑏 = ⟨ ( 1^st ‘ 𝑏 ) , ( 2^nd ‘ 𝑏 ) ⟩ )
76	75	fveq2d	⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑏 ) = ( ↑ ‘ ⟨ ( 1^st ‘ 𝑏 ) , ( 2^nd ‘ 𝑏 ) ⟩ ) )
77		df-ov	⊢ ( ( 1^st ‘ 𝑏 ) ↑ ( 2^nd ‘ 𝑏 ) ) = ( ↑ ‘ ⟨ ( 1^st ‘ 𝑏 ) , ( 2^nd ‘ 𝑏 ) ⟩ )
78	76 77	eqtr4di	⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑏 ) = ( ( 1^st ‘ 𝑏 ) ↑ ( 2^nd ‘ 𝑏 ) ) )
79	74 78	eqeqan12d	⊢ ( ( 𝑎 ∈ ( ℙ × ℕ ) ∧ 𝑏 ∈ ( ℙ × ℕ ) ) → ( ( ↑ ‘ 𝑎 ) = ( ↑ ‘ 𝑏 ) ↔ ( ( 1^st ‘ 𝑎 ) ↑ ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ 𝑏 ) ↑ ( 2^nd ‘ 𝑏 ) ) ) )
80		xp1st	⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( 1^st ‘ 𝑎 ) ∈ ℙ )
81		xp2nd	⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( 2^nd ‘ 𝑎 ) ∈ ℕ )
82	80 81	jca	⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( ( 1^st ‘ 𝑎 ) ∈ ℙ ∧ ( 2^nd ‘ 𝑎 ) ∈ ℕ ) )
83		xp1st	⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( 1^st ‘ 𝑏 ) ∈ ℙ )
84		xp2nd	⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( 2^nd ‘ 𝑏 ) ∈ ℕ )
85	83 84	jca	⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( ( 1^st ‘ 𝑏 ) ∈ ℙ ∧ ( 2^nd ‘ 𝑏 ) ∈ ℕ ) )
86		prmexpb	⊢ ( ( ( ( 1^st ‘ 𝑎 ) ∈ ℙ ∧ ( 1^st ‘ 𝑏 ) ∈ ℙ ) ∧ ( ( 2^nd ‘ 𝑎 ) ∈ ℕ ∧ ( 2^nd ‘ 𝑏 ) ∈ ℕ ) ) → ( ( ( 1^st ‘ 𝑎 ) ↑ ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ 𝑏 ) ↑ ( 2^nd ‘ 𝑏 ) ) ↔ ( ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ∧ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ) )
87	86	an4s	⊢ ( ( ( ( 1^st ‘ 𝑎 ) ∈ ℙ ∧ ( 2^nd ‘ 𝑎 ) ∈ ℕ ) ∧ ( ( 1^st ‘ 𝑏 ) ∈ ℙ ∧ ( 2^nd ‘ 𝑏 ) ∈ ℕ ) ) → ( ( ( 1^st ‘ 𝑎 ) ↑ ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ 𝑏 ) ↑ ( 2^nd ‘ 𝑏 ) ) ↔ ( ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ∧ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ) )
88	82 85 87	syl2an	⊢ ( ( 𝑎 ∈ ( ℙ × ℕ ) ∧ 𝑏 ∈ ( ℙ × ℕ ) ) → ( ( ( 1^st ‘ 𝑎 ) ↑ ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ 𝑏 ) ↑ ( 2^nd ‘ 𝑏 ) ) ↔ ( ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ∧ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ) )
89		xpopth	⊢ ( ( 𝑎 ∈ ( ℙ × ℕ ) ∧ 𝑏 ∈ ( ℙ × ℕ ) ) → ( ( ( 1^st ‘ 𝑎 ) = ( 1^st ‘ 𝑏 ) ∧ ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ 𝑏 ) ) ↔ 𝑎 = 𝑏 ) )
90	79 88 89	3bitrd	⊢ ( ( 𝑎 ∈ ( ℙ × ℕ ) ∧ 𝑏 ∈ ( ℙ × ℕ ) ) → ( ( ↑ ‘ 𝑎 ) = ( ↑ ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) )
91	70 90	syl6	⊢ ( 𝜑 → ( ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ∧ 𝑏 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ) → ( ( ↑ ‘ 𝑎 ) = ( ↑ ‘ 𝑏 ) ↔ 𝑎 = 𝑏 ) ) )
92	57 91	dom2lem	⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) : ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) –1-1→ V )
93		f1f1orn	⊢ ( ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) : ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) –1-1→ V → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) : ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) –1-1-onto→ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) )
94	92 93	syl	⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) : ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) –1-1-onto→ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) )
95		fveq2	⊢ ( 𝑎 = 𝑧 → ( ↑ ‘ 𝑎 ) = ( ↑ ‘ 𝑧 ) )
96		eqid	⊢ ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) = ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) )
97		fvex	⊢ ( ↑ ‘ 𝑧 ) ∈ V
98	95 96 97	fvmpt	⊢ ( 𝑧 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) → ( ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ‘ 𝑧 ) = ( ↑ ‘ 𝑧 ) )
99	98	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ) → ( ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ‘ 𝑧 ) = ( ↑ ‘ 𝑧 ) )
100		fveq2	⊢ ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑎 ) = ( ↑ ‘ ⟨ 𝑝 , 𝑘 ⟩ ) )
101	100 10	eqtr4di	⊢ ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑎 ) = ( 𝑝 ↑ 𝑘 ) )
102	101	eleq1d	⊢ ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( ( ↑ ‘ 𝑎 ) ∈ 𝐴 ↔ ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 ) )
103	42 102	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
104	103	impancom	⊢ ( ( 𝜑 ∧ 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ) → ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
105	104	expimpd	⊢ ( 𝜑 → ( ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
106	105	exlimdvv	⊢ ( 𝜑 → ( ∃ 𝑝 ∃ 𝑘 ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
107	58 106	biimtrid	⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
108	107	imp	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 )
109	108	fmpttd	⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) : ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ⟶ 𝐴 )
110	109	frnd	⊢ ( 𝜑 → ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ⊆ 𝐴 )
111	110	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) → 𝑦 ∈ 𝐴 )
112	47	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ
113	45	eleq1d	⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
114	112 113	rspc	⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ℂ → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
115	40 114	mpan9	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ )
116	111 115	syldan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ )
117	49 55 94 99 116	fsumf1o	⊢ ( 𝜑 → Σ 𝑦 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = Σ 𝑧 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ⦋ ( ↑ ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
118	48 117	eqtrid	⊢ ( 𝜑 → Σ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) 𝐵 = Σ 𝑧 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ⦋ ( ↑ ‘ 𝑧 ) / 𝑥 ⦌ 𝐵 )
119	110	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) → 𝑥 ∈ 𝐴 )
120	119 6	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) → 𝐵 ∈ ℂ )
121		eldif	⊢ ( 𝑥 ∈ ( 𝐴 ∖ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) )
122	96 56	elrnmpti	⊢ ( 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ↔ ∃ 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) 𝑥 = ( ↑ ‘ 𝑎 ) )
123	101	eqeq2d	⊢ ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( 𝑥 = ( ↑ ‘ 𝑎 ) ↔ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) )
124	123	rexiunxp	⊢ ( ∃ 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) 𝑥 = ( ↑ ‘ 𝑎 ) ↔ ∃ 𝑝 ∈ 𝑃 ∃ 𝑘 ∈ 𝐾 𝑥 = ( 𝑝 ↑ 𝑘 ) )
125	122 124	bitri	⊢ ( 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ↔ ∃ 𝑝 ∈ 𝑃 ∃ 𝑘 ∈ 𝐾 𝑥 = ( 𝑝 ↑ 𝑘 ) )
126		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) → 𝑥 = ( 𝑝 ↑ 𝑘 ) )
127		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) → 𝑥 ∈ 𝐴 )
128	126 127	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) → ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 )
129	5	rbaibd	⊢ ( ( 𝜑 ∧ ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 ) → ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ↔ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) )
130	129	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 ) → ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ↔ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) )
131	128 130	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) → ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ↔ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) )
132	131	pm5.32da	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 = ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) ↔ ( 𝑥 = ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) ) )
133		ancom	⊢ ( ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) ↔ ( 𝑥 = ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) )
134		ancom	⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) ↔ ( 𝑥 = ( 𝑝 ↑ 𝑘 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ) )
135	132 133 134	3bitr4g	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) ) )
136	135	2exbidv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑝 ∃ 𝑘 ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) ↔ ∃ 𝑝 ∃ 𝑘 ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) ) )
137		r2ex	⊢ ( ∃ 𝑝 ∈ 𝑃 ∃ 𝑘 ∈ 𝐾 𝑥 = ( 𝑝 ↑ 𝑘 ) ↔ ∃ 𝑝 ∃ 𝑘 ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) )
138		r2ex	⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝑥 = ( 𝑝 ↑ 𝑘 ) ↔ ∃ 𝑝 ∃ 𝑘 ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) ∧ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) )
139	136 137 138	3bitr4g	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑝 ∈ 𝑃 ∃ 𝑘 ∈ 𝐾 𝑥 = ( 𝑝 ↑ 𝑘 ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) )
140	3	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℕ )
141		isppw2	⊢ ( 𝑥 ∈ ℕ → ( ( Λ ‘ 𝑥 ) ≠ 0 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) )
142	140 141	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( Λ ‘ 𝑥 ) ≠ 0 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝑥 = ( 𝑝 ↑ 𝑘 ) ) )
143	139 142	bitr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑝 ∈ 𝑃 ∃ 𝑘 ∈ 𝐾 𝑥 = ( 𝑝 ↑ 𝑘 ) ↔ ( Λ ‘ 𝑥 ) ≠ 0 ) )
144	125 143	bitrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ↔ ( Λ ‘ 𝑥 ) ≠ 0 ) )
145	144	necon2bbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( Λ ‘ 𝑥 ) = 0 ↔ ¬ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) )
146	145	pm5.32da	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ ( Λ ‘ 𝑥 ) = 0 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) ) )
147	7	ex	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ ( Λ ‘ 𝑥 ) = 0 ) → 𝐵 = 0 ) )
148	146 147	sylbird	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) → 𝐵 = 0 ) )
149	121 148	biimtrid	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) → 𝐵 = 0 ) )
150	149	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) ) → 𝐵 = 0 )
151	110 120 150 2	fsumss	⊢ ( 𝜑 → Σ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) 𝐵 = Σ 𝑥 ∈ 𝐴 𝐵 )
152	44 118 151	3eqtr2rd	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 𝐵 = Σ 𝑝 ∈ 𝑃 Σ 𝑘 ∈ 𝐾 𝐶 )

Metamath Proof Explorer

Theorem fsumvma

Proof