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 ‘ 𝐴 ) )