| Step | Hyp | Ref
| Expression |
| 1 | | fzfid 14014 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
| 2 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝜑) |
| 3 | | elfznn 13593 |
. . . . 5
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℕ) |
| 4 | | rpvmasum2.g |
. . . . . . 7
⊢ 𝐺 = (DChr‘𝑁) |
| 5 | | rpvmasum.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
| 6 | | rpvmasum2.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝐺) |
| 7 | | rpvmasum.l |
. . . . . . 7
⊢ 𝐿 = (ℤRHom‘𝑍) |
| 8 | | rpvmasum2.w |
. . . . . . . . . . 11
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
| 9 | 8 | ssrab3 4082 |
. . . . . . . . . 10
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
| 10 | | dchrisum0.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
| 11 | 9, 10 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
| 12 | 11 | eldifad 3963 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
| 13 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑋 ∈ 𝐷) |
| 14 | | nnz 12634 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
| 15 | 14 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℤ) |
| 16 | 4, 5, 6, 7, 13, 15 | dchrzrhcl 27289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
| 17 | | nnrp 13046 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
| 18 | 17 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+) |
| 19 | 18 | rpsqrtcld 15450 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈
ℝ+) |
| 20 | 19 | rpcnd 13079 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ∈
ℂ) |
| 21 | 19 | rpne0d 13082 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (√‘𝑚) ≠ 0) |
| 22 | 16, 20, 21 | divcld 12043 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 23 | 2, 3, 22 | syl2an 596 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 24 | 1, 23 | fsumcl 15769 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 25 | | dchrisum0lem2.u |
. . . . 5
⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈) |
| 26 | | rlimcl 15539 |
. . . . 5
⊢ (𝐻 ⇝𝑟
𝑈 → 𝑈 ∈ ℂ) |
| 27 | 25, 26 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ ℂ) |
| 28 | 27 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑈 ∈
ℂ) |
| 29 | | 0xr 11308 |
. . . . . . . . 9
⊢ 0 ∈
ℝ* |
| 30 | | 0lt1 11785 |
. . . . . . . . 9
⊢ 0 <
1 |
| 31 | | df-ioo 13391 |
. . . . . . . . . 10
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
| 32 | | df-ico 13393 |
. . . . . . . . . 10
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
| 33 | | xrltletr 13199 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤)) |
| 34 | 31, 32, 33 | ixxss1 13405 |
. . . . . . . . 9
⊢ ((0
∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆
(0(,)+∞)) |
| 35 | 29, 30, 34 | mp2an 692 |
. . . . . . . 8
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
| 36 | | ioorp 13465 |
. . . . . . . 8
⊢
(0(,)+∞) = ℝ+ |
| 37 | 35, 36 | sseqtri 4032 |
. . . . . . 7
⊢
(1[,)+∞) ⊆ ℝ+ |
| 38 | | resmpt 6055 |
. . . . . . 7
⊢
((1[,)+∞) ⊆ ℝ+ → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))) |
| 39 | 37, 38 | ax-mp 5 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 40 | 37 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ+) |
| 41 | 3 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
ℕ) |
| 42 | | 2fveq3 6911 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑚 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑚))) |
| 43 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑚 → (√‘𝑎) = (√‘𝑚)) |
| 44 | 42, 43 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑚 → ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 45 | | dchrisum0lem1.f |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
| 46 | | ovex 7464 |
. . . . . . . . . . 11
⊢ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) ∈ V |
| 47 | 44, 45, 46 | fvmpt3i 7021 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 48 | 41, 47 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 49 | 40, 48 | sylanl2 681 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐹‘𝑚) = ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 50 | | 1re 11261 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
| 51 | | elicopnf 13485 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
| 52 | 50, 51 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
| 53 | | flge1nn 13861 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
| 54 | 52, 53 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1[,)+∞) →
(⌊‘𝑥) ∈
ℕ) |
| 55 | 54 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) →
(⌊‘𝑥) ∈
ℕ) |
| 56 | | nnuz 12921 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
| 57 | 55, 56 | eleqtrdi 2851 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) →
(⌊‘𝑥) ∈
(ℤ≥‘1)) |
| 58 | 40, 23 | sylanl2 681 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
| 59 | 49, 57, 58 | fsumser 15766 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) → Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
| 60 | 59 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1[,)+∞) ↦ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = (𝑥 ∈ (1[,)+∞) ↦ (seq1( + ,
𝐹)‘(⌊‘𝑥)))) |
| 61 | 39, 60 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦
(seq1( + , 𝐹)‘(⌊‘𝑥)))) |
| 62 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑚 = (⌊‘𝑥) → (seq1( + , 𝐹)‘𝑚) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
| 63 | | rpssre 13042 |
. . . . . . . . 9
⊢
ℝ+ ⊆ ℝ |
| 64 | 63 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ+
⊆ ℝ) |
| 65 | 37, 64 | sstrid 3995 |
. . . . . . 7
⊢ (𝜑 → (1[,)+∞) ⊆
ℝ) |
| 66 | | 1zzd 12648 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
| 67 | 44 | cbvmptv 5255 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 68 | 45, 67 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) |
| 69 | 22, 68 | fmptd 7134 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) |
| 70 | 69 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ ℂ) |
| 71 | 56, 66, 70 | serf 14071 |
. . . . . . . . 9
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
| 72 | 71 | feqmptd 6977 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) = (𝑚 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑚))) |
| 73 | | dchrisum0.s |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆) |
| 74 | 72, 73 | eqbrtrrd 5167 |
. . . . . . 7
⊢ (𝜑 → (𝑚 ∈ ℕ ↦ (seq1( + , 𝐹)‘𝑚)) ⇝ 𝑆) |
| 75 | 71 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq1( + , 𝐹)‘𝑚) ∈ ℂ) |
| 76 | 52 | simprbi 496 |
. . . . . . . 8
⊢ (𝑥 ∈ (1[,)+∞) → 1
≤ 𝑥) |
| 77 | 76 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1[,)+∞)) → 1 ≤ 𝑥) |
| 78 | 56, 62, 65, 66, 74, 75, 77 | climrlim2 15583 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1[,)+∞) ↦ (seq1( + ,
𝐹)‘(⌊‘𝑥))) ⇝𝑟 𝑆) |
| 79 | | rlimo1 15653 |
. . . . . 6
⊢ ((𝑥 ∈ (1[,)+∞) ↦
(seq1( + , 𝐹)‘(⌊‘𝑥))) ⇝𝑟 𝑆 → (𝑥 ∈ (1[,)+∞) ↦ (seq1( + ,
𝐹)‘(⌊‘𝑥))) ∈ 𝑂(1)) |
| 80 | 78, 79 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (1[,)+∞) ↦ (seq1( + ,
𝐹)‘(⌊‘𝑥))) ∈ 𝑂(1)) |
| 81 | 61, 80 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) ∈
𝑂(1)) |
| 82 | 24 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))):ℝ+⟶ℂ) |
| 83 | | 1red 11262 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
| 84 | 82, 64, 83 | o1resb 15602 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ+
↦ Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ↾ (1[,)+∞)) ∈
𝑂(1))) |
| 85 | 81, 84 | mpbird 257 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ 𝑂(1)) |
| 86 | | o1const 15656 |
. . . 4
⊢
((ℝ+ ⊆ ℝ ∧ 𝑈 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 𝑈) ∈
𝑂(1)) |
| 87 | 63, 27, 86 | sylancr 587 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 𝑈) ∈
𝑂(1)) |
| 88 | 24, 28, 85, 87 | o1mul2 15661 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) ∈ 𝑂(1)) |
| 89 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
| 90 | | 2z 12649 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
| 91 | | rpexpcl 14121 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑥↑2) ∈
ℝ+) |
| 92 | 89, 90, 91 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ+) |
| 93 | 3 | nnrpd 13075 |
. . . . . . . 8
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℝ+) |
| 94 | | rpdivcl 13060 |
. . . . . . . 8
⊢ (((𝑥↑2) ∈
ℝ+ ∧ 𝑚
∈ ℝ+) → ((𝑥↑2) / 𝑚) ∈
ℝ+) |
| 95 | 92, 93, 94 | syl2an 596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝑥↑2) / 𝑚) ∈
ℝ+) |
| 96 | | dchrisum0lem2.h |
. . . . . . . . 9
⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑦))(1 /
(√‘𝑑)) −
(2 · (√‘𝑦)))) |
| 97 | 96 | divsqrsumf 27024 |
. . . . . . . 8
⊢ 𝐻:ℝ+⟶ℝ |
| 98 | 97 | ffvelcdmi 7103 |
. . . . . . 7
⊢ (((𝑥↑2) / 𝑚) ∈ ℝ+ → (𝐻‘((𝑥↑2) / 𝑚)) ∈ ℝ) |
| 99 | 95, 98 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐻‘((𝑥↑2) / 𝑚)) ∈ ℝ) |
| 100 | 99 | recnd 11289 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐻‘((𝑥↑2) / 𝑚)) ∈ ℂ) |
| 101 | 23, 100 | mulcld 11281 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) ∈ ℂ) |
| 102 | 1, 101 | fsumcl 15769 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) ∈ ℂ) |
| 103 | 24, 28 | mulcld 11281 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈) ∈ ℂ) |
| 104 | 25 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝐻
⇝𝑟 𝑈) |
| 105 | 104, 26 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑈 ∈
ℂ) |
| 106 | 23, 105 | mulcld 11281 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈) ∈ ℂ) |
| 107 | 1, 101, 106 | fsumsub 15824 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
| 108 | 23, 100, 105 | subdid 11719 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) = ((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
| 109 | 108 | sumeq2dv 15738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) = Σ𝑚 ∈ (1...(⌊‘𝑥))((((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
| 110 | 1, 28, 23 | fsummulc1 15821 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈) = Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) |
| 111 | 110 | oveq2d 7447 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
| 112 | 107, 109,
111 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) = (Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) |
| 113 | 112 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)))) |
| 114 | 100, 105 | subcld 11620 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈) ∈ ℂ) |
| 115 | 23, 114 | mulcld 11281 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ∈ ℂ) |
| 116 | 1, 115 | fsumcl 15769 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ∈ ℂ) |
| 117 | 116 | abscld 15475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ ℝ) |
| 118 | 115 | abscld 15475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ ℝ) |
| 119 | 1, 118 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ ℝ) |
| 120 | | 1red 11262 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℝ) |
| 121 | 1, 115 | fsumabs 15837 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ Σ𝑚 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)))) |
| 122 | | rprege0 13050 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
| 123 | 122 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
| 124 | 123 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
| 125 | | reflcl 13836 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
| 126 | 124, 125 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ∈
ℝ) |
| 127 | 126, 89 | rerpdivcld 13108 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) / 𝑥) ∈
ℝ) |
| 128 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
| 129 | 128 | rprecred 13088 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑥) ∈
ℝ) |
| 130 | 23 | abscld 15475 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ ℝ) |
| 131 | 93 | rpsqrtcld 15450 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ (√‘𝑚)
∈ ℝ+) |
| 132 | 131 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑚)
∈ ℝ+) |
| 133 | 132 | rprecred 13088 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘𝑚)) ∈ ℝ) |
| 134 | 114 | abscld 15475 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ∈ ℝ) |
| 135 | 132, 128 | rpdivcld 13094 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚) /
𝑥) ∈
ℝ+) |
| 136 | 63, 135 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚) /
𝑥) ∈
ℝ) |
| 137 | 23 | absge0d 15483 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)))) |
| 138 | 114 | absge0d 15483 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) |
| 139 | 2, 3, 16 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
| 140 | 132 | rpcnd 13079 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑚)
∈ ℂ) |
| 141 | 132 | rpne0d 13082 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑚)
≠ 0) |
| 142 | 139, 140,
141 | absdivd 15494 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = ((abs‘(𝑋‘(𝐿‘𝑚))) / (abs‘(√‘𝑚)))) |
| 143 | 132 | rprege0d 13084 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚)
∈ ℝ ∧ 0 ≤ (√‘𝑚))) |
| 144 | | absid 15335 |
. . . . . . . . . . . . . . . 16
⊢
(((√‘𝑚)
∈ ℝ ∧ 0 ≤ (√‘𝑚)) → (abs‘(√‘𝑚)) = (√‘𝑚)) |
| 145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(√‘𝑚)) = (√‘𝑚)) |
| 146 | 145 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑚))) / (abs‘(√‘𝑚))) = ((abs‘(𝑋‘(𝐿‘𝑚))) / (√‘𝑚))) |
| 147 | 142, 146 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) = ((abs‘(𝑋‘(𝐿‘𝑚))) / (√‘𝑚))) |
| 148 | 139 | abscld 15475 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑚))) ∈ ℝ) |
| 149 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
| 150 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑍) =
(Base‘𝑍) |
| 151 | 12 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑋 ∈ 𝐷) |
| 152 | | rpvmasum.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 153 | 152 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 154 | 5, 150, 7 | znzrhfo 21566 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
| 155 | | fof 6820 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
| 156 | 153, 154,
155 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
| 157 | 156 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿:ℤ⟶(Base‘𝑍)) |
| 158 | | elfzelz 13564 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℤ) |
| 159 | | ffvelcdm 7101 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑚 ∈ ℤ) → (𝐿‘𝑚) ∈ (Base‘𝑍)) |
| 160 | 157, 158,
159 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑚) ∈ (Base‘𝑍)) |
| 161 | 4, 6, 5, 150, 151, 160 | dchrabs2 27306 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑚))) ≤ 1) |
| 162 | 148, 149,
132, 161 | lediv1dd 13135 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑚))) / (√‘𝑚)) ≤ (1 / (√‘𝑚))) |
| 163 | 147, 162 | eqbrtrd 5165 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ (1 / (√‘𝑚))) |
| 164 | 96, 104 | divsqrtsum2 27026 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ ((𝑥↑2) / 𝑚) ∈ ℝ+)
→ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ≤ (1 / (√‘((𝑥↑2) / 𝑚)))) |
| 165 | 95, 164 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ≤ (1 / (√‘((𝑥↑2) / 𝑚)))) |
| 166 | 92 | rprege0d 13084 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝑥↑2) ∈ ℝ ∧ 0
≤ (𝑥↑2))) |
| 167 | | sqrtdiv 15304 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥↑2) ∈ ℝ ∧ 0
≤ (𝑥↑2)) ∧
𝑚 ∈
ℝ+) → (√‘((𝑥↑2) / 𝑚)) = ((√‘(𝑥↑2)) / (√‘𝑚))) |
| 168 | 166, 93, 167 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑚)) = ((√‘(𝑥↑2)) / (√‘𝑚))) |
| 169 | 122 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
| 170 | | sqrtsq 15308 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(√‘(𝑥↑2))
= 𝑥) |
| 171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘(𝑥↑2)) = 𝑥) |
| 172 | 171 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘(𝑥↑2)) / (√‘𝑚)) = (𝑥 / (√‘𝑚))) |
| 173 | 168, 172 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (√‘((𝑥↑2) / 𝑚)) = (𝑥 / (√‘𝑚))) |
| 174 | 173 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘((𝑥↑2) / 𝑚))) = (1 / (𝑥 / (√‘𝑚)))) |
| 175 | | rpcnne0 13053 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
| 176 | 175 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
| 177 | 132 | rpcnne0d 13086 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚)
∈ ℂ ∧ (√‘𝑚) ≠ 0)) |
| 178 | | recdiv 11973 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧
((√‘𝑚) ∈
ℂ ∧ (√‘𝑚) ≠ 0)) → (1 / (𝑥 / (√‘𝑚))) = ((√‘𝑚) / 𝑥)) |
| 179 | 176, 177,
178 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (𝑥 /
(√‘𝑚))) =
((√‘𝑚) / 𝑥)) |
| 180 | 174, 179 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘((𝑥↑2) / 𝑚))) = ((√‘𝑚) / 𝑥)) |
| 181 | 165, 180 | breqtrd 5169 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)) ≤ ((√‘𝑚) / 𝑥)) |
| 182 | 130, 133,
134, 136, 137, 138, 163, 181 | lemul12ad 12210 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) · (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ ((1 / (√‘𝑚)) ·
((√‘𝑚) / 𝑥))) |
| 183 | 23, 114 | absmuld 15493 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) = ((abs‘((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) · (abs‘((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈)))) |
| 184 | | 1cnd 11256 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℂ) |
| 185 | | dmdcan 11977 |
. . . . . . . . . . . . 13
⊢
((((√‘𝑚)
∈ ℂ ∧ (√‘𝑚) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ 1 ∈ ℂ) →
(((√‘𝑚) / 𝑥) · (1 /
(√‘𝑚))) = (1 /
𝑥)) |
| 186 | 177, 176,
184, 185 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((√‘𝑚)
/ 𝑥) · (1 /
(√‘𝑚))) = (1 /
𝑥)) |
| 187 | 135 | rpcnd 13079 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑚) /
𝑥) ∈
ℂ) |
| 188 | | reccl 11929 |
. . . . . . . . . . . . . 14
⊢
(((√‘𝑚)
∈ ℂ ∧ (√‘𝑚) ≠ 0) → (1 / (√‘𝑚)) ∈
ℂ) |
| 189 | 177, 188 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘𝑚)) ∈ ℂ) |
| 190 | 187, 189 | mulcomd 11282 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((√‘𝑚)
/ 𝑥) · (1 /
(√‘𝑚))) = ((1 /
(√‘𝑚)) ·
((√‘𝑚) / 𝑥))) |
| 191 | 186, 190 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑥) = ((1 /
(√‘𝑚)) ·
((√‘𝑚) / 𝑥))) |
| 192 | 182, 183,
191 | 3brtr4d 5175 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ (1 / 𝑥)) |
| 193 | 1, 118, 129, 192 | fsumle 15835 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ Σ𝑚 ∈ (1...(⌊‘𝑥))(1 / 𝑥)) |
| 194 | | flge0nn0 13860 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
| 195 | | hashfz1 14385 |
. . . . . . . . . . . 12
⊢
((⌊‘𝑥)
∈ ℕ0 → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
| 196 | 123, 194,
195 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
| 197 | 196 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((♯‘(1...(⌊‘𝑥))) · (1 / 𝑥)) = ((⌊‘𝑥) · (1 / 𝑥))) |
| 198 | 89 | rpreccld 13087 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℝ+) |
| 199 | 198 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
𝑥) ∈
ℂ) |
| 200 | | fsumconst 15826 |
. . . . . . . . . . 11
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧ (1 / 𝑥) ∈ ℂ) → Σ𝑚 ∈
(1...(⌊‘𝑥))(1 /
𝑥) =
((♯‘(1...(⌊‘𝑥))) · (1 / 𝑥))) |
| 201 | 1, 199, 200 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(1 /
𝑥) =
((♯‘(1...(⌊‘𝑥))) · (1 / 𝑥))) |
| 202 | 126 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ∈
ℂ) |
| 203 | 175 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
| 204 | 203 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
| 205 | 203 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ≠ 0) |
| 206 | 202, 204,
205 | divrecd 12046 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) / 𝑥) = ((⌊‘𝑥) · (1 / 𝑥))) |
| 207 | 197, 201,
206 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(1 /
𝑥) = ((⌊‘𝑥) / 𝑥)) |
| 208 | 193, 207 | breqtrd 5169 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ ((⌊‘𝑥) / 𝑥)) |
| 209 | | flle 13839 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
| 210 | 124, 209 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ≤
𝑥) |
| 211 | 124 | recnd 11289 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
| 212 | 211 | mulridd 11278 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 · 1) = 𝑥) |
| 213 | 210, 212 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(⌊‘𝑥) ≤
(𝑥 ·
1)) |
| 214 | | rpregt0 13049 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
| 215 | 214 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 <
𝑥)) |
| 216 | | ledivmul 12144 |
. . . . . . . . . 10
⊢
(((⌊‘𝑥)
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (((⌊‘𝑥) / 𝑥) ≤ 1 ↔ (⌊‘𝑥) ≤ (𝑥 · 1))) |
| 217 | 126, 120,
215, 216 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((⌊‘𝑥) / 𝑥) ≤ 1 ↔
(⌊‘𝑥) ≤
(𝑥 ·
1))) |
| 218 | 213, 217 | mpbird 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) / 𝑥) ≤ 1) |
| 219 | 119, 127,
120, 208, 218 | letrd 11418 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑚 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ 1) |
| 220 | 117, 119,
120, 121, 219 | letrd 11418 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ 1) |
| 221 | 220 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ≤ 1) |
| 222 | 64, 116, 83, 83, 221 | elo1d 15572 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · ((𝐻‘((𝑥↑2) / 𝑚)) − 𝑈))) ∈ 𝑂(1)) |
| 223 | 113, 222 | eqeltrrd 2842 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚))) − (Σ𝑚 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈))) ∈ 𝑂(1)) |
| 224 | 102, 103,
223 | o1dif 15666 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+
↦ (Σ𝑚 ∈
(1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · 𝑈)) ∈ 𝑂(1))) |
| 225 | 88, 224 | mpbird 257 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1)) |