dchrisum0lem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dchrisum0lem1		Structured version Visualization version GIF version

Theorem dchrisum0lem1 25205

Description: Lemma for dchrisum0 25209. (Contributed by Mario Carneiro, 12-May-2016.) (Revised by Mario Carneiro, 7-Jun-2016.)

**Hypotheses**
Ref	Expression
rpvmasum.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l	⊢ 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a	⊢ (𝜑 → 𝑁 ∈ ℕ)
rpvmasum2.g	⊢ 𝐺 = (DChr‘𝑁)
rpvmasum2.d	⊢ 𝐷 = (Base‘𝐺)
rpvmasum2.1	⊢ 1 = (0_g‘𝐺)
rpvmasum2.w	⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}
dchrisum0.b	⊢ (𝜑 → 𝑋 ∈ 𝑊)
dchrisum0lem1.f	⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))
dchrisum0.c	⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
dchrisum0.s	⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)
dchrisum0.1	⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))

**Assertion**
Ref	Expression
dchrisum0lem1	⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))

Distinct variable groups: 𝑥,𝑚,𝑦, 1 𝑚,𝑑,𝑥,𝑦,𝐶 𝐹,𝑑,𝑥,𝑦 𝑎,𝑑,𝑚,𝑥,𝑦 𝑚,𝑁,𝑥,𝑦 𝜑,𝑑,𝑚,𝑥 𝑆,𝑑,𝑚,𝑥,𝑦 𝑥,𝑊 𝑚,𝑍,𝑥,𝑦 𝐷,𝑚,𝑥,𝑦 𝐿,𝑎,𝑑,𝑚,𝑥,𝑦 𝑋,𝑎,𝑑,𝑚,𝑥,𝑦 𝑚,𝐹 Allowed substitution hints: 𝜑(𝑦,𝑎) 𝐶(𝑎) 𝐷(𝑎,𝑑) 𝑆(𝑎) 1 (𝑎,𝑑) 𝐹(𝑎) 𝐺(𝑥,𝑦,𝑚,𝑎,𝑑) 𝑁(𝑎,𝑑) 𝑊(𝑦,𝑚,𝑎,𝑑) 𝑍(𝑎,𝑑)

**Proof of Theorem dchrisum0lem1**
Step	Hyp	Ref	Expression
1		fzfid 12772	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘𝑥)) ∈ Fin)
2		fzfid 12772	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∈ Fin)
3		fzfid 12772	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) ∈ Fin)
4		elfznn 12370	. . . . . . 7 ⊢ (𝑑 ∈ (1...(⌊‘𝑥)) → 𝑑 ∈ ℕ)
5		elfzuz 12338	. . . . . . 7 ⊢ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))
6	4, 5	anim12i 590	. . . . . 6 ⊢ ((𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) → (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1))))
7	6	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) → (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))))
8		elfzuz 12338	. . . . . . 7 ⊢ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) → 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))
9		elfznn 12370	. . . . . . 7 ⊢ (𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℕ)
10	8, 9	anim12ci 591	. . . . . 6 ⊢ ((𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1))))
11	10	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))))
12		eluzelz 11697	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)) → 𝑚 ∈ ℤ)
13	12	ad2antll 765	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈ ℤ)
14	13	zred 11482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈ ℝ)
15		simpr 477	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
16		2z 11409	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℤ
17		rpexpcl 12879	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (𝑥↑2) ∈ ℝ⁺)
18	15, 16, 17	sylancl 694	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑2) ∈ ℝ⁺)
19	18	rpred 11872	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑2) ∈ ℝ)
20	19	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) ∈ ℝ)
21		simprl 794	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑑 ∈ ℕ)
22	21	nnrpd 11870	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑑 ∈ ℝ⁺)
23	14, 20, 22	lemuldivd 11921	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑚 · 𝑑) ≤ (𝑥↑2) ↔ 𝑚 ≤ ((𝑥↑2) / 𝑑)))
24	21	nnred 11035	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑑 ∈ ℝ)
25	15	rprege0d 11879	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
26		flge0nn0 12621	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
27		nn0p1nn 11332	. . . . . . . . . . . . . 14 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → ((⌊‘𝑥) + 1) ∈ ℕ)
28	25, 26, 27	3syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) + 1) ∈ ℕ)
29	28	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((⌊‘𝑥) + 1) ∈ ℕ)
30		simprr 796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))
31		eluznn 11758	. . . . . . . . . . . 12 ⊢ ((((⌊‘𝑥) + 1) ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
32	29, 30, 31	syl2anc 693	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈ ℕ)
33	32	nnrpd 11870	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈ ℝ⁺)
34	24, 20, 33	lemuldiv2d 11922	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑚 · 𝑑) ≤ (𝑥↑2) ↔ 𝑑 ≤ ((𝑥↑2) / 𝑚)))
35	23, 34	bitr3d 270	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) ↔ 𝑑 ≤ ((𝑥↑2) / 𝑚)))
36		rpcn 11841	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
37	36	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℂ)
38	37	sqvald 13005	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑2) = (𝑥 · 𝑥))
39	38	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) = (𝑥 · 𝑥))
40		simplr 792	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑥 ∈ ℝ⁺)
41	40	rpred 11872	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑥 ∈ ℝ)
42		reflcl 12597	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
43		peano2re 10209	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘𝑥) ∈ ℝ → ((⌊‘𝑥) + 1) ∈ ℝ)
44	41, 42, 43	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((⌊‘𝑥) + 1) ∈ ℝ)
45		fllep1 12602	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1))
46	41, 45	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑥 ≤ ((⌊‘𝑥) + 1))
47		eluzle 11700	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)) → ((⌊‘𝑥) + 1) ≤ 𝑚)
48	47	ad2antll 765	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((⌊‘𝑥) + 1) ≤ 𝑚)
49	41, 44, 14, 46, 48	letrd 10194	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑥 ≤ 𝑚)
50	41, 14, 40	lemul1d 11915	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑥 ≤ 𝑚 ↔ (𝑥 · 𝑥) ≤ (𝑚 · 𝑥)))
51	49, 50	mpbid 222	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑥 · 𝑥) ≤ (𝑚 · 𝑥))
52	39, 51	eqbrtrd 4675	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) ≤ (𝑚 · 𝑥))
53	20, 41, 33	ledivmuld 11925	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (((𝑥↑2) / 𝑚) ≤ 𝑥 ↔ (𝑥↑2) ≤ (𝑚 · 𝑥)))
54	52, 53	mpbird 247	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑚) ≤ 𝑥)
55		nnre 11027	. . . . . . . . . . . . 13 ⊢ (𝑑 ∈ ℕ → 𝑑 ∈ ℝ)
56	55	ad2antrl 764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 𝑑 ∈ ℝ)
57	20, 32	nndivred 11069	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑚) ∈ ℝ)
58		letr 10131	. . . . . . . . . . . 12 ⊢ ((𝑑 ∈ ℝ ∧ ((𝑥↑2) / 𝑚) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑑 ≤ ((𝑥↑2) / 𝑚) ∧ ((𝑥↑2) / 𝑚) ≤ 𝑥) → 𝑑 ≤ 𝑥))
59	56, 57, 41, 58	syl3anc 1326	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑑 ≤ ((𝑥↑2) / 𝑚) ∧ ((𝑥↑2) / 𝑚) ≤ 𝑥) → 𝑑 ≤ 𝑥))
60	54, 59	mpan2d 710	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑑 ≤ ((𝑥↑2) / 𝑚) → 𝑑 ≤ 𝑥))
61	35, 60	sylbid 230	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) → 𝑑 ≤ 𝑥))
62	61	pm4.71rd 667	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) ↔ (𝑑 ≤ 𝑥 ∧ 𝑚 ≤ ((𝑥↑2) / 𝑑))))
63		nnge1 11046	. . . . . . . . . . . . . 14 ⊢ (𝑑 ∈ ℕ → 1 ≤ 𝑑)
64	63	ad2antrl 764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → 1 ≤ 𝑑)
65		1re 10039	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℝ
66		0lt1 10550	. . . . . . . . . . . . . . . 16 ⊢ 0 < 1
67	65, 66	pm3.2i 471	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ ℝ ∧ 0 < 1)
68	67	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (1 ∈ ℝ ∧ 0 < 1))
69	22	rpregt0d 11878	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑑 ∈ ℝ ∧ 0 < 𝑑))
70	18	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) ∈ ℝ⁺)
71	70	rpregt0d 11878	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) ∈ ℝ ∧ 0 < (𝑥↑2)))
72		lediv2 10913	. . . . . . . . . . . . . 14 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑑 ∈ ℝ ∧ 0 < 𝑑) ∧ ((𝑥↑2) ∈ ℝ ∧ 0 < (𝑥↑2))) → (1 ≤ 𝑑 ↔ ((𝑥↑2) / 𝑑) ≤ ((𝑥↑2) / 1)))
73	68, 69, 71, 72	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (1 ≤ 𝑑 ↔ ((𝑥↑2) / 𝑑) ≤ ((𝑥↑2) / 1)))
74	64, 73	mpbid 222	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑑) ≤ ((𝑥↑2) / 1))
75	20	recnd 10068	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) ∈ ℂ)
76	75	div1d 10793	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 1) = (𝑥↑2))
77	74, 76	breqtrd 4679	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑑) ≤ (𝑥↑2))
78		simpl 473	. . . . . . . . . . . . 13 ⊢ ((𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1))) → 𝑑 ∈ ℕ)
79		nndivre 11056	. . . . . . . . . . . . 13 ⊢ (((𝑥↑2) ∈ ℝ ∧ 𝑑 ∈ ℕ) → ((𝑥↑2) / 𝑑) ∈ ℝ)
80	19, 78, 79	syl2an 494	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑑) ∈ ℝ)
81		letr 10131	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℝ ∧ ((𝑥↑2) / 𝑑) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → ((𝑚 ≤ ((𝑥↑2) / 𝑑) ∧ ((𝑥↑2) / 𝑑) ≤ (𝑥↑2)) → 𝑚 ≤ (𝑥↑2)))
82	14, 80, 20, 81	syl3anc 1326	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑚 ≤ ((𝑥↑2) / 𝑑) ∧ ((𝑥↑2) / 𝑑) ≤ (𝑥↑2)) → 𝑚 ≤ (𝑥↑2)))
83	77, 82	mpan2d 710	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) → 𝑚 ≤ (𝑥↑2)))
84	35, 83	sylbird 250	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑑 ≤ ((𝑥↑2) / 𝑚) → 𝑚 ≤ (𝑥↑2)))
85	84	pm4.71rd 667	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑑 ≤ ((𝑥↑2) / 𝑚) ↔ (𝑚 ≤ (𝑥↑2) ∧ 𝑑 ≤ ((𝑥↑2) / 𝑚))))
86	35, 62, 85	3bitr3d 298	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑑 ≤ 𝑥 ∧ 𝑚 ≤ ((𝑥↑2) / 𝑑)) ↔ (𝑚 ≤ (𝑥↑2) ∧ 𝑑 ≤ ((𝑥↑2) / 𝑚))))
87		fznnfl 12661	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥)))
88	87	baibd 948	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ 𝑑 ≤ 𝑥))
89	41, 21, 88	syl2anc 693	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ 𝑑 ≤ 𝑥))
90	80	flcld 12599	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (⌊‘((𝑥↑2) / 𝑑)) ∈ ℤ)
91		elfz5 12334	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈ ℤ) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) ↔ 𝑚 ≤ (⌊‘((𝑥↑2) / 𝑑))))
92	30, 90, 91	syl2anc 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) ↔ 𝑚 ≤ (⌊‘((𝑥↑2) / 𝑑))))
93		flge 12606	. . . . . . . . . 10 ⊢ ((((𝑥↑2) / 𝑑) ∈ ℝ ∧ 𝑚 ∈ ℤ) → (𝑚 ≤ ((𝑥↑2) / 𝑑) ↔ 𝑚 ≤ (⌊‘((𝑥↑2) / 𝑑))))
94	80, 13, 93	syl2anc 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) ↔ 𝑚 ≤ (⌊‘((𝑥↑2) / 𝑑))))
95	92, 94	bitr4d 271	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) ↔ 𝑚 ≤ ((𝑥↑2) / 𝑑)))
96	89, 95	anbi12d 747	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) ↔ (𝑑 ≤ 𝑥 ∧ 𝑚 ≤ ((𝑥↑2) / 𝑑))))
97	20	flcld 12599	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (⌊‘(𝑥↑2)) ∈ ℤ)
98		elfz5 12334	. . . . . . . . . 10 ⊢ ((𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)) ∧ (⌊‘(𝑥↑2)) ∈ ℤ) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ↔ 𝑚 ≤ (⌊‘(𝑥↑2))))
99	30, 97, 98	syl2anc 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ↔ 𝑚 ≤ (⌊‘(𝑥↑2))))
100		flge 12606	. . . . . . . . . 10 ⊢ (((𝑥↑2) ∈ ℝ ∧ 𝑚 ∈ ℤ) → (𝑚 ≤ (𝑥↑2) ↔ 𝑚 ≤ (⌊‘(𝑥↑2))))
101	20, 13, 100	syl2anc 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ (𝑥↑2) ↔ 𝑚 ≤ (⌊‘(𝑥↑2))))
102	99, 101	bitr4d 271	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ↔ 𝑚 ≤ (𝑥↑2)))
103		fznnfl 12661	. . . . . . . . . 10 ⊢ (((𝑥↑2) / 𝑚) ∈ ℝ → (𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ ((𝑥↑2) / 𝑚))))
104	103	baibd 948	. . . . . . . . 9 ⊢ ((((𝑥↑2) / 𝑚) ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))) ↔ 𝑑 ≤ ((𝑥↑2) / 𝑚)))
105	57, 21, 104	syl2anc 693	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → (𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))) ↔ 𝑑 ≤ ((𝑥↑2) / 𝑚)))
106	102, 105	anbi12d 747	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) ↔ (𝑚 ≤ (𝑥↑2) ∧ 𝑑 ≤ ((𝑥↑2) / 𝑚))))
107	86, 96, 106	3bitr4d 300	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1)))) → ((𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) ↔ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))))))
108	107	ex 450	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝑑 ∈ ℕ ∧ 𝑚 ∈ (ℤ_≥‘((⌊‘𝑥) + 1))) → ((𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) ↔ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))))))
109	7, 11, 108	pm5.21ndd 369	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) ↔ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))))))
110		ssun2 3777	. . . . . . . 8 ⊢ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) ⊆ ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))))
111	28	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((⌊‘𝑥) + 1) ∈ ℕ)
112		nnuz 11723	. . . . . . . . . 10 ⊢ ℕ = (ℤ_≥‘1)
113	111, 112	syl6eleq 2711	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((⌊‘𝑥) + 1) ∈ (ℤ_≥‘1))
114		dchrisum0lem1a 25175	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (𝑥 ≤ ((𝑥↑2) / 𝑑) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈ (ℤ_≥‘(⌊‘𝑥))))
115	114	simprd 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (⌊‘((𝑥↑2) / 𝑑)) ∈ (ℤ_≥‘(⌊‘𝑥)))
116		fzsplit2 12366	. . . . . . . . 9 ⊢ ((((⌊‘𝑥) + 1) ∈ (ℤ_≥‘1) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈ (ℤ_≥‘(⌊‘𝑥))) → (1...(⌊‘((𝑥↑2) / 𝑑))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))))
117	113, 115, 116	syl2anc 693	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘((𝑥↑2) / 𝑑))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))))
118	110, 117	syl5sseqr 3654	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) ⊆ (1...(⌊‘((𝑥↑2) / 𝑑))))
119	118	sselda 3603	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑))))
120		rpvmasum2.g	. . . . . . . . 9 ⊢ 𝐺 = (DChr‘𝑁)
121		rpvmasum.z	. . . . . . . . 9 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
122		rpvmasum2.d	. . . . . . . . 9 ⊢ 𝐷 = (Base‘𝐺)
123		rpvmasum.l	. . . . . . . . 9 ⊢ 𝐿 = (ℤRHom‘𝑍)
124		rpvmasum2.w	. . . . . . . . . . . . 13 ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}
125		ssrab2 3687	. . . . . . . . . . . . 13 ⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 })
126	124, 125	eqsstri 3635	. . . . . . . . . . . 12 ⊢ 𝑊 ⊆ (𝐷 ∖ { 1 })
127		dchrisum0.b	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝑊)
128	126, 127	sseldi 3601	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 }))
129	128	eldifad 3586	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
130	129	ad3antrrr 766	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑋 ∈ 𝐷)
131		elfzelz 12342	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈ ℤ)
132	131	adantl 482	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℤ)
133	120, 121, 122, 123, 130, 132	dchrzrhcl 24970	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ)
134		elfznn 12370	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈ ℕ)
135	134	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℕ)
136	135	nnrpd 11870	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℝ⁺)
137	136	rpsqrtcld 14150	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ∈ ℝ⁺)
138	137	rpcnd 11874	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ∈ ℂ)
139	137	rpne0d 11877	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ≠ 0)
140	133, 138, 139	divcld 10801	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ)
141	4	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℕ)
142	141	nnrpd 11870	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → 𝑑 ∈ ℝ⁺)
143	142	rpsqrtcld 14150	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (√‘𝑑) ∈ ℝ⁺)
144	143	rpcnne0d 11881	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((√‘𝑑) ∈ ℂ ∧ (√‘𝑑) ≠ 0))
145	144	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → ((√‘𝑑) ∈ ℂ ∧ (√‘𝑑) ≠ 0))
146	145	simpld 475	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑑) ∈ ℂ)
147	145	simprd 479	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑑) ≠ 0)
148	140, 146, 147	divcld 10801	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘((𝑥↑2) / 𝑑)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ)
149	119, 148	syldan 487	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ)
150	149	anasss 679	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ)
151	1, 2, 3, 109, 150	fsumcom2 14505	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))
152	151	mpteq2dva 4744	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) = (𝑥 ∈ ℝ⁺ ↦ Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))
153	65	a1i 11	. . 3 ⊢ (𝜑 → 1 ∈ ℝ)
154		2cn 11091	. . . . . . . 8 ⊢ 2 ∈ ℂ
155	15	rpsqrtcld 14150	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (√‘𝑥) ∈ ℝ⁺)
156	155	rpcnd 11874	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (√‘𝑥) ∈ ℂ)
157		mulcl 10020	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (√‘𝑥) ∈ ℂ) → (2 · (√‘𝑥)) ∈ ℂ)
158	154, 156, 157	sylancr 695	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (2 · (√‘𝑥)) ∈ ℂ)
159	143	rprecred 11883	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 / (√‘𝑑)) ∈ ℝ)
160	1, 159	fsumrecl 14465	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) ∈ ℝ)
161	160	recnd 10068	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) ∈ ℂ)
162	161, 158	subcld 10392	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))) ∈ ℂ)
163		2re 11090	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
164		dchrisum0.c	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
165		elrege0 12278	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ (0[,)+∞) ↔ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
166	164, 165	sylib 208	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶))
167	166	simpld 475	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℝ)
168		remulcl 10021	. . . . . . . . . . 11 ⊢ ((2 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (2 · 𝐶) ∈ ℝ)
169	163, 167, 168	sylancr 695	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝐶) ∈ ℝ)
170	169	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (2 · 𝐶) ∈ ℝ)
171	170, 155	rerpdivcld 11903	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((2 · 𝐶) / (√‘𝑥)) ∈ ℝ)
172	171	recnd 10068	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((2 · 𝐶) / (√‘𝑥)) ∈ ℂ)
173	158, 162, 172	adddird 10065	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (((2 · (√‘𝑥)) + (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥)))) · ((2 · 𝐶) / (√‘𝑥))) = (((2 · (√‘𝑥)) · ((2 · 𝐶) / (√‘𝑥))) + ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥)))))
174	158, 161	pncan3d 10395	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((2 · (√‘𝑥)) + (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥)))) = Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)))
175	174	oveq1d 6665	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (((2 · (√‘𝑥)) + (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥)))) · ((2 · 𝐶) / (√‘𝑥))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))))
176		2cnd 11093	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 2 ∈ ℂ)
177	176, 156, 172	mulassd 10063	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((2 · (√‘𝑥)) · ((2 · 𝐶) / (√‘𝑥))) = (2 · ((√‘𝑥) · ((2 · 𝐶) / (√‘𝑥)))))
178	170	recnd 10068	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (2 · 𝐶) ∈ ℂ)
179	155	rpne0d 11877	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (√‘𝑥) ≠ 0)
180	178, 156, 179	divcan2d 10803	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((√‘𝑥) · ((2 · 𝐶) / (√‘𝑥))) = (2 · 𝐶))
181	180	oveq2d 6666	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (2 · ((√‘𝑥) · ((2 · 𝐶) / (√‘𝑥)))) = (2 · (2 · 𝐶)))
182	177, 181	eqtrd 2656	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((2 · (√‘𝑥)) · ((2 · 𝐶) / (√‘𝑥))) = (2 · (2 · 𝐶)))
183	182	oveq1d 6665	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (((2 · (√‘𝑥)) · ((2 · 𝐶) / (√‘𝑥))) + ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥)))) = ((2 · (2 · 𝐶)) + ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥)))))
184	173, 175, 183	3eqtr3d 2664	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))) = ((2 · (2 · 𝐶)) + ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥)))))
185	184	mpteq2dva 4744	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))) = (𝑥 ∈ ℝ⁺ ↦ ((2 · (2 · 𝐶)) + ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥))))))
186		remulcl 10021	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ (2 · 𝐶) ∈ ℝ) → (2 · (2 · 𝐶)) ∈ ℝ)
187	163, 169, 186	sylancr 695	. . . . . . 7 ⊢ (𝜑 → (2 · (2 · 𝐶)) ∈ ℝ)
188	187	recnd 10068	. . . . . 6 ⊢ (𝜑 → (2 · (2 · 𝐶)) ∈ ℂ)
189	188	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (2 · (2 · 𝐶)) ∈ ℂ)
190	162, 172	mulcld 10060	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥))) ∈ ℂ)
191		rpssre 11843	. . . . . 6 ⊢ ℝ⁺ ⊆ ℝ
192		o1const 14350	. . . . . 6 ⊢ ((ℝ⁺ ⊆ ℝ ∧ (2 · (2 · 𝐶)) ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ (2 · (2 · 𝐶))) ∈ 𝑂(1))
193	191, 188, 192	sylancr 695	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (2 · (2 · 𝐶))) ∈ 𝑂(1))
194		eqid 2622	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))))
195	194	divsqrsum 24708	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥)))) ∈ dom ⇝_𝑟
196		rlimdmo1 14348	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥)))) ∈ dom ⇝_𝑟 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥)))) ∈ 𝑂(1))
197	195, 196	mp1i 13	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥)))) ∈ 𝑂(1))
198	178, 156, 179	divrecd 10804	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((2 · 𝐶) / (√‘𝑥)) = ((2 · 𝐶) · (1 / (√‘𝑥))))
199	198	mpteq2dva 4744	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((2 · 𝐶) / (√‘𝑥))) = (𝑥 ∈ ℝ⁺ ↦ ((2 · 𝐶) · (1 / (√‘𝑥)))))
200	155	rprecred 11883	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1 / (√‘𝑥)) ∈ ℝ)
201	169	recnd 10068	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝐶) ∈ ℂ)
202		rlimconst 14275	. . . . . . . . . 10 ⊢ ((ℝ⁺ ⊆ ℝ ∧ (2 · 𝐶) ∈ ℂ) → (𝑥 ∈ ℝ⁺ ↦ (2 · 𝐶)) ⇝_𝑟 (2 · 𝐶))
203	191, 201, 202	sylancr 695	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (2 · 𝐶)) ⇝_𝑟 (2 · 𝐶))
204		sqrtlim 24699	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ ↦ (1 / (√‘𝑥))) ⇝_𝑟 0
205	204	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (1 / (√‘𝑥))) ⇝_𝑟 0)
206	170, 200, 203, 205	rlimmul 14375	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((2 · 𝐶) · (1 / (√‘𝑥)))) ⇝_𝑟 ((2 · 𝐶) · 0))
207	199, 206	eqbrtrd 4675	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((2 · 𝐶) / (√‘𝑥))) ⇝_𝑟 ((2 · 𝐶) · 0))
208		rlimo1 14347	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ↦ ((2 · 𝐶) / (√‘𝑥))) ⇝_𝑟 ((2 · 𝐶) · 0) → (𝑥 ∈ ℝ⁺ ↦ ((2 · 𝐶) / (√‘𝑥))) ∈ 𝑂(1))
209	207, 208	syl 17	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((2 · 𝐶) / (√‘𝑥))) ∈ 𝑂(1))
210	162, 172, 197, 209	o1mul2 14355	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥)))) ∈ 𝑂(1))
211	189, 190, 193, 210	o1add2 14354	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ ((2 · (2 · 𝐶)) + ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥))))) ∈ 𝑂(1))
212	185, 211	eqeltrd 2701	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))) ∈ 𝑂(1))
213	160, 171	remulcld 10070	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))) ∈ ℝ)
214	3, 149	fsumcl 14464	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ)
215	1, 214	fsumcl 14464	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ)
216	215	abscld 14175	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ ℝ)
217	213	recnd 10068	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))) ∈ ℂ)
218	217	abscld 14175	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘(Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))) ∈ ℝ)
219	214	abscld 14175	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ ℝ)
220	1, 219	fsumrecl 14465	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ ℝ)
221	1, 214	fsumabs 14533	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))
222	171	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((2 · 𝐶) / (√‘𝑥)) ∈ ℝ)
223	159, 222	remulcld 10070	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))) ∈ ℝ)
224	119, 140	syldan 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ)
225	3, 224	fsumcl 14464	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ)
226	225	abscld 14175	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ ℝ)
227		rpvmasum.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ)
228		rpvmasum2.1	. . . . . . . . . . 11 ⊢ 1 = (0_g‘𝐺)
229		dchrisum0lem1.f	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))
230		dchrisum0.s	. . . . . . . . . . 11 ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)
231		dchrisum0.1	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))
232	121, 123, 227, 120, 122, 228, 124, 127, 229, 164, 230, 231	dchrisum0lem1b 25204	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ ((2 · 𝐶) / (√‘𝑥)))
233	226, 222, 143, 232	lediv1dd 11930	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (√‘𝑑)) ≤ (((2 · 𝐶) / (√‘𝑥)) / (√‘𝑑)))
234	143	rpcnd 11874	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (√‘𝑑) ∈ ℂ)
235	143	rpne0d 11877	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (√‘𝑑) ≠ 0)
236	225, 234, 235	absdivd 14194	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) = ((abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (abs‘(√‘𝑑))))
237	3, 234, 224, 235	fsumdivc 14518	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))
238	237	fveq2d 6195	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) = (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))
239	143	rprege0d 11879	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((√‘𝑑) ∈ ℝ ∧ 0 ≤ (√‘𝑑)))
240		absid 14036	. . . . . . . . . . . 12 ⊢ (((√‘𝑑) ∈ ℝ ∧ 0 ≤ (√‘𝑑)) → (abs‘(√‘𝑑)) = (√‘𝑑))
241	239, 240	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘(√‘𝑑)) = (√‘𝑑))
242	241	oveq2d 6666	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (abs‘(√‘𝑑))) = ((abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (√‘𝑑)))
243	236, 238, 242	3eqtr3rd 2665	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (√‘𝑑)) = (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))
244	172	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → ((2 · 𝐶) / (√‘𝑥)) ∈ ℂ)
245	244, 234, 235	divrec2d 10805	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (((2 · 𝐶) / (√‘𝑥)) / (√‘𝑑)) = ((1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))))
246	233, 243, 245	3brtr3d 4684	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ ((1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))))
247	1, 219, 223, 246	fsumle 14531	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))))
248	159	recnd 10068	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (1 / (√‘𝑑)) ∈ ℂ)
249	1, 172, 248	fsummulc1 14517	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))) = Σ𝑑 ∈ (1...(⌊‘𝑥))((1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))))
250	247, 249	breqtrrd 4681	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))))
251	216, 220, 213, 221, 250	letrd 10194	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))))
252	213	leabsd 14153	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))) ≤ (abs‘(Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))))
253	216, 213, 218, 251, 252	letrd 10194	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ (abs‘(Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))))
254	253	adantrr 753	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ (abs‘(Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))))
255	153, 212, 213, 215, 254	o1le 14383	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))
256	152, 255	eqeltrrd 2702	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 {crab 2916 ∖ cdif 3571 ∪ cun 3572 ⊆ wss 3574 {csn 4177 class class class wbr 4653 ↦ cmpt 4729 dom cdm 5114 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 +∞cpnf 10071 < clt 10074 ≤ cle 10075 − cmin 10266 / cdiv 10684 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ℝ⁺crp 11832 [,)cico 12177 ...cfz 12326 ⌊cfl 12591 seqcseq 12801 ↑cexp 12860 √csqrt 13973 abscabs 13974 ⇝ cli 14215 ⇝_𝑟 crli 14216 𝑂(1)co1 14217 Σcsu 14416 Basecbs 15857 0_gc0g 16100 ℤRHomczrh 19848 ℤ/nℤczn 19851 DChrcdchr 24957

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015 ax-mulf 10016

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-tpos 7352 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-ec 7744 df-qs 7748 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ioc 12180 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-shft 13807 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-limsup 14202 df-clim 14219 df-rlim 14220 df-o1 14221 df-lo1 14222 df-sum 14417 df-ef 14798 df-sin 14800 df-cos 14801 df-pi 14803 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-starv 15956 df-sca 15957 df-vsca 15958 df-ip 15959 df-tset 15960 df-ple 15961 df-ds 15964 df-unif 15965 df-hom 15966 df-cco 15967 df-rest 16083 df-topn 16084 df-0g 16102 df-gsum 16103 df-topgen 16104 df-pt 16105 df-prds 16108 df-xrs 16162 df-qtop 16167 df-imas 16168 df-qus 16169 df-xps 16170 df-mre 16246 df-mrc 16247 df-acs 16249 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-mhm 17335 df-submnd 17336 df-grp 17425 df-minusg 17426 df-sbg 17427 df-mulg 17541 df-subg 17591 df-nsg 17592 df-eqg 17593 df-ghm 17658 df-cntz 17750 df-cmn 18195 df-abl 18196 df-mgp 18490 df-ur 18502 df-ring 18549 df-cring 18550 df-oppr 18623 df-dvdsr 18641 df-unit 18642 df-rnghom 18715 df-subrg 18778 df-lmod 18865 df-lss 18933 df-lsp 18972 df-sra 19172 df-rgmod 19173 df-lidl 19174 df-rsp 19175 df-2idl 19232 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-fbas 19743 df-fg 19744 df-cnfld 19747 df-zring 19819 df-zrh 19852 df-zn 19855 df-top 20699 df-topon 20716 df-topsp 20737 df-bases 20750 df-cld 20823 df-ntr 20824 df-cls 20825 df-nei 20902 df-lp 20940 df-perf 20941 df-cn 21031 df-cnp 21032 df-haus 21119 df-cmp 21190 df-tx 21365 df-hmeo 21558 df-fil 21650 df-fm 21742 df-flim 21743 df-flf 21744 df-xms 22125 df-ms 22126 df-tms 22127 df-cncf 22681 df-limc 23630 df-dv 23631 df-log 24303 df-cxp 24304 df-dchr 24958

This theorem is referenced by: dchrisum0lem3 25208

W3C validator