Metamath Proof Explorer

Theorem 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 syl6eqr ⊢ ( 𝑧 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑧 ) = ( 𝑝 ↑ 𝑘 ) )
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 nfcv ⊢ Ⅎ 𝑦 𝐵
46 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
47 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
48 45 46 47 cbvsumi ⊢ Σ 𝑥 ∈ 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 syl5bi ⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) → 𝑎 ∈ ( ℙ × ℕ ) ) )
68 67 ssrdv ⊢ ( 𝜑 → ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ⊆ ( ℙ × ℕ ) )
69 68 sseld ⊢ ( 𝜑 → ( 𝑏 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) → 𝑏 ∈ ( ℙ × ℕ ) ) )
70 67 69 anim12d ⊢ ( 𝜑 → ( ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ∧ 𝑏 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ) → ( 𝑎 ∈ ( ℙ × ℕ ) ∧ 𝑏 ∈ ( ℙ × ℕ ) ) ) )
71 1st2nd2 ⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → 𝑎 = ⟨ ( 1st ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ )
72 71 fveq2d ⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑎 ) = ( ↑ ‘ ⟨ ( 1st ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ ) )
73 df-ov ⊢ ( ( 1st ‘ 𝑎 ) ↑ ( 2nd ‘ 𝑎 ) ) = ( ↑ ‘ ⟨ ( 1st ‘ 𝑎 ) , ( 2nd ‘ 𝑎 ) ⟩ )
74 72 73 syl6eqr ⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑎 ) = ( ( 1st ‘ 𝑎 ) ↑ ( 2nd ‘ 𝑎 ) ) )
75 1st2nd2 ⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → 𝑏 = ⟨ ( 1st ‘ 𝑏 ) , ( 2nd ‘ 𝑏 ) ⟩ )
76 75 fveq2d ⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑏 ) = ( ↑ ‘ ⟨ ( 1st ‘ 𝑏 ) , ( 2nd ‘ 𝑏 ) ⟩ ) )
77 df-ov ⊢ ( ( 1st ‘ 𝑏 ) ↑ ( 2nd ‘ 𝑏 ) ) = ( ↑ ‘ ⟨ ( 1st ‘ 𝑏 ) , ( 2nd ‘ 𝑏 ) ⟩ )
78 76 77 syl6eqr ⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑏 ) = ( ( 1st ‘ 𝑏 ) ↑ ( 2nd ‘ 𝑏 ) ) )
79 74 78 eqeqan12d ⊢ ( ( 𝑎 ∈ ( ℙ × ℕ ) ∧ 𝑏 ∈ ( ℙ × ℕ ) ) → ( ( ↑ ‘ 𝑎 ) = ( ↑ ‘ 𝑏 ) ↔ ( ( 1st ‘ 𝑎 ) ↑ ( 2nd ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑏 ) ↑ ( 2nd ‘ 𝑏 ) ) ) )
80 xp1st ⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( 1st ‘ 𝑎 ) ∈ ℙ )
81 xp2nd ⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( 2nd ‘ 𝑎 ) ∈ ℕ )
82 80 81 jca ⊢ ( 𝑎 ∈ ( ℙ × ℕ ) → ( ( 1st ‘ 𝑎 ) ∈ ℙ ∧ ( 2nd ‘ 𝑎 ) ∈ ℕ ) )
83 xp1st ⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( 1st ‘ 𝑏 ) ∈ ℙ )
84 xp2nd ⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( 2nd ‘ 𝑏 ) ∈ ℕ )
85 83 84 jca ⊢ ( 𝑏 ∈ ( ℙ × ℕ ) → ( ( 1st ‘ 𝑏 ) ∈ ℙ ∧ ( 2nd ‘ 𝑏 ) ∈ ℕ ) )
86 prmexpb ⊢ ( ( ( ( 1st ‘ 𝑎 ) ∈ ℙ ∧ ( 1st ‘ 𝑏 ) ∈ ℙ ) ∧ ( ( 2nd ‘ 𝑎 ) ∈ ℕ ∧ ( 2nd ‘ 𝑏 ) ∈ ℕ ) ) → ( ( ( 1st ‘ 𝑎 ) ↑ ( 2nd ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑏 ) ↑ ( 2nd ‘ 𝑏 ) ) ↔ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) = ( 2nd ‘ 𝑏 ) ) ) )
87 86 an4s ⊢ ( ( ( ( 1st ‘ 𝑎 ) ∈ ℙ ∧ ( 2nd ‘ 𝑎 ) ∈ ℕ ) ∧ ( ( 1st ‘ 𝑏 ) ∈ ℙ ∧ ( 2nd ‘ 𝑏 ) ∈ ℕ ) ) → ( ( ( 1st ‘ 𝑎 ) ↑ ( 2nd ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑏 ) ↑ ( 2nd ‘ 𝑏 ) ) ↔ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) = ( 2nd ‘ 𝑏 ) ) ) )
88 82 85 87 syl2an ⊢ ( ( 𝑎 ∈ ( ℙ × ℕ ) ∧ 𝑏 ∈ ( ℙ × ℕ ) ) → ( ( ( 1st ‘ 𝑎 ) ↑ ( 2nd ‘ 𝑎 ) ) = ( ( 1st ‘ 𝑏 ) ↑ ( 2nd ‘ 𝑏 ) ) ↔ ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) = ( 2nd ‘ 𝑏 ) ) ) )
89 xpopth ⊢ ( ( 𝑎 ∈ ( ℙ × ℕ ) ∧ 𝑏 ∈ ( ℙ × ℕ ) ) → ( ( ( 1st ‘ 𝑎 ) = ( 1st ‘ 𝑏 ) ∧ ( 2nd ‘ 𝑎 ) = ( 2nd ‘ 𝑏 ) ) ↔ 𝑎 = 𝑏 ) )
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 syl6eqr ⊢ ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑎 ) = ( 𝑝 ↑ 𝑘 ) )
102 101 eleq1d ⊢ ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( ( ↑ ‘ 𝑎 ) ∈ 𝐴 ↔ ( 𝑝 ↑ 𝑘 ) ∈ 𝐴 ) )
103 42 102 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
104 103 impancom ⊢ ( ( 𝜑 ∧ 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ) → ( ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
105 104 expimpd ⊢ ( 𝜑 → ( ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
106 105 exlimdvv ⊢ ( 𝜑 → ( ∃ 𝑝 ∃ 𝑘 ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑘 ∈ 𝐾 ) ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
107 58 106 syl5bi ⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 ) )
108 107 imp ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ) → ( ↑ ‘ 𝑎 ) ∈ 𝐴 )
109 108 fmpttd ⊢ ( 𝜑 → ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) : ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ⟶ 𝐴 )
110 109 frnd ⊢ ( 𝜑 → ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ⊆ 𝐴 )
111 110 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) → 𝑦 ∈ 𝐴 )
112 46 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ ℂ
113 47 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 syl5eq ⊢ ( 𝜑 → Σ 𝑥 ∈ 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 syl5bb ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 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 syl5bi ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) → 𝐵 = 0 ) )
150 149 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) ) ) → 𝐵 = 0 )
151 110 120 150 2 fsumss ⊢ ( 𝜑 → Σ 𝑥 ∈ ran ( 𝑎 ∈ ∪ 𝑝 ∈ 𝑃 ( { 𝑝 } × 𝐾 ) ↦ ( ↑ ‘ 𝑎 ) ) 𝐵 = Σ 𝑥 ∈ 𝐴 𝐵 )
152 44 118 151 3eqtr2rd ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 𝐵 = Σ 𝑝 ∈ 𝑃 Σ 𝑘 ∈ 𝐾 𝐶 )