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 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 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 eqtr4di ( 𝑎 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑎 ) = ( ( 1st𝑎 ) ↑ ( 2nd𝑎 ) ) )
75 1st2nd2 ( 𝑏 ∈ ( ℙ × ℕ ) → 𝑏 = ⟨ ( 1st𝑏 ) , ( 2nd𝑏 ) ⟩ )
76 75 fveq2d ( 𝑏 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑏 ) = ( ↑ ‘ ⟨ ( 1st𝑏 ) , ( 2nd𝑏 ) ⟩ ) )
77 df-ov ( ( 1st𝑏 ) ↑ ( 2nd𝑏 ) ) = ( ↑ ‘ ⟨ ( 1st𝑏 ) , ( 2nd𝑏 ) ⟩ )
78 76 77 eqtr4di ( 𝑏 ∈ ( ℙ × ℕ ) → ( ↑ ‘ 𝑏 ) = ( ( 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 eqtr4di ( 𝑎 = ⟨ 𝑝 , 𝑘 ⟩ → ( ↑ ‘ 𝑎 ) = ( 𝑝𝑘 ) )
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 ( 𝜑 → Σ 𝑥𝐴 𝐵 = Σ 𝑝𝑃 Σ 𝑘𝐾 𝐶 )