dchrisum0lem3 - Metamath Proof Explorer

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

Theorem dchrisum0lem3 27463

Description: Lemma for dchrisum0 27464. (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 = (0_g‘𝐺)
rpvmasum2.w	⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}
dchrisum0.b	⊢ (𝜑 → 𝑋 ∈ 𝑊)
dchrisum0lem1.f	⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))
dchrisum0.c	⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
dchrisum0.s	⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)
dchrisum0.1	⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))

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

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

Proof of Theorem dchrisum0lem3 Dummy variables 𝑐 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1red 11119	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		sumex 15601	. . . 4 ⊢ Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V
3	2	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V)
4		sumex 15601	. . . 4 ⊢ Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V
5	4	a1i 11	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ V)
6		rpvmasum.z	. . . . 5 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
7		rpvmasum.l	. . . . 5 ⊢ 𝐿 = (ℤRHom‘𝑍)
8		rpvmasum.a	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9		rpvmasum2.g	. . . . 5 ⊢ 𝐺 = (DChr‘𝑁)
10		rpvmasum2.d	. . . . 5 ⊢ 𝐷 = (Base‘𝐺)
11		rpvmasum2.1	. . . . 5 ⊢ 1 = (0_g‘𝐺)
12		rpvmasum2.w	. . . . . . . 8 ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}
13	12	ssrab3 4031	. . . . . . 7 ⊢ 𝑊 ⊆ (𝐷 ∖ { 1 })
14		difss 4085	. . . . . . 7 ⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷
15	13, 14	sstri 3939	. . . . . 6 ⊢ 𝑊 ⊆ 𝐷
16		dchrisum0.b	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑊)
17	15, 16	sselid 3927	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
18	13, 16	sselid 3927	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 }))
19		eldifsni 4741	. . . . . 6 ⊢ (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋 ≠ 1 )
20	18, 19	syl 17	. . . . 5 ⊢ (𝜑 → 𝑋 ≠ 1 )
21		eqid 2731	. . . . 5 ⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))
22	6, 7, 8, 9, 10, 11, 17, 20, 21	dchrmusumlema 27437	. . . 4 ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))
23	8	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ)
24	16	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑋 ∈ 𝑊)
25		dchrisum0lem1.f	. . . . . . 7 ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))
26		dchrisum0.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))
27	26	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝐶 ∈ (0[,)+∞))
28		dchrisum0.s	. . . . . . . 8 ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)
29	28	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , 𝐹) ⇝ 𝑆)
30		dchrisum0.1	. . . . . . . 8 ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))
31	30	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))
32		eqid 2731	. . . . . . 7 ⊢ (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) = (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦))))
33	32	divsqrsum 26925	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) ∈ dom ⇝_𝑟
34	32	divsqrsumf 26924	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))):ℝ⁺⟶ℝ
35		ax-resscn 11069	. . . . . . . . . . . 12 ⊢ ℝ ⊆ ℂ
36		fss 6673	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))):ℝ⁺⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))):ℝ⁺⟶ℂ)
37	34, 35, 36	mp2an 692	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))):ℝ⁺⟶ℂ
38	37	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))):ℝ⁺⟶ℂ)
39		rpsup 13776	. . . . . . . . . . 11 ⊢ sup(ℝ⁺, ℝ^*, < ) = +∞
40	39	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → sup(ℝ⁺, ℝ^*, < ) = +∞)
41	38, 40	rlimdm 15464	. . . . . . . . 9 ⊢ (𝜑 → ((𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) ∈ dom ⇝_𝑟 ↔ (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) ⇝_𝑟 ( ⇝_𝑟 ‘(𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))))))
42	33, 41	mpbii 233	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) ⇝_𝑟 ( ⇝_𝑟 ‘(𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦))))))
43	42	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦)))) ⇝_𝑟 ( ⇝_𝑟 ‘(𝑦 ∈ ℝ⁺ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦))))))
44		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞))
45		simprrl 780	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡)
46		simprrr 781	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))
47	6, 7, 23, 9, 10, 11, 12, 24, 25, 27, 29, 31, 32, 43, 21, 44, 45, 46	dchrisum0lem2 27462	. . . . . 6 ⊢ ((𝜑 ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ⁺ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))
48	47	rexlimdvaa 3134	. . . . 5 ⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ⁺ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)))
49	48	exlimdv 1934	. . . 4 ⊢ (𝜑 → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ⁺ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)))
50	22, 49	mpd 15	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))
51	6, 7, 8, 9, 10, 11, 12, 16, 25, 26, 28, 30	dchrisum0lem1 27460	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))
52	3, 5, 50, 51	o1add2 15537	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) ∈ 𝑂(1))
53		ovexd 7387	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ V)
54		fzfid 13886	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (1...(⌊‘(𝑥↑2))) ∈ Fin)
55		fzfid 13886	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → (1...(⌊‘((𝑥↑2) / 𝑚))) ∈ Fin)
56	17	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → 𝑋 ∈ 𝐷)
57		elfzelz 13430	. . . . . . . 8 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥↑2))) → 𝑚 ∈ ℤ)
58	57	adantl 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℤ)
59	9, 6, 10, 7, 56, 58	dchrzrhcl 27189	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ)
60	59	adantr 480	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ)
61		elfznn 13459	. . . . . . . . . 10 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥↑2))) → 𝑚 ∈ ℕ)
62	61	adantl 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℕ)
63	62	nnrpd 12938	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → 𝑚 ∈ ℝ⁺)
64		elfznn 13459	. . . . . . . . 9 ⊢ (𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℕ)
65	64	nnrpd 12938	. . . . . . . 8 ⊢ (𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℝ⁺)
66		rpmulcl 12921	. . . . . . . 8 ⊢ ((𝑚 ∈ ℝ⁺ ∧ 𝑑 ∈ ℝ⁺) → (𝑚 · 𝑑) ∈ ℝ⁺)
67	63, 65, 66	syl2an 596	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑚 · 𝑑) ∈ ℝ⁺)
68	67	rpsqrtcld 15325	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ∈ ℝ⁺)
69	68	rpcnd 12942	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ∈ ℂ)
70	68	rpne0d 12945	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) ≠ 0)
71	60, 69, 70	divcld 11903	. . . 4 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ)
72	55, 71	fsumcl 15646	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ)
73	54, 72	fsumcl 15646	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) ∈ ℂ)
74	73	abscld 15352	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ ℝ)
75	74	adantrr 717	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ ℝ)
76	62	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑚 ∈ ℕ)
77	76	nnrpd 12938	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑚 ∈ ℝ⁺)
78	77	rprege0d 12947	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑚 ∈ ℝ ∧ 0 ≤ 𝑚))
79	64	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℕ)
80	79	nnrpd 12938	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → 𝑑 ∈ ℝ⁺)
81	80	rprege0d 12947	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑑 ∈ ℝ ∧ 0 ≤ 𝑑))
82		sqrtmul 15172	. . . . . . . . . . 11 ⊢ (((𝑚 ∈ ℝ ∧ 0 ≤ 𝑚) ∧ (𝑑 ∈ ℝ ∧ 0 ≤ 𝑑)) → (√‘(𝑚 · 𝑑)) = ((√‘𝑚) · (√‘𝑑)))
83	78, 81, 82	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘(𝑚 · 𝑑)) = ((√‘𝑚) · (√‘𝑑)))
84	83	oveq2d 7368	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑))))
85	77	rpsqrtcld 15325	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑚) ∈ ℝ⁺)
86	85	rpcnne0d 12949	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((√‘𝑚) ∈ ℂ ∧ (√‘𝑚) ≠ 0))
87	80	rpsqrtcld 15325	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (√‘𝑑) ∈ ℝ⁺)
88	87	rpcnne0d 12949	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((√‘𝑑) ∈ ℂ ∧ (√‘𝑑) ≠ 0))
89		divdiv1 11838	. . . . . . . . . 10 ⊢ (((𝑋‘(𝐿‘𝑚)) ∈ ℂ ∧ ((√‘𝑚) ∈ ℂ ∧ (√‘𝑚) ≠ 0) ∧ ((√‘𝑑) ∈ ℂ ∧ (√‘𝑑) ≠ 0)) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑))))
90	60, 86, 88, 89	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = ((𝑋‘(𝐿‘𝑚)) / ((√‘𝑚) · (√‘𝑑))))
91	84, 90	eqtr4d 2769	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))
92	91	sumeq2dv 15615	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))
93	92	sumeq2dv 15615	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))
94	93	adantrr 717	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))
95		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ⁺)
96	95	rpred 12940	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → 𝑥 ∈ ℝ)
97		reflcl 13706	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ∈ ℝ)
98	96, 97	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) ∈ ℝ)
99	98	ltp1d 12058	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (⌊‘𝑥) < ((⌊‘𝑥) + 1))
100		fzdisj 13457	. . . . . . . 8 ⊢ ((⌊‘𝑥) < ((⌊‘𝑥) + 1) → ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))) = ∅)
101	99, 100	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))) = ∅)
102	101	adantrr 717	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → ((1...(⌊‘𝑥)) ∩ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))) = ∅)
103	95	rprege0d 12947	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
104		flge0nn0 13730	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
105		nn0p1nn 12426	. . . . . . . . . 10 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → ((⌊‘𝑥) + 1) ∈ ℕ)
106	103, 104, 105	3syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) + 1) ∈ ℕ)
107		nnuz 12781	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
108	106, 107	eleqtrdi 2841	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → ((⌊‘𝑥) + 1) ∈ (ℤ_≥‘1))
109	108	adantrr 717	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → ((⌊‘𝑥) + 1) ∈ (ℤ_≥‘1))
110	96	adantrr 717	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
111		2z 12510	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
112		rpexpcl 13993	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (𝑥↑2) ∈ ℝ⁺)
113	95, 111, 112	sylancl 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (𝑥↑2) ∈ ℝ⁺)
114	113	adantrr 717	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (𝑥↑2) ∈ ℝ⁺)
115	114	rpred 12940	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (𝑥↑2) ∈ ℝ)
116	110	recnd 11146	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℂ)
117	116	mulridd 11135	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) = 𝑥)
118		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
119		1red 11119	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ)
120		rpregt0 12911	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
121	120	ad2antrl 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
122		lemul2 11980	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (1 ≤ 𝑥 ↔ (𝑥 · 1) ≤ (𝑥 · 𝑥)))
123	119, 110, 121, 122	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (1 ≤ 𝑥 ↔ (𝑥 · 1) ≤ (𝑥 · 𝑥)))
124	118, 123	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (𝑥 · 1) ≤ (𝑥 · 𝑥))
125	117, 124	eqbrtrrd 5117	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 𝑥 ≤ (𝑥 · 𝑥))
126	116	sqvald 14056	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (𝑥↑2) = (𝑥 · 𝑥))
127	125, 126	breqtrrd 5121	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → 𝑥 ≤ (𝑥↑2))
128		flword2 13723	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ ∧ 𝑥 ≤ (𝑥↑2)) → (⌊‘(𝑥↑2)) ∈ (ℤ_≥‘(⌊‘𝑥)))
129	110, 115, 127, 128	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (⌊‘(𝑥↑2)) ∈ (ℤ_≥‘(⌊‘𝑥)))
130		fzsplit2 13455	. . . . . . 7 ⊢ ((((⌊‘𝑥) + 1) ∈ (ℤ_≥‘1) ∧ (⌊‘(𝑥↑2)) ∈ (ℤ_≥‘(⌊‘𝑥))) → (1...(⌊‘(𝑥↑2))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))))
131	109, 129, 130	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (1...(⌊‘(𝑥↑2))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))))
132		fzfid 13886	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (1...(⌊‘(𝑥↑2))) ∈ Fin)
133	92, 72	eqeltrrd 2832	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ)
134	133	adantlrr 721	. . . . . 6 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘(𝑥↑2)))) → Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ)
135	102, 131, 132, 134	fsumsplit 15654	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))
136	94, 135	eqtrd 2766	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))))
137	136	fveq2d 6832	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))))
138	75, 137	eqled 11222	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ≤ (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) + Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))))
139	1, 52, 53, 73, 138	o1le 15566	1 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∃wex 1780 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 {crab 3395 Vcvv 3436 ∖ cdif 3894 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 ∅c0 4282 {csn 4575 class class class wbr 5093 ↦ cmpt 5174 dom cdm 5619 ⟶wf 6483 ‘cfv 6487 (class class class)co 7352 supcsup 9330 ℂcc 11010 ℝcr 11011 0cc0 11012 1c1 11013 + caddc 11015 · cmul 11017 +∞cpnf 11149 ℝ^*cxr 11151 < clt 11152 ≤ cle 11153 − cmin 11350 / cdiv 11780 ℕcn 12131 2c2 12186 ℕ₀cn0 12387 ℤcz 12474 ℤ_≥cuz 12738 ℝ⁺crp 12896 [,)cico 13253 ...cfz 13413 ⌊cfl 13700 seqcseq 13914 ↑cexp 13974 √csqrt 15146 abscabs 15147 ⇝ cli 15397 ⇝_𝑟 crli 15398 𝑂(1)co1 15399 Σcsu 15599 Basecbs 17126 0_gc0g 17349 ℤRHomczrh 21442 ℤ/nℤczn 21445 DChrcdchr 27176

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-inf2 9537 ax-cnex 11068 ax-resscn 11069 ax-1cn 11070 ax-icn 11071 ax-addcl 11072 ax-addrcl 11073 ax-mulcl 11074 ax-mulrcl 11075 ax-mulcom 11076 ax-addass 11077 ax-mulass 11078 ax-distr 11079 ax-i2m1 11080 ax-1ne0 11081 ax-1rid 11082 ax-rnegex 11083 ax-rrecex 11084 ax-cnre 11085 ax-pre-lttri 11086 ax-pre-lttrn 11087 ax-pre-ltadd 11088 ax-pre-mulgt0 11089 ax-pre-sup 11090 ax-addf 11091 ax-mulf 11092

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-tp 4580 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-iin 4944 df-disj 5061 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-isom 6496 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-of 7616 df-om 7803 df-1st 7927 df-2nd 7928 df-supp 8097 df-tpos 8162 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-2o 8392 df-oadd 8395 df-omul 8396 df-er 8628 df-ec 8630 df-qs 8634 df-map 8758 df-pm 8759 df-ixp 8828 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-fsupp 9252 df-fi 9301 df-sup 9332 df-inf 9333 df-oi 9402 df-card 9838 df-acn 9841 df-pnf 11154 df-mnf 11155 df-xr 11156 df-ltxr 11157 df-le 11158 df-sub 11352 df-neg 11353 df-div 11781 df-nn 12132 df-2 12194 df-3 12195 df-4 12196 df-5 12197 df-6 12198 df-7 12199 df-8 12200 df-9 12201 df-n0 12388 df-xnn0 12461 df-z 12475 df-dec 12595 df-uz 12739 df-q 12853 df-rp 12897 df-xneg 13017 df-xadd 13018 df-xmul 13019 df-ioo 13255 df-ioc 13256 df-ico 13257 df-icc 13258 df-fz 13414 df-fzo 13561 df-fl 13702 df-mod 13780 df-seq 13915 df-exp 13975 df-fac 14187 df-bc 14216 df-hash 14244 df-shft 14980 df-cj 15012 df-re 15013 df-im 15014 df-sqrt 15148 df-abs 15149 df-limsup 15384 df-clim 15401 df-rlim 15402 df-o1 15403 df-lo1 15404 df-sum 15600 df-ef 15980 df-sin 15982 df-cos 15983 df-pi 15985 df-dvds 16170 df-gcd 16412 df-phi 16683 df-struct 17064 df-sets 17081 df-slot 17099 df-ndx 17111 df-base 17127 df-ress 17148 df-plusg 17180 df-mulr 17181 df-starv 17182 df-sca 17183 df-vsca 17184 df-ip 17185 df-tset 17186 df-ple 17187 df-ds 17189 df-unif 17190 df-hom 17191 df-cco 17192 df-rest 17332 df-topn 17333 df-0g 17351 df-gsum 17352 df-topgen 17353 df-pt 17354 df-prds 17357 df-xrs 17412 df-qtop 17417 df-imas 17418 df-qus 17419 df-xps 17420 df-mre 17494 df-mrc 17495 df-acs 17497 df-mgm 18554 df-sgrp 18633 df-mnd 18649 df-mhm 18697 df-submnd 18698 df-grp 18855 df-minusg 18856 df-sbg 18857 df-mulg 18987 df-subg 19042 df-nsg 19043 df-eqg 19044 df-ghm 19131 df-cntz 19235 df-od 19446 df-cmn 19700 df-abl 19701 df-mgp 20065 df-rng 20077 df-ur 20106 df-ring 20159 df-cring 20160 df-oppr 20261 df-dvdsr 20281 df-unit 20282 df-invr 20312 df-dvr 20325 df-rhm 20396 df-subrng 20467 df-subrg 20491 df-drng 20652 df-lmod 20801 df-lss 20871 df-lsp 20911 df-sra 21113 df-rgmod 21114 df-lidl 21151 df-rsp 21152 df-2idl 21193 df-psmet 21289 df-xmet 21290 df-met 21291 df-bl 21292 df-mopn 21293 df-fbas 21294 df-fg 21295 df-cnfld 21298 df-zring 21390 df-zrh 21446 df-zn 21449 df-top 22815 df-topon 22832 df-topsp 22854 df-bases 22867 df-cld 22940 df-ntr 22941 df-cls 22942 df-nei 23019 df-lp 23057 df-perf 23058 df-cn 23148 df-cnp 23149 df-haus 23236 df-cmp 23308 df-tx 23483 df-hmeo 23676 df-fil 23767 df-fm 23859 df-flim 23860 df-flf 23861 df-xms 24241 df-ms 24242 df-tms 24243 df-cncf 24804 df-limc 25800 df-dv 25801 df-log 26498 df-cxp 26499 df-dchr 27177

This theorem is referenced by: dchrisum0 27464

W3C validator