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) )