This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrisum0lem2a

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 ⊢ ( 𝜑 → 𝐻 ⇝𝑟 𝑈 )
Assertion dchrisum0lem2a ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 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 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
16 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝜑 )
17 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℕ )
18 7 ssrab3 ⊢ 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
19 18 8 sselid ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 1 } ) )
20 19 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑋 ∈ 𝐷 )
22 nnz ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℤ )
24 4 1 5 2 21 23 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
25 nnrp ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ+ )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ+ )
27 26 rpsqrtcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( √ ‘ 𝑚 ) ∈ ℝ+ )
28 27 rpcnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( √ ‘ 𝑚 ) ∈ ℂ )
29 27 rpne0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( √ ‘ 𝑚 ) ≠ 0 )
30 24 28 29 divcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
31 16 17 30 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
32 15 31 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
33 rlimcl ⊢ ( 𝐻 ⇝𝑟 𝑈 → 𝑈 ∈ ℂ )
34 14 33 syl ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑈 ∈ ℂ )
36 0xr ⊢ 0 ∈ ℝ*
37 0lt1 ⊢ 0 < 1
38 df-ioo ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
39 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
40 xrltletr ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 0 < 1 ∧ 1 ≤ 𝑤 ) → 0 < 𝑤 ) )
41 38 39 40 ixxss1 ⊢ ( ( 0 ∈ ℝ* ∧ 0 < 1 ) → ( 1 [,) +∞ ) ⊆ ( 0 (,) +∞ ) )
42 36 37 41 mp2an ⊢ ( 1 [,) +∞ ) ⊆ ( 0 (,) +∞ )
43 ioorp ⊢ ( 0 (,) +∞ ) = ℝ+
44 42 43 sseqtri ⊢ ( 1 [,) +∞ ) ⊆ ℝ+
45 resmpt ⊢ ( ( 1 [,) +∞ ) ⊆ ℝ+ → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ↾ ( 1 [,) +∞ ) ) = ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) )
46 44 45 ax-mp ⊢ ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ↾ ( 1 [,) +∞ ) ) = ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
47 44 sseli ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ+ )
48 17 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ )
49 2fveq3 ⊢ ( 𝑎 = 𝑚 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) )
50 fveq2 ⊢ ( 𝑎 = 𝑚 → ( √ ‘ 𝑎 ) = ( √ ‘ 𝑚 ) )
51 49 50 oveq12d ⊢ ( 𝑎 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
52 ovex ⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) ∈ V
53 51 9 52 fvmpt3i ⊢ ( 𝑚 ∈ ℕ → ( 𝐹 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
54 48 53 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
55 47 54 sylanl2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
56 1re ⊢ 1 ∈ ℝ
57 elicopnf ⊢ ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
58 56 57 ax-mp ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) )
59 flge1nn ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
60 58 59 sylbi ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
62 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
63 61 62 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) )
64 47 31 sylanl2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
65 55 63 64 fsumser ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
66 65 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) = ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) )
67 46 66 eqtrid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ↾ ( 1 [,) +∞ ) ) = ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) )
68 fveq2 ⊢ ( 𝑚 = ( ⌊ ‘ 𝑥 ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑚 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
69 rpssre ⊢ ℝ+ ⊆ ℝ
70 69 a1i ⊢ ( 𝜑 → ℝ+ ⊆ ℝ )
71 44 70 sstrid ⊢ ( 𝜑 → ( 1 [,) +∞ ) ⊆ ℝ )
72 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
73 51 cbvmptv ⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
74 9 73 eqtri ⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
75 30 74 fmptd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℂ )
76 75 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
77 62 72 76 serf ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
78 77 feqmptd ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) = ( 𝑚 ∈ ℕ ↦ ( seq 1 ( + , 𝐹 ) ‘ 𝑚 ) ) )
79 78 11 eqbrtrrd ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( seq 1 ( + , 𝐹 ) ‘ 𝑚 ) ) ⇝ 𝑆 )
80 77 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑚 ) ∈ ℂ )
81 58 simprbi ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 1 ≤ 𝑥 )
82 81 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑥 )
83 62 68 71 72 79 80 82 climrlim2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ⇝𝑟 𝑆 )
84 rlimo1 ⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ⇝𝑟 𝑆 → ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
85 83 84 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
86 67 85 eqeltrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ↾ ( 1 [,) +∞ ) ) ∈ 𝑂(1) )
87 32 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) : ℝ+ ⟶ ℂ )
88 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
89 87 70 88 o1resb ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ↾ ( 1 [,) +∞ ) ) ∈ 𝑂(1) ) )
90 86 89 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ∈ 𝑂(1) )
91 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ 𝑈 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 𝑈 ) ∈ 𝑂(1) )
92 69 34 91 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ 𝑈 ) ∈ 𝑂(1) )
93 32 35 90 92 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) ∈ 𝑂(1) )
94 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
95 2z ⊢ 2 ∈ ℤ
96 rpexpcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
97 94 95 96 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
98 17 nnrpd ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℝ+ )
99 rpdivcl ⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ )
100 97 98 99 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ )
101 13 divsqrsumf ⊢ 𝐻 : ℝ+ ⟶ ℝ
102 101 ffvelcdmi ⊢ ( ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ → ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ∈ ℝ )
103 100 102 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ∈ ℝ )
104 103 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ∈ ℂ )
105 31 104 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ ℂ )
106 15 105 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ ℂ )
107 32 35 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ∈ ℂ )
108 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐻 ⇝𝑟 𝑈 )
109 108 33 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑈 ∈ ℂ )
110 31 109 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ∈ ℂ )
111 15 105 110 fsumsub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) )
112 31 104 109 subdid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) )
113 112 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) )
114 15 35 31 fsummulc1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) )
115 114 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) − ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) )
116 111 113 115 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) − ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) )
117 116 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) − ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) ) )
118 104 109 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ∈ ℂ )
119 31 118 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ∈ ℂ )
120 15 119 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ∈ ℂ )
121 120 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ∈ ℝ )
122 119 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ∈ ℝ )
123 15 122 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ∈ ℝ )
124 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℝ )
125 15 119 fsumabs ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) )
126 rprege0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
127 126 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
128 127 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
129 reflcl ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
130 128 129 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
131 130 94 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
132 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
133 132 rprecred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑥 ) ∈ ℝ )
134 31 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ∈ ℝ )
135 98 rpsqrtcld ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → ( √ ‘ 𝑚 ) ∈ ℝ+ )
136 135 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑚 ) ∈ ℝ+ )
137 136 rprecred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( √ ‘ 𝑚 ) ) ∈ ℝ )
138 118 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ∈ ℝ )
139 136 132 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑚 ) / 𝑥 ) ∈ ℝ+ )
140 69 139 sselid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑚 ) / 𝑥 ) ∈ ℝ )
141 31 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) )
142 118 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) )
143 16 17 24 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
144 136 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑚 ) ∈ ℂ )
145 136 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑚 ) ≠ 0 )
146 143 144 145 absdivd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( abs ‘ ( √ ‘ 𝑚 ) ) ) )
147 136 rprege0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑚 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑚 ) ) )
148 absid ⊢ ( ( ( √ ‘ 𝑚 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑚 ) ) → ( abs ‘ ( √ ‘ 𝑚 ) ) = ( √ ‘ 𝑚 ) )
149 147 148 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( √ ‘ 𝑚 ) ) = ( √ ‘ 𝑚 ) )
150 149 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( abs ‘ ( √ ‘ 𝑚 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( √ ‘ 𝑚 ) ) )
151 146 150 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( √ ‘ 𝑚 ) ) )
152 143 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) ∈ ℝ )
153 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
154 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
155 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
156 3 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
157 1 154 2 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
158 fof ⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
159 156 157 158 3syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
161 elfzelz ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℤ )
162 ffvelcdm ⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑚 ∈ ℤ ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) )
163 160 161 162 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐿 ‘ 𝑚 ) ∈ ( Base ‘ 𝑍 ) )
164 4 5 1 154 155 163 dchrabs2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) ≤ 1 )
165 152 153 136 164 lediv1dd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( √ ‘ 𝑚 ) ) ≤ ( 1 / ( √ ‘ 𝑚 ) ) )
166 151 165 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ≤ ( 1 / ( √ ‘ 𝑚 ) ) )
167 13 108 divsqrtsum2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ ) → ( abs ‘ ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ≤ ( 1 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
168 100 167 mpdan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ≤ ( 1 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
169 97 rprege0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ↑ 2 ) ) )
170 sqrtdiv ⊢ ( ( ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ↑ 2 ) ) ∧ 𝑚 ∈ ℝ+ ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( ( √ ‘ ( 𝑥 ↑ 2 ) ) / ( √ ‘ 𝑚 ) ) )
171 169 98 170 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( ( √ ‘ ( 𝑥 ↑ 2 ) ) / ( √ ‘ 𝑚 ) ) )
172 126 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
173 sqrtsq ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( √ ‘ ( 𝑥 ↑ 2 ) ) = 𝑥 )
174 172 173 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( 𝑥 ↑ 2 ) ) = 𝑥 )
175 174 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ ( 𝑥 ↑ 2 ) ) / ( √ ‘ 𝑚 ) ) = ( 𝑥 / ( √ ‘ 𝑚 ) ) )
176 171 175 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( 𝑥 / ( √ ‘ 𝑚 ) ) )
177 176 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( 1 / ( 𝑥 / ( √ ‘ 𝑚 ) ) ) )
178 rpcnne0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
179 178 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
180 136 rpcnne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) )
181 recdiv ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) ) → ( 1 / ( 𝑥 / ( √ ‘ 𝑚 ) ) ) = ( ( √ ‘ 𝑚 ) / 𝑥 ) )
182 179 180 181 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( 𝑥 / ( √ ‘ 𝑚 ) ) ) = ( ( √ ‘ 𝑚 ) / 𝑥 ) )
183 177 182 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( ( √ ‘ 𝑚 ) / 𝑥 ) )
184 168 183 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ≤ ( ( √ ‘ 𝑚 ) / 𝑥 ) )
185 134 137 138 140 141 142 166 184 lemul12ad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) · ( abs ‘ ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ≤ ( ( 1 / ( √ ‘ 𝑚 ) ) · ( ( √ ‘ 𝑚 ) / 𝑥 ) ) )
186 31 118 absmuld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) = ( ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) · ( abs ‘ ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) )
187 1cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℂ )
188 dmdcan ⊢ ( ( ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ 1 ∈ ℂ ) → ( ( ( √ ‘ 𝑚 ) / 𝑥 ) · ( 1 / ( √ ‘ 𝑚 ) ) ) = ( 1 / 𝑥 ) )
189 180 179 187 188 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( √ ‘ 𝑚 ) / 𝑥 ) · ( 1 / ( √ ‘ 𝑚 ) ) ) = ( 1 / 𝑥 ) )
190 139 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑚 ) / 𝑥 ) ∈ ℂ )
191 reccl ⊢ ( ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) → ( 1 / ( √ ‘ 𝑚 ) ) ∈ ℂ )
192 180 191 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( √ ‘ 𝑚 ) ) ∈ ℂ )
193 190 192 mulcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( √ ‘ 𝑚 ) / 𝑥 ) · ( 1 / ( √ ‘ 𝑚 ) ) ) = ( ( 1 / ( √ ‘ 𝑚 ) ) · ( ( √ ‘ 𝑚 ) / 𝑥 ) ) )
194 189 193 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑥 ) = ( ( 1 / ( √ ‘ 𝑚 ) ) · ( ( √ ‘ 𝑚 ) / 𝑥 ) ) )
195 185 186 194 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ≤ ( 1 / 𝑥 ) )
196 15 122 133 195 fsumle ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑥 ) )
197 flge0nn0 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
198 hashfz1 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
199 127 197 198 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
200 199 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · ( 1 / 𝑥 ) ) = ( ( ⌊ ‘ 𝑥 ) · ( 1 / 𝑥 ) ) )
201 94 rpreccld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ+ )
202 201 rpcnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℂ )
203 fsumconst ⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ ( 1 / 𝑥 ) ∈ ℂ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑥 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · ( 1 / 𝑥 ) ) )
204 15 202 203 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑥 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · ( 1 / 𝑥 ) ) )
205 130 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ∈ ℂ )
206 178 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
207 206 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
208 206 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
209 205 207 208 divrecd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) = ( ( ⌊ ‘ 𝑥 ) · ( 1 / 𝑥 ) ) )
210 200 204 209 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑥 ) = ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) )
211 196 210 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ≤ ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) )
212 flle ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
213 128 212 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
214 128 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
215 214 mulridd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · 1 ) = 𝑥 )
216 213 215 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ≤ ( 𝑥 · 1 ) )
217 rpregt0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
218 217 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
219 ledivmul ⊢ ( ( ( ⌊ ‘ 𝑥 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) ≤ 1 ↔ ( ⌊ ‘ 𝑥 ) ≤ ( 𝑥 · 1 ) ) )
220 130 124 218 219 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) ≤ 1 ↔ ( ⌊ ‘ 𝑥 ) ≤ ( 𝑥 · 1 ) ) )
221 216 220 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) / 𝑥 ) ≤ 1 )
222 123 131 124 211 221 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ≤ 1 )
223 121 123 124 125 222 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ≤ 1 )
224 223 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ≤ 1 )
225 70 120 88 88 224 elo1d ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) − 𝑈 ) ) ) ∈ 𝑂(1) )
226 117 225 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) − ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) ) ∈ 𝑂(1) )
227 106 107 226 o1dif ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · 𝑈 ) ) ∈ 𝑂(1) ) )
228 93 227 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ∈ 𝑂(1) )