Proof of Theorem dchrisum0lem1
Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
2 | | fzfid 12634 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2))) ∈ Fin) |
3 | | fzfid 12634 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑))) ∈ Fin) |
4 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) |
5 | | elfzuz 12209 |
. . . . . . 7
⊢ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1))) |
6 | 4, 5 | anim12i 588 |
. . . . . 6
⊢ ((𝑑 ∈
(1...(⌊‘𝑥))
∧ 𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))) → (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) |
7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝑑 ∈
(1...(⌊‘𝑥))
∧ 𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))) → (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1))))) |
8 | | elfzuz 12209 |
. . . . . . 7
⊢ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) → 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1))) |
9 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚))) → 𝑑 ∈ ℕ) |
10 | 8, 9 | anim12ci 589 |
. . . . . 6
⊢ ((𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) |
11 | 10 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈
(1...(⌊‘((𝑥↑2) / 𝑚)))) → (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1))))) |
12 | | eluzelz 11573 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)) → 𝑚 ∈ ℤ) |
13 | 12 | ad2antll 761 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈ ℤ) |
14 | 13 | zred 11358 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈ ℝ) |
15 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
16 | | 2z 11286 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
17 | | rpexpcl 12741 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ+
∧ 2 ∈ ℤ) → (𝑥↑2) ∈
ℝ+) |
18 | 15, 16, 17 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ+) |
19 | 18 | rpred 11748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) ∈
ℝ) |
20 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) ∈ ℝ) |
21 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑑 ∈ ℕ) |
22 | 21 | nnrpd 11746 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑑 ∈ ℝ+) |
23 | 14, 20, 22 | lemuldivd 11797 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑚 · 𝑑) ≤ (𝑥↑2) ↔ 𝑚 ≤ ((𝑥↑2) / 𝑑))) |
24 | 21 | nnred 10912 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑑 ∈ ℝ) |
25 | 15 | rprege0d 11755 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) |
26 | | flge0nn0 12483 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
27 | | nn0p1nn 11209 |
. . . . . . . . . . . . . 14
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((⌊‘𝑥) + 1)
∈ ℕ) |
29 | 28 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((⌊‘𝑥) + 1) ∈
ℕ) |
30 | | simprr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1))) |
31 | | eluznn 11634 |
. . . . . . . . . . . 12
⊢
((((⌊‘𝑥)
+ 1) ∈ ℕ ∧ 𝑚
∈ (ℤ≥‘((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ) |
32 | 29, 30, 31 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈ ℕ) |
33 | 32 | nnrpd 11746 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑚 ∈ ℝ+) |
34 | 24, 20, 33 | lemuldiv2d 11798 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑚 · 𝑑) ≤ (𝑥↑2) ↔ 𝑑 ≤ ((𝑥↑2) / 𝑚))) |
35 | 23, 34 | bitr3d 269 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) ↔ 𝑑 ≤ ((𝑥↑2) / 𝑚))) |
36 | | rpcn 11717 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
38 | 37 | sqvald 12867 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥↑2) = (𝑥 · 𝑥)) |
39 | 38 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) = (𝑥 · 𝑥)) |
40 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑥 ∈ ℝ+) |
41 | 40 | rpred 11748 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑥 ∈ ℝ) |
42 | | reflcl 12459 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
43 | | peano2re 10088 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘𝑥)
∈ ℝ → ((⌊‘𝑥) + 1) ∈ ℝ) |
44 | 41, 42, 43 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((⌊‘𝑥) + 1) ∈
ℝ) |
45 | | fllep1 12464 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
46 | 41, 45 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑥 ≤ ((⌊‘𝑥) + 1)) |
47 | | eluzle 11576 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)) → ((⌊‘𝑥) + 1) ≤ 𝑚) |
48 | 47 | ad2antll 761 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((⌊‘𝑥) + 1) ≤ 𝑚) |
49 | 41, 44, 14, 46, 48 | letrd 10073 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑥 ≤ 𝑚) |
50 | 41, 14, 40 | lemul1d 11791 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑥 ≤ 𝑚 ↔ (𝑥 · 𝑥) ≤ (𝑚 · 𝑥))) |
51 | 49, 50 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑥 · 𝑥) ≤ (𝑚 · 𝑥)) |
52 | 39, 51 | eqbrtrd 4605 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) ≤ (𝑚 · 𝑥)) |
53 | 20, 41, 33 | ledivmuld 11801 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (((𝑥↑2) / 𝑚) ≤ 𝑥 ↔ (𝑥↑2) ≤ (𝑚 · 𝑥))) |
54 | 52, 53 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑚) ≤ 𝑥) |
55 | | nnre 10904 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℕ → 𝑑 ∈
ℝ) |
56 | 55 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 𝑑 ∈ ℝ) |
57 | 20, 32 | nndivred 10946 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑚) ∈ ℝ) |
58 | | letr 10010 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∈ ℝ ∧ ((𝑥↑2) / 𝑚) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑑 ≤ ((𝑥↑2) / 𝑚) ∧ ((𝑥↑2) / 𝑚) ≤ 𝑥) → 𝑑 ≤ 𝑥)) |
59 | 56, 57, 41, 58 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑑 ≤ ((𝑥↑2) / 𝑚) ∧ ((𝑥↑2) / 𝑚) ≤ 𝑥) → 𝑑 ≤ 𝑥)) |
60 | 54, 59 | mpan2d 706 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑑 ≤ ((𝑥↑2) / 𝑚) → 𝑑 ≤ 𝑥)) |
61 | 35, 60 | sylbid 229 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) → 𝑑 ≤ 𝑥)) |
62 | 61 | pm4.71rd 665 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) ↔ (𝑑 ≤ 𝑥 ∧ 𝑚 ≤ ((𝑥↑2) / 𝑑)))) |
63 | | nnge1 10923 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ ℕ → 1 ≤
𝑑) |
64 | 63 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → 1 ≤ 𝑑) |
65 | | 1re 9918 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
66 | | 0lt1 10429 |
. . . . . . . . . . . . . . . 16
⊢ 0 <
1 |
67 | 65, 66 | pm3.2i 470 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℝ ∧ 0 < 1) |
68 | 67 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (1 ∈ ℝ ∧ 0
< 1)) |
69 | 22 | rpregt0d 11754 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑑 ∈ ℝ ∧ 0 < 𝑑)) |
70 | 18 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) ∈
ℝ+) |
71 | 70 | rpregt0d 11754 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) ∈ ℝ ∧ 0 < (𝑥↑2))) |
72 | | lediv2 10792 |
. . . . . . . . . . . . . 14
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑑 ∈ ℝ ∧ 0 < 𝑑) ∧ ((𝑥↑2) ∈ ℝ ∧ 0 < (𝑥↑2))) → (1 ≤ 𝑑 ↔ ((𝑥↑2) / 𝑑) ≤ ((𝑥↑2) / 1))) |
73 | 68, 69, 71, 72 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (1 ≤ 𝑑 ↔ ((𝑥↑2) / 𝑑) ≤ ((𝑥↑2) / 1))) |
74 | 64, 73 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑑) ≤ ((𝑥↑2) / 1)) |
75 | 20 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑥↑2) ∈ ℂ) |
76 | 75 | div1d 10672 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 1) = (𝑥↑2)) |
77 | 74, 76 | breqtrd 4609 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑑) ≤ (𝑥↑2)) |
78 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1))) → 𝑑 ∈ ℕ) |
79 | | nndivre 10933 |
. . . . . . . . . . . . 13
⊢ (((𝑥↑2) ∈ ℝ ∧
𝑑 ∈ ℕ) →
((𝑥↑2) / 𝑑) ∈
ℝ) |
80 | 19, 78, 79 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑥↑2) / 𝑑) ∈ ℝ) |
81 | | letr 10010 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℝ ∧ ((𝑥↑2) / 𝑑) ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → ((𝑚 ≤ ((𝑥↑2) / 𝑑) ∧ ((𝑥↑2) / 𝑑) ≤ (𝑥↑2)) → 𝑚 ≤ (𝑥↑2))) |
82 | 14, 80, 20, 81 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑚 ≤ ((𝑥↑2) / 𝑑) ∧ ((𝑥↑2) / 𝑑) ≤ (𝑥↑2)) → 𝑚 ≤ (𝑥↑2))) |
83 | 77, 82 | mpan2d 706 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) → 𝑚 ≤ (𝑥↑2))) |
84 | 35, 83 | sylbird 249 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑑 ≤ ((𝑥↑2) / 𝑚) → 𝑚 ≤ (𝑥↑2))) |
85 | 84 | pm4.71rd 665 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑑 ≤ ((𝑥↑2) / 𝑚) ↔ (𝑚 ≤ (𝑥↑2) ∧ 𝑑 ≤ ((𝑥↑2) / 𝑚)))) |
86 | 35, 62, 85 | 3bitr3d 297 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑑 ≤ 𝑥 ∧ 𝑚 ≤ ((𝑥↑2) / 𝑑)) ↔ (𝑚 ≤ (𝑥↑2) ∧ 𝑑 ≤ ((𝑥↑2) / 𝑚)))) |
87 | | fznnfl 12523 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → (𝑑 ∈
(1...(⌊‘𝑥))
↔ (𝑑 ∈ ℕ
∧ 𝑑 ≤ 𝑥))) |
88 | 87 | baibd 946 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑑 ∈
(1...(⌊‘𝑥))
↔ 𝑑 ≤ 𝑥)) |
89 | 41, 21, 88 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑑 ∈ (1...(⌊‘𝑥)) ↔ 𝑑 ≤ 𝑥)) |
90 | 80 | flcld 12461 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (⌊‘((𝑥↑2) / 𝑑)) ∈ ℤ) |
91 | | elfz5 12205 |
. . . . . . . . . 10
⊢ ((𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈ ℤ) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) ↔ 𝑚 ≤ (⌊‘((𝑥↑2) / 𝑑)))) |
92 | 30, 90, 91 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) ↔ 𝑚 ≤ (⌊‘((𝑥↑2) / 𝑑)))) |
93 | | flge 12468 |
. . . . . . . . . 10
⊢ ((((𝑥↑2) / 𝑑) ∈ ℝ ∧ 𝑚 ∈ ℤ) → (𝑚 ≤ ((𝑥↑2) / 𝑑) ↔ 𝑚 ≤ (⌊‘((𝑥↑2) / 𝑑)))) |
94 | 80, 13, 93 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ ((𝑥↑2) / 𝑑) ↔ 𝑚 ≤ (⌊‘((𝑥↑2) / 𝑑)))) |
95 | 92, 94 | bitr4d 270 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))) ↔ 𝑚 ≤ ((𝑥↑2) / 𝑑))) |
96 | 89, 95 | anbi12d 743 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) ↔ (𝑑 ≤ 𝑥 ∧ 𝑚 ≤ ((𝑥↑2) / 𝑑)))) |
97 | 20 | flcld 12461 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (⌊‘(𝑥↑2)) ∈
ℤ) |
98 | | elfz5 12205 |
. . . . . . . . . 10
⊢ ((𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)) ∧ (⌊‘(𝑥↑2)) ∈ ℤ) →
(𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2))) ↔ 𝑚 ≤ (⌊‘(𝑥↑2)))) |
99 | 30, 97, 98 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ↔ 𝑚 ≤ (⌊‘(𝑥↑2)))) |
100 | | flge 12468 |
. . . . . . . . . 10
⊢ (((𝑥↑2) ∈ ℝ ∧
𝑚 ∈ ℤ) →
(𝑚 ≤ (𝑥↑2) ↔ 𝑚 ≤ (⌊‘(𝑥↑2)))) |
101 | 20, 13, 100 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ≤ (𝑥↑2) ↔ 𝑚 ≤ (⌊‘(𝑥↑2)))) |
102 | 99, 101 | bitr4d 270 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ↔ 𝑚 ≤ (𝑥↑2))) |
103 | | fznnfl 12523 |
. . . . . . . . . 10
⊢ (((𝑥↑2) / 𝑚) ∈ ℝ → (𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))) ↔ (𝑑 ∈ ℕ ∧ 𝑑 ≤ ((𝑥↑2) / 𝑚)))) |
104 | 103 | baibd 946 |
. . . . . . . . 9
⊢ ((((𝑥↑2) / 𝑚) ∈ ℝ ∧ 𝑑 ∈ ℕ) → (𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))) ↔ 𝑑 ≤ ((𝑥↑2) / 𝑚))) |
105 | 57, 21, 104 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → (𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))) ↔ 𝑑 ≤ ((𝑥↑2) / 𝑚))) |
106 | 102, 105 | anbi12d 743 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))) ↔ (𝑚 ≤ (𝑥↑2) ∧ 𝑑 ≤ ((𝑥↑2) / 𝑚)))) |
107 | 86, 96, 106 | 3bitr4d 299 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1)))) → ((𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) ↔ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))))) |
108 | 107 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝑑 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘((⌊‘𝑥) + 1))) → ((𝑑 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) ↔ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚))))))) |
109 | 7, 11, 108 | pm5.21ndd 368 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝑑 ∈
(1...(⌊‘𝑥))
∧ 𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))) ↔ (𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2))) ∧ 𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))))) |
110 | | ssun2 3739 |
. . . . . . . 8
⊢
(((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑))) ⊆ ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))) |
111 | 28 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘𝑥) +
1) ∈ ℕ) |
112 | | nnuz 11599 |
. . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) |
113 | 111, 112 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((⌊‘𝑥) +
1) ∈ (ℤ≥‘1)) |
114 | | dchrisum0lem1a 24975 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ≤ ((𝑥↑2) / 𝑑) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥)))) |
115 | 114 | simprd 478 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥))) |
116 | | fzsplit2 12237 |
. . . . . . . . 9
⊢
((((⌊‘𝑥)
+ 1) ∈ (ℤ≥‘1) ∧ (⌊‘((𝑥↑2) / 𝑑)) ∈
(ℤ≥‘(⌊‘𝑥))) → (1...(⌊‘((𝑥↑2) / 𝑑))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))))) |
117 | 113, 115,
116 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘((𝑥↑2) / 𝑑))) = ((1...(⌊‘𝑥)) ∪ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑))))) |
118 | 110, 117 | syl5sseqr 3617 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑))) ⊆ (1...(⌊‘((𝑥↑2) / 𝑑)))) |
119 | 118 | sselda 3568 |
. . . . . 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 3650 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
126 | 124, 125 | eqsstri 3598 |
. . . . . . . . . . . 12
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
127 | | dchrisum0.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
128 | 126, 127 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
129 | 128 | eldifad 3552 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
130 | 129 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑋 ∈ 𝐷) |
131 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈ ℤ) |
132 | 131 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℤ) |
133 | 120, 121,
122, 123, 130, 132 | dchrzrhcl 24770 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (𝑋‘(𝐿‘𝑚)) ∈ ℂ) |
134 | | elfznn 12241 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑))) → 𝑚 ∈ ℕ) |
135 | 134 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℕ) |
136 | 135 | nnrpd 11746 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → 𝑚 ∈ ℝ+) |
137 | 136 | rpsqrtcld 13998 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ∈
ℝ+) |
138 | 137 | rpcnd 11750 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ∈ ℂ) |
139 | 137 | rpne0d 11753 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑚) ≠ 0) |
140 | 133, 138,
139 | divcld 10680 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
141 | 4 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) |
142 | 141 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ+) |
143 | 142 | rpsqrtcld 13998 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑑)
∈ ℝ+) |
144 | 143 | rpcnne0d 11757 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑑)
∈ ℂ ∧ (√‘𝑑) ≠ 0)) |
145 | 144 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → ((√‘𝑑) ∈ ℂ ∧
(√‘𝑑) ≠
0)) |
146 | 145 | simpld 474 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑑) ∈ ℂ) |
147 | 145 | simprd 478 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (√‘𝑑) ≠ 0) |
148 | 140, 146,
147 | divcld 10680 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘((𝑥↑2) / 𝑑)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
149 | 119, 148 | syldan 486 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
150 | 149 | anasss 677 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑑 ∈
(1...(⌊‘𝑥))
∧ 𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑))))) → (((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
151 | 1, 2, 3, 109, 150 | fsumcom2 14347 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
152 | 151 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) = (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
153 | 65 | a1i 11 |
. . 3
⊢ (𝜑 → 1 ∈
ℝ) |
154 | | 2cn 10968 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
155 | 15 | rpsqrtcld 13998 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℝ+) |
156 | 155 | rpcnd 11750 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ∈
ℂ) |
157 | | mulcl 9899 |
. . . . . . . 8
⊢ ((2
∈ ℂ ∧ (√‘𝑥) ∈ ℂ) → (2 ·
(√‘𝑥)) ∈
ℂ) |
158 | 154, 156,
157 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· (√‘𝑥))
∈ ℂ) |
159 | 143 | rprecred 11759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘𝑑)) ∈ ℝ) |
160 | 1, 159 | fsumrecl 14312 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ∈
ℝ) |
161 | 160 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ∈
ℂ) |
162 | 161, 158 | subcld 10271 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥))) ∈ ℂ) |
163 | | 2re 10967 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
164 | | dchrisum0.c |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
165 | | elrege0 12149 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 ∈ ℝ ∧ 0
≤ 𝐶)) |
166 | 164, 165 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) |
167 | 166 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
168 | | remulcl 9900 |
. . . . . . . . . . 11
⊢ ((2
∈ ℝ ∧ 𝐶
∈ ℝ) → (2 · 𝐶) ∈ ℝ) |
169 | 163, 167,
168 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝐶) ∈
ℝ) |
170 | 169 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· 𝐶) ∈
ℝ) |
171 | 170, 155 | rerpdivcld 11779 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· 𝐶) /
(√‘𝑥)) ∈
ℝ) |
172 | 171 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· 𝐶) /
(√‘𝑥)) ∈
ℂ) |
173 | 158, 162,
172 | adddird 9944 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((2
· (√‘𝑥))
+ (Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥)))) · ((2 · 𝐶) / (√‘𝑥))) = (((2 · (√‘𝑥)) · ((2 · 𝐶) / (√‘𝑥))) + ((Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥))))) |
174 | 158, 161 | pncan3d 10274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· (√‘𝑥))
+ (Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥)))) = Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑))) |
175 | 174 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((2
· (√‘𝑥))
+ (Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥)))) · ((2 · 𝐶) / (√‘𝑥))) = (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))) |
176 | | 2cnd 10970 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈
ℂ) |
177 | 176, 156,
172 | mulassd 9942 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· (√‘𝑥))
· ((2 · 𝐶) /
(√‘𝑥))) = (2
· ((√‘𝑥)
· ((2 · 𝐶) /
(√‘𝑥))))) |
178 | 170 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· 𝐶) ∈
ℂ) |
179 | 155 | rpne0d 11753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(√‘𝑥) ≠
0) |
180 | 178, 156,
179 | divcan2d 10682 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((√‘𝑥) ·
((2 · 𝐶) /
(√‘𝑥))) = (2
· 𝐶)) |
181 | 180 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· ((√‘𝑥)
· ((2 · 𝐶) /
(√‘𝑥)))) = (2
· (2 · 𝐶))) |
182 | 177, 181 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· (√‘𝑥))
· ((2 · 𝐶) /
(√‘𝑥))) = (2
· (2 · 𝐶))) |
183 | 182 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((2
· (√‘𝑥))
· ((2 · 𝐶) /
(√‘𝑥))) +
((Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥)))) = ((2 · (2 · 𝐶)) + ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 ·
(√‘𝑥)))
· ((2 · 𝐶) /
(√‘𝑥))))) |
184 | 173, 175,
183 | 3eqtr3d 2652 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥))) = ((2
· (2 · 𝐶)) +
((Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥))))) |
185 | 184 | mpteq2dva 4672 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥)))) =
(𝑥 ∈
ℝ+ ↦ ((2 · (2 · 𝐶)) + ((Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 ·
(√‘𝑥)))
· ((2 · 𝐶) /
(√‘𝑥)))))) |
186 | | remulcl 9900 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ (2 · 𝐶) ∈ ℝ) → (2 · (2
· 𝐶)) ∈
ℝ) |
187 | 163, 169,
186 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → (2 · (2 ·
𝐶)) ∈
ℝ) |
188 | 187 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (2 · (2 ·
𝐶)) ∈
ℂ) |
189 | 188 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· (2 · 𝐶))
∈ ℂ) |
190 | 162, 172 | mulcld 9939 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥))) ∈ ℂ) |
191 | | rpssre 11719 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
192 | | o1const 14198 |
. . . . . 6
⊢
((ℝ+ ⊆ ℝ ∧ (2 · (2 ·
𝐶)) ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ (2 · (2 · 𝐶))) ∈ 𝑂(1)) |
193 | 191, 188,
192 | sylancr 694 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2
· (2 · 𝐶)))
∈ 𝑂(1)) |
194 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥)))) |
195 | 194 | divsqrsum 24508 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥)))) ∈ dom
⇝𝑟 |
196 | | rlimdmo1 14196 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
↦ (Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥)))) ∈ dom ⇝𝑟
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) − (2 ·
(√‘𝑥)))) ∈
𝑂(1)) |
197 | 195, 196 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥)))) ∈ 𝑂(1)) |
198 | 178, 156,
179 | divrecd 10683 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· 𝐶) /
(√‘𝑥)) = ((2
· 𝐶) · (1 /
(√‘𝑥)))) |
199 | 198 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2
· 𝐶) /
(√‘𝑥))) =
(𝑥 ∈
ℝ+ ↦ ((2 · 𝐶) · (1 / (√‘𝑥))))) |
200 | 155 | rprecred 11759 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1 /
(√‘𝑥)) ∈
ℝ) |
201 | 169 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝐶) ∈
ℂ) |
202 | | rlimconst 14123 |
. . . . . . . . . 10
⊢
((ℝ+ ⊆ ℝ ∧ (2 · 𝐶) ∈ ℂ) → (𝑥 ∈ ℝ+
↦ (2 · 𝐶))
⇝𝑟 (2 · 𝐶)) |
203 | 191, 201,
202 | sylancr 694 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2
· 𝐶))
⇝𝑟 (2 · 𝐶)) |
204 | | sqrtlim 24499 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
↦ (1 / (√‘𝑥))) ⇝𝑟
0 |
205 | 204 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (1 /
(√‘𝑥)))
⇝𝑟 0) |
206 | 170, 200,
203, 205 | rlimmul 14223 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2
· 𝐶) · (1 /
(√‘𝑥))))
⇝𝑟 ((2 · 𝐶) · 0)) |
207 | 199, 206 | eqbrtrd 4605 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2
· 𝐶) /
(√‘𝑥)))
⇝𝑟 ((2 · 𝐶) · 0)) |
208 | | rlimo1 14195 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ+
↦ ((2 · 𝐶) /
(√‘𝑥)))
⇝𝑟 ((2 · 𝐶) · 0) → (𝑥 ∈ ℝ+ ↦ ((2
· 𝐶) /
(√‘𝑥))) ∈
𝑂(1)) |
209 | 207, 208 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2
· 𝐶) /
(√‘𝑥))) ∈
𝑂(1)) |
210 | 162, 172,
197, 209 | o1mul2 14203 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥)))) ∈ 𝑂(1)) |
211 | 189, 190,
193, 210 | o1add2 14202 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2
· (2 · 𝐶)) +
((Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) −
(2 · (√‘𝑥))) · ((2 · 𝐶) / (√‘𝑥))))) ∈ 𝑂(1)) |
212 | 185, 211 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥)))) ∈
𝑂(1)) |
213 | 160, 171 | remulcld 9949 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥))) ∈
ℝ) |
214 | 3, 149 | fsumcl 14311 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
215 | 1, 214 | fsumcl 14311 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) ∈ ℂ) |
216 | 215 | abscld 14023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ ℝ) |
217 | 213 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥))) ∈
ℂ) |
218 | 217 | abscld 14023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥)))) ∈
ℝ) |
219 | 214 | abscld 14023 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ ℝ) |
220 | 1, 219 | fsumrecl 14312 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ ℝ) |
221 | 1, 214 | fsumabs 14374 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
222 | 171 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝐶) /
(√‘𝑥)) ∈
ℝ) |
223 | 159, 222 | remulcld 9949 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥))) ∈ ℝ) |
224 | 119, 140 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))) → ((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
225 | 3, 224 | fsumcl 14311 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) ∈ ℂ) |
226 | 225 | abscld 14023 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ∈ ℝ) |
227 | | rpvmasum.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
228 | | rpvmasum2.1 |
. . . . . . . . . . 11
⊢ 1 =
(0g‘𝐺) |
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 25004 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ ((2 · 𝐶) / (√‘𝑥))) |
233 | 226, 222,
143, 232 | lediv1dd 11806 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (√‘𝑑)) ≤ (((2 · 𝐶) / (√‘𝑥)) / (√‘𝑑))) |
234 | 143 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑑)
∈ ℂ) |
235 | 143 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (√‘𝑑)
≠ 0) |
236 | 225, 234,
235 | absdivd 14042 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) = ((abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (abs‘(√‘𝑑)))) |
237 | 3, 234, 224, 235 | fsumdivc 14360 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)) = Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) |
238 | 237 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) = (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
239 | 143 | rprege0d 11755 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((√‘𝑑)
∈ ℝ ∧ 0 ≤ (√‘𝑑))) |
240 | | absid 13884 |
. . . . . . . . . . . 12
⊢
(((√‘𝑑)
∈ ℝ ∧ 0 ≤ (√‘𝑑)) → (abs‘(√‘𝑑)) = (√‘𝑑)) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(√‘𝑑)) = (√‘𝑑)) |
242 | 241 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (abs‘(√‘𝑑))) = ((abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (√‘𝑑))) |
243 | 236, 238,
242 | 3eqtr3rd 2653 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) / (√‘𝑑)) = (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑)))) |
244 | 172 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((2 · 𝐶) /
(√‘𝑥)) ∈
ℂ) |
245 | 244, 234,
235 | divrec2d 10684 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((2 · 𝐶) /
(√‘𝑥)) /
(√‘𝑑)) = ((1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥)))) |
246 | 233, 243,
245 | 3brtr3d 4614 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘Σ𝑚
∈ (((⌊‘𝑥)
+ 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ ((1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))) |
247 | 1, 219, 223, 246 | fsumle 14372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))) |
248 | 159 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 / (√‘𝑑)) ∈ ℂ) |
249 | 1, 172, 248 | fsummulc1 14359 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥))) =
Σ𝑑 ∈
(1...(⌊‘𝑥))((1
/ (√‘𝑑))
· ((2 · 𝐶) /
(√‘𝑥)))) |
250 | 247, 249 | breqtrrd 4611 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))) |
251 | 216, 220,
213, 221, 250 | letrd 10073 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ (Σ𝑑 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑑)) · ((2 · 𝐶) / (√‘𝑥)))) |
252 | 213 | leabsd 14001 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥))) ≤
(abs‘(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥))))) |
253 | 216, 213,
218, 251, 252 | letrd 10073 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ (abs‘(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥))))) |
254 | 253 | adantrr 749 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ≤ (abs‘(Σ𝑑 ∈
(1...(⌊‘𝑥))(1 /
(√‘𝑑)) ·
((2 · 𝐶) /
(√‘𝑥))))) |
255 | 153, 212,
213, 215, 254 | o1le 14231 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |
256 | 152, 255 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑚 ∈
(((⌊‘𝑥) +
1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1)) |