dchrvmasum2lem

Description: Give an expression for log x remarkably similar to sum_ n <_ x ( X ( n ) Lam ( n ) / n ) given in dchrvmasumlem1 . Part of Lemma 9.4.3 of Shapiro, p. 380. (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 = ( 0_g ‘ 𝐺 )
	dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrvmasum.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ⁺ )
	dchrvmasum2.2	⊢ ( 𝜑 → 1 ≤ 𝐴 )
Assertion	dchrvmasum2lem	⊢ ( 𝜑 → ( log ‘ 𝐴 ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )

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 = ( 0_g ‘ 𝐺 )
7		dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrvmasum.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ⁺ )
10		dchrvmasum2.2	⊢ ( 𝜑 → 1 ≤ 𝐴 )
11		2fveq3	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) )
12		id	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → 𝑛 = ( 𝑑 · 𝑚 ) )
13	11 12	oveq12d	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
14		oveq2	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( 𝐴 / 𝑛 ) = ( 𝐴 / ( 𝑑 · 𝑚 ) ) )
15	14	fveq2d	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( log ‘ ( 𝐴 / 𝑛 ) ) = ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) )
16	13 15	oveq12d	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) )
17	16	oveq2d	⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
18	9	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
19		elrabi	⊢ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } → 𝑑 ∈ ℕ )
20	19	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → 𝑑 ∈ ℕ )
21		mucl	⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
22	20 21	syl	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
23	22	zcnd	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
24	7	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑋 ∈ 𝐷 )
25		elfzelz	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℤ )
26	25	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℤ )
27	4 1 5 2 24 26	dchrzrhcl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
28		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
29	28	adantl	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
30	29	nncnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℂ )
31	29	nnne0d	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ≠ 0 )
32	27 30 31	divcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ∈ ℂ )
33	28	nnrpd	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℝ⁺ )
34		rpdivcl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺ ) → ( 𝐴 / 𝑛 ) ∈ ℝ⁺ )
35	9 33 34	syl2an	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑛 ) ∈ ℝ⁺ )
36	35	relogcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ ( 𝐴 / 𝑛 ) ) ∈ ℝ )
37	36	recnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ ( 𝐴 / 𝑛 ) ) ∈ ℂ )
38	32 37	mulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ∈ ℂ )
39	38	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ∈ ℂ )
40	23 39	mulcld	⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) ∈ ℂ )
41	17 18 40	dvdsflsumcom	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
42		2fveq3	⊢ ( 𝑛 = 1 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) )
43		id	⊢ ( 𝑛 = 1 → 𝑛 = 1 )
44	42 43	oveq12d	⊢ ( 𝑛 = 1 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) )
45		oveq2	⊢ ( 𝑛 = 1 → ( 𝐴 / 𝑛 ) = ( 𝐴 / 1 ) )
46	45	fveq2d	⊢ ( 𝑛 = 1 → ( log ‘ ( 𝐴 / 𝑛 ) ) = ( log ‘ ( 𝐴 / 1 ) ) )
47	44 46	oveq12d	⊢ ( 𝑛 = 1 → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) · ( log ‘ ( 𝐴 / 1 ) ) ) )
48		fzfid	⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
49		fz1ssnn	⊢ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ℕ
50	49	a1i	⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ℕ )
51		flge1nn	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ )
52	18 10 51	syl2anc	⊢ ( 𝜑 → ( ⌊ ‘ 𝐴 ) ∈ ℕ )
53		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
54	52 53	eleqtrdi	⊢ ( 𝜑 → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 1 ) )
55		eluzfz1	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ_≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
56	54 55	syl	⊢ ( 𝜑 → 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
57	47 48 50 56 38	musumsum	⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) · ( log ‘ ( 𝐴 / 1 ) ) ) )
58	4 1 5 2 7	dchrzrh1	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = 1 )
59	58	oveq1d	⊢ ( 𝜑 → ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) = ( 1 / 1 ) )
60		1div1e1	⊢ ( 1 / 1 ) = 1
61	59 60	syl6eq	⊢ ( 𝜑 → ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) = 1 )
62	9	rpcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
63	62	div1d	⊢ ( 𝜑 → ( 𝐴 / 1 ) = 𝐴 )
64	63	fveq2d	⊢ ( 𝜑 → ( log ‘ ( 𝐴 / 1 ) ) = ( log ‘ 𝐴 ) )
65	61 64	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) · ( log ‘ ( 𝐴 / 1 ) ) ) = ( 1 · ( log ‘ 𝐴 ) ) )
66	9	relogcld	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
67	66	recnd	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
68	67	mulid2d	⊢ ( 𝜑 → ( 1 · ( log ‘ 𝐴 ) ) = ( log ‘ 𝐴 ) )
69	57 65 68	3eqtrrd	⊢ ( 𝜑 → ( log ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) )
70		fzfid	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ∈ Fin )
71	7	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑋 ∈ 𝐷 )
72		elfzelz	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℤ )
73	72	adantl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℤ )
74	4 1 5 2 71 73	dchrzrhcl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
75		fznnfl	⊢ ( 𝐴 ∈ ℝ → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ) )
76	18 75	syl	⊢ ( 𝜑 → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ) )
77	76	simprbda	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℕ )
78	77 21	syl	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
79	78	zred	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
80	79 77	nndivred	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
81	80	recnd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
82	74 81	mulcld	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
83	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑋 ∈ 𝐷 )
84		elfzelz	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℤ )
85	84	adantl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℤ )
86	4 1 5 2 83 85	dchrzrhcl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
87		elfznn	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℕ )
88	87	nnrpd	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℝ⁺ )
89		rpdivcl	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝑑 ∈ ℝ⁺ ) → ( 𝐴 / 𝑑 ) ∈ ℝ⁺ )
90	9 88 89	syl2an	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑑 ) ∈ ℝ⁺ )
91		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℕ )
92	91	nnrpd	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℝ⁺ )
93		rpdivcl	⊢ ( ( ( 𝐴 / 𝑑 ) ∈ ℝ⁺ ∧ 𝑚 ∈ ℝ⁺ ) → ( ( 𝐴 / 𝑑 ) / 𝑚 ) ∈ ℝ⁺ )
94	90 92 93	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝐴 / 𝑑 ) / 𝑚 ) ∈ ℝ⁺ )
95	94	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ∈ ℝ )
96	91	adantl	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℕ )
97	95 96	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ∈ ℝ )
98	97	recnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ∈ ℂ )
99	86 98	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
100	70 82 99	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )
101	74	adantr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
102	79	adantr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
103	102	recnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
104	77	nnrpd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℝ⁺ )
105	104	adantr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ∈ ℝ⁺ )
106	105	rpcnne0d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) )
107		div12	⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ ∧ ( μ ‘ 𝑑 ) ∈ ℂ ∧ ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ) )
108	101 103 106 107	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ) )
109	95	recnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ∈ ℂ )
110	96	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℝ⁺ )
111	110	rpcnne0d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
112		div12	⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ ∧ ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ∈ ℂ ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) = ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
113	86 109 111 112	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) = ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
114	108 113	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = ( ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
115	105	rpcnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ∈ ℂ )
116	105	rpne0d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ≠ 0 )
117	101 115 116	divcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ∈ ℂ )
118	96	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℂ )
119	96	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ≠ 0 )
120	86 118 119	divcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
121	117 120	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
122	103 109 121	mulassd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) · ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) )
123	103 117 109 120	mul4d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( ( ( μ ‘ 𝑑 ) · ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
124	72	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ∈ ℤ )
125	4 1 5 2 83 124 85	dchrzrhmul	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) )
126	125	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
127		divmuldiv	⊢ ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ ∧ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ ) ∧ ( ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
128	101 86 106 111 127	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
129	126 128	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
130	62	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝐴 ∈ ℂ )
131		divdiv1	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( ( 𝐴 / 𝑑 ) / 𝑚 ) = ( 𝐴 / ( 𝑑 · 𝑚 ) ) )
132	130 106 111 131	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝐴 / 𝑑 ) / 𝑚 ) = ( 𝐴 / ( 𝑑 · 𝑚 ) ) )
133	132	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝐴 / ( 𝑑 · 𝑚 ) ) = ( ( 𝐴 / 𝑑 ) / 𝑚 ) )
134	133	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) = ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) )
135	129 134	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) · ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) )
136	121 109	mulcomd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) · ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
137	135 136	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
138	137	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) )
139	122 123 138	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
140	114 139	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
141	140	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
142	100 141	eqtrd	⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
143	142	sumeq2dv	⊢ ( 𝜑 → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
144	41 69 143	3eqtr4d	⊢ ( 𝜑 → ( log ‘ 𝐴 ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )

Metamath Proof Explorer

Theorem dchrvmasum2lem

Proof