Metamath Proof Explorer

Theorem pclogsum

Description: The logarithmic analogue of pcprod . The sum of the logarithms of the primes dividing A multiplied by their powers yields the logarithm of A . (Contributed by Mario Carneiro, 15-Apr-2016)

Ref Expression
Assertion pclogsum ( 𝐴 ∈ ℕ → Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) = ( log ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ↔ ( 𝑝 ∈ ( 1 ... 𝐴 ) ∧ 𝑝 ∈ ℙ ) )
2 1 baib ⊢ ( 𝑝 ∈ ( 1 ... 𝐴 ) → ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ↔ 𝑝 ∈ ℙ ) )
3 2 ifbid ⊢ ( 𝑝 ∈ ( 1 ... 𝐴 ) → if ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 ) = if ( 𝑝 ∈ ℙ , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 ) )
4 fvif ⊢ ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) = if ( 𝑝 ∈ ℙ , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , ( log ‘ 1 ) )
5 log1 ⊢ ( log ‘ 1 ) = 0
6 ifeq2 ⊢ ( ( log ‘ 1 ) = 0 → if ( 𝑝 ∈ ℙ , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , ( log ‘ 1 ) ) = if ( 𝑝 ∈ ℙ , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 ) )
7 5 6 ax-mp ⊢ if ( 𝑝 ∈ ℙ , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , ( log ‘ 1 ) ) = if ( 𝑝 ∈ ℙ , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 )
8 4 7 eqtri ⊢ ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) = if ( 𝑝 ∈ ℙ , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 )
9 3 8 eqtr4di ⊢ ( 𝑝 ∈ ( 1 ... 𝐴 ) → if ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 ) = ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) )
10 9 sumeq2i ⊢ Σ 𝑝 ∈ ( 1 ... 𝐴 ) if ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 ) = Σ 𝑝 ∈ ( 1 ... 𝐴 ) ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) )
11 inss1 ⊢ ( ( 1 ... 𝐴 ) ∩ ℙ ) ⊆ ( 1 ... 𝐴 )
12 simpr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) )
13 12 elin1d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 1 ... 𝐴 ) )
14 elfznn ⊢ ( 𝑝 ∈ ( 1 ... 𝐴 ) → 𝑝 ∈ ℕ )
15 13 14 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
16 12 elin2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
17 simpl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℕ )
18 16 17 pccld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
19 15 18 nnexpcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ ℕ )
20 19 nnrpd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ ℝ+ )
21 20 relogcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) ∈ ℝ )
22 21 recnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) ∈ ℂ )
23 22 ralrimiva ⊢ ( 𝐴 ∈ ℕ → ∀ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) ∈ ℂ )
24 fzfi ⊢ ( 1 ... 𝐴 ) ∈ Fin
25 24 olci ⊢ ( ( 1 ... 𝐴 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... 𝐴 ) ∈ Fin )
26 sumss2 ⊢ ( ( ( ( ( 1 ... 𝐴 ) ∩ ℙ ) ⊆ ( 1 ... 𝐴 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) ∈ ℂ ) ∧ ( ( 1 ... 𝐴 ) ⊆ ( ℤ≥ ‘ 1 ) ∨ ( 1 ... 𝐴 ) ∈ Fin ) ) → Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = Σ 𝑝 ∈ ( 1 ... 𝐴 ) if ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 ) )
27 25 26 mpan2 ⊢ ( ( ( ( 1 ... 𝐴 ) ∩ ℙ ) ⊆ ( 1 ... 𝐴 ) ∧ ∀ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) ∈ ℂ ) → Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = Σ 𝑝 ∈ ( 1 ... 𝐴 ) if ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 ) )
28 11 23 27 sylancr ⊢ ( 𝐴 ∈ ℕ → Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = Σ 𝑝 ∈ ( 1 ... 𝐴 ) if ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 ) )
29 15 nnrpd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
30 18 nn0zd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( 𝑝 pCnt 𝐴 ) ∈ ℤ )
31 relogexp ⊢ ( ( 𝑝 ∈ ℝ+ ∧ ( 𝑝 pCnt 𝐴 ) ∈ ℤ ) → ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) )
32 29 30 31 syl2anc ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ) → ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) )
33 32 sumeq2dv ⊢ ( 𝐴 ∈ ℕ → Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) = Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) )
34 28 33 eqtr3d ⊢ ( 𝐴 ∈ ℕ → Σ 𝑝 ∈ ( 1 ... 𝐴 ) if ( 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) , ( log ‘ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ) , 0 ) = Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) )
35 14 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → 𝑝 ∈ ℕ )
36 eleq1w ⊢ ( 𝑛 = 𝑝 → ( 𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ ) )
37 id ⊢ ( 𝑛 = 𝑝 → 𝑛 = 𝑝 )
38 oveq1 ⊢ ( 𝑛 = 𝑝 → ( 𝑛 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐴 ) )
39 37 38 oveq12d ⊢ ( 𝑛 = 𝑝 → ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) = ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) )
40 36 39 ifbieq1d ⊢ ( 𝑛 = 𝑝 → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) )
41 40 fveq2d ⊢ ( 𝑛 = 𝑝 → ( log ‘ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) = ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) )
42 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( log ‘ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( log ‘ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) )
43 fvex ⊢ ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) ∈ V
44 41 42 43 fvmpt ⊢ ( 𝑝 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( log ‘ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ) ‘ 𝑝 ) = ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) )
45 35 44 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( log ‘ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ) ‘ 𝑝 ) = ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) )
46 elnnuz ⊢ ( 𝐴 ∈ ℕ ↔ 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
47 46 biimpi ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
48 35 adantr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℕ )
49 simpr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
50 simpll ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℕ )
51 49 50 pccld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
52 48 51 nnexpcld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ ℕ )
53 1nn ⊢ 1 ∈ ℕ
54 53 a1i ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) ∧ ¬ 𝑝 ∈ ℙ ) → 1 ∈ ℕ )
55 52 54 ifclda ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ∈ ℕ )
56 55 nnrpd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ∈ ℝ+ )
57 56 relogcld ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) ∈ ℝ )
58 57 recnd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) ∈ ℂ )
59 45 47 58 fsumser ⊢ ( 𝐴 ∈ ℕ → Σ 𝑝 ∈ ( 1 ... 𝐴 ) ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( log ‘ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ) ) ‘ 𝐴 ) )
60 rpmulcl ⊢ ( ( 𝑝 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( 𝑝 · 𝑚 ) ∈ ℝ+ )
61 60 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑝 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) ) → ( 𝑝 · 𝑚 ) ∈ ℝ+ )
62 eqid ⊢ ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) )
63 ovex ⊢ ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) ∈ V
64 1ex ⊢ 1 ∈ V
65 63 64 ifex ⊢ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ∈ V
66 40 62 65 fvmpt ⊢ ( 𝑝 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ‘ 𝑝 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) )
67 35 66 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ‘ 𝑝 ) = if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) )
68 67 56 eqeltrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ‘ 𝑝 ) ∈ ℝ+ )
69 relogmul ⊢ ( ( 𝑝 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( log ‘ ( 𝑝 · 𝑚 ) ) = ( ( log ‘ 𝑝 ) + ( log ‘ 𝑚 ) ) )
70 69 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝑝 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) ) → ( log ‘ ( 𝑝 · 𝑚 ) ) = ( ( log ‘ 𝑝 ) + ( log ‘ 𝑚 ) ) )
71 67 fveq2d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → ( log ‘ ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ‘ 𝑝 ) ) = ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) )
72 71 45 eqtr4d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑝 ∈ ( 1 ... 𝐴 ) ) → ( log ‘ ( ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ‘ 𝑝 ) ) = ( ( 𝑛 ∈ ℕ ↦ ( log ‘ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ) ‘ 𝑝 ) )
73 61 68 47 70 72 seqhomo ⊢ ( 𝐴 ∈ ℕ → ( log ‘ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ) ‘ 𝐴 ) ) = ( seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( log ‘ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ) ) ‘ 𝐴 ) )
74 62 pcprod ⊢ ( 𝐴 ∈ ℕ → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ) ‘ 𝐴 ) = 𝐴 )
75 74 fveq2d ⊢ ( 𝐴 ∈ ℕ → ( log ‘ ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝐴 ) ) , 1 ) ) ) ‘ 𝐴 ) ) = ( log ‘ 𝐴 ) )
76 59 73 75 3eqtr2d ⊢ ( 𝐴 ∈ ℕ → Σ 𝑝 ∈ ( 1 ... 𝐴 ) ( log ‘ if ( 𝑝 ∈ ℙ , ( 𝑝 ↑ ( 𝑝 pCnt 𝐴 ) ) , 1 ) ) = ( log ‘ 𝐴 ) )
77 10 34 76 3eqtr3a ⊢ ( 𝐴 ∈ ℕ → Σ 𝑝 ∈ ( ( 1 ... 𝐴 ) ∩ ℙ ) ( ( 𝑝 pCnt 𝐴 ) · ( log ‘ 𝑝 ) ) = ( log ‘ 𝐴 ) )