Metamath Proof Explorer

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 addid1d ⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ( Σ 𝑛 ∈ ( 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 ( 𝜓 , ( 𝐴 / 𝑑 ) , 𝑚 ) ) / 𝑚 ) ) ) )