This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vmaval

Description: Value of the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Hypothesis vmaval.1 ⊢ S = p ∈ ℙ | p ∥ A
Assertion vmaval ⊢ A ∈ ℕ → Λ ⁡ A = if S = 1 log ⁡ ⋃ S 0

Proof

Step Hyp Ref Expression
1 vmaval.1 ⊢ S = p ∈ ℙ | p ∥ A
2 prmex ⊢ ℙ ∈ V
3 2 rabex ⊢ p ∈ ℙ | p ∥ x ∈ V
4 3 a1i ⊢ x = A → p ∈ ℙ | p ∥ x ∈ V
5 id ⊢ s = p ∈ ℙ | p ∥ x → s = p ∈ ℙ | p ∥ x
6 breq2 ⊢ x = A → p ∥ x ↔ p ∥ A
7 6 rabbidv ⊢ x = A → p ∈ ℙ | p ∥ x = p ∈ ℙ | p ∥ A
8 7 1 eqtr4di ⊢ x = A → p ∈ ℙ | p ∥ x = S
9 5 8 sylan9eqr ⊢ x = A ∧ s = p ∈ ℙ | p ∥ x → s = S
10 9 fveqeq2d ⊢ x = A ∧ s = p ∈ ℙ | p ∥ x → s = 1 ↔ S = 1
11 9 unieqd ⊢ x = A ∧ s = p ∈ ℙ | p ∥ x → ⋃ s = ⋃ S
12 11 fveq2d ⊢ x = A ∧ s = p ∈ ℙ | p ∥ x → log ⁡ ⋃ s = log ⁡ ⋃ S
13 10 12 ifbieq1d ⊢ x = A ∧ s = p ∈ ℙ | p ∥ x → if s = 1 log ⁡ ⋃ s 0 = if S = 1 log ⁡ ⋃ S 0
14 4 13 csbied ⊢ x = A → ⦋ p ∈ ℙ | p ∥ x / s⦌ if s = 1 log ⁡ ⋃ s 0 = if S = 1 log ⁡ ⋃ S 0
15 df-vma ⊢ Λ = x ∈ ℕ ⟼ ⦋ p ∈ ℙ | p ∥ x / s⦌ if s = 1 log ⁡ ⋃ s 0
16 fvex ⊢ log ⁡ ⋃ S ∈ V
17 c0ex ⊢ 0 ∈ V
18 16 17 ifex ⊢ if S = 1 log ⁡ ⋃ S 0 ∈ V
19 14 15 18 fvmpt ⊢ A ∈ ℕ → Λ ⁡ A = if S = 1 log ⁡ ⋃ S 0