Metamath Proof Explorer

Theorem dchrisum0lem3

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 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑦 ) ) )
Assertion dchrisum0lem3 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 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 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
14 sumex ⊢ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ V
15 14 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ V )
16 sumex ⊢ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ V
17 16 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ V )
18 7 ssrab3 ⊢ 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
19 difss ⊢ ( 𝐷 ∖ { 1 } ) ⊆ 𝐷
20 18 19 sstri ⊢ 𝑊 ⊆ 𝐷
21 20 8 sseldi ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
22 18 8 sseldi ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐷 ∖ { 1 } ) )
23 eldifsni ⊢ ( 𝑋 ∈ ( 𝐷 ∖ { 1 } ) → 𝑋 ≠ 1 )
24 22 23 syl ⊢ ( 𝜑 → 𝑋 ≠ 1 )
25 eqid ⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
26 1 2 3 4 5 6 21 24 25 dchrmusumlema ⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) )
27 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑁 ∈ ℕ )
28 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑋 ∈ 𝑊 )
29 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
30 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
31 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / ( √ ‘ 𝑦 ) ) )
32 eqid ⊢ ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) )
33 32 divsqrsum ⊢ ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) ∈ dom ⇝𝑟
34 32 divsqrsumf ⊢ ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) : ℝ+ ⟶ ℝ
35 ax-resscn ⊢ ℝ ⊆ ℂ
36 fss ⊢ ( ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) : ℝ+ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) : ℝ+ ⟶ ℂ )
37 34 35 36 mp2an ⊢ ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) : ℝ+ ⟶ ℂ
38 37 a1i ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) : ℝ+ ⟶ ℂ )
39 rpsup ⊢ sup ( ℝ+ , ℝ* , < ) = +∞
40 39 a1i ⊢ ( 𝜑 → sup ( ℝ+ , ℝ* , < ) = +∞ )
41 38 40 rlimdm ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) ∈ dom ⇝𝑟 ↔ ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) ) ) )
42 33 41 mpbii ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( 1 / ( √ ‘ 𝑑 ) ) − ( 2 · ( √ ‘ 𝑦 ) ) ) ) ) )
44 simprl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑐 ∈ ( 0 [,) +∞ ) )
45 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 )
46 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) )
47 1 2 27 4 5 6 7 28 9 29 30 31 32 43 25 44 45 46 dchrisum0lem2 ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) )
48 47 rexlimdvaa ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) ) )
49 48 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) ) )
50 26 49 mpd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) )
51 1 2 3 4 5 6 7 8 9 10 11 12 dchrisum0lem1 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ 𝑂(1) )
52 15 17 50 51 o1add2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ) ∈ 𝑂(1) )
53 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ∈ V )
54 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ∈ Fin )
55 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ∈ Fin )
56 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → 𝑋 ∈ 𝐷 )
57 elfzelz ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) → 𝑚 ∈ ℤ )
58 57 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → 𝑚 ∈ ℤ )
59 4 1 5 2 56 58 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
60 59 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
61 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) → 𝑚 ∈ ℕ )
62 61 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → 𝑚 ∈ ℕ )
63 62 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → 𝑚 ∈ ℝ+ )
64 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) → 𝑑 ∈ ℕ )
65 64 nnrpd ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) → 𝑑 ∈ ℝ+ )
66 rpmulcl ⊢ ( ( 𝑚 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) → ( 𝑚 · 𝑑 ) ∈ ℝ+ )
67 63 65 66 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( 𝑚 · 𝑑 ) ∈ ℝ+ )
68 67 rpsqrtcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ ( 𝑚 · 𝑑 ) ) ∈ ℝ+ )
69 68 rpcnd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ ( 𝑚 · 𝑑 ) ) ∈ ℂ )
70 68 rpne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ ( 𝑚 · 𝑑 ) ) ≠ 0 )
71 60 69 70 divcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ∈ ℂ )
72 55 71 fsumcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ∈ ℂ )
73 54 72 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ∈ ℂ )
74 73 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∈ ℝ )
75 74 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∈ ℝ )
76 62 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → 𝑚 ∈ ℕ )
77 76 nnrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → 𝑚 ∈ ℝ+ )
78 77 rprege0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) )
79 64 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → 𝑑 ∈ ℕ )
80 79 nnrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → 𝑑 ∈ ℝ+ )
81 80 rprege0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( 𝑑 ∈ ℝ ∧ 0 ≤ 𝑑 ) )
82 sqrtmul ⊢ ( ( ( 𝑚 ∈ ℝ ∧ 0 ≤ 𝑚 ) ∧ ( 𝑑 ∈ ℝ ∧ 0 ≤ 𝑑 ) ) → ( √ ‘ ( 𝑚 · 𝑑 ) ) = ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑑 ) ) )
83 78 81 82 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ ( 𝑚 · 𝑑 ) ) = ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑑 ) ) )
84 83 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑑 ) ) ) )
85 77 rpsqrtcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ 𝑚 ) ∈ ℝ+ )
86 85 rpcnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) )
87 80 rpsqrtcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( √ ‘ 𝑑 ) ∈ ℝ+ )
88 87 rpcnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( √ ‘ 𝑑 ) ∈ ℂ ∧ ( √ ‘ 𝑑 ) ≠ 0 ) )
89 divdiv1 ⊢ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ ∧ ( ( √ ‘ 𝑚 ) ∈ ℂ ∧ ( √ ‘ 𝑚 ) ≠ 0 ) ∧ ( ( √ ‘ 𝑑 ) ∈ ℂ ∧ ( √ ‘ 𝑑 ) ≠ 0 ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑑 ) ) ) )
90 60 86 88 89 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( ( √ ‘ 𝑚 ) · ( √ ‘ 𝑑 ) ) ) )
91 84 90 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) )
92 91 sumeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) )
93 92 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) )
94 93 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) )
95 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
96 95 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
97 reflcl ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
98 96 97 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
99 98 ltp1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) < ( ( ⌊ ‘ 𝑥 ) + 1 ) )
100 fzdisj ⊢ ( ( ⌊ ‘ 𝑥 ) < ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) = ∅ )
101 99 100 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) = ∅ )
102 101 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) = ∅ )
103 95 rprege0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
104 flge0nn0 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
105 nn0p1nn ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
106 103 104 105 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
107 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
108 106 107 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
109 108 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
110 96 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
111 2z ⊢ 2 ∈ ℤ
112 rpexpcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
113 95 111 112 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
114 113 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
115 114 rpred ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ )
116 110 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℂ )
117 116 mulid1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 · 1 ) = 𝑥 )
118 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
119 1red ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ℝ )
120 rpregt0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
121 120 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
122 lemul2 ⊢ ( ( 1 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → ( 1 ≤ 𝑥 ↔ ( 𝑥 · 1 ) ≤ ( 𝑥 · 𝑥 ) ) )
123 119 110 121 122 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ≤ 𝑥 ↔ ( 𝑥 · 1 ) ≤ ( 𝑥 · 𝑥 ) ) )
124 118 123 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 · 1 ) ≤ ( 𝑥 · 𝑥 ) )
125 117 124 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ≤ ( 𝑥 · 𝑥 ) )
126 116 sqvald ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ↑ 2 ) = ( 𝑥 · 𝑥 ) )
127 125 126 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ≤ ( 𝑥 ↑ 2 ) )
128 flword2 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 ↑ 2 ) ∈ ℝ ∧ 𝑥 ≤ ( 𝑥 ↑ 2 ) ) → ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) )
129 110 115 127 128 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) )
130 fzsplit2 ⊢ ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) = ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∪ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) )
131 109 129 130 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) = ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∪ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) )
132 fzfid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ∈ Fin )
133 92 72 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
134 133 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ∈ ℂ )
135 102 131 132 134 fsumsplit ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) )
136 94 135 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) )
137 136 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) = ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ) )
138 75 137 eqled ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ≤ ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) + Σ 𝑚 ∈ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ 𝑚 ) ) / ( √ ‘ 𝑑 ) ) ) ) )
139 13 52 53 73 138 o1le ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 ↑ 2 ) ) ) Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ ( ( 𝑥 ↑ 2 ) / 𝑚 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / ( √ ‘ ( 𝑚 · 𝑑 ) ) ) ) ∈ 𝑂(1) )