Metamath Proof Explorer

Theorem dchrisum0lem1

Description: Lemma for dchrisum0 . (Contributed by Mario Carneiro, 12-May-2016) (Revised by Mario Carneiro, 7-Jun-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 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑦 ) ) )
Assertion dchrisum0lem1 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 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 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
14 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ∈ Fin )
15 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ∈ Fin )
16 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
17 elfzuz ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
18 16 17 anim12i ⊢ ( ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
19 18 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) )
20 elfzuz ⊢ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
21 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) → 𝑑 ∈ ℕ )
22 20 21 anim12ci ⊢ ( ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) )
24 eluzelz ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → 𝑚 ∈ ℤ )
25 24 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑚 ∈ ℤ )
26 25 zred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑚 ∈ ℝ )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
28 2z ⊢ 2 ∈ ℤ
29 rpexpcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
30 27 28 29 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
31 30 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) ∈ ℝ )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ )
33 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑑 ∈ ℕ )
34 33 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑑 ∈ ℝ+ )
35 26 32 34 lemuldivd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑚 · 𝑑 ) ≤ ( 𝑥 ↑ 2 ) ↔ 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) )
36 33 nnred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑑 ∈ ℝ )
37 27 rprege0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
38 flge0nn0 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
39 nn0p1nn ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
40 37 38 39 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
41 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
42 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
43 eluznn ⊢ ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℕ )
44 41 42 43 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑚 ∈ ℕ )
45 44 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑚 ∈ ℝ+ )
46 36 32 45 lemuldiv2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑚 · 𝑑 ) ≤ ( 𝑥 ↑ 2 ) ↔ 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) )
47 35 46 bitr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ↔ 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) )
48 rpcn ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
50 49 sqvald ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) = ( 𝑥 · 𝑥 ) )
51 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑥 ↑ 2 ) = ( 𝑥 · 𝑥 ) )
52 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑥 ∈ ℝ+ )
53 52 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑥 ∈ ℝ )
54 reflcl ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
55 peano2re ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℝ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ )
56 53 54 55 3syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ )
57 fllep1 ⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
58 53 57 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
59 eluzle ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ≤ 𝑚 )
60 59 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ≤ 𝑚 )
61 53 56 26 58 60 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑥 ≤ 𝑚 )
62 53 26 52 lemul1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑥 ≤ 𝑚 ↔ ( 𝑥 · 𝑥 ) ≤ ( 𝑚 · 𝑥 ) ) )
63 61 62 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑥 · 𝑥 ) ≤ ( 𝑚 · 𝑥 ) )
64 51 63 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑥 ↑ 2 ) ≤ ( 𝑚 · 𝑥 ) )
65 32 53 45 ledivmuld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( ( 𝑥 ↑ 2 ) / 𝑚 ) ≤ 𝑥 ↔ ( 𝑥 ↑ 2 ) ≤ ( 𝑚 · 𝑥 ) ) )
66 64 65 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑚 ) ≤ 𝑥 )
67 nnre ⊢ ( 𝑑 ∈ ℕ → 𝑑 ∈ ℝ )
68 67 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 𝑑 ∈ ℝ )
69 32 44 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ )
70 letr ⊢ ( ( 𝑑 ∈ ℝ ∧ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∧ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ≤ 𝑥 ) → 𝑑 ≤ 𝑥 ) )
71 68 69 53 70 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∧ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ≤ 𝑥 ) → 𝑑 ≤ 𝑥 ) )
72 66 71 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) → 𝑑 ≤ 𝑥 ) )
73 47 72 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) → 𝑑 ≤ 𝑥 ) )
74 73 pm4.71rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ↔ ( 𝑑 ≤ 𝑥 ∧ 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
75 nnge1 ⊢ ( 𝑑 ∈ ℕ → 1 ≤ 𝑑 )
76 75 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → 1 ≤ 𝑑 )
77 1re ⊢ 1 ∈ ℝ
78 0lt1 ⊢ 0 < 1
79 77 78 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 0 < 1 )
80 34 rpregt0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑑 ∈ ℝ ∧ 0 < 𝑑 ) )
81 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
82 81 rpregt0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 0 < ( 𝑥 ↑ 2 ) ) )
83 lediv2 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑑 ∈ ℝ ∧ 0 < 𝑑 ) ∧ ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 0 < ( 𝑥 ↑ 2 ) ) ) → ( 1 ≤ 𝑑 ↔ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ≤ ( ( 𝑥 ↑ 2 ) / 1 ) ) )
84 79 80 82 83 mp3an2i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 1 ≤ 𝑑 ↔ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ≤ ( ( 𝑥 ↑ 2 ) / 1 ) ) )
85 76 84 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑑 ) ≤ ( ( 𝑥 ↑ 2 ) / 1 ) )
86 32 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℂ )
87 86 div1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑥 ↑ 2 ) / 1 ) = ( 𝑥 ↑ 2 ) )
88 85 87 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑑 ) ≤ ( 𝑥 ↑ 2 ) )
89 simpl ⊢ ( ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑑 ∈ ℕ )
90 nndivre ⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ )
91 31 89 90 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ )
92 letr ⊢ ( ( 𝑚 ∈ ℝ ∧ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ ∧ ( 𝑥 ↑ 2 ) ∈ ℝ ) → ( ( 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∧ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ≤ ( 𝑥 ↑ 2 ) ) → 𝑚 ≤ ( 𝑥 ↑ 2 ) ) )
93 26 91 32 92 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∧ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ≤ ( 𝑥 ↑ 2 ) ) → 𝑚 ≤ ( 𝑥 ↑ 2 ) ) )
94 88 93 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) → 𝑚 ≤ ( 𝑥 ↑ 2 ) ) )
95 47 94 sylbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) → 𝑚 ≤ ( 𝑥 ↑ 2 ) ) )
96 95 pm4.71rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ↔ ( 𝑚 ≤ ( 𝑥 ↑ 2 ) ∧ 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
97 47 74 96 3bitr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑑 ≤ 𝑥 ∧ 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ↔ ( 𝑚 ≤ ( 𝑥 ↑ 2 ) ∧ 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
98 fznnfl ⊢ ( 𝑥 ∈ ℝ → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥 ) ) )
99 98 baibd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ 𝑑 ≤ 𝑥 ) )
100 53 33 99 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ 𝑑 ≤ 𝑥 ) )
101 91 flcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ℤ )
102 elfz5 ⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∧ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ℤ ) → ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ↔ 𝑚 ≤ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
103 42 101 102 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ↔ 𝑚 ≤ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
104 flge ⊢ ( ( ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ ∧ 𝑚 ∈ ℤ ) → ( 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ↔ 𝑚 ≤ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
105 91 25 104 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ↔ 𝑚 ≤ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
106 103 105 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ↔ 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) )
107 100 106 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) ↔ ( 𝑑 ≤ 𝑥 ∧ 𝑚 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
108 32 flcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ∈ ℤ )
109 elfz5 ⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∧ ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ∈ ℤ ) → ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ↔ 𝑚 ≤ ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) )
110 42 108 109 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ↔ 𝑚 ≤ ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) )
111 flge ⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 𝑚 ∈ ℤ ) → ( 𝑚 ≤ ( 𝑥 ↑ 2 ) ↔ 𝑚 ≤ ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) )
112 32 25 111 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ≤ ( 𝑥 ↑ 2 ) ↔ 𝑚 ≤ ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) )
113 110 112 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ↔ 𝑚 ≤ ( 𝑥 ↑ 2 ) ) )
114 fznnfl ⊢ ( ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
115 114 baibd ⊢ ( ( ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ↔ 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) )
116 69 33 115 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ↔ 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) )
117 113 116 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ↔ ( 𝑚 ≤ ( 𝑥 ↑ 2 ) ∧ 𝑑 ≤ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
118 97 107 117 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) → ( ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) ↔ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
119 118 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑑 ∈ ℕ ∧ 𝑚 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) ↔ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) ) )
120 19 23 119 pm5.21ndd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) ↔ ( 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
121 ssun2 ⊢ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∪ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
122 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
123 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
124 122 123 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
125 dchrisum0lem1a ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∧ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) ) )
126 125 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) )
127 fzsplit2 ⊢ ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) = ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∪ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) )
128 124 126 127 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) = ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∪ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) )
129 121 128 sseqtrrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
130 129 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
131 7 ssrab3 ⊢ 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
132 131 8 sseldi ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 1 } ) )
133 132 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
134 133 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑋 ∈ 𝐷 )
135 elfzelz ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) → 𝑚 ∈ ℤ )
136 135 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑚 ∈ ℤ )
137 4 1 5 2 134 136 dchrzrhcl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
138 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) → 𝑚 ∈ ℕ )
139 138 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑚 ∈ ℕ )
140 139 nnrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑚 ∈ ℝ+ )
141 140 rpsqrtcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( √ ‘ 𝑚 ) ∈ ℝ+ )
142 141 rpcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( √ ‘ 𝑚 ) ∈ ℂ )
143 141 rpne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( √ ‘ 𝑚 ) ≠ 0 )
144 137 142 143 divcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
145 16 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
146 145 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ+ )
147 146 rpsqrtcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑑 ) ∈ ℝ+ )
148 147 rpcnne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑑 ) ∈ ℂ ∧ ( √ ‘ 𝑑 ) ≠ 0 ) )
149 148 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( ( √ ‘ 𝑑 ) ∈ ℂ ∧ ( √ ‘ 𝑑 ) ≠ 0 ) )
150 149 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( √ ‘ 𝑑 ) ∈ ℂ )
151 149 simprd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( √ ‘ 𝑑 ) ≠ 0 )
152 144 150 151 divcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
153 130 152 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
154 153 anasss ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
155 13 14 15 120 154 fsumcom2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) )
156 155 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) )
157 77 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
158 2cn ⊢ 2 ∈ ℂ
159 27 rpsqrtcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
160 159 rpcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℂ )
161 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( √ ‘ 𝑥 ) ∈ ℂ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℂ )
162 158 160 161 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( √ ‘ 𝑥 ) ) ∈ ℂ )
163 147 rprecred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℝ )
164 13 163 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℝ )
165 164 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℂ )
166 165 162 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ∈ ℂ )
167 2re ⊢ 2 ∈ ℝ
168 elrege0 ⊢ ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
169 10 168 sylib ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
170 169 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
171 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 2 · 𝐶 ) ∈ ℝ )
172 167 170 171 sylancr ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∈ ℝ )
173 172 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · 𝐶 ) ∈ ℝ )
174 173 159 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ∈ ℝ )
175 174 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ∈ ℂ )
176 162 166 175 adddird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 2 · ( √ ‘ 𝑥 ) ) + ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) = ( ( ( 2 · ( √ ‘ 𝑥 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) + ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) )
177 162 165 pncan3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · ( √ ‘ 𝑥 ) ) + ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) )
178 177 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 2 · ( √ ‘ 𝑥 ) ) + ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) )
179 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
180 179 160 175 mulassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · ( √ ‘ 𝑥 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) = ( 2 · ( ( √ ‘ 𝑥 ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) )
181 173 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · 𝐶 ) ∈ ℂ )
182 159 rpne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ≠ 0 )
183 181 160 182 divcan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( √ ‘ 𝑥 ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) = ( 2 · 𝐶 ) )
184 183 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( ( √ ‘ 𝑥 ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) = ( 2 · ( 2 · 𝐶 ) ) )
185 180 184 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · ( √ ‘ 𝑥 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) = ( 2 · ( 2 · 𝐶 ) ) )
186 185 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( 2 · ( √ ‘ 𝑥 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) + ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) = ( ( 2 · ( 2 · 𝐶 ) ) + ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) )
187 176 178 186 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) = ( ( 2 · ( 2 · 𝐶 ) ) + ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) )
188 187 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 2 · ( 2 · 𝐶 ) ) + ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) ) )
189 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( 2 · 𝐶 ) ∈ ℝ ) → ( 2 · ( 2 · 𝐶 ) ) ∈ ℝ )
190 167 172 189 sylancr ⊢ ( 𝜑 → ( 2 · ( 2 · 𝐶 ) ) ∈ ℝ )
191 190 recnd ⊢ ( 𝜑 → ( 2 · ( 2 · 𝐶 ) ) ∈ ℂ )
192 191 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( 2 · 𝐶 ) ) ∈ ℂ )
193 166 175 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ∈ ℂ )
194 rpssre ⊢ ℝ+ ⊆ ℝ
195 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ ( 2 · ( 2 · 𝐶 ) ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( 2 · 𝐶 ) ) ) ∈ 𝑂(1) )
196 194 191 195 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( 2 · 𝐶 ) ) ) ∈ 𝑂(1) )
197 eqid ⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) )
198 197 divsqrsum ⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) ∈ dom ⇝𝑟
199 rlimdmo1 ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) ∈ dom ⇝𝑟 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
200 198 199 mp1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
201 181 160 182 divrecd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) = ( ( 2 · 𝐶 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) )
202 201 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( 2 · 𝐶 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) ) )
203 159 rprecred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( √ ‘ 𝑥 ) ) ∈ ℝ )
204 172 recnd ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∈ ℂ )
205 rlimconst ⊢ ( ( ℝ+ ⊆ ℝ ∧ ( 2 · 𝐶 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( 2 · 𝐶 ) ) ⇝𝑟 ( 2 · 𝐶 ) )
206 194 204 205 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 2 · 𝐶 ) ) ⇝𝑟 ( 2 · 𝐶 ) )
207 sqrtlim ⊢ ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑥 ) ) ) ⇝𝑟 0
208 207 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 1 / ( √ ‘ 𝑥 ) ) ) ⇝𝑟 0 )
209 173 203 206 208 rlimmul ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( 2 · 𝐶 ) · ( 1 / ( √ ‘ 𝑥 ) ) ) ) ⇝𝑟 ( ( 2 · 𝐶 ) · 0 ) )
210 202 209 eqbrtrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ⇝𝑟 ( ( 2 · 𝐶 ) · 0 ) )
211 rlimo1 ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ⇝𝑟 ( ( 2 · 𝐶 ) · 0 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
212 210 211 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
213 166 175 200 212 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
214 192 193 196 213 o1add2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( 2 · ( 2 · 𝐶 ) ) + ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
215 188 214 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
216 164 174 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ∈ ℝ )
217 15 153 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
218 13 217 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
219 218 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ ℝ )
220 216 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ∈ ℂ )
221 220 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) ∈ ℝ )
222 217 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ ℝ )
223 13 222 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ ℝ )
224 13 217 fsumabs ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) )
225 174 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ∈ ℝ )
226 163 225 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ∈ ℝ )
227 130 144 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
228 15 227 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
229 228 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ∈ ℝ )
230 1 2 3 4 5 6 7 8 9 10 11 12 dchrisum0lem1b ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ≤ ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) )
231 229 225 147 230 lediv1dd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) / ( √ ‘ 𝑑 ) ) ≤ ( ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) / ( √ ‘ 𝑑 ) ) )
232 147 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑑 ) ∈ ℂ )
233 147 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑑 ) ≠ 0 )
234 228 232 233 absdivd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) = ( ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) / ( abs ‘ ( √ ‘ 𝑑 ) ) ) )
235 15 232 227 233 fsumdivc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) )
236 235 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) = ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) )
237 147 rprege0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑑 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑑 ) ) )
238 absid ⊢ ( ( ( √ ‘ 𝑑 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑑 ) ) → ( abs ‘ ( √ ‘ 𝑑 ) ) = ( √ ‘ 𝑑 ) )
239 237 238 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( √ ‘ 𝑑 ) ) = ( √ ‘ 𝑑 ) )
240 239 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) / ( abs ‘ ( √ ‘ 𝑑 ) ) ) = ( ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) / ( √ ‘ 𝑑 ) ) )
241 234 236 240 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) / ( √ ‘ 𝑑 ) ) = ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) )
242 175 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ∈ ℂ )
243 242 232 233 divrec2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) / ( √ ‘ 𝑑 ) ) = ( ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) )
244 231 241 243 3brtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ≤ ( ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) )
245 13 222 226 244 fsumle ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) )
246 163 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℂ )
247 13 175 246 fsummulc1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) )
248 245 247 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ≤ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) )
249 219 223 216 224 248 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ≤ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) )
250 216 leabsd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) )
251 219 216 221 249 250 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ≤ ( abs ‘ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) )
252 251 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ≤ ( abs ‘ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑑 ) ) · ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ) ) )
253 157 215 216 218 252 o1le ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) )
254 156 253 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) )