Theorem dchrvmasum2if

Description: Combine the results of dchrvmasumlem1 and dchrvmasum2lem inside a conditional. (Contributed by Mario Carneiro, 4-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
	dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrvmasum.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	dchrvmasum2.2	⊢ ( 𝜑 → 1 ≤ 𝐴 )
Assertion	dchrvmasum2if	⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum.1	⊢ 1 = ( 0g ‘ 𝐺 )
7		dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrvmasum.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
10		dchrvmasum2.2	⊢ ( 𝜑 → 1 ≤ 𝐴 )
11		fzfid	⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
12	7	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑋 ∈ 𝐷 )
13		elfzelz	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℤ )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℤ )
15	4 1 5 2 12 14	dchrzrhcl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
16		elfznn	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℕ )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℕ )
18		mucl	⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
19	18	zred	⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℝ )
20		nndivre	⊢ ( ( ( μ ‘ 𝑑 ) ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
21	19 20	mpancom	⊢ ( 𝑑 ∈ ℕ → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
22	17 21	syl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
23	22	recnd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
24	15 23	mulcld	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
25		fzfid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ∈ Fin )
26	12	adantr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑋 ∈ 𝐷 )
27		elfzelz	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℤ )
28	27	adantl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℤ )
29	4 1 5 2 26 28	dchrzrhcl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
30		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℕ )
31	30	adantl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℕ )
32	31	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℝ+ )
33	32	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
34	33 31	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ 𝑚 ) / 𝑚 ) ∈ ℝ )
35	34	recnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ 𝑚 ) / 𝑚 ) ∈ ℂ )
36	29 35	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ∈ ℂ )
37	25 36	fsumcl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ∈ ℂ )
38	24 37	mulcld	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) ∈ ℂ )
39	16	nnrpd	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℝ+ )
40		rpdivcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) → ( 𝐴 / 𝑑 ) ∈ ℝ+ )
41	9 39 40	syl2an	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑑 ) ∈ ℝ+ )
42	41	adantr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝐴 / 𝑑 ) ∈ ℝ+ )
43	42 32	rpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝐴 / 𝑑 ) / 𝑚 ) ∈ ℝ+ )
44	43	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ∈ ℝ )
45	44 31	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ∈ ℝ )
46	45	recnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ∈ ℂ )
47	29 46	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
48	25 47	fsumcl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
49	24 48	mulcld	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) ∈ ℂ )
50	11 38 49	fsumadd	⊢ ( 𝜑 → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) + ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) ) )
51	42 32	relogdivd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) = ( ( log ‘ ( 𝐴 / 𝑑 ) ) − ( log ‘ 𝑚 ) ) )
52	51	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ 𝑚 ) + ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) = ( ( log ‘ 𝑚 ) + ( ( log ‘ ( 𝐴 / 𝑑 ) ) − ( log ‘ 𝑚 ) ) ) )
53	33	recnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ )
54	41	relogcld	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ ( 𝐴 / 𝑑 ) ) ∈ ℝ )
55	54	recnd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ ( 𝐴 / 𝑑 ) ) ∈ ℂ )
56	55	adantr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( 𝐴 / 𝑑 ) ) ∈ ℂ )
57	53 56	pncan3d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ 𝑚 ) + ( ( log ‘ ( 𝐴 / 𝑑 ) ) − ( log ‘ 𝑚 ) ) ) = ( log ‘ ( 𝐴 / 𝑑 ) ) )
58	52 57	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( 𝐴 / 𝑑 ) ) = ( ( log ‘ 𝑚 ) + ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) )
59	58	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) = ( ( ( log ‘ 𝑚 ) + ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) / 𝑚 ) )
60	44	recnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ∈ ℂ )
61	31	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℂ )
62	31	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ≠ 0 )
63	53 60 61 62	divdird	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( log ‘ 𝑚 ) + ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) / 𝑚 ) = ( ( ( log ‘ 𝑚 ) / 𝑚 ) + ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) )
64	59 63	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) = ( ( ( log ‘ 𝑚 ) / 𝑚 ) + ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) )
65	64	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( ( log ‘ 𝑚 ) / 𝑚 ) + ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )
66	29 35 46	adddid	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( ( log ‘ 𝑚 ) / 𝑚 ) + ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) + ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )
67	65 66	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) + ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )
68	67	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) + ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )
69	25 36 47	fsumadd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) + ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )
70	68 69	eqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )
71	70	oveq2d	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) ) )
72	24 37 48	adddid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) + ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) ) )
73	71 72	eqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) + ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) ) )
74	73	sumeq2dv	⊢ ( 𝜑 → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) + ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) ) )
75	1 2 3 4 5 6 7 8 9	dchrvmasumlem1	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) )
76	1 2 3 4 5 6 7 8 9 10	dchrvmasum2lem	⊢ ( 𝜑 → ( log ‘ 𝐴 ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )
77	75 76	oveq12d	⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + ( log ‘ 𝐴 ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) ) )
78	50 74 77	3eqtr4rd	⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + ( log ‘ 𝐴 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) ) )
79	78	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + ( log ‘ 𝐴 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) ) )
80		iftrue	⊢ ( 𝜓 → if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) = ( log ‘ 𝐴 ) )
81	80	oveq2d	⊢ ( 𝜓 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + ( log ‘ 𝐴 ) ) )
82	81	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + ( log ‘ 𝐴 ) ) )
83		iftrue	⊢ ( 𝜓 → if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) = ( 𝐴 / 𝑑 ) )
84	83	fveq2d	⊢ ( 𝜓 → ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) = ( log ‘ ( 𝐴 / 𝑑 ) ) )
85	84	oveq1d	⊢ ( 𝜓 → ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) = ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) )
86	85	oveq2d	⊢ ( 𝜓 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) )
87	86	sumeq2sdv	⊢ ( 𝜓 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) )
88	87	oveq2d	⊢ ( 𝜓 → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) ) )
89	88	sumeq2sdv	⊢ ( 𝜓 → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) ) )
90	89	adantl	⊢ ( ( 𝜑 ∧ 𝜓 ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( 𝐴 / 𝑑 ) ) / 𝑚 ) ) ) )
91	79 82 90	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) )
92	7	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑋 ∈ 𝐷 )
93		elfzelz	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℤ )
94	93	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℤ )
95	4 1 5 2 92 94	dchrzrhcl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
96		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
97	96	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
98		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
99		nndivre	⊢ ( ( ( Λ ‘ 𝑛 ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
100	98 99	mpancom	⊢ ( 𝑛 ∈ ℕ → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
101	100	recnd	⊢ ( 𝑛 ∈ ℕ → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
102	97 101	syl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
103	95 102	mulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
104	11 103	fsumcl	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
105	104	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
106	105	addridd	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + 0 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
107		iffalse	⊢ ( ¬ 𝜓 → if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) = 0 )
108	107	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) = 0 )
109	108	oveq2d	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + 0 ) )
110		iffalse	⊢ ( ¬ 𝜓 → if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) = 𝑚 )
111	110	fveq2d	⊢ ( ¬ 𝜓 → ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) = ( log ‘ 𝑚 ) )
112	111	oveq1d	⊢ ( ¬ 𝜓 → ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) = ( ( log ‘ 𝑚 ) / 𝑚 ) )
113	112	oveq2d	⊢ ( ¬ 𝜓 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
114	113	sumeq2sdv	⊢ ( ¬ 𝜓 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
115	114	oveq2d	⊢ ( ¬ 𝜓 → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) )
116	115	sumeq2sdv	⊢ ( ¬ 𝜓 → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) )
117	75	eqcomd	⊢ ( 𝜑 → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
118	116 117	sylan9eqr	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
119	106 109 118	3eqtr4d	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) )
120	91 119	pm2.61dan	⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝜓 , ( log ‘ 𝐴 ) , 0 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ if ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) )