Step | Hyp | Ref
| Expression |
1 | | rpvmasum.z |
. . 3
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
2 | | rpvmasum.l |
. . 3
⊢ 𝐿 = (ℤRHom‘𝑍) |
3 | | rpvmasum.a |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | | rpvmasum2.g |
. . 3
⊢ 𝐺 = (DChr‘𝑁) |
5 | | rpvmasum2.d |
. . 3
⊢ 𝐷 = (Base‘𝐺) |
6 | | rpvmasum2.1 |
. . 3
⊢ 1 =
(0g‘𝐺) |
7 | | rpvmasum2.w |
. . . . . 6
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
8 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
9 | 7, 8 | eqsstri 3598 |
. . . . 5
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
10 | | dchrisum0.b |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
11 | 9, 10 | sseldi 3566 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
12 | 11 | eldifad 3552 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
13 | | eldifsni 4261 |
. . . 4
⊢ (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋 ≠ 1 ) |
14 | 11, 13 | syl 17 |
. . 3
⊢ (𝜑 → 𝑋 ≠ 1 ) |
15 | | fveq2 6103 |
. . . 4
⊢ (𝑛 = 𝑥 → (√‘𝑛) = (√‘𝑥)) |
16 | 15 | oveq2d 6565 |
. . 3
⊢ (𝑛 = 𝑥 → (1 / (√‘𝑛)) = (1 / (√‘𝑥))) |
17 | | 1nn 10908 |
. . . 4
⊢ 1 ∈
ℕ |
18 | 17 | a1i 11 |
. . 3
⊢ (𝜑 → 1 ∈
ℕ) |
19 | | rpsqrtcl 13853 |
. . . . 5
⊢ (𝑛 ∈ ℝ+
→ (√‘𝑛)
∈ ℝ+) |
20 | 19 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) →
(√‘𝑛) ∈
ℝ+) |
21 | 20 | rprecred 11759 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → (1 /
(√‘𝑛)) ∈
ℝ) |
22 | | simp3r 1083 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ≤ 𝑥) |
23 | | simp2l 1080 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℝ+) |
24 | 23 | rprege0d 11755 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛)) |
25 | | simp2r 1081 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
26 | 25 | rprege0d 11755 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
27 | | sqrtle 13849 |
. . . . . 6
⊢ (((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) ∧ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) → (𝑛 ≤ 𝑥 ↔ (√‘𝑛) ≤ (√‘𝑥))) |
28 | 24, 26, 27 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑛 ≤ 𝑥 ↔ (√‘𝑛) ≤ (√‘𝑥))) |
29 | 22, 28 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (√‘𝑛) ≤ (√‘𝑥)) |
30 | 23 | rpsqrtcld 13998 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (√‘𝑛) ∈
ℝ+) |
31 | 25 | rpsqrtcld 13998 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (√‘𝑥) ∈
ℝ+) |
32 | 30, 31 | lerecd 11767 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((√‘𝑛) ≤ (√‘𝑥) ↔ (1 / (√‘𝑥)) ≤ (1 /
(√‘𝑛)))) |
33 | 29, 32 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 / (√‘𝑥)) ≤ (1 /
(√‘𝑛))) |
34 | | sqrtlim 24499 |
. . . 4
⊢ (𝑛 ∈ ℝ+
↦ (1 / (√‘𝑛))) ⇝𝑟
0 |
35 | 34 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ (1 /
(√‘𝑛)))
⇝𝑟 0) |
36 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = 𝑛 → (𝐿‘𝑎) = (𝐿‘𝑛)) |
37 | 36 | fveq2d 6107 |
. . . . 5
⊢ (𝑎 = 𝑛 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑛))) |
38 | | fveq2 6103 |
. . . . . 6
⊢ (𝑎 = 𝑛 → (√‘𝑎) = (√‘𝑛)) |
39 | 38 | oveq2d 6565 |
. . . . 5
⊢ (𝑎 = 𝑛 → (1 / (√‘𝑎)) = (1 / (√‘𝑛))) |
40 | 37, 39 | oveq12d 6567 |
. . . 4
⊢ (𝑎 = 𝑛 → ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))) = ((𝑋‘(𝐿‘𝑛)) · (1 / (√‘𝑛)))) |
41 | 40 | cbvmptv 4678 |
. . 3
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))) = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · (1 / (√‘𝑛)))) |
42 | 1, 2, 3, 4, 5, 6, 12, 14, 16, 18, 21, 33, 35, 41 | dchrisum 24981 |
. 2
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥))))) |
43 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ 𝐷) |
44 | | nnz 11276 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
45 | 44 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) |
46 | 4, 1, 5, 2, 43, 45 | dchrzrhcl 24770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
47 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
48 | 47 | nnrpd 11746 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
49 | 48 | rpsqrtcld 13998 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (√‘𝑛) ∈
ℝ+) |
50 | 49 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (√‘𝑛) ∈
ℂ) |
51 | 49 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (√‘𝑛) ≠ 0) |
52 | 46, 50, 51 | divrecd 10683 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛)) = ((𝑋‘(𝐿‘𝑛)) · (1 / (√‘𝑛)))) |
53 | 52 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛))) = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · (1 / (√‘𝑛))))) |
54 | | dchrisum0lem1.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
55 | 37, 38 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑛 → ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) = ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛))) |
56 | 55 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛))) |
57 | 54, 56 | eqtri 2632 |
. . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛))) |
58 | 53, 57, 41 | 3eqtr4g 2669 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) |
59 | 58 | seqeq3d 12671 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐹) = seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))) |
60 | 59 | breq1d 4593 |
. . . . . 6
⊢ (𝜑 → (seq1( + , 𝐹) ⇝ 𝑡 ↔ seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡)) |
61 | 60 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → (seq1( + ,
𝐹) ⇝ 𝑡 ↔ seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡)) |
62 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (⌊‘𝑦) = (⌊‘𝑥)) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
64 | 63 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡) = ((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) |
65 | 64 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡))) |
66 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (√‘𝑦) = (√‘𝑥)) |
67 | 66 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑐 / (√‘𝑦)) = (𝑐 / (√‘𝑥))) |
68 | 65, 67 | breq12d 4596 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / (√‘𝑥)))) |
69 | 68 | cbvralv 3147 |
. . . . . 6
⊢
(∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)) ↔ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / (√‘𝑥))) |
70 | 58 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) |
71 | 70 | seqeq3d 12671 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
seq1( + , 𝐹) = seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))) |
72 | 71 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(seq1( + , 𝐹)‘(⌊‘𝑥)) = (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥))) |
73 | 72 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡) = ((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) |
74 | 73 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) = (abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡))) |
75 | | elrege0 12149 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ (0[,)+∞) ↔
(𝑐 ∈ ℝ ∧ 0
≤ 𝑐)) |
76 | 75 | simplbi 475 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (0[,)+∞) →
𝑐 ∈
ℝ) |
77 | 76 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑐 ∈
ℝ) |
78 | 77 | recnd 9947 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑐 ∈
ℂ) |
79 | | 1re 9918 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
80 | | elicopnf 12140 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℝ → (𝑥 ∈
(1[,)+∞) ↔ (𝑥
∈ ℝ ∧ 1 ≤ 𝑥))) |
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 1
≤ 𝑥)) |
82 | 81 | simplbi 475 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (1[,)+∞) →
𝑥 ∈
ℝ) |
83 | 82 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑥 ∈
ℝ) |
84 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 0
∈ ℝ) |
85 | | 1red 9934 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 1
∈ ℝ) |
86 | | 0lt1 10429 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
87 | 86 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 0
< 1) |
88 | 81 | simprbi 479 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1[,)+∞) → 1
≤ 𝑥) |
89 | 88 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 1
≤ 𝑥) |
90 | 84, 85, 83, 87, 89 | ltletrd 10076 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 0
< 𝑥) |
91 | 83, 90 | elrpd 11745 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑥 ∈
ℝ+) |
92 | 91 | rpsqrtcld 13998 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(√‘𝑥) ∈
ℝ+) |
93 | 92 | rpcnd 11750 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(√‘𝑥) ∈
ℂ) |
94 | 92 | rpne0d 11753 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(√‘𝑥) ≠
0) |
95 | 78, 93, 94 | divrecd 10683 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(𝑐 / (√‘𝑥)) = (𝑐 · (1 / (√‘𝑥)))) |
96 | 74, 95 | breq12d 4596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
((abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / (√‘𝑥)) ↔ (abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥))))) |
97 | 96 | ralbidva 2968 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → (∀𝑥 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / (√‘𝑥)) ↔ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥))))) |
98 | 69, 97 | syl5bb 271 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → (∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)) ↔ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥))))) |
99 | 61, 98 | anbi12d 743 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → ((seq1( + ,
𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) ↔ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥)))))) |
100 | 99 | rexbidva 3031 |
. . 3
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) ↔ ∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥)))))) |
101 | 100 | exbidv 1837 |
. 2
⊢ (𝜑 → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) ↔ ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥)))))) |
102 | 42, 101 | mpbird 246 |
1
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)))) |