Theorem dchrisum0lem2

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	⊢ ( 𝜑 → 𝐻 ⇝𝑟 𝑈 )
	dchrisum0lem2.k	⊢ 𝐾 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
	dchrisum0lem2.e	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,) +∞ ) )
	dchrisum0lem2.t	⊢ ( 𝜑 → seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
	dchrisum0lem2.3	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑦 ) )
Assertion	dchrisum0lem2	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 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		dchrisum0lem2.k	⊢ 𝐾 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
16		dchrisum0lem2.e	⊢ ( 𝜑 → 𝐸 ∈ ( 0 [,) +∞ ) )
17		dchrisum0lem2.t	⊢ ( 𝜑 → seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
18		dchrisum0lem2.3	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑦 ) )
19		2cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
20		rpcn	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
22		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
23	7	ssrab3	⊢ 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
24	23 8	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 1 } ) )
25	24	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
26	25	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
27		elfzelz	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℤ )
28	27	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℤ )
29	4 1 5 2 26 28	dchrzrhcl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
30		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℕ )
31	30	nnrpd	⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℝ+ )
32	31	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ )
33	32	rpcnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℂ )
34	32	rpne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ≠ 0 )
35	29 33 34	divcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
36	22 35	fsumcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
37	21 36	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
38		rpssre	⊢ ℝ+ ⊆ ℝ
39		2cn	⊢ 2 ∈ ℂ
40		o1const	⊢ ( ( ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) )
41	38 39 40	mp2an	⊢ ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1)
42	41	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ 2 ) ∈ 𝑂(1) )
43	38	a1i	⊢ ( 𝜑 → ℝ+ ⊆ ℝ )
44		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
45		elrege0	⊢ ( 𝐸 ∈ ( 0 [,) +∞ ) ↔ ( 𝐸 ∈ ℝ ∧ 0 ≤ 𝐸 ) )
46	45	simplbi	⊢ ( 𝐸 ∈ ( 0 [,) +∞ ) → 𝐸 ∈ ℝ )
47	16 46	syl	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
48	21 36	absmuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( ( abs ‘ 𝑥 ) · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
49		rprege0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
50	49	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
51		absid	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( abs ‘ 𝑥 ) = 𝑥 )
52	50 51	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ 𝑥 ) = 𝑥 )
53	52	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( abs ‘ 𝑥 ) · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
54	48 53	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
55	54	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
56	36	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
57	56	subid1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) − 0 ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
58	30	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ )
59		2fveq3	⊢ ( 𝑎 = 𝑚 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) )
60		id	⊢ ( 𝑎 = 𝑚 → 𝑎 = 𝑚 )
61	59 60	oveq12d	⊢ ( 𝑎 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
62		ovex	⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ∈ V
63	61 15 62	fvmpt3i	⊢ ( 𝑚 ∈ ℕ → ( 𝐾 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
64	58 63	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐾 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
65	64	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐾 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
66		rpregt0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
67	66	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
68	67	simpld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
69		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
70		flge1nn	⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
71	68 69 70	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
72		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
73	71 72	eleqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) )
74	35	adantlrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
75	65 73 74	fsumser	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
76		eldifsni	⊢ ( 𝑋 ∈ ( 𝐷 ∖ { 1 } ) → 𝑋 ≠ 1 )
77	24 76	syl	⊢ ( 𝜑 → 𝑋 ≠ 1 )
78	1 2 3 4 5 6 25 77 15 16 17 18 7	dchrvmaeq0	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑊 ↔ 𝑇 = 0 ) )
79	8 78	mpbid	⊢ ( 𝜑 → 𝑇 = 0 )
80	79	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑇 = 0 )
81	80	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 = 𝑇 )
82	75 81	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) − 0 ) = ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) )
83	57 82	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) )
84	83	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) ) )
85		2fveq3	⊢ ( 𝑦 = 𝑥 → ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) )
86	85	fvoveq1d	⊢ ( 𝑦 = 𝑥 → ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) ) )
87		oveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐸 / 𝑦 ) = ( 𝐸 / 𝑥 ) )
88	86 87	breq12d	⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑦 ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑥 ) ) )
89	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑦 ) )
90		1re	⊢ 1 ∈ ℝ
91		elicopnf	⊢ ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
92	90 91	ax-mp	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) )
93	68 69 92	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ( 1 [,) +∞ ) )
94	88 89 93	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐾 ) ‘ ( ⌊ ‘ 𝑥 ) ) − 𝑇 ) ) ≤ ( 𝐸 / 𝑥 ) )
95	84 94	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ≤ ( 𝐸 / 𝑥 ) )
96	56	abscld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℝ )
97	47	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝐸 ∈ ℝ )
98		lemuldiv2	⊢ ( ( ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℝ ∧ 𝐸 ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ≤ 𝐸 ↔ ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ≤ ( 𝐸 / 𝑥 ) ) )
99	96 97 67 98	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ≤ 𝐸 ↔ ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ≤ ( 𝐸 / 𝑥 ) ) )
100	95 99	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 · ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ≤ 𝐸 )
101	55 100	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ≤ 𝐸 )
102	43 37 44 47 101	elo1d	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ∈ 𝑂(1) )
103	19 37 42 102	o1mul2	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) ∈ 𝑂(1) )
104		fzfid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ Fin )
105	32	rpsqrtcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑚 ) ∈ ℝ+ )
106	105	rpcnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑚 ) ∈ ℂ )
107	105	rpne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ 𝑚 ) ≠ 0 )
108	29 106 107	divcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
109	108	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ∈ ℂ )
110		elfznn	⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) → 𝑑 ∈ ℕ )
111	110	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → 𝑑 ∈ ℕ )
112	111	nnrpd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → 𝑑 ∈ ℝ+ )
113	112	rpsqrtcld	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ 𝑑 ) ∈ ℝ+ )
114	113	rpcnd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ 𝑑 ) ∈ ℂ )
115	113	rpne0d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ 𝑑 ) ≠ 0 )
116	109 114 115	divcld	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
117	104 116	fsumcl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
118	22 117	fsumcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
119		mulcl	⊢ ( ( 2 ∈ ℂ ∧ ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ∈ ℂ ) → ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ∈ ℂ )
120	39 37 119	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ∈ ℂ )
121		2re	⊢ 2 ∈ ℝ
122		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
123		2z	⊢ 2 ∈ ℤ
124		rpexpcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
125	122 123 124	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
126		rpdivcl	⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ )
127	125 31 126	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ )
128	127	rpsqrtcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ∈ ℝ+ )
129	128	rpred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ∈ ℝ )
130		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ∈ ℝ ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ ℝ )
131	121 129 130	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ ℝ )
132	131	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ ℂ )
133	108 132	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ∈ ℂ )
134	22 117 133	fsumsub	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
135	113	rpcnne0d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( √ ‘ 𝑑 ) ∈ ℂ ∧ ( √ ‘ 𝑑 ) ≠ 0 ) )
136		reccl	⊢ ( ( ( √ ‘ 𝑑 ) ∈ ℂ ∧ ( √ ‘ 𝑑 ) ≠ 0 ) → ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℂ )
137	135 136	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℂ )
138	104 137	fsumcl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ∈ ℂ )
139	108 138 132	subdid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
140		fveq2	⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( ⌊ ‘ 𝑦 ) = ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) )
141	140	oveq2d	⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) = ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
142	141	sumeq1d	⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) )
143		fveq2	⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( √ ‘ 𝑦 ) = ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) )
144	143	oveq2d	⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( 2 · ( √ ‘ 𝑦 ) ) = ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) )
145	142 144	oveq12d	⊢ ( 𝑦 = ( ( 𝑥 ↑ 2 ) / 𝑚 ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
146		ovex	⊢ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ∈ V
147	145 13 146	fvmpt3i	⊢ ( ( ( 𝑥 ↑ 2 ) / 𝑚 ) ∈ ℝ+ → ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
148	127 147	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
149	148	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
150	109 114 115	divrecd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 1 / ( √ ‘ 𝑑 ) ) ) )
151	150	sumeq2dv	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 1 / ( √ ‘ 𝑑 ) ) ) )
152	104 108 137	fsummulc2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 1 / ( √ ‘ 𝑑 ) ) ) )
153	151 152	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ) )
154	153	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( 1 / ( √ ‘ 𝑑 ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
155	139 149 154	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
156	155	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
157		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 2 · 𝑥 ) ∈ ℂ )
158	39 21 157	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · 𝑥 ) ∈ ℂ )
159	22 158 35	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 𝑥 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 2 · 𝑥 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
160	19 21 36	mulassd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 2 · 𝑥 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
161	158	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · 𝑥 ) ∈ ℂ )
162	161 108 106 107	div12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑥 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) ) )
163	105	rpcnne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) )
164		divdiv1	⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ ∧ ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) ∧ ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) ) )
165	29 163 163 164	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) ) )
166	32	rprege0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) )
167		remsqsqrt	⊢ ( ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) → ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) = 𝑚 )
168	166 167	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) = 𝑚 )
169	168	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑚 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
170	165 169	eqtr2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) )
171	170	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑥 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( 2 · 𝑥 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) ) )
172	125	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
173	172	rprege0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ↑ 2 ) ) )
174		sqrtdiv	⊢ ( ( ( ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ↑ 2 ) ) ∧ 𝑚 ∈ ℝ+ ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( ( √ ‘ ( 𝑥 ↑ 2 ) ) / ( √ ‘ 𝑚 ) ) )
175	173 32 174	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( ( √ ‘ ( 𝑥 ↑ 2 ) ) / ( √ ‘ 𝑚 ) ) )
176	49	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
177		sqrtsq	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( √ ‘ ( 𝑥 ↑ 2 ) ) = 𝑥 )
178	176 177	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( 𝑥 ↑ 2 ) ) = 𝑥 )
179	178	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( √ ‘ ( 𝑥 ↑ 2 ) ) / ( √ ‘ 𝑚 ) ) = ( 𝑥 / ( √ ‘ 𝑚 ) ) )
180	175 179	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) = ( 𝑥 / ( √ ‘ 𝑚 ) ) )
181	180	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( 2 · ( 𝑥 / ( √ ‘ 𝑚 ) ) ) )
182		2cnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℂ )
183	21	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
184		divass	⊢ ( ( 2 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) ) → ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) = ( 2 · ( 𝑥 / ( √ ‘ 𝑚 ) ) ) )
185	182 183 163 184	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) = ( 2 · ( 𝑥 / ( √ ‘ 𝑚 ) ) ) )
186	181 185	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) )
187	186	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( ( 2 · 𝑥 ) / ( √ ‘ 𝑚 ) ) ) )
188	162 171 187	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑥 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
189	188	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 2 · 𝑥 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
190	159 160 189	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) )
191	190	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 2 · ( √ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ) )
192	134 156 191	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) )
193	192	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) ) )
194	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dchrisum0lem2a	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) · ( 𝐻 ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) ∈ 𝑂(1) )
195	193 194	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) − ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) ) ∈ 𝑂(1) )
196	118 120 195	o1dif	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( 2 · ( 𝑥 · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) ) ∈ 𝑂(1) ) )
197	103 196	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) )