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 3720 |
. . . . . 6
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
9 | 7, 8 | eqsstri 3668 |
. . . . 5
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
10 | | dchrisum0.b |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
11 | 9, 10 | sseldi 3634 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐷 ∖ { 1 })) |
12 | 11 | eldifad 3619 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
13 | | eldifsni 4353 |
. . . 4
⊢ (𝑋 ∈ (𝐷 ∖ { 1 }) → 𝑋 ≠ 1 ) |
14 | 11, 13 | syl 17 |
. . 3
⊢ (𝜑 → 𝑋 ≠ 1 ) |
15 | | fveq2 6229 |
. . . 4
⊢ (𝑛 = 𝑥 → (√‘𝑛) = (√‘𝑥)) |
16 | 15 | oveq2d 6706 |
. . 3
⊢ (𝑛 = 𝑥 → (1 / (√‘𝑛)) = (1 / (√‘𝑥))) |
17 | | 1nn 11069 |
. . . 4
⊢ 1 ∈
ℕ |
18 | 17 | a1i 11 |
. . 3
⊢ (𝜑 → 1 ∈
ℕ) |
19 | | rpsqrtcl 14049 |
. . . . 5
⊢ (𝑛 ∈ ℝ+
→ (√‘𝑛)
∈ ℝ+) |
20 | 19 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) →
(√‘𝑛) ∈
ℝ+) |
21 | 20 | rprecred 11921 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → (1 /
(√‘𝑛)) ∈
ℝ) |
22 | | simp3r 1110 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ≤ 𝑥) |
23 | | simp2l 1107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑛 ∈ ℝ+) |
24 | 23 | rprege0d 11917 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛)) |
25 | | simp2r 1108 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
26 | 25 | rprege0d 11917 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
27 | | sqrtle 14045 |
. . . . . 6
⊢ (((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) ∧ (𝑥 ∈ ℝ ∧ 0 ≤
𝑥)) → (𝑛 ≤ 𝑥 ↔ (√‘𝑛) ≤ (√‘𝑥))) |
28 | 24, 26, 27 | syl2anc 694 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (𝑛 ≤ 𝑥 ↔ (√‘𝑛) ≤ (√‘𝑥))) |
29 | 22, 28 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (√‘𝑛) ≤ (√‘𝑥)) |
30 | 23 | rpsqrtcld 14194 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (√‘𝑛) ∈
ℝ+) |
31 | 25 | rpsqrtcld 14194 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (√‘𝑥) ∈
ℝ+) |
32 | 30, 31 | lerecd 11929 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → ((√‘𝑛) ≤ (√‘𝑥) ↔ (1 / (√‘𝑥)) ≤ (1 /
(√‘𝑛)))) |
33 | 29, 32 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+)
∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → (1 / (√‘𝑥)) ≤ (1 /
(√‘𝑛))) |
34 | | sqrtlim 24744 |
. . . 4
⊢ (𝑛 ∈ ℝ+
↦ (1 / (√‘𝑛))) ⇝𝑟
0 |
35 | 34 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ (1 /
(√‘𝑛)))
⇝𝑟 0) |
36 | | fveq2 6229 |
. . . . . 6
⊢ (𝑎 = 𝑛 → (𝐿‘𝑎) = (𝐿‘𝑛)) |
37 | 36 | fveq2d 6233 |
. . . . 5
⊢ (𝑎 = 𝑛 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑛))) |
38 | | fveq2 6229 |
. . . . . 6
⊢ (𝑎 = 𝑛 → (√‘𝑎) = (√‘𝑛)) |
39 | 38 | oveq2d 6706 |
. . . . 5
⊢ (𝑎 = 𝑛 → (1 / (√‘𝑎)) = (1 / (√‘𝑛))) |
40 | 37, 39 | oveq12d 6708 |
. . . 4
⊢ (𝑎 = 𝑛 → ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))) = ((𝑋‘(𝐿‘𝑛)) · (1 / (√‘𝑛)))) |
41 | 40 | cbvmptv 4783 |
. . 3
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))) = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · (1 / (√‘𝑛)))) |
42 | 1, 2, 3, 4, 5, 6, 12, 14, 16, 18, 21, 33, 35, 41 | dchrisum 25226 |
. 2
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥))))) |
43 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ 𝐷) |
44 | | nnz 11437 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℤ) |
45 | 44 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℤ) |
46 | 4, 1, 5, 2, 43, 45 | dchrzrhcl 25015 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
47 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
48 | 47 | nnrpd 11908 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
49 | 48 | rpsqrtcld 14194 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (√‘𝑛) ∈
ℝ+) |
50 | 49 | rpcnd 11912 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (√‘𝑛) ∈
ℂ) |
51 | 49 | rpne0d 11915 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (√‘𝑛) ≠ 0) |
52 | 46, 50, 51 | divrecd 10842 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛)) = ((𝑋‘(𝐿‘𝑛)) · (1 / (√‘𝑛)))) |
53 | 52 | mpteq2dva 4777 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛))) = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · (1 / (√‘𝑛))))) |
54 | | dchrisum0lem1.f |
. . . . . . . . . 10
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) |
55 | 37, 38 | oveq12d 6708 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑛 → ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)) = ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛))) |
56 | 55 | cbvmptv 4783 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎))) = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛))) |
57 | 54, 56 | eqtri 2673 |
. . . . . . . . 9
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) / (√‘𝑛))) |
58 | 53, 57, 41 | 3eqtr4g 2710 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) |
59 | 58 | seqeq3d 12849 |
. . . . . . 7
⊢ (𝜑 → seq1( + , 𝐹) = seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))) |
60 | 59 | breq1d 4695 |
. . . . . 6
⊢ (𝜑 → (seq1( + , 𝐹) ⇝ 𝑡 ↔ seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡)) |
61 | 60 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → (seq1( + ,
𝐹) ⇝ 𝑡 ↔ seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡)) |
62 | | fveq2 6229 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (⌊‘𝑦) = (⌊‘𝑥)) |
63 | 62 | fveq2d 6233 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘𝑥))) |
64 | 63 | oveq1d 6705 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡) = ((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) |
65 | 64 | fveq2d 6233 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡))) |
66 | | fveq2 6229 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (√‘𝑦) = (√‘𝑥)) |
67 | 66 | oveq2d 6706 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑐 / (√‘𝑦)) = (𝑐 / (√‘𝑥))) |
68 | 65, 67 | breq12d 4698 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / (√‘𝑥)))) |
69 | 68 | cbvralv 3201 |
. . . . . 6
⊢
(∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)) ↔ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / (√‘𝑥))) |
70 | 58 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) |
71 | 70 | seqeq3d 12849 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
seq1( + , 𝐹) = seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))) |
72 | 71 | fveq1d 6231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(seq1( + , 𝐹)‘(⌊‘𝑥)) = (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥))) |
73 | 72 | oveq1d 6705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡) = ((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) |
74 | 73 | fveq2d 6233 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) = (abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡))) |
75 | | elrege0 12316 |
. . . . . . . . . . . 12
⊢ (𝑐 ∈ (0[,)+∞) ↔
(𝑐 ∈ ℝ ∧ 0
≤ 𝑐)) |
76 | 75 | simplbi 475 |
. . . . . . . . . . 11
⊢ (𝑐 ∈ (0[,)+∞) →
𝑐 ∈
ℝ) |
77 | 76 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑐 ∈
ℝ) |
78 | 77 | recnd 10106 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑐 ∈
ℂ) |
79 | | 1re 10077 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
80 | | elicopnf 12307 |
. . . . . . . . . . . . . . 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 10079 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 0
∈ ℝ) |
85 | | 1red 10093 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 1
∈ ℝ) |
86 | | 0lt1 10588 |
. . . . . . . . . . . . . 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 10235 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) → 0
< 𝑥) |
91 | 83, 90 | elrpd 11907 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
𝑥 ∈
ℝ+) |
92 | 91 | rpsqrtcld 14194 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(√‘𝑥) ∈
ℝ+) |
93 | 92 | rpcnd 11912 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(√‘𝑥) ∈
ℂ) |
94 | 92 | rpne0d 11915 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(√‘𝑥) ≠
0) |
95 | 78, 93, 94 | divrecd 10842 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
(𝑐 / (√‘𝑥)) = (𝑐 · (1 / (√‘𝑥)))) |
96 | 74, 95 | breq12d 4698 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) ∧ 𝑥 ∈ (1[,)+∞)) →
((abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / (√‘𝑥)) ↔ (abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥))))) |
97 | 96 | ralbidva 3014 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → (∀𝑥 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 / (√‘𝑥)) ↔ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥))))) |
98 | 69, 97 | syl5bb 272 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → (∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)) ↔ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥))))) |
99 | 61, 98 | anbi12d 747 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (0[,)+∞)) → ((seq1( + ,
𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) ↔ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥)))))) |
100 | 99 | rexbidva 3078 |
. . 3
⊢ (𝜑 → (∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) ↔ ∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥)))))) |
101 | 100 | exbidv 1890 |
. 2
⊢ (𝜑 → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))) ↔ ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎))))) ⇝ 𝑡 ∧ ∀𝑥 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑋‘(𝐿‘𝑎)) · (1 / (√‘𝑎)))))‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · (1 / (√‘𝑥)))))) |
102 | 42, 101 | mpbird 247 |
1
⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦)))) |