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