Theorem dchrisum0lem2a 27366

Description: Lemma for dchrisum0 27369. (Contributed by Mario Carneiro, 12-May-2016.)

Hypotheses

Ref	Expression
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	⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)
dchrisum0.1	⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))
dchrisum0lem2.h	⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦))))
dchrisum0lem2.u	⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈)

Assertion

Ref	Expression
dchrisum0lem2a	⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1))

Distinct variable groups:   𝑥,𝑚,𝑦, 1   𝑚,𝑑,𝑥,𝑦,𝐶   𝐹,𝑑,𝑥,𝑦   𝑎,𝑑,𝑚,𝑥,𝑦   𝑚,𝑁,𝑥,𝑦   𝜑,𝑑,𝑚,𝑥   𝑆,𝑑,𝑚,𝑥,𝑦   𝑈,𝑚,𝑥   𝑥,𝑊   𝑚,𝑍,𝑥,𝑦   𝐷,𝑚,𝑥,𝑦   𝐿,𝑎,𝑑,𝑚,𝑥,𝑦   𝑋,𝑎,𝑑,𝑚,𝑥,𝑦   𝑚,𝐹

Allowed substitution hints:   𝜑(𝑦,𝑎)   𝐶(𝑎)   𝐷(𝑎,𝑑)   𝑆(𝑎)   𝑈(𝑦,𝑎,𝑑)   1 (𝑎,𝑑)   𝐹(𝑎)   𝐺(𝑥,𝑦,𝑚,𝑎,𝑑)   𝐻(𝑥,𝑦,𝑚,𝑎,𝑑)   𝑁(𝑎,𝑑)   𝑊(𝑦,𝑚,𝑎,𝑑)   𝑍(𝑎,𝑑)

Proof of Theorem dchrisum0lem2a

Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 13935	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
2		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝜑)
3		elfznn 13527	. . . . 5 ⊢ (𝑚 ∈ (1...(⌊‘𝑥)) → 𝑚 ∈ ℕ)
4		rpvmasum2.g	. . . . . . 7 ⊢ 𝐺 = (DChr‘𝑁)
5		rpvmasum.z	. . . . . . 7 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
6		rpvmasum2.d	. . . . . . 7 ⊢ 𝐷 = (Base‘𝐺)
7		rpvmasum.l	. . . . . . 7 ⊢ 𝐿 = (ℤRHom‘𝑍)
8		rpvmasum2.w	. . . . . . . . . . 11 ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}
9	8	ssrab3 4072	. . . . . . . . . 10 ⊢ 𝑊 ⊆ (𝐷 ∖ { 1 })
10		dchrisum0.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝑊)
11	9, 10	sselid 3972	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 }))
12	11	eldifad 3952	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
13	12	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑋 ∈ 𝐷)
14		nnz 12576	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℤ)
15	14	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℤ)
16	4, 5, 6, 7, 13, 15	dchrzrhcl 27094	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ)
17		nnrp 12982	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
18	17	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
19	18	rpsqrtcld 15355	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈ ℝ+)
20	19	rpcnd 13015	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈ ℂ)
21	19	rpne0d 13018	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ≠ 0)
22	16, 20, 21	divcld 11987	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ)
23	2, 3, 22	syl2an 595	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ)
24	1, 23	fsumcl 15676	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ)
25		dchrisum0lem2.u	. . . . 5 ⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈)
26		rlimcl 15444	. . . . 5 ⊢ (𝐻 ⇝𝑟 𝑈 → 𝑈 ∈ ℂ)
27	25, 26	syl 17	. . . 4 ⊢ (𝜑 → 𝑈 ∈ ℂ)
28	27	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑈 ∈ ℂ)
29		0xr 11258	. . . . . . . . 9 ⊢ 0 ∈ ℝ*
30		0lt1 11733	. . . . . . . . 9 ⊢ 0 < 1
31		df-ioo 13325	. . . . . . . . . 10 ⊢ (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
32		df-ico 13327	. . . . . . . . . 10 ⊢ [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)})
33		xrltletr 13133	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤))
34	31, 32, 33	ixxss1 13339	. . . . . . . . 9 ⊢ ((0 ∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆ (0(,)+∞))
35	29, 30, 34	mp2an 689	. . . . . . . 8 ⊢ (1[,)+∞) ⊆ (0(,)+∞)
36		ioorp 13399	. . . . . . . 8 ⊢ (0(,)+∞) = ℝ+
37	35, 36	sseqtri 4010	. . . . . . 7 ⊢ (1[,)+∞) ⊆ ℝ+
38		resmpt 6027	. . . . . . 7 ⊢ ((1[,)+∞) ⊆ ℝ+ → ((𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))))
39	37, 38	ax-mp 5	. . . . . 6 ⊢ ((𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))
40	37	sseli 3970	. . . . . . . . 9 ⊢ (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ+)
41	3	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ)
42		2fveq3 6886	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑚 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑚)))
43		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑚 → (√‘𝑎) = (√‘𝑚))
44	42, 43	oveq12d 7419	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑚 → ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))
45		dchrisum0lem1.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))
46		ovex 7434	. . . . . . . . . . 11 ⊢ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) ∈ V
47	44, 45, 46	fvmpt3i 6993	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ → (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))
48	41, 47	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))
49	40, 48	sylanl2 678	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))
50		1re 11211	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
51		elicopnf 13419	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ → (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)))
52	50, 51	ax-mp 5	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥))
53		flge1nn 13783	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
54	52, 53	sylbi 216	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℕ)
55	54	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) → (⌊‘𝑥) ∈ ℕ)
56		nnuz 12862	. . . . . . . . 9 ⊢ ℕ = (ℤ≥‘1)
57	55, 56	eleqtrdi 2835	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) → (⌊‘𝑥) ∈ (ℤ≥‘1))
58	40, 23	sylanl2 678	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ)
59	49, 57, 58	fsumser 15673	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥)))
60	59	mpteq2dva 5238	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1[,)+∞) ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = (𝑥 ∈ (1[,)+∞) ↦ (seq1( + , 𝐹)‘(⌊‘𝑥))))
61	39, 60	eqtrid 2776	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦ (seq1( + , 𝐹)‘(⌊‘𝑥))))
62		fveq2 6881	. . . . . . 7 ⊢ (𝑚 = (⌊‘𝑥) → (seq1( + , 𝐹)‘𝑚) = (seq1( + , 𝐹)‘(⌊‘𝑥)))
63		rpssre 12978	. . . . . . . . 9 ⊢ ℝ+ ⊆ ℝ
64	63	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ+ ⊆ ℝ)
65	37, 64	sstrid 3985	. . . . . . 7 ⊢ (𝜑 → (1[,)+∞) ⊆ ℝ)
66		1zzd 12590	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
67	44	cbvmptv 5251	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))
68	45, 67	eqtri 2752	. . . . . . . . . . . 12 ⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))
69	22, 68	fmptd 7105	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℕ⟶ℂ)
70	69	ffvelcdmda 7076	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ ℂ)
71	56, 66, 70	serf 13993	. . . . . . . . 9 ⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ)
72	71	feqmptd 6950	. . . . . . . 8 ⊢ (𝜑 → seq1( + , 𝐹) = (𝑚 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑚)))
73		dchrisum0.s	. . . . . . . 8 ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)
74	72, 73	eqbrtrrd 5162	. . . . . . 7 ⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑚)) ⇝ 𝑆)
75	71	ffvelcdmda 7076	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq1( + , 𝐹)‘𝑚) ∈ ℂ)
76	52	simprbi 496	. . . . . . . 8 ⊢ (𝑥 ∈ (1[,)+∞) → 1 ≤ 𝑥)
77	76	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) → 1 ≤ 𝑥)
78	56, 62, 65, 66, 74, 75, 77	climrlim2 15488	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1[,)+∞) ↦ (seq1( + , 𝐹)‘(⌊‘𝑥))) ⇝𝑟 𝑆)
79		rlimo1 15558	. . . . . 6 ⊢ ((𝑥 ∈ (1[,)+∞) ↦ (seq1( + , 𝐹)‘(⌊‘𝑥))) ⇝𝑟 𝑆 → (𝑥 ∈ (1[,)+∞) ↦ (seq1( + , 𝐹)‘(⌊‘𝑥))) ∈ 𝑂(1))
80	78, 79	syl 17	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (1[,)+∞) ↦ (seq1( + , 𝐹)‘(⌊‘𝑥))) ∈ 𝑂(1))
81	61, 80	eqeltrd 2825	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) ∈ 𝑂(1))
82	24	fmpttd 7106	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))):ℝ+⟶ℂ)
83		1red 11212	. . . . 5 ⊢ (𝜑 → 1 ∈ ℝ)
84	82, 64, 83	o1resb 15507	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) ∈ 𝑂(1)))
85	81, 84	mpbird 257	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ 𝑂(1))
86		o1const 15561	. . . 4 ⊢ ((ℝ+ ⊆ ℝ ∧ 𝑈 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 𝑈) ∈ 𝑂(1))
87	63, 27, 86	sylancr 586	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 𝑈) ∈ 𝑂(1))
88	24, 28, 85, 87	o1mul2 15566	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) ∈ 𝑂(1))
89		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
90		2z 12591	. . . . . . . . 9 ⊢ 2 ∈ ℤ
91		rpexpcl 14043	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ+ ∧ 2 ∈ ℤ) → (𝑥↑2) ∈ ℝ+)
92	89, 90, 91	sylancl 585	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈ ℝ+)
93	3	nnrpd 13011	. . . . . . . 8 ⊢ (𝑚 ∈ (1...(⌊‘𝑥)) → 𝑚 ∈ ℝ+)
94		rpdivcl 12996	. . . . . . . 8 ⊢ (((𝑥↑2) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → ((𝑥↑2) / 𝑚) ∈ ℝ+)
95	92, 93, 94	syl2an 595	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((𝑥↑2) / 𝑚) ∈ ℝ+)
96		dchrisum0lem2.h	. . . . . . . . 9 ⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦))))
97	96	divsqrsumf 26829	. . . . . . . 8 ⊢ 𝐻:ℝ+⟶ℝ
98	97	ffvelcdmi 7075	. . . . . . 7 ⊢ (((𝑥↑2) / 𝑚) ∈ ℝ+ → (𝐻‘((𝑥↑2) / 𝑚)) ∈ ℝ)
99	95, 98	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝐻‘((𝑥↑2) / 𝑚)) ∈ ℝ)
100	99	recnd 11239	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝐻‘((𝑥↑2) / 𝑚)) ∈ ℂ)
101	23, 100	mulcld 11231	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) ∈ ℂ)
102	1, 101	fsumcl 15676	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) ∈ ℂ)
103	24, 28	mulcld 11231	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈) ∈ ℂ)
104	25	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝐻 ⇝𝑟 𝑈)
105	104, 26	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑈 ∈ ℂ)
106	23, 105	mulcld 11231	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈) ∈ ℂ)
107	1, 101, 106	fsumsub 15731	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)))
108	23, 100, 105	subdid 11667	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) = ((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)))
109	108	sumeq2dv 15646	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) = Σ𝑚 ∈ (1...(⌊‘𝑥))((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)))
110	1, 28, 23	fsummulc1 15728	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈) = Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))
111	110	oveq2d 7417	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)))
112	107, 109, 111	3eqtr4d 2774	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)))
113	112	mpteq2dva 5238	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))))
114	100, 105	subcld 11568	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈) ∈ ℂ)
115	23, 114	mulcld 11231	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ∈ ℂ)
116	1, 115	fsumcl 15676	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ∈ ℂ)
117	116	abscld 15380	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ ℝ)
118	115	abscld 15380	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ ℝ)
119	1, 118	fsumrecl 15677	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ ℝ)
120		1red 11212	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℝ)
121	1, 115	fsumabs 15744	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ Σ𝑚 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))))
122		rprege0 12986	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
123	122	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
124	123	simpld 494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
125		reflcl 13758	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
126	124, 125	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℝ)
127	126, 89	rerpdivcld 13044	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) / 𝑥) ∈ ℝ)
128		simplr 766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
129	128	rprecred 13024	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1 / 𝑥) ∈ ℝ)
130	23	abscld 15380	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ ℝ)
131	93	rpsqrtcld 15355	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1...(⌊‘𝑥)) → (√‘𝑚) ∈ ℝ+)
132	131	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (√‘𝑚) ∈ ℝ+)
133	132	rprecred 13024	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1 / (√‘𝑚)) ∈ ℝ)
134	114	abscld 15380	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ∈ ℝ)
135	132, 128	rpdivcld 13030	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((√‘𝑚) / 𝑥) ∈ ℝ+)
136	63, 135	sselid 3972	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((√‘𝑚) / 𝑥) ∈ ℝ)
137	23	absge0d 15388	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))))
138	114	absge0d 15388	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)))
139	2, 3, 16	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ)
140	132	rpcnd 13015	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (√‘𝑚) ∈ ℂ)
141	132	rpne0d 13018	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (√‘𝑚) ≠ 0)
142	139, 140, 141	absdivd 15399	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = ((abs‘(𝑋‘(𝐿‘𝑚))) / (abs‘(√‘𝑚))))
143	132	rprege0d 13020	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((√‘𝑚) ∈ ℝ ∧ 0 ≤ (√‘𝑚)))
144		absid 15240	. . . . . . . . . . . . . . . 16 ⊢ (((√‘𝑚) ∈ ℝ ∧ 0 ≤ (√‘𝑚)) → (abs‘(√‘𝑚)) = (√‘𝑚))
145	143, 144	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘(√‘𝑚)) = (√‘𝑚))
146	145	oveq2d 7417	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑋‘(𝐿‘𝑚))) / (abs‘(√‘𝑚))) = ((abs‘(𝑋‘(𝐿‘𝑚))) / (√‘𝑚)))
147	142, 146	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = ((abs‘(𝑋‘(𝐿‘𝑚))) / (√‘𝑚)))
148	139	abscld 15380	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑋‘(𝐿‘𝑚))) ∈ ℝ)
149		1red 11212	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
150		eqid 2724	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑍) = (Base‘𝑍)
151	12	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑋 ∈ 𝐷)
152		rpvmasum.a	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ ℕ)
153	152	nnnn0d 12529	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
154	5, 150, 7	znzrhfo 21410	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → 𝐿:ℤ–onto→(Base‘𝑍))
155		fof 6795	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
156	153, 154, 155	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍))
157	156	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿:ℤ⟶(Base‘𝑍))
158		elfzelz 13498	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (1...(⌊‘𝑥)) → 𝑚 ∈ ℤ)
159		ffvelcdm 7073	. . . . . . . . . . . . . . . 16 ⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑚 ∈ ℤ) → (𝐿‘𝑚) ∈ (Base‘𝑍))
160	157, 158, 159	syl2an 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝐿‘𝑚) ∈ (Base‘𝑍))
161	4, 6, 5, 150, 151, 160	dchrabs2 27111	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑋‘(𝐿‘𝑚))) ≤ 1)
162	148, 149, 132, 161	lediv1dd 13071	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑋‘(𝐿‘𝑚))) / (√‘𝑚)) ≤ (1 / (√‘𝑚)))
163	147, 162	eqbrtrd 5160	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ (1 / (√‘𝑚)))
164	96, 104	divsqrtsum2 26831	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ ((𝑥↑2) / 𝑚) ∈ ℝ+) → (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ≤ (1 / (√‘((𝑥↑2) / 𝑚))))
165	95, 164	mpdan 684	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ≤ (1 / (√‘((𝑥↑2) / 𝑚))))
166	92	rprege0d 13020	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝑥↑2) ∈ ℝ ∧ 0 ≤ (𝑥↑2)))
167		sqrtdiv 15209	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥↑2) ∈ ℝ ∧ 0 ≤ (𝑥↑2)) ∧ 𝑚 ∈ ℝ+) → (√‘((𝑥↑2) / 𝑚)) = ((√‘(𝑥↑2)) / (√‘𝑚)))
168	166, 93, 167	syl2an 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (√‘((𝑥↑2) / 𝑚)) = ((√‘(𝑥↑2)) / (√‘𝑚)))
169	122	ad2antlr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
170		sqrtsq 15213	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (√‘(𝑥↑2)) = 𝑥)
171	169, 170	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (√‘(𝑥↑2)) = 𝑥)
172	171	oveq1d 7416	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((√‘(𝑥↑2)) / (√‘𝑚)) = (𝑥 / (√‘𝑚)))
173	168, 172	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (√‘((𝑥↑2) / 𝑚)) = (𝑥 / (√‘𝑚)))
174	173	oveq2d 7417	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1 / (√‘((𝑥↑2) / 𝑚))) = (1 / (𝑥 / (√‘𝑚))))
175		rpcnne0 12989	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
176	175	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
177	132	rpcnne0d 13022	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((√‘𝑚) ∈ ℂ ∧ (√‘𝑚) ≠ 0))
178		recdiv 11917	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ ((√‘𝑚) ∈ ℂ ∧ (√‘𝑚) ≠ 0)) → (1 / (𝑥 / (√‘𝑚))) = ((√‘𝑚) / 𝑥))
179	176, 177, 178	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1 / (𝑥 / (√‘𝑚))) = ((√‘𝑚) / 𝑥))
180	174, 179	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1 / (√‘((𝑥↑2) / 𝑚))) = ((√‘𝑚) / 𝑥))
181	165, 180	breqtrd 5164	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ≤ ((√‘𝑚) / 𝑥))
182	130, 133, 134, 136, 137, 138, 163, 181	lemul12ad 12153	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) · (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ ((1 / (√‘𝑚)) · ((√‘𝑚) / 𝑥)))
183	23, 114	absmuld 15398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) = ((abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) · (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))))
184		1cnd 11206	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
185		dmdcan 11921	. . . . . . . . . . . . 13 ⊢ ((((√‘𝑚) ∈ ℂ ∧ (√‘𝑚) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ 1 ∈ ℂ) → (((√‘𝑚) / 𝑥) · (1 / (√‘𝑚))) = (1 / 𝑥))
186	177, 176, 184, 185	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((√‘𝑚) / 𝑥) · (1 / (√‘𝑚))) = (1 / 𝑥))
187	135	rpcnd 13015	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((√‘𝑚) / 𝑥) ∈ ℂ)
188		reccl 11876	. . . . . . . . . . . . . 14 ⊢ (((√‘𝑚) ∈ ℂ ∧ (√‘𝑚) ≠ 0) → (1 / (√‘𝑚)) ∈ ℂ)
189	177, 188	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1 / (√‘𝑚)) ∈ ℂ)
190	187, 189	mulcomd 11232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((√‘𝑚) / 𝑥) · (1 / (√‘𝑚))) = ((1 / (√‘𝑚)) · ((√‘𝑚) / 𝑥)))
191	186, 190	eqtr3d 2766	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1 / 𝑥) = ((1 / (√‘𝑚)) · ((√‘𝑚) / 𝑥)))
192	182, 183, 191	3brtr4d 5170	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ (1 / 𝑥))
193	1, 118, 129, 192	fsumle 15742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ Σ𝑚 ∈ (1...(⌊‘𝑥))(1 / 𝑥))
194		flge0nn0 13782	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
195		hashfz1 14303	. . . . . . . . . . . 12 ⊢ ((⌊‘𝑥) ∈ ℕ0 → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
196	123, 194, 195	3syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥))
197	196	oveq1d 7416	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((♯‘(1...(⌊‘𝑥))) · (1 / 𝑥)) = ((⌊‘𝑥) · (1 / 𝑥)))
198	89	rpreccld 13023	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
199	198	rpcnd 13015	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℂ)
200		fsumconst 15733	. . . . . . . . . . 11 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ (1 / 𝑥) ∈ ℂ) → Σ𝑚 ∈ (1...(⌊‘𝑥))(1 / 𝑥) = ((♯‘(1...(⌊‘𝑥))) · (1 / 𝑥)))
201	1, 199, 200	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(1 / 𝑥) = ((♯‘(1...(⌊‘𝑥))) · (1 / 𝑥)))
202	126	recnd 11239	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℂ)
203	175	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
204	203	simpld 494	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
205	203	simprd 495	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0)
206	202, 204, 205	divrecd 11990	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) / 𝑥) = ((⌊‘𝑥) · (1 / 𝑥)))
207	197, 201, 206	3eqtr4d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(1 / 𝑥) = ((⌊‘𝑥) / 𝑥))
208	193, 207	breqtrd 5164	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ ((⌊‘𝑥) / 𝑥))
209		flle 13761	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
210	124, 209	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ≤ 𝑥)
211	124	recnd 11239	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
212	211	mulridd 11228	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 · 1) = 𝑥)
213	210, 212	breqtrrd 5166	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ≤ (𝑥 · 1))
214		rpregt0 12985	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
215	214	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
216		ledivmul 12087	. . . . . . . . . 10 ⊢ (((⌊‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (((⌊‘𝑥) / 𝑥) ≤ 1 ↔ (⌊‘𝑥) ≤ (𝑥 · 1)))
217	126, 120, 215, 216	syl3anc 1368	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((⌊‘𝑥) / 𝑥) ≤ 1 ↔ (⌊‘𝑥) ≤ (𝑥 · 1)))
218	213, 217	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) / 𝑥) ≤ 1)
219	119, 127, 120, 208, 218	letrd 11368	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑚 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ 1)
220	117, 119, 120, 121, 219	letrd 11368	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ 1)
221	220	adantrr 714	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ 1)
222	64, 116, 83, 83, 221	elo1d 15477	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ 𝑂(1))
223	113, 222	eqeltrrd 2826	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) ∈ 𝑂(1))
224	102, 103, 223	o1dif 15571	. 2 ⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+ ↦ (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) ∈ 𝑂(1)))
225	88, 224	mpbird 257	1 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098   ≠ wne 2932  ∀wral 3053  {crab 3424   ∖ cdif 3937   ⊆ wss 3940  {csn 4620   class class class wbr 5138   ↦ cmpt 5221   ↾ cres 5668  ⟶wf 6529  –onto→wfo 6531  ‘cfv 6533  (class class class)co 7401  Fincfn 8935  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111  +∞cpnf 11242  ℝ^*cxr 11244   < clt 11245   ≤ cle 11246   − cmin 11441   / cdiv 11868  ℕcn 12209  2c2 12264  ℕ₀cn0 12469  ℤcz 12555  ℤ_≥cuz 12819  ℝ⁺crp 12971  (,)cioo 13321  [,)cico 13323  ...cfz 13481  ⌊cfl 13752  seqcseq 13963  ↑cexp 14024  ♯chash 14287  √csqrt 15177  abscabs 15178   ⇝ cli 15425   ⇝_𝑟 crli 15426  𝑂(1)co1 15427  Σcsu 15629  Basecbs 17143  0_gc0g 17384  ℤRHomczrh 21354  ℤ/nℤczn 21357  DChrcdchr 27081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-iin 4990  df-disj 5104  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-of 7663  df-om 7849  df-1st 7968  df-2nd 7969  df-supp 8141  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-omul 8466  df-er 8699  df-ec 8701  df-qs 8705  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-acn 9933  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-fac 14231  df-bc 14260  df-hash 14288  df-shft 15011  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-limsup 15412  df-clim 15429  df-rlim 15430  df-o1 15431  df-lo1 15432  df-sum 15630  df-ef 16008  df-sin 16010  df-cos 16011  df-pi 16013  df-dvds 16195  df-struct 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-ip 17214  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-hom 17220  df-cco 17221  df-rest 17367  df-topn 17368  df-0g 17386  df-gsum 17387  df-topgen 17388  df-pt 17389  df-prds 17392  df-xrs 17447  df-qtop 17452  df-imas 17453  df-qus 17454  df-xps 17455  df-mre 17529  df-mrc 17530  df-acs 17532  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-mhm 18703  df-submnd 18704  df-grp 18856  df-minusg 18857  df-sbg 18858  df-mulg 18986  df-subg 19040  df-nsg 19041  df-eqg 19042  df-ghm 19129  df-cntz 19223  df-od 19438  df-cmn 19692  df-abl 19693  df-mgp 20030  df-rng 20048  df-ur 20077  df-ring 20130  df-cring 20131  df-oppr 20226  df-dvdsr 20249  df-unit 20250  df-invr 20280  df-dvr 20293  df-rhm 20364  df-subrng 20436  df-subrg 20461  df-drng 20579  df-lmod 20698  df-lss 20769  df-lsp 20809  df-sra 21011  df-rgmod 21012  df-lidl 21057  df-rsp 21058  df-2idl 21097  df-psmet 21220  df-xmet 21221  df-met 21222  df-bl 21223  df-mopn 21224  df-fbas 21225  df-fg 21226  df-cnfld 21229  df-zring 21302  df-zrh 21358  df-zn 21361  df-top 22718  df-topon 22735  df-topsp 22757  df-bases 22771  df-cld 22845  df-ntr 22846  df-cls 22847  df-nei 22924  df-lp 22962  df-perf 22963  df-cn 23053  df-cnp 23054  df-haus 23141  df-cmp 23213  df-tx 23388  df-hmeo 23581  df-fil 23672  df-fm 23764  df-flim 23765  df-flf 23766  df-xms 24148  df-ms 24149  df-tms 24150  df-cncf 24720  df-limc 25717  df-dv 25718  df-log 26407  df-cxp 26408  df-dchr 27082

This theorem is referenced by:  dchrisum0lem2  27367