Step | Hyp | Ref
| Expression |
1 | | rpvmasum.z |
. . 3
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
2 | | rpvmasum.l |
. . 3
⊢ 𝐿 = (ℤRHom‘𝑍) |
3 | | rpvmasum.a |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | | rpvmasum.g |
. . 3
⊢ 𝐺 = (DChr‘𝑁) |
5 | | rpvmasum.d |
. . 3
⊢ 𝐷 = (Base‘𝐺) |
6 | | rpvmasum.1 |
. . 3
⊢ 1 =
(0g‘𝐺) |
7 | | dchrisum.b |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
8 | | dchrisum.n1 |
. . 3
⊢ (𝜑 → 𝑋 ≠ 1 ) |
9 | | oveq2 6557 |
. . 3
⊢ (𝑛 = 𝑥 → (1 / 𝑛) = (1 / 𝑥)) |
10 | | 1nn 10908 |
. . . 4
⊢ 1 ∈
ℕ |
11 | 10 | a1i 11 |
. . 3
⊢ (𝜑 → 1 ∈
ℕ) |
12 | | rpreccl 11733 |
. . . . 5
⊢ (𝑛 ∈ ℝ+
→ (1 / 𝑛) ∈
ℝ+) |
13 | 12 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → (1 /
𝑛) ∈
ℝ+) |
14 | 13 | rpred 11748 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → (1 /
𝑛) ∈
ℝ) |
15 | | simp3r 1083 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ≤ 𝑥) |
16 | | rpregt0 11722 |
. . . . . 6
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℝ
∧ 0 < 𝑛)) |
17 | | rpregt0 11722 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
18 | | lerec 10785 |
. . . . . 6
⊢ (((𝑛 ∈ ℝ ∧ 0 <
𝑛) ∧ (𝑥 ∈ ℝ ∧ 0 <
𝑥)) → (𝑛 ≤ 𝑥 ↔ (1 / 𝑥) ≤ (1 / 𝑛))) |
19 | 16, 17, 18 | syl2an 493 |
. . . . 5
⊢ ((𝑛 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (𝑛 ≤ 𝑥 ↔ (1 / 𝑥) ≤ (1 / 𝑛))) |
20 | 19 | 3ad2ant2 1076 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑛 ≤ 𝑥 ↔ (1 / 𝑥) ≤ (1 / 𝑛))) |
21 | 15, 20 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 / 𝑥) ≤ (1 / 𝑛)) |
22 | | ax-1cn 9873 |
. . . 4
⊢ 1 ∈
ℂ |
23 | | divrcnv 14423 |
. . . 4
⊢ (1 ∈
ℂ → (𝑛 ∈
ℝ+ ↦ (1 / 𝑛)) ⇝𝑟
0) |
24 | 22, 23 | mp1i 13 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ (1 /
𝑛))
⇝𝑟 0) |
25 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = 𝑛 → (𝐿‘𝑎) = (𝐿‘𝑛)) |
26 | 25 | fveq2d 6107 |
. . . . 5
⊢ (𝑎 = 𝑛 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑛))) |
27 | | oveq2 6557 |
. . . . 5
⊢ (𝑎 = 𝑛 → (1 / 𝑎) = (1 / 𝑛)) |
28 | 26, 27 | oveq12d 6567 |
. . . 4
⊢ (𝑎 = 𝑛 → ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎)) = ((𝑋‘(𝐿‘𝑛)) · (1 / 𝑛))) |
29 | 28 | cbvmptv 4678 |
. . 3
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))) = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · (1 / 𝑛))) |
30 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 11,
14, 21, 24, 29 | dchrisum 24981 |
. 2
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎)))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / 𝑥)))) |
31 | 7 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ 𝐷) |
32 | | nnz 11276 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
33 | 32 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) |
34 | 4, 1, 5, 2, 31, 33 | dchrzrhcl 24770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
35 | | nncn 10905 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
36 | 35 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
37 | | nnne0 10930 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0) |
38 | 37 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) |
39 | 34, 36, 38 | divrecd 10683 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑋‘(𝐿‘𝑛)) / 𝑛) = ((𝑋‘(𝐿‘𝑛)) · (1 / 𝑛))) |
40 | 39 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) / 𝑛)) = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · (1 / 𝑛)))) |
41 | | dchrisumn0.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) |
42 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑛 → 𝑎 = 𝑛) |
43 | 26, 42 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑛 → ((𝑋‘(𝐿‘𝑎)) / 𝑎) = ((𝑋‘(𝐿‘𝑛)) / 𝑛)) |
44 | 43 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) / 𝑛)) |
45 | 41, 44 | eqtri 2632 |
. . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) / 𝑛)) |
46 | 40, 45, 29 | 3eqtr4g 2669 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎)))) |
47 | 46 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎)))) |
48 | 47 | seqeq3d 12671 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → seq1( + ,
𝐹) = seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))) |
49 | 48 | breq1d 4593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → (seq1( + ,
𝐹) ⇝ 𝑡 ↔ seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎)))) ⇝ 𝑡)) |
50 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (⌊‘𝑦) = (⌊‘𝑥)) |
51 | 50 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
52 | 51 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡) = ((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) |
53 | 52 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡))) |
54 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑐 / 𝑦) = (𝑐 / 𝑥)) |
55 | 53, 54 | breq12d 4596 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / 𝑥))) |
56 | 55 | cbvralv 3147 |
. . . . . 6
⊢
(∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦) ↔ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / 𝑥)) |
57 | 46 | seqeq3d 12671 |
. . . . . . . . . . . 12
⊢ (𝜑 → seq1( + , 𝐹) = seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))) |
58 | 57 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝜑 → (seq1( + , 𝐹)‘(⌊‘𝑥)) = (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥))) |
59 | 58 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → ((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡) = ((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡)) |
60 | 59 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘((seq1( + ,
𝐹)‘(⌊‘𝑥)) − 𝑡)) = (abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡))) |
61 | 60 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) = (abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡))) |
62 | | elrege0 12149 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ (0[,)+∞) ↔
(𝑐 ∈ ℝ ∧ 0
≤ 𝑐)) |
63 | 62 | simplbi 475 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (0[,)+∞) →
𝑐 ∈
ℝ) |
64 | 63 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝑐 ∈ (0[,)+∞) →
𝑐 ∈
ℂ) |
65 | 64 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑐 ∈
ℂ) |
66 | | 1re 9918 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
67 | | elicopnf 12140 |
. . . . . . . . . . . . 13
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
69 | 68 | simplbi 475 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ) |
70 | 69 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑥 ∈
ℝ) |
71 | 70 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑥 ∈
ℂ) |
72 | | 0red 9920 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 0
∈ ℝ) |
73 | | 1red 9934 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 1
∈ ℝ) |
74 | | 0lt1 10429 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
75 | 74 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 0
< 1) |
76 | 68 | simprbi 479 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1[,)+∞) → 1
≤ 𝑥) |
77 | 76 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 1
≤ 𝑥) |
78 | 72, 73, 70, 75, 77 | ltletrd 10076 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 0
< 𝑥) |
79 | 78 | gt0ne0d 10471 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑥 ≠ 0) |
80 | 65, 71, 79 | divrecd 10683 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(𝑐 / 𝑥) = (𝑐 · (1 / 𝑥))) |
81 | 61, 80 | breq12d 4596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
((abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / 𝑥) ↔ (abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / 𝑥)))) |
82 | 81 | ralbidva 2968 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → (∀𝑥 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / 𝑥) ↔ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / 𝑥)))) |
83 | 56, 82 | syl5bb 271 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → (∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦) ↔ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / 𝑥)))) |
84 | 49, 83 | anbi12d 743 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → ((seq1( + ,
𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) ↔ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎)))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / 𝑥))))) |
85 | 84 | rexbidva 3031 |
. . 3
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) ↔ ∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎)))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / 𝑥))))) |
86 | 85 | exbidv 1837 |
. 2
⊢ (𝜑 → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) ↔ ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎)))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / 𝑎))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / 𝑥))))) |
87 | 30, 86 | mpbird 246 |
1
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) |