Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
2 | | simpl 473 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝜑) |
3 | | elfznn 12370 |
. . . . 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 | | ssrab2 3687 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
10 | 8, 9 | eqsstri 3635 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
11 | | dchrisum0.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
12 | 10, 11 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
13 | 12 | eldifad 3586 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
14 | 13 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑋 ∈ 𝐷) |
15 | | nnz 11399 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
16 | 15 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℤ) |
17 | 4, 5, 6, 7, 14, 16 | dchrzrhcl 24970 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
18 | | nnrp 11842 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
19 | 18 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+) |
20 | 19 | rpsqrtcld 14150 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈
ℝ+) |
21 | 20 | rpcnd 11874 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈
ℂ) |
22 | 20 | rpne0d 11877 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ≠ 0) |
23 | 17, 21, 22 | divcld 10801 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
24 | 2, 3, 23 | syl2an 494 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
25 | 1, 24 | fsumcl 14464 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
26 | | dchrisum0lem2.u |
. . . . 5
⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈) |
27 | | rlimcl 14234 |
. . . . 5
⊢ (𝐻 ⇝𝑟
𝑈 → 𝑈 ∈ ℂ) |
28 | 26, 27 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ ℂ) |
29 | 28 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑈 ∈
ℂ) |
30 | | 0xr 10086 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
31 | | 0lt1 10550 |
. . . . . . . . 9
⊢ 0 <
1 |
32 | | df-ioo 12179 |
. . . . . . . . . 10
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
33 | | df-ico 12181 |
. . . . . . . . . 10
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
34 | | xrltletr 11988 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤)) |
35 | 32, 33, 34 | ixxss1 12193 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆
(0(,)+∞)) |
36 | 30, 31, 35 | mp2an 708 |
. . . . . . . 8
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
37 | | ioorp 12251 |
. . . . . . . 8
⊢
(0(,)+∞) = ℝ+ |
38 | 36, 37 | sseqtri 3637 |
. . . . . . 7
⊢
(1[,)+∞) ⊆ ℝ+ |
39 | | resmpt 5449 |
. . . . . . 7
⊢
((1[,)+∞) ⊆ ℝ+ → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))) |
40 | 38, 39 | ax-mp 5 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
41 | 38 | sseli 3599 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ+) |
42 | 3 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
ℕ) |
43 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑚 → (𝐿‘𝑎) = (𝐿‘𝑚)) |
44 | 43 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑚 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑚))) |
45 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑚 → (√‘𝑎) = (√‘𝑚)) |
46 | 44, 45 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑚 → ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
47 | | dchrisum0lem1.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
48 | | ovex 6678 |
. . . . . . . . . . 11
⊢ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) ∈ V |
49 | 46, 47, 48 | fvmpt3i 6287 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
50 | 42, 49 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
51 | 41, 50 | sylanl2 683 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
52 | | 1re 10039 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
53 | | elicopnf 12269 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
55 | | flge1nn 12622 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
56 | 54, 55 | sylbi 207 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℕ) |
57 | 56 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) →
(⌊‘𝑥) ∈
ℕ) |
58 | | nnuz 11723 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
59 | 57, 58 | syl6eleq 2711 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) →
(⌊‘𝑥) ∈
(ℤ≥‘1)) |
60 | 41, 24 | sylanl2 683 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
61 | 51, 59, 60 | fsumser 14461 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) → Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
62 | 61 | mpteq2dva 4744 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1[,)+∞) ↦ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = (𝑥 ∈ (1[,)+∞) ↦ (seq1( + ,
𝐹)‘(⌊‘𝑥)))) |
63 | 40, 62 | syl5eq 2668 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦
(seq1( + , 𝐹)‘(⌊‘𝑥)))) |
64 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑚 = (⌊‘𝑥) → (seq1( + , 𝐹)‘𝑚) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
65 | | rpssre 11843 |
. . . . . . . . 9
⊢
ℝ+ ⊆ ℝ |
66 | 65 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ+
⊆ ℝ) |
67 | 38, 66 | syl5ss 3614 |
. . . . . . 7
⊢ (𝜑 → (1[,)+∞) ⊆
ℝ) |
68 | | 1zzd 11408 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
69 | 46 | cbvmptv 4750 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
70 | 47, 69 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
71 | 23, 70 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) |
72 | 71 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ ℂ) |
73 | 58, 68, 72 | serf 12829 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
74 | 73 | feqmptd 6249 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) = (𝑚 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑚))) |
75 | | dchrisum0.s |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) |
76 | 74, 75 | eqbrtrrd 4677 |
. . . . . . 7
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑚)) ⇝ 𝑆) |
77 | 73 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq1( + , 𝐹)‘𝑚) ∈ ℂ) |
78 | 54 | simprbi 480 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) → 1
≤ 𝑥) |
79 | 78 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) → 1 ≤ 𝑥) |
80 | 58, 64, 67, 68, 76, 77, 79 | climrlim2 14278 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1[,)+∞) ↦ (seq1( + ,
𝐹)‘(⌊‘𝑥))) ⇝𝑟 𝑆) |
81 | | rlimo1 14347 |
. . . . . 6
⊢ ((𝑥 ∈ (1[,)+∞) ↦
(seq1( + , 𝐹)‘(⌊‘𝑥))) ⇝𝑟 𝑆 → (𝑥 ∈ (1[,)+∞) ↦ (seq1( + ,
𝐹)‘(⌊‘𝑥))) ∈ 𝑂(1)) |
82 | 80, 81 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (1[,)+∞) ↦ (seq1( + ,
𝐹)‘(⌊‘𝑥))) ∈ 𝑂(1)) |
83 | 63, 82 | eqeltrd 2701 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) ∈
𝑂(1)) |
84 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
85 | 25, 84 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))):ℝ+⟶ℂ) |
86 | | 1red 10055 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
87 | 85, 66, 86 | o1resb 14297 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) ∈
𝑂(1))) |
88 | 83, 87 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ 𝑂(1)) |
89 | | o1const 14350 |
. . . 4
⊢
((ℝ+ ⊆ ℝ ∧ 𝑈 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 𝑈) ∈
𝑂(1)) |
90 | 65, 28, 89 | sylancr 695 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 𝑈) ∈
𝑂(1)) |
91 | 25, 29, 88, 90 | o1mul2 14355 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) ∈ 𝑂(1)) |
92 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
93 | | 2z 11409 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
94 | | rpexpcl 12879 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑥↑2) ∈
ℝ+) |
95 | 92, 93, 94 | sylancl 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ+) |
96 | 3 | nnrpd 11870 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℝ+) |
97 | | rpdivcl 11856 |
. . . . . . . 8
⊢ (((𝑥↑2) ∈
ℝ+ ∧ 𝑚
∈ ℝ+) → ((𝑥↑2) / 𝑚) ∈
ℝ+) |
98 | 95, 96, 97 | syl2an 494 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) / 𝑚) ∈
ℝ+) |
99 | | dchrisum0lem2.h |
. . . . . . . . 9
⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) |
100 | 99 | divsqrsumf 24707 |
. . . . . . . 8
⊢ 𝐻:ℝ+⟶ℝ |
101 | 100 | ffvelrni 6358 |
. . . . . . 7
⊢ (((𝑥↑2) / 𝑚) ∈ ℝ+ → (𝐻‘((𝑥↑2) / 𝑚)) ∈ ℝ) |
102 | 98, 101 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐻‘((𝑥↑2) / 𝑚)) ∈ ℝ) |
103 | 102 | recnd 10068 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐻‘((𝑥↑2) / 𝑚)) ∈ ℂ) |
104 | 24, 103 | mulcld 10060 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) ∈ ℂ) |
105 | 1, 104 | fsumcl 14464 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) ∈ ℂ) |
106 | 25, 29 | mulcld 10060 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈) ∈ ℂ) |
107 | 26 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝐻
⇝𝑟 𝑈) |
108 | 107, 27 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑈 ∈
ℂ) |
109 | 24, 108 | mulcld 10060 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈) ∈ ℂ) |
110 | 1, 104, 109 | fsumsub 14520 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
111 | 24, 103, 108 | subdid 10486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) = ((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
112 | 111 | sumeq2dv 14433 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) = Σ𝑚 ∈ (1...(⌊‘𝑥))((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
113 | 1, 29, 24 | fsummulc1 14517 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈) = Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) |
114 | 113 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
115 | 110, 112,
114 | 3eqtr4d 2666 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
116 | 115 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)))) |
117 | 103, 108 | subcld 10392 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈) ∈ ℂ) |
118 | 24, 117 | mulcld 10060 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ∈ ℂ) |
119 | 1, 118 | fsumcl 14464 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ∈ ℂ) |
120 | 119 | abscld 14175 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ ℝ) |
121 | 118 | abscld 14175 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ ℝ) |
122 | 1, 121 | fsumrecl 14465 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ ℝ) |
123 | | 1red 10055 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℝ) |
124 | 1, 118 | fsumabs 14533 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ Σ𝑚 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)))) |
125 | | rprege0 11847 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
126 | 125 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
127 | 126 | simpld 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
128 | | reflcl 12597 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
129 | 127, 128 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ∈
ℝ) |
130 | 129, 92 | rerpdivcld 11903 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) / 𝑥) ∈
ℝ) |
131 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
132 | 131 | rprecred 11883 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑥) ∈
ℝ) |
133 | 24 | abscld 14175 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ ℝ) |
134 | 96 | rpsqrtcld 14150 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ (√‘𝑚)
∈ ℝ+) |
135 | 134 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑚)
∈ ℝ+) |
136 | 135 | rprecred 11883 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘𝑚)) ∈ ℝ) |
137 | 117 | abscld 14175 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ∈ ℝ) |
138 | 135, 131 | rpdivcld 11889 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚) /
𝑥) ∈
ℝ+) |
139 | 65, 138 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚) /
𝑥) ∈
ℝ) |
140 | 24 | absge0d 14183 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))) |
141 | 117 | absge0d 14183 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) |
142 | 2, 3, 17 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
143 | 135 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑚)
∈ ℂ) |
144 | 135 | rpne0d 11877 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑚)
≠ 0) |
145 | 142, 143,
144 | absdivd 14194 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = ((abs‘(𝑋‘(𝐿‘𝑚))) / (abs‘(√‘𝑚)))) |
146 | 135 | rprege0d 11879 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚)
∈ ℝ ∧ 0 ≤ (√‘𝑚))) |
147 | | absid 14036 |
. . . . . . . . . . . . . . . 16
⊢
(((√‘𝑚)
∈ ℝ ∧ 0 ≤ (√‘𝑚)) → (abs‘(√‘𝑚)) = (√‘𝑚)) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(√‘𝑚)) = (√‘𝑚)) |
149 | 148 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑚))) / (abs‘(√‘𝑚))) = ((abs‘(𝑋‘(𝐿‘𝑚))) / (√‘𝑚))) |
150 | 145, 149 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = ((abs‘(𝑋‘(𝐿‘𝑚))) / (√‘𝑚))) |
151 | 142 | abscld 14175 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑚))) ∈ ℝ) |
152 | | 1red 10055 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
153 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑍) =
(Base‘𝑍) |
154 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑋 ∈ 𝐷) |
155 | | rpvmasum.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℕ) |
156 | 155 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
157 | 5, 153, 7 | znzrhfo 19896 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
158 | | fof 6115 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
159 | 156, 157,
158 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
160 | 159 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿:ℤ⟶(Base‘𝑍)) |
161 | | elfzelz 12342 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℤ) |
162 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑚 ∈ ℤ) → (𝐿‘𝑚) ∈ (Base‘𝑍)) |
163 | 160, 161,
162 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑚) ∈ (Base‘𝑍)) |
164 | 4, 6, 5, 153, 154, 163 | dchrabs2 24987 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑚))) ≤ 1) |
165 | 151, 152,
135, 164 | lediv1dd 11930 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑚))) / (√‘𝑚)) ≤ (1 / (√‘𝑚))) |
166 | 150, 165 | eqbrtrd 4675 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ (1 / (√‘𝑚))) |
167 | 99, 107 | divsqrtsum2 24709 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ ((𝑥↑2) / 𝑚) ∈ ℝ+)
→ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ≤ (1 / (√‘((𝑥↑2) / 𝑚)))) |
168 | 98, 167 | mpdan 702 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ≤ (1 / (√‘((𝑥↑2) / 𝑚)))) |
169 | 95 | rprege0d 11879 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝑥↑2) ∈ ℝ ∧ 0
≤ (𝑥↑2))) |
170 | | sqrtdiv 14006 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥↑2) ∈ ℝ ∧ 0
≤ (𝑥↑2)) ∧
𝑚 ∈
ℝ+) → (√‘((𝑥↑2) / 𝑚)) = ((√‘(𝑥↑2)) / (√‘𝑚))) |
171 | 169, 96, 170 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑚)) = ((√‘(𝑥↑2)) / (√‘𝑚))) |
172 | 125 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
173 | | sqrtsq 14010 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(√‘(𝑥↑2))
= 𝑥) |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘(𝑥↑2)) = 𝑥) |
175 | 174 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘(𝑥↑2)) / (√‘𝑚)) = (𝑥 / (√‘𝑚))) |
176 | 171, 175 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑚)) = (𝑥 / (√‘𝑚))) |
177 | 176 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘((𝑥↑2) / 𝑚))) = (1 / (𝑥 / (√‘𝑚)))) |
178 | | rpcnne0 11850 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
179 | 178 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
180 | 135 | rpcnne0d 11881 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚)
∈ ℂ ∧ (√‘𝑚) ≠ 0)) |
181 | | recdiv 10731 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧
((√‘𝑚) ∈
ℂ ∧ (√‘𝑚) ≠ 0)) → (1 / (𝑥 / (√‘𝑚))) = ((√‘𝑚) / 𝑥)) |
182 | 179, 180,
181 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑥 /
(√‘𝑚))) =
((√‘𝑚) / 𝑥)) |
183 | 177, 182 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘((𝑥↑2) / 𝑚))) = ((√‘𝑚) / 𝑥)) |
184 | 168, 183 | breqtrd 4679 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ≤ ((√‘𝑚) / 𝑥)) |
185 | 133, 136,
137, 139, 140, 141, 166, 184 | lemul12ad 10966 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) · (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ ((1 / (√‘𝑚)) ·
((√‘𝑚) / 𝑥))) |
186 | 24, 117 | absmuld 14193 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) = ((abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) · (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)))) |
187 | | 1cnd 10056 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℂ) |
188 | | dmdcan 10735 |
. . . . . . . . . . . . 13
⊢
((((√‘𝑚)
∈ ℂ ∧ (√‘𝑚) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ 1 ∈ ℂ) →
(((√‘𝑚) / 𝑥) · (1 /
(√‘𝑚))) = (1 /
𝑥)) |
189 | 180, 179,
187, 188 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((√‘𝑚)
/ 𝑥) · (1 /
(√‘𝑚))) = (1 /
𝑥)) |
190 | 138 | rpcnd 11874 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚) /
𝑥) ∈
ℂ) |
191 | | reccl 10692 |
. . . . . . . . . . . . . 14
⊢
(((√‘𝑚)
∈ ℂ ∧ (√‘𝑚) ≠ 0) → (1 / (√‘𝑚)) ∈
ℂ) |
192 | 180, 191 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘𝑚)) ∈ ℂ) |
193 | 190, 192 | mulcomd 10061 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((√‘𝑚)
/ 𝑥) · (1 /
(√‘𝑚))) = ((1 /
(√‘𝑚)) ·
((√‘𝑚) / 𝑥))) |
194 | 189, 193 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑥) = ((1 /
(√‘𝑚)) ·
((√‘𝑚) / 𝑥))) |
195 | 185, 186,
194 | 3brtr4d 4685 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ (1 / 𝑥)) |
196 | 1, 121, 132, 195 | fsumle 14531 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ Σ𝑚 ∈ (1...(⌊‘𝑥))(1 / 𝑥)) |
197 | | flge0nn0 12621 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
198 | | hashfz1 13134 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℕ0 → (#‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
199 | 126, 197,
198 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(#‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
200 | 199 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((#‘(1...(⌊‘𝑥))) · (1 / 𝑥)) = ((⌊‘𝑥) · (1 / 𝑥))) |
201 | 92 | rpreccld 11882 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ+) |
202 | 201 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℂ) |
203 | | fsumconst 14522 |
. . . . . . . . . . 11
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧ (1 / 𝑥) ∈ ℂ) → Σ𝑚 ∈
(1...(⌊‘𝑥))(1 /
𝑥) =
((#‘(1...(⌊‘𝑥))) · (1 / 𝑥))) |
204 | 1, 202, 203 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(1 /
𝑥) =
((#‘(1...(⌊‘𝑥))) · (1 / 𝑥))) |
205 | 129 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ∈
ℂ) |
206 | 178 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
207 | 206 | simpld 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
208 | 206 | simprd 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
209 | 205, 207,
208 | divrecd 10804 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) / 𝑥) = ((⌊‘𝑥) · (1 / 𝑥))) |
210 | 200, 204,
209 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(1 /
𝑥) = ((⌊‘𝑥) / 𝑥)) |
211 | 196, 210 | breqtrd 4679 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ ((⌊‘𝑥) / 𝑥)) |
212 | | flle 12600 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
213 | 127, 212 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ≤
𝑥) |
214 | 127 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
215 | 214 | mulid1d 10057 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 · 1) = 𝑥) |
216 | 213, 215 | breqtrrd 4681 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ≤
(𝑥 ·
1)) |
217 | | rpregt0 11846 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
218 | 217 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 <
𝑥)) |
219 | | ledivmul 10899 |
. . . . . . . . . 10
⊢
(((⌊‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (((⌊‘𝑥) / 𝑥) ≤ 1 ↔ (⌊‘𝑥) ≤ (𝑥 · 1))) |
220 | 129, 123,
218, 219 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((⌊‘𝑥) / 𝑥) ≤ 1 ↔
(⌊‘𝑥) ≤
(𝑥 ·
1))) |
221 | 216, 220 | mpbird 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) / 𝑥) ≤ 1) |
222 | 122, 130,
123, 211, 221 | letrd 10194 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ 1) |
223 | 120, 122,
123, 124, 222 | letrd 10194 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ 1) |
224 | 223 | adantrr 753 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ 1) |
225 | 66, 119, 86, 86, 224 | elo1d 14267 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ 𝑂(1)) |
226 | 116, 225 | eqeltrrd 2702 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) ∈ 𝑂(1)) |
227 | 105, 106,
226 | o1dif 14360 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+
↦ (Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) ∈ 𝑂(1))) |
228 | 91, 227 | mpbird 247 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1)) |