Metamath Proof Explorer

Theorem dchrisum0lem1b

Description: Lemma for dchrisum0lem1 . (Contributed 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 dchrisum0lem1b ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ≤ ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) )

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 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ∈ Fin )
14 ssun2 ⊢ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∪ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
16 15 rprege0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
17 flge0nn0 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
19 nn0p1nn ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
20 18 19 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
22 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
23 21 22 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
24 dchrisum0lem1a ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∧ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) ) )
25 24 simprd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) )
26 fzsplit2 ⊢ ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) = ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∪ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) )
27 23 25 26 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) = ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∪ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) )
28 14 27 sseqtrrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
29 28 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
30 7 ssrab3 ⊢ 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
31 30 8 sselid ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 1 } ) )
32 31 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
33 32 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑋 ∈ 𝐷 )
34 elfzelz ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) → 𝑚 ∈ ℤ )
35 34 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑚 ∈ ℤ )
36 4 1 5 2 33 35 dchrzrhcl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
37 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) → 𝑚 ∈ ℕ )
38 37 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑚 ∈ ℕ )
39 38 nnrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → 𝑚 ∈ ℝ+ )
40 39 rpsqrtcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( √ ‘ 𝑚 ) ∈ ℝ+ )
41 40 rpcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( √ ‘ 𝑚 ) ∈ ℂ )
42 40 rpne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( √ ‘ 𝑚 ) ≠ 0 )
43 36 41 42 divcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
44 29 43 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
45 13 44 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
46 45 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ∈ ℝ )
47 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
48 32 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑋 ∈ 𝐷 )
49 nnz ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
50 49 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℤ )
51 4 1 5 2 48 50 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
52 nnrp ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ+ )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ+ )
54 53 rpsqrtcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( √ ‘ 𝑚 ) ∈ ℝ+ )
55 54 rpcnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( √ ‘ 𝑚 ) ∈ ℂ )
56 54 rpne0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( √ ‘ 𝑚 ) ≠ 0 )
57 51 55 56 divcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
58 2fveq3 ⊢ ( 𝑎 = 𝑚 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) )
59 fveq2 ⊢ ( 𝑎 = 𝑚 → ( √ ‘ 𝑎 ) = ( √ ‘ 𝑚 ) )
60 58 59 oveq12d ⊢ ( 𝑎 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
61 60 cbvmptv ⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
62 9 61 eqtri ⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
63 57 62 fmptd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℂ )
64 63 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
65 22 47 64 serf ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
66 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
67 15 rpregt0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
68 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
69 68 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
70 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
71 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
72 71 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
73 72 nnred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ )
74 72 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ 𝑑 )
75 15 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
76 fznnfl ⊢ ( 𝑥 ∈ ℝ → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥 ) ) )
77 75 76 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥 ) ) )
78 77 simplbda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ≤ 𝑥 )
79 70 73 69 74 78 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ 𝑥 )
80 flge1nn ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
81 69 79 80 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
82 eluznn ⊢ ( ( ( ⌊ ‘ 𝑥 ) ∈ ℕ ∧ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ℕ )
83 81 25 82 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ℕ )
84 66 83 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ∈ ℂ )
85 climcl ⊢ ( seq 1 ( + , 𝐹 ) ⇝ 𝑆 → 𝑆 ∈ ℂ )
86 11 85 syl ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
87 86 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑆 ∈ ℂ )
88 84 87 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ∈ ℂ )
89 88 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) ∈ ℝ )
90 66 81 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ∈ ℂ )
91 87 90 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ∈ ℂ )
92 91 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑆 − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ∈ ℝ )
93 89 92 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) + ( abs ‘ ( 𝑆 − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) ∈ ℝ )
94 2re ⊢ 2 ∈ ℝ
95 elrege0 ⊢ ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
96 10 95 sylib ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
97 96 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
98 remulcl ⊢ ( ( 2 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 2 · 𝐶 ) ∈ ℝ )
99 94 97 98 sylancr ⊢ ( 𝜑 → ( 2 · 𝐶 ) ∈ ℝ )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · 𝐶 ) ∈ ℝ )
101 15 rpsqrtcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
102 100 101 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ∈ ℝ )
103 102 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) ∈ ℝ )
104 ssun1 ⊢ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∪ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
105 104 27 sseqtrrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
106 105 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
107 ovex ⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / ( √ ‘ 𝑎 ) ) ∈ V
108 60 9 107 fvmpt3i ⊢ ( 𝑚 ∈ ℕ → ( 𝐹 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
109 38 108 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) → ( 𝐹 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
110 106 109 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
111 81 22 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) )
112 106 43 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
113 110 111 112 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
114 113 90 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
115 114 45 pncan2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) = Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
116 reflcl ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
117 69 116 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
118 117 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ 𝑥 ) < ( ( ⌊ ‘ 𝑥 ) + 1 ) )
119 fzdisj ⊢ ( ( ⌊ ‘ 𝑥 ) < ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) = ∅ )
120 118 119 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) = ∅ )
121 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ∈ Fin )
122 120 27 121 43 fsumsplit ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) )
123 83 22 eleqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ( ℤ≥ ‘ 1 ) )
124 109 123 43 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
125 122 124 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
126 125 113 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) )
127 115 126 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) = ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) )
128 127 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) )
129 84 90 87 abs3difd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ≤ ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) + ( abs ‘ ( 𝑆 − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) )
130 128 129 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ≤ ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) + ( abs ‘ ( 𝑆 − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) )
131 97 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐶 ∈ ℝ )
132 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
133 132 rpsqrtcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑥 ) ∈ ℝ+ )
134 131 133 rerpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 / ( √ ‘ 𝑥 ) ) ∈ ℝ )
135 2z ⊢ 2 ∈ ℤ
136 rpexpcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
137 15 135 136 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
138 137 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
139 72 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ+ )
140 138 139 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ+ )
141 140 rpsqrtcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ℝ+ )
142 131 141 rerpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ∈ ℝ )
143 2fveq3 ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑑 ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
144 143 fvoveq1d ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑑 ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) )
145 fveq2 ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑑 ) → ( √ ‘ 𝑦 ) = ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) )
146 145 oveq2d ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑑 ) → ( 𝐶 / ( √ ‘ 𝑦 ) ) = ( 𝐶 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
147 144 146 breq12d ⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑑 ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑦 ) ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ) )
148 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑦 ) ) )
149 137 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) ∈ ℝ )
150 nndivre ⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ )
151 149 71 150 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ )
152 24 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) )
153 70 69 151 79 152 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) )
154 1re ⊢ 1 ∈ ℝ
155 elicopnf ⊢ ( 1 ∈ ℝ → ( ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ( 1 [,) +∞ ) ↔ ( ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ ∧ 1 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
156 154 155 ax-mp ⊢ ( ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ( 1 [,) +∞ ) ↔ ( ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ ∧ 1 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) )
157 151 153 156 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ( 1 [,) +∞ ) )
158 147 148 157 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
159 133 rpregt0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( √ ‘ 𝑥 ) ) )
160 141 rpregt0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ℝ ∧ 0 < ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
161 96 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
162 132 rprege0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
163 140 rprege0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) )
164 sqrtle ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ∧ ( ( ( 𝑥 ↑ 2 ) / 𝑑 ) ∈ ℝ ∧ 0 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) → ( 𝑥 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ↔ ( √ ‘ 𝑥 ) ≤ ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
165 162 163 164 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ≤ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ↔ ( √ ‘ 𝑥 ) ≤ ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) )
166 152 165 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑥 ) ≤ ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) )
167 lediv2a ⊢ ( ( ( ( ( √ ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( √ ‘ 𝑥 ) ) ∧ ( ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ∈ ℝ ∧ 0 < ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ ( √ ‘ 𝑥 ) ≤ ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) → ( 𝐶 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ≤ ( 𝐶 / ( √ ‘ 𝑥 ) ) )
168 159 160 161 166 167 syl31anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 / ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ≤ ( 𝐶 / ( √ ‘ 𝑥 ) ) )
169 89 142 134 158 168 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑥 ) ) )
170 87 90 abssubd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑆 − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑆 ) ) )
171 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
172 171 fvoveq1d ⊢ ( 𝑦 = 𝑥 → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑆 ) ) )
173 fveq2 ⊢ ( 𝑦 = 𝑥 → ( √ ‘ 𝑦 ) = ( √ ‘ 𝑥 ) )
174 173 oveq2d ⊢ ( 𝑦 = 𝑥 → ( 𝐶 / ( √ ‘ 𝑦 ) ) = ( 𝐶 / ( √ ‘ 𝑥 ) ) )
175 172 174 breq12d ⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑦 ) ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑥 ) ) ) )
176 elicopnf ⊢ ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
177 154 176 ax-mp ⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) )
178 69 79 177 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 1 [,) +∞ ) )
179 175 148 178 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑥 ) ) )
180 170 179 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑆 − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ≤ ( 𝐶 / ( √ ‘ 𝑥 ) ) )
181 89 92 134 134 169 180 le2addd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) + ( abs ‘ ( 𝑆 − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) ≤ ( ( 𝐶 / ( √ ‘ 𝑥 ) ) + ( 𝐶 / ( √ ‘ 𝑥 ) ) ) )
182 2cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℂ )
183 97 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
184 183 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
185 184 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐶 ∈ ℂ )
186 101 rpcnne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) )
187 186 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) )
188 divass ⊢ ( ( 2 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ ( ( √ ‘ 𝑥 ) ∈ ℂ ∧ ( √ ‘ 𝑥 ) ≠ 0 ) ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) = ( 2 · ( 𝐶 / ( √ ‘ 𝑥 ) ) ) )
189 182 185 187 188 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) = ( 2 · ( 𝐶 / ( √ ‘ 𝑥 ) ) ) )
190 134 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 / ( √ ‘ 𝑥 ) ) ∈ ℂ )
191 190 2timesd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( 𝐶 / ( √ ‘ 𝑥 ) ) ) = ( ( 𝐶 / ( √ ‘ 𝑥 ) ) + ( 𝐶 / ( √ ‘ 𝑥 ) ) ) )
192 189 191 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) = ( ( 𝐶 / ( √ ‘ 𝑥 ) ) + ( 𝐶 / ( √ ‘ 𝑥 ) ) ) )
193 181 192 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) − 𝑆 ) ) + ( abs ‘ ( 𝑆 − ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑥 ) ) ) ) ) ≤ ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) )
194 46 93 103 130 193 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) ≤ ( ( 2 · 𝐶 ) / ( √ ‘ 𝑥 ) ) )