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 ⊢ 𝑆 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 }
Assertion vmaval ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) = if ( ( ♯ ‘ 𝑆 ) = 1 , ( log ‘ ∪ 𝑆 ) , 0 ) )

Proof

Step Hyp Ref Expression
1 vmaval.1 ⊢ 𝑆 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 }
2 prmex ⊢ ℙ ∈ V
3 2 rabex ⊢ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ∈ V
4 3 a1i ⊢ ( 𝑥 = 𝐴 → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ∈ V )
5 id ⊢ ( 𝑠 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } → 𝑠 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } )
6 breq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑝 ∥ 𝑥 ↔ 𝑝 ∥ 𝐴 ) )
7 6 rabbidv ⊢ ( 𝑥 = 𝐴 → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐴 } )
8 7 1 eqtr4di ⊢ ( 𝑥 = 𝐴 → { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } = 𝑆 )
9 5 8 sylan9eqr ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑠 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) → 𝑠 = 𝑆 )
10 9 fveqeq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑠 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) → ( ( ♯ ‘ 𝑠 ) = 1 ↔ ( ♯ ‘ 𝑆 ) = 1 ) )
11 9 unieqd ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑠 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) → ∪ 𝑠 = ∪ 𝑆 )
12 11 fveq2d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑠 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) → ( log ‘ ∪ 𝑠 ) = ( log ‘ ∪ 𝑆 ) )
13 10 12 ifbieq1d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑠 = { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } ) → if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) = if ( ( ♯ ‘ 𝑆 ) = 1 , ( log ‘ ∪ 𝑆 ) , 0 ) )
14 4 13 csbied ⊢ ( 𝑥 = 𝐴 → ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) = if ( ( ♯ ‘ 𝑆 ) = 1 , ( log ‘ ∪ 𝑆 ) , 0 ) )
15 df-vma ⊢ Λ = ( 𝑥 ∈ ℕ ↦ ⦋ { 𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑥 } / 𝑠 ⦌ if ( ( ♯ ‘ 𝑠 ) = 1 , ( log ‘ ∪ 𝑠 ) , 0 ) )
16 fvex ⊢ ( log ‘ ∪ 𝑆 ) ∈ V
17 c0ex ⊢ 0 ∈ V
18 16 17 ifex ⊢ if ( ( ♯ ‘ 𝑆 ) = 1 , ( log ‘ ∪ 𝑆 ) , 0 ) ∈ V
19 14 15 18 fvmpt ⊢ ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) = if ( ( ♯ ‘ 𝑆 ) = 1 , ( log ‘ ∪ 𝑆 ) , 0 ) )