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	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 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) )