Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  vmasum Structured version   Visualization version   GIF version

Theorem vmasum 25800
 Description: The sum of the von Mangoldt function over the divisors of 𝑛. Equation 9.2.4 of [Shapiro], p. 328 and theorem 2.10 in [ApostolNT] p. 32. (Contributed by Mario Carneiro, 15-Apr-2016.)
Assertion
Ref Expression
vmasum (𝐴 ∈ ℕ → Σ𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴} (Λ‘𝑛) = (log‘𝐴))
Distinct variable group:   𝑥,𝑛,𝐴

Proof of Theorem vmasum
Dummy variables 𝑘 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6645 . . 3 (𝑛 = (𝑝𝑘) → (Λ‘𝑛) = (Λ‘(𝑝𝑘)))
2 fzfid 13336 . . . 4 (𝐴 ∈ ℕ → (1...𝐴) ∈ Fin)
3 dvdsssfz1 15660 . . . 4 (𝐴 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥𝐴} ⊆ (1...𝐴))
42, 3ssfid 8725 . . 3 (𝐴 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥𝐴} ∈ Fin)
5 ssrab2 4007 . . . 4 {𝑥 ∈ ℕ ∣ 𝑥𝐴} ⊆ ℕ
65a1i 11 . . 3 (𝐴 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥𝐴} ⊆ ℕ)
7 inss1 4155 . . . 4 ((1...𝐴) ∩ ℙ) ⊆ (1...𝐴)
8 ssfi 8722 . . . 4 (((1...𝐴) ∈ Fin ∧ ((1...𝐴) ∩ ℙ) ⊆ (1...𝐴)) → ((1...𝐴) ∩ ℙ) ∈ Fin)
92, 7, 8sylancl 589 . . 3 (𝐴 ∈ ℕ → ((1...𝐴) ∩ ℙ) ∈ Fin)
10 pccl 16176 . . . . . . . . . 10 ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑝 pCnt 𝐴) ∈ ℕ0)
1110ancoms 462 . . . . . . . . 9 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈ ℕ0)
1211nn0zd 12073 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈ ℤ)
13 fznn 12970 . . . . . . . 8 ((𝑝 pCnt 𝐴) ∈ ℤ → (𝑘 ∈ (1...(𝑝 pCnt 𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))))
1412, 13syl 17 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑘 ∈ (1...(𝑝 pCnt 𝐴)) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))))
1514anbi2d 631 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)))))
16 an12 644 . . . . . . 7 ((𝑝 ∈ (1...𝐴) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))))
17 prmz 16009 . . . . . . . . . . . . . . 15 (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
1817adantl 485 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℤ)
19 iddvdsexp 15625 . . . . . . . . . . . . . 14 ((𝑝 ∈ ℤ ∧ 𝑘 ∈ ℕ) → 𝑝 ∥ (𝑝𝑘))
2018, 19sylan 583 . . . . . . . . . . . . 13 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∥ (𝑝𝑘))
2117ad2antlr 726 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℤ)
22 prmnn 16008 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
2322adantl 485 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
24 nnnn0 11892 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
25 nnexpcl 13438 . . . . . . . . . . . . . . . 16 ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (𝑝𝑘) ∈ ℕ)
2623, 24, 25syl2an 598 . . . . . . . . . . . . . . 15 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℕ)
2726nnzd 12074 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℤ)
28 nnz 11992 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
2928ad2antrr 725 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℤ)
30 dvdstr 15638 . . . . . . . . . . . . . 14 ((𝑝 ∈ ℤ ∧ (𝑝𝑘) ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝑝 ∥ (𝑝𝑘) ∧ (𝑝𝑘) ∥ 𝐴) → 𝑝𝐴))
3121, 27, 29, 30syl3anc 1368 . . . . . . . . . . . . 13 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝 ∥ (𝑝𝑘) ∧ (𝑝𝑘) ∥ 𝐴) → 𝑝𝐴))
3220, 31mpand 694 . . . . . . . . . . . 12 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝𝑘) ∥ 𝐴𝑝𝐴))
33 simpll 766 . . . . . . . . . . . . 13 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℕ)
34 dvdsle 15652 . . . . . . . . . . . . 13 ((𝑝 ∈ ℤ ∧ 𝐴 ∈ ℕ) → (𝑝𝐴𝑝𝐴))
3521, 33, 34syl2anc 587 . . . . . . . . . . . 12 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝𝐴𝑝𝐴))
3632, 35syld 47 . . . . . . . . . . 11 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝𝑘) ∥ 𝐴𝑝𝐴))
3722ad2antlr 726 . . . . . . . . . . . 12 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ)
38 fznn 12970 . . . . . . . . . . . . 13 (𝐴 ∈ ℤ → (𝑝 ∈ (1...𝐴) ↔ (𝑝 ∈ ℕ ∧ 𝑝𝐴)))
3938baibd 543 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ℕ) → (𝑝 ∈ (1...𝐴) ↔ 𝑝𝐴))
4029, 37, 39syl2anc 587 . . . . . . . . . . 11 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑝 ∈ (1...𝐴) ↔ 𝑝𝐴))
4136, 40sylibrd 262 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝𝑘) ∥ 𝐴𝑝 ∈ (1...𝐴)))
4241pm4.71rd 566 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝𝑘) ∥ 𝐴 ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑝𝑘) ∥ 𝐴)))
43 breq1 5033 . . . . . . . . . . 11 (𝑥 = (𝑝𝑘) → (𝑥𝐴 ↔ (𝑝𝑘) ∥ 𝐴))
4443elrab3 3629 . . . . . . . . . 10 ((𝑝𝑘) ∈ ℕ → ((𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴} ↔ (𝑝𝑘) ∥ 𝐴))
4526, 44syl 17 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴} ↔ (𝑝𝑘) ∥ 𝐴))
46 simplr 768 . . . . . . . . . . 11 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℙ)
4724adantl 485 . . . . . . . . . . 11 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0)
48 pcdvdsb 16195 . . . . . . . . . . 11 ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → (𝑘 ≤ (𝑝 pCnt 𝐴) ↔ (𝑝𝑘) ∥ 𝐴))
4946, 29, 47, 48syl3anc 1368 . . . . . . . . . 10 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → (𝑘 ≤ (𝑝 pCnt 𝐴) ↔ (𝑝𝑘) ∥ 𝐴))
5049anbi2d 631 . . . . . . . . 9 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)) ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑝𝑘) ∥ 𝐴)))
5142, 45, 503bitr4rd 315 . . . . . . . 8 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ ℕ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴)) ↔ (𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴}))
5251pm5.32da 582 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑘 ∈ ℕ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴})))
5316, 52syl5bb 286 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 ∈ (1...𝐴) ∧ (𝑘 ∈ ℕ ∧ 𝑘 ≤ (𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴})))
5415, 53bitrd 282 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ℙ) → ((𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑘 ∈ ℕ ∧ (𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴})))
5554pm5.32da 582 . . . 4 (𝐴 ∈ ℕ → ((𝑝 ∈ ℙ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))) ↔ (𝑝 ∈ ℙ ∧ (𝑘 ∈ ℕ ∧ (𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴}))))
56 elin 3897 . . . . . 6 (𝑝 ∈ ((1...𝐴) ∩ ℙ) ↔ (𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ))
5756anbi1i 626 . . . . 5 ((𝑝 ∈ ((1...𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ ((𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))))
58 anass 472 . . . . 5 (((𝑝 ∈ (1...𝐴) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑝 ∈ (1...𝐴) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))))
59 an12 644 . . . . 5 ((𝑝 ∈ (1...𝐴) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))) ↔ (𝑝 ∈ ℙ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))))
6057, 58, 593bitri 300 . . . 4 ((𝑝 ∈ ((1...𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ (𝑝 ∈ ℙ ∧ (𝑝 ∈ (1...𝐴) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴)))))
61 anass 472 . . . 4 (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴}) ↔ (𝑝 ∈ ℙ ∧ (𝑘 ∈ ℕ ∧ (𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴})))
6255, 60, 613bitr4g 317 . . 3 (𝐴 ∈ ℕ → ((𝑝 ∈ ((1...𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴})))
636sselda 3915 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴}) → 𝑛 ∈ ℕ)
64 vmacl 25703 . . . . 5 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
6563, 64syl 17 . . . 4 ((𝐴 ∈ ℕ ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴}) → (Λ‘𝑛) ∈ ℝ)
6665recnd 10658 . . 3 ((𝐴 ∈ ℕ ∧ 𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴}) → (Λ‘𝑛) ∈ ℂ)
67 simprr 772 . . 3 ((𝐴 ∈ ℕ ∧ (𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴} ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0)
681, 4, 6, 9, 62, 66, 67fsumvma 25797 . 2 (𝐴 ∈ ℕ → Σ𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴} (Λ‘𝑛) = Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝𝑘)))
69 elinel2 4123 . . . . . . 7 (𝑝 ∈ ((1...𝐴) ∩ ℙ) → 𝑝 ∈ ℙ)
7069ad2antlr 726 . . . . . 6 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) → 𝑝 ∈ ℙ)
71 elfznn 12931 . . . . . . 7 (𝑘 ∈ (1...(𝑝 pCnt 𝐴)) → 𝑘 ∈ ℕ)
7271adantl 485 . . . . . 6 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) → 𝑘 ∈ ℕ)
73 vmappw 25701 . . . . . 6 ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
7470, 72, 73syl2anc 587 . . . . 5 (((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(𝑝 pCnt 𝐴))) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
7574sumeq2dv 15052 . . . 4 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝𝑘)) = Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(log‘𝑝))
76 fzfid 13336 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (1...(𝑝 pCnt 𝐴)) ∈ Fin)
7769, 22syl 17 . . . . . . . . 9 (𝑝 ∈ ((1...𝐴) ∩ ℙ) → 𝑝 ∈ ℕ)
7877adantl 485 . . . . . . . 8 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ)
7978nnrpd 12417 . . . . . . 7 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+)
8079relogcld 25214 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
8180recnd 10658 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℂ)
82 fsumconst 15137 . . . . 5 (((1...(𝑝 pCnt 𝐴)) ∈ Fin ∧ (log‘𝑝) ∈ ℂ) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(log‘𝑝) = ((♯‘(1...(𝑝 pCnt 𝐴))) · (log‘𝑝)))
8376, 81, 82syl2anc 587 . . . 4 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(log‘𝑝) = ((♯‘(1...(𝑝 pCnt 𝐴))) · (log‘𝑝)))
8469, 11sylan2 595 . . . . . 6 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (𝑝 pCnt 𝐴) ∈ ℕ0)
85 hashfz1 13702 . . . . . 6 ((𝑝 pCnt 𝐴) ∈ ℕ0 → (♯‘(1...(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴))
8684, 85syl 17 . . . . 5 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → (♯‘(1...(𝑝 pCnt 𝐴))) = (𝑝 pCnt 𝐴))
8786oveq1d 7150 . . . 4 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → ((♯‘(1...(𝑝 pCnt 𝐴))) · (log‘𝑝)) = ((𝑝 pCnt 𝐴) · (log‘𝑝)))
8875, 83, 873eqtrd 2837 . . 3 ((𝐴 ∈ ℕ ∧ 𝑝 ∈ ((1...𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝𝑘)) = ((𝑝 pCnt 𝐴) · (log‘𝑝)))
8988sumeq2dv 15052 . 2 (𝐴 ∈ ℕ → Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(𝑝 pCnt 𝐴))(Λ‘(𝑝𝑘)) = Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝)))
90 pclogsum 25799 . 2 (𝐴 ∈ ℕ → Σ𝑝 ∈ ((1...𝐴) ∩ ℙ)((𝑝 pCnt 𝐴) · (log‘𝑝)) = (log‘𝐴))
9168, 89, 903eqtrd 2837 1 (𝐴 ∈ ℕ → Σ𝑛 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐴} (Λ‘𝑛) = (log‘𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {crab 3110   ∩ cin 3880   ⊆ wss 3881   class class class wbr 5030  ‘cfv 6324  (class class class)co 7135  Fincfn 8492  ℂcc 10524  ℝcr 10525  0cc0 10526  1c1 10527   · cmul 10531   ≤ cle 10665  ℕcn 11625  ℕ0cn0 11885  ℤcz 11969  ...cfz 12885  ↑cexp 13425  ♯chash 13686  Σcsu 15034   ∥ cdvds 15599  ℙcprime 16005   pCnt cpc 16163  logclog 25146  Λcvma 25677 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-fi 8859  df-sup 8890  df-inf 8891  df-oi 8958  df-dju 9314  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426  df-fac 13630  df-bc 13659  df-hash 13687  df-shft 14418  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-limsup 14820  df-clim 14837  df-rlim 14838  df-sum 15035  df-ef 15413  df-sin 15415  df-cos 15416  df-pi 15418  df-dvds 15600  df-gcd 15834  df-prm 16006  df-pc 16164  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-mulg 18217  df-cntz 18439  df-cmn 18900  df-psmet 20083  df-xmet 20084  df-met 20085  df-bl 20086  df-mopn 20087  df-fbas 20088  df-fg 20089  df-cnfld 20092  df-top 21499  df-topon 21516  df-topsp 21538  df-bases 21551  df-cld 21624  df-ntr 21625  df-cls 21626  df-nei 21703  df-lp 21741  df-perf 21742  df-cn 21832  df-cnp 21833  df-haus 21920  df-tx 22167  df-hmeo 22360  df-fil 22451  df-fm 22543  df-flim 22544  df-flf 22545  df-xms 22927  df-ms 22928  df-tms 22929  df-cncf 23483  df-limc 24469  df-dv 24470  df-log 25148  df-vma 25683 This theorem is referenced by:  logfac2  25801  dchrvmasumlem1  26079  vmalogdivsum2  26122  logsqvma  26126
 Copyright terms: Public domain W3C validator