Theorem logsqvma

Description: A formula for log ^ 2 ( N ) in terms of the primes. Equation 10.4.6 of Shapiro, p. 418. (Contributed by Mario Carneiro, 13-May-2016)

	Ref	Expression
Assertion	logsqvma	⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) + ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) = ( ( log ‘ 𝑁 ) ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		fzfid	⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
2		dvdsssfz1	⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
3	1 2	ssfid	⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∈ Fin )
4		fzfid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 1 ... 𝑑 ) ∈ Fin )
5		elrabi	⊢ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → 𝑑 ∈ ℕ )
6	5	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑑 ∈ ℕ )
7		dvdsssfz1	⊢ ( 𝑑 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ⊆ ( 1 ... 𝑑 ) )
8	6 7	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ⊆ ( 1 ... 𝑑 ) )
9	4 8	ssfid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ∈ Fin )
10		elrabi	⊢ ( 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } → 𝑢 ∈ ℕ )
11	10	ad2antll	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → 𝑢 ∈ ℕ )
12		vmacl	⊢ ( 𝑢 ∈ ℕ → ( Λ ‘ 𝑢 ) ∈ ℝ )
13	11 12	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( Λ ‘ 𝑢 ) ∈ ℝ )
14		breq1	⊢ ( 𝑥 = 𝑢 → ( 𝑥 ∥ 𝑑 ↔ 𝑢 ∥ 𝑑 ) )
15	14	elrab	⊢ ( 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ↔ ( 𝑢 ∈ ℕ ∧ 𝑢 ∥ 𝑑 ) )
16	15	simprbi	⊢ ( 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } → 𝑢 ∥ 𝑑 )
17	16	ad2antll	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → 𝑢 ∥ 𝑑 )
18	5	ad2antrl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → 𝑑 ∈ ℕ )
19		nndivdvds	⊢ ( ( 𝑑 ∈ ℕ ∧ 𝑢 ∈ ℕ ) → ( 𝑢 ∥ 𝑑 ↔ ( 𝑑 / 𝑢 ) ∈ ℕ ) )
20	18 11 19	syl2anc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( 𝑢 ∥ 𝑑 ↔ ( 𝑑 / 𝑢 ) ∈ ℕ ) )
21	17 20	mpbid	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( 𝑑 / 𝑢 ) ∈ ℕ )
22		vmacl	⊢ ( ( 𝑑 / 𝑢 ) ∈ ℕ → ( Λ ‘ ( 𝑑 / 𝑢 ) ) ∈ ℝ )
23	21 22	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( Λ ‘ ( 𝑑 / 𝑢 ) ) ∈ ℝ )
24	13 23	remulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) ∈ ℝ )
25	24	recnd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) ) → ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) ∈ ℂ )
26	25	anassrs	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ) → ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) ∈ ℂ )
27	9 26	fsumcl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) ∈ ℂ )
28		vmacl	⊢ ( 𝑑 ∈ ℕ → ( Λ ‘ 𝑑 ) ∈ ℝ )
29	6 28	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( Λ ‘ 𝑑 ) ∈ ℝ )
30	6	nnrpd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑑 ∈ ℝ+ )
31	30	relogcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ 𝑑 ) ∈ ℝ )
32	29 31	remulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ∈ ℝ )
33	32	recnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ∈ ℂ )
34	3 27 33	fsumadd	⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) + ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) + Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
35		id	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
36		fvoveq1	⊢ ( 𝑑 = ( 𝑢 · 𝑘 ) → ( Λ ‘ ( 𝑑 / 𝑢 ) ) = ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) )
37	36	oveq2d	⊢ ( 𝑑 = ( 𝑢 · 𝑘 ) → ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) = ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) )
38	35 37 25	fsumdvdscom	⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) = Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) )
39		ssrab2	⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ⊆ ℕ
40		simpr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } )
41	39 40	sselid	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑘 ∈ ℕ )
42	41	nncnd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑘 ∈ ℂ )
43		ssrab2	⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ℕ
44		simpr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
45	43 44	sselid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ ℕ )
46	45	nncnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ ℂ )
47	46	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑢 ∈ ℂ )
48	45	nnne0d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ≠ 0 )
49	48	adantr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → 𝑢 ≠ 0 )
50	42 47 49	divcan3d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( ( 𝑢 · 𝑘 ) / 𝑢 ) = 𝑘 )
51	50	fveq2d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) = ( Λ ‘ 𝑘 ) )
52	51	sumeq2dv	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ 𝑘 ) )
53		dvdsdivcl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑢 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
54	43 53	sselid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑢 ) ∈ ℕ )
55		vmasum	⊢ ( ( 𝑁 / 𝑢 ) ∈ ℕ → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ 𝑘 ) = ( log ‘ ( 𝑁 / 𝑢 ) ) )
56	54 55	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ 𝑘 ) = ( log ‘ ( 𝑁 / 𝑢 ) ) )
57		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
58	57	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑁 ∈ ℝ+ )
59	45	nnrpd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → 𝑢 ∈ ℝ+ )
60	58 59	relogdivd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ ( 𝑁 / 𝑢 ) ) = ( ( log ‘ 𝑁 ) − ( log ‘ 𝑢 ) ) )
61	52 56 60	3eqtrd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) = ( ( log ‘ 𝑁 ) − ( log ‘ 𝑢 ) ) )
62	61	oveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) = ( ( Λ ‘ 𝑢 ) · ( ( log ‘ 𝑁 ) − ( log ‘ 𝑢 ) ) ) )
63		fzfid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 1 ... ( 𝑁 / 𝑢 ) ) ∈ Fin )
64		dvdsssfz1	⊢ ( ( 𝑁 / 𝑢 ) ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ⊆ ( 1 ... ( 𝑁 / 𝑢 ) ) )
65	54 64	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ⊆ ( 1 ... ( 𝑁 / 𝑢 ) ) )
66	63 65	ssfid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ∈ Fin )
67	45 12	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( Λ ‘ 𝑢 ) ∈ ℝ )
68	67	recnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( Λ ‘ 𝑢 ) ∈ ℂ )
69		vmacl	⊢ ( 𝑘 ∈ ℕ → ( Λ ‘ 𝑘 ) ∈ ℝ )
70	41 69	syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( Λ ‘ 𝑘 ) ∈ ℝ )
71	70	recnd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( Λ ‘ 𝑘 ) ∈ ℂ )
72	51 71	eqeltrd	⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ) → ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ∈ ℂ )
73	66 68 72	fsummulc2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) )
74		relogcl	⊢ ( 𝑁 ∈ ℝ+ → ( log ‘ 𝑁 ) ∈ ℝ )
75	74	recnd	⊢ ( 𝑁 ∈ ℝ+ → ( log ‘ 𝑁 ) ∈ ℂ )
76	58 75	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ 𝑁 ) ∈ ℂ )
77	59	relogcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ 𝑢 ) ∈ ℝ )
78	77	recnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( log ‘ 𝑢 ) ∈ ℂ )
79	68 76 78	subdid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · ( ( log ‘ 𝑁 ) − ( log ‘ 𝑢 ) ) ) = ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) )
80	62 73 79	3eqtr3d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) = ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) )
81	80	sumeq2dv	⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑢 ) } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( ( 𝑢 · 𝑘 ) / 𝑢 ) ) ) = Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) )
82	68 76	mulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) ∈ ℂ )
83	68 78	mulcld	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ∈ ℂ )
84	3 82 83	fsumsub	⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) = ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) )
85	57 75	syl	⊢ ( 𝑁 ∈ ℕ → ( log ‘ 𝑁 ) ∈ ℂ )
86	85	sqvald	⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ 𝑁 ) ↑ 2 ) = ( ( log ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) )
87		vmasum	⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Λ ‘ 𝑢 ) = ( log ‘ 𝑁 ) )
88	87	oveq1d	⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) = ( ( log ‘ 𝑁 ) · ( log ‘ 𝑁 ) ) )
89	3 85 68	fsummulc1	⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) = Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) )
90	86 88 89	3eqtr2rd	⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) = ( ( log ‘ 𝑁 ) ↑ 2 ) )
91		fveq2	⊢ ( 𝑢 = 𝑑 → ( Λ ‘ 𝑢 ) = ( Λ ‘ 𝑑 ) )
92		fveq2	⊢ ( 𝑢 = 𝑑 → ( log ‘ 𝑢 ) = ( log ‘ 𝑑 ) )
93	91 92	oveq12d	⊢ ( 𝑢 = 𝑑 → ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) = ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) )
94	93	cbvsumv	⊢ Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) )
95	94	a1i	⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) )
96	90 95	oveq12d	⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) = ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
97	84 96	eqtrd	⊢ ( 𝑁 ∈ ℕ → Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑁 ) ) − ( ( Λ ‘ 𝑢 ) · ( log ‘ 𝑢 ) ) ) = ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
98	38 81 97	3eqtrd	⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) = ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
99	98	oveq1d	⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) + Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) = ( ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) + Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) )
100	85	sqcld	⊢ ( 𝑁 ∈ ℕ → ( ( log ‘ 𝑁 ) ↑ 2 ) ∈ ℂ )
101	3 33	fsumcl	⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ∈ ℂ )
102	100 101	npcand	⊢ ( 𝑁 ∈ ℕ → ( ( ( ( log ‘ 𝑁 ) ↑ 2 ) − Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) + Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) = ( ( log ‘ 𝑁 ) ↑ 2 ) )
103	34 99 102	3eqtrd	⊢ ( 𝑁 ∈ ℕ → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ( Σ 𝑢 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑 } ( ( Λ ‘ 𝑢 ) · ( Λ ‘ ( 𝑑 / 𝑢 ) ) ) + ( ( Λ ‘ 𝑑 ) · ( log ‘ 𝑑 ) ) ) = ( ( log ‘ 𝑁 ) ↑ 2 ) )