Metamath Proof Explorer

Theorem dchrisum0lem2

Description: Lemma for dchrisum0 . (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum2.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum2.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum2.1 ⊢ 1 = ( 0g ‘ 𝐺 )
rpvmasum2.w ⊢ 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 }
dchrisum0.b ⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
dchrisum0lem1.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) )
dchrisum0.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
dchrisum0.s ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
dchrisum0.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑦 ) ) )
dchrisum0lem2.h ⊢ 𝐻 = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) )
dchrisum0lem2.u ⊢ ( 𝜑 → 𝐻 ⇝𝑟 𝑈 )
dchrisum0lem2.k ⊢ 𝐾 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
dchrisum0lem2.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,) +∞ ) )
dchrisum0lem2.t ⊢ ( 𝜑 → seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
dchrisum0lem2.3 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑦 ) )
Assertion dchrisum0lem2 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum2.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum2.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum2.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 rpvmasum2.w ⊢ 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = 0 }
8 dchrisum0.b ⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
9 dchrisum0lem1.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) )
10 dchrisum0.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
11 dchrisum0.s ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
12 dchrisum0.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑦 ) ) )
13 dchrisum0lem2.h ⊢ 𝐻 = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) )
14 dchrisum0lem2.u ⊢ ( 𝜑 → 𝐻 ⇝𝑟 𝑈 )
15 dchrisum0lem2.k ⊢ 𝐾 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
16 dchrisum0lem2.e ⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,) +∞ ) )
17 dchrisum0lem2.t ⊢ ( 𝜑 → seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
18 dchrisum0lem2.3 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑦 ) )
19 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
20 rpcn ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
22 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
23 7 ssrab3 ⊢ 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
24 23 8 sselid ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 1 } ) )
25 24 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
27 elfzelz ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℤ )
28 27 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℤ )
29 4 1 5 2 26 28 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
30 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℕ )
31 30 nnrpd ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℝ+ )
32 31 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ )
33 32 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℂ )
34 32 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ≠ 0 )
35 29 33 34 divcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
36 22 35 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
37 21 36 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
38 rpssre ⊢ ℝ+ ⊆ ℝ
39 2cn ⊢ 2 ∈ ℂ
40 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) )
41 38 39 40 mp2an ⊢ ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1)
42 41 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) )
43 38 a1i ⊢ ( 𝜑 → ℝ+ ⊆ ℝ )
44 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
45 elrege0 ⊢ ( 𝐸 ∈ ( 0 [,) +∞ ) ↔ ( 𝐸 ∈ ℝ ∧ 0 ≤ 𝐸 ) )
46 45 simplbi ⊢ ( 𝐸 ∈ ( 0 [,) +∞ ) → 𝐸 ∈ ℝ )
47 16 46 syl ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
48 21 36 absmuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( ( abs ‘ 𝑥 ) · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
49 rprege0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
51 absid ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( abs ‘ 𝑥 ) = 𝑥 )
52 50 51 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ 𝑥 ) = 𝑥 )
53 52 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( abs ‘ 𝑥 ) · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
54 48 53 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
55 54 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
56 36 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
57 56 subid1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) − 0 ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
58 30 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ )
59 2fveq3 ⊢ ( 𝑎 = 𝑚 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) )
60 id ⊢ ( 𝑎 = 𝑚 → 𝑎 = 𝑚 )
61 59 60 oveq12d ⊢ ( 𝑎 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
62 ovex ⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ∈ V
63 61 15 62 fvmpt3i ⊢ ( 𝑚 ∈ ℕ → ( 𝐾 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
64 58 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐾 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
65 64 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐾 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
66 rpregt0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
67 66 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
68 67 simpld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
69 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
70 flge1nn ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
71 68 69 70 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
72 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
73 71 72 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) )
74 35 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
75 65 73 74 fsumser ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
76 eldifsni ⊢ ( 𝑋 ∈ ( 𝐷 ∖ { 1 } ) → 𝑋 ≠ 1 )
77 24 76 syl ⊢ ( 𝜑 → 𝑋 ≠ 1 )
78 1 2 3 4 5 6 25 77 15 16 17 18 7 dchrvmaeq0 ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑊 ↔ 𝑇 = 0 ) )
79 8 78 mpbid ⊢ ( 𝜑 → 𝑇 = 0 )
80 79 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑇 = 0 )
81 80 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 = 𝑇 )
82 75 81 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) − 0 ) = ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) )
83 57 82 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) )
84 83 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) ) )
85 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
86 85 fvoveq1d ⊢ ( 𝑦 = 𝑥 → ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) ) )
87 oveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐸 / 𝑦 ) = ( 𝐸 / 𝑥 ) )
88 86 87 breq12d ⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑦 ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑥 ) ) )
89 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑦 ) )
90 1re ⊢ 1 ∈ ℝ
91 elicopnf ⊢ ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
92 90 91 ax-mp ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) )
93 68 69 92 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ( 1 [,) +∞ ) )
94 88 89 93 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑥 ) )
95 84 94 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ≤ ( 𝐸 / 𝑥 ) )
96 56 abscld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℝ )
97 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝐸 ∈ ℝ )
98 lemuldiv2 ⊢ ( ( ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℝ ∧ 𝐸 ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ≤ 𝐸 ↔ ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ≤ ( 𝐸 / 𝑥 ) ) )
99 96 97 67 98 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ≤ 𝐸 ↔ ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ≤ ( 𝐸 / 𝑥 ) ) )
100 95 99 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ≤ 𝐸 )
101 55 100 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ≤ 𝐸 )
102 43 37 44 47 101 elo1d ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ∈ 𝑂(1) )
103 19 37 42 102 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) ∈ 𝑂(1) )
104 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ Fin )
105 32 rpsqrtcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑚 ) ∈ ℝ+ )
106 105 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑚 ) ∈ ℂ )
107 105 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑚 ) ≠ 0 )
108 29 106 107 divcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
109 108 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
110 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) → 𝑑 ∈ ℕ )
111 110 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → 𝑑 ∈ ℕ )
112 111 nnrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → 𝑑 ∈ ℝ+ )
113 112 rpsqrtcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ 𝑑 ) ∈ ℝ+ )
114 113 rpcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ 𝑑 ) ∈ ℂ )
115 113 rpne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ 𝑑 ) ≠ 0 )
116 109 114 115 divcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
117 104 116 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
118 22 117 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
119 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℂ ) → ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ∈ ℂ )
120 39 37 119 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ∈ ℂ )
121 2re ⊢ 2 ∈ ℝ
122 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
123 2z ⊢ 2 ∈ ℤ
124 rpexpcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
125 122 123 124 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
126 rpdivcl ⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ )
127 125 31 126 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ )
128 127 rpsqrtcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ∈ ℝ+ )
129 128 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ∈ ℝ )
130 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ∈ ℝ ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ ℝ )
131 121 129 130 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ ℝ )
132 131 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ ℂ )
133 108 132 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ∈ ℂ )
134 22 117 133 fsumsub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
135 113 rpcnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( √ ‘ 𝑑 ) ∈ ℂ ∧ ( √ ‘ 𝑑 ) ≠ 0 ) )
136 reccl ⊢ ( ( ( √ ‘ 𝑑 ) ∈ ℂ ∧ ( √ ‘ 𝑑 ) ≠ 0 ) → ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℂ )
137 135 136 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℂ )
138 104 137 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℂ )
139 108 138 132 subdid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
140 fveq2 ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( ⌊ ‘ 𝑦 ) = ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) )
141 140 oveq2d ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) = ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
142 141 sumeq1d ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) )
143 fveq2 ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( √ ‘ 𝑦 ) = ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) )
144 143 oveq2d ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( 2 · ( √ ‘ 𝑦 ) ) = ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
145 142 144 oveq12d ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
146 ovex ⊢ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ∈ V
147 145 13 146 fvmpt3i ⊢ ( ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ → ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
148 127 147 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
149 148 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
150 109 114 115 divrecd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 1 / ( √ ‘ 𝑑 ) ) ) )
151 150 sumeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 1 / ( √ ‘ 𝑑 ) ) ) )
152 104 108 137 fsummulc2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 1 / ( √ ‘ 𝑑 ) ) ) )
153 151 152 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ) )
154 153 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
155 139 149 154 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
156 155 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
157 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 2 · 𝑥 ) ∈ ℂ )
158 39 21 157 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · 𝑥 ) ∈ ℂ )
159 22 158 35 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 𝑥 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 2 · 𝑥 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
160 19 21 36 mulassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 𝑥 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
161 158 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · 𝑥 ) ∈ ℂ )
162 161 108 106 107 div12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑥 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) ) )
163 105 rpcnne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) )
164 divdiv1 ⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ ∧ ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) ∧ ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) ) )
165 29 163 163 164 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) ) )
166 32 rprege0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) )
167 remsqsqrt ⊢ ( ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) → ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) = 𝑚 )
168 166 167 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) = 𝑚 )
169 168 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
170 165 169 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
171 170 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑥 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( 2 · 𝑥 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) )
172 125 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
173 172 rprege0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ↑ 2 ) ) )
174 sqrtdiv ⊢ ( ( ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ↑ 2 ) ) ∧ 𝑚 ∈ ℝ+ ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( ( √ ‘ ( 𝑥 ↑ 2 ) ) / ( √ ‘ 𝑚 ) ) )
175 173 32 174 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( ( √ ‘ ( 𝑥 ↑ 2 ) ) / ( √ ‘ 𝑚 ) ) )
176 49 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
177 sqrtsq ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( √ ‘ ( 𝑥 ↑ 2 ) ) = 𝑥 )
178 176 177 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( 𝑥 ↑ 2 ) ) = 𝑥 )
179 178 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ ( 𝑥 ↑ 2 ) ) / ( √ ‘ 𝑚 ) ) = ( 𝑥 / ( √ ‘ 𝑚 ) ) )
180 175 179 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( 𝑥 / ( √ ‘ 𝑚 ) ) )
181 180 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( 2 · ( 𝑥 / ( √ ‘ 𝑚 ) ) ) )
182 2cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℂ )
183 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
184 divass ⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) ) → ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) = ( 2 · ( 𝑥 / ( √ ‘ 𝑚 ) ) ) )
185 182 183 163 184 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) = ( 2 · ( 𝑥 / ( √ ‘ 𝑚 ) ) ) )
186 181 185 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) )
187 186 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) ) )
188 162 171 187 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑥 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
189 188 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 2 · 𝑥 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
190 159 160 189 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
191 190 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
192 134 156 191 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) )
193 192 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) ) )
194 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dchrisum0lem2a ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ∈ 𝑂(1) )
195 193 194 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) ) ∈ 𝑂(1) )
196 118 120 195 o1dif ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) ∈ 𝑂(1) ) )
197 103 196 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) )