Step | Hyp | Ref
| Expression |
1 | | mbfi1fseq.1 |
. . 3
⊢ (𝜑 → 𝐹 ∈ MblFn) |
2 | | mbfi1fseq.2 |
. . 3
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
3 | | mbfi1fseq.3 |
. . 3
⊢ 𝐽 = (𝑚 ∈ ℕ, 𝑦 ∈ ℝ ↦
((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚))) |
4 | | mbfi1fseq.4 |
. . 3
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) |
5 | 1, 2, 3, 4 | mbfi1fseqlem4 24883 |
. 2
⊢ (𝜑 → 𝐺:ℕ⟶dom
∫1) |
6 | 1, 2, 3, 4 | mbfi1fseqlem5 24884 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(0𝑝 ∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1)))) |
7 | 6 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1)))) |
8 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
9 | 8 | recnd 11003 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
10 | 9 | abscld 15148 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈
ℝ) |
11 | 2 | ffvelrnda 6961 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
12 | | elrege0 13186 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
13 | 11, 12 | sylib 217 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
14 | 13 | simpld 495 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
15 | 10, 14 | readdcld 11004 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ) |
16 | | arch 12230 |
. . . . 5
⊢
(((abs‘𝑥) +
(𝐹‘𝑥)) ∈ ℝ → ∃𝑘 ∈ ℕ
((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑘 ∈ ℕ
((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘) |
18 | | eqid 2738 |
. . . . 5
⊢
(ℤ≥‘𝑘) = (ℤ≥‘𝑘) |
19 | | nnz 12342 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
20 | 19 | ad2antrl 725 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℤ) |
21 | | nnuz 12621 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
22 | | 1zzd 12351 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℤ) |
23 | | halfcn 12188 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℂ |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 2) ∈
ℂ) |
25 | | halfre 12187 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
26 | | halfge0 12190 |
. . . . . . . . . . . 12
⊢ 0 ≤ (1
/ 2) |
27 | | absid 15008 |
. . . . . . . . . . . 12
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) |
28 | 25, 26, 27 | mp2an 689 |
. . . . . . . . . . 11
⊢
(abs‘(1 / 2)) = (1 / 2) |
29 | | halflt1 12191 |
. . . . . . . . . . 11
⊢ (1 / 2)
< 1 |
30 | 28, 29 | eqbrtri 5095 |
. . . . . . . . . 10
⊢
(abs‘(1 / 2)) < 1 |
31 | 30 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘(1 / 2))
< 1) |
32 | 24, 31 | expcnv 15576 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛)) ⇝
0) |
33 | 14 | recnd 11003 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ) |
34 | | nnex 11979 |
. . . . . . . . . 10
⊢ ℕ
∈ V |
35 | 34 | mptex 7099 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V) |
37 | | nnnn0 12240 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
38 | 37 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0) |
39 | | oveq2 7283 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑗)) |
40 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
↦ ((1 / 2)↑𝑛)) =
(𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛)) |
41 | | ovex 7308 |
. . . . . . . . . . 11
⊢ ((1 /
2)↑𝑗) ∈
V |
42 | 39, 40, 41 | fvmpt 6875 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗)) |
43 | 38, 42 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗)) |
44 | | expcl 13800 |
. . . . . . . . . 10
⊢ (((1 / 2)
∈ ℂ ∧ 𝑗
∈ ℕ0) → ((1 / 2)↑𝑗) ∈ ℂ) |
45 | 23, 38, 44 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((1 / 2)↑𝑗) ∈
ℂ) |
46 | 43, 45 | eqeltrd 2839 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗) ∈
ℂ) |
47 | 39 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑥) − ((1 / 2)↑𝑛)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
48 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) |
49 | | ovex 7308 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ V |
50 | 47, 48, 49 | fvmpt 6875 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
51 | 50 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
52 | 43 | oveq2d 7291 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑥) − ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
53 | 51, 52 | eqtr4d 2781 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗))) |
54 | 21, 22, 32, 33, 36, 46, 53 | climsubc2 15348 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ ((𝐹‘𝑥) − 0)) |
55 | 33 | subid1d 11321 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) − 0) = (𝐹‘𝑥)) |
56 | 54, 55 | breqtrd 5100 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥)) |
57 | 56 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥)) |
58 | 34 | mptex 7099 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V |
59 | 58 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V) |
60 | | simprl 768 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℕ) |
61 | | eluznn 12658 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑘)) → 𝑗 ∈ ℕ) |
62 | 60, 61 | sylan 580 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℕ) |
63 | 62, 50 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
64 | 14 | ad2antrr 723 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ∈ ℝ) |
65 | 62, 37 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℕ0) |
66 | | reexpcl 13799 |
. . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ 𝑗
∈ ℕ0) → ((1 / 2)↑𝑗) ∈ ℝ) |
67 | 25, 65, 66 | sylancr 587 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((1 / 2)↑𝑗) ∈
ℝ) |
68 | 64, 67 | resubcld 11403 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ ℝ) |
69 | 63, 68 | eqeltrd 2839 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ∈ ℝ) |
70 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝐺‘𝑛) = (𝐺‘𝑗)) |
71 | 70 | fveq1d 6776 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → ((𝐺‘𝑛)‘𝑥) = ((𝐺‘𝑗)‘𝑥)) |
72 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) |
73 | | fvex 6787 |
. . . . . . . 8
⊢ ((𝐺‘𝑗)‘𝑥) ∈ V |
74 | 71, 72, 73 | fvmpt 6875 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥)) |
75 | 62, 74 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥)) |
76 | 5 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝐺:ℕ⟶dom
∫1) |
77 | 76, 62 | ffvelrnd 6962 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐺‘𝑗) ∈ dom
∫1) |
78 | | i1ff 24840 |
. . . . . . . 8
⊢ ((𝐺‘𝑗) ∈ dom ∫1 → (𝐺‘𝑗):ℝ⟶ℝ) |
79 | 77, 78 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐺‘𝑗):ℝ⟶ℝ) |
80 | 8 | ad2antrr 723 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ∈ ℝ) |
81 | 79, 80 | ffvelrnd 6962 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) ∈ ℝ) |
82 | 75, 81 | eqeltrd 2839 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ∈ ℝ) |
83 | 33 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ∈ ℂ) |
84 | | 2nn 12046 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
85 | | nnexpcl 13795 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
86 | 84, 65, 85 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ∈
ℕ) |
87 | 86 | nnred 11988 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ∈
ℝ) |
88 | 87 | recnd 11003 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ∈
ℂ) |
89 | 86 | nnne0d 12023 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ≠ 0) |
90 | 83, 88, 89 | divcan4d 11757 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) = (𝐹‘𝑥)) |
91 | 90 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) = (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗))) |
92 | | 2cnd 12051 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 2 ∈
ℂ) |
93 | | 2ne0 12077 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
94 | 93 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 2 ≠
0) |
95 | | eluzelz 12592 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑘) → 𝑗 ∈ ℤ) |
96 | 95 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℤ) |
97 | 92, 94, 96 | exprecd 13872 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗))) |
98 | 91, 97 | oveq12d 7293 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗)))) |
99 | 64, 87 | remulcld 11005 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ) |
100 | 99 | recnd 11003 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℂ) |
101 | | 1cnd 10970 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 1 ∈
ℂ) |
102 | 100, 101,
88, 89 | divsubdird 11790 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗)))) |
103 | 98, 102 | eqtr4d 2781 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗))) |
104 | | fllep1 13521 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)) |
105 | 99, 104 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)) |
106 | | 1red 10976 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 1 ∈
ℝ) |
107 | | reflcl 13516 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ →
(⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ) |
108 | 99, 107 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ) |
109 | 99, 106, 108 | lesubaddd 11572 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))) |
110 | 105, 109 | mpbird 256 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗)))) |
111 | | peano2rem 11288 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈
ℝ) |
112 | 99, 111 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈
ℝ) |
113 | 86 | nngt0d 12022 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 0 < (2↑𝑗)) |
114 | | lediv1 11840 |
. . . . . . . . 9
⊢
(((((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ
∧ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 <
(2↑𝑗))) →
((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤
(⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))) |
115 | 112, 108,
87, 113, 114 | syl112anc 1373 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))) |
116 | 110, 115 | mpbid 231 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
117 | 103, 116 | eqbrtrd 5096 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
118 | 1, 2, 3, 4 | mbfi1fseqlem2 24881 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))) |
119 | 62, 118 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))) |
120 | 119 | fveq1d 6776 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥)) |
121 | | ovex 7308 |
. . . . . . . . . . 11
⊢ (𝑗𝐽𝑥) ∈ V |
122 | | vex 3436 |
. . . . . . . . . . 11
⊢ 𝑗 ∈ V |
123 | 121, 122 | ifex 4509 |
. . . . . . . . . 10
⊢ if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) ∈ V |
124 | | c0ex 10969 |
. . . . . . . . . 10
⊢ 0 ∈
V |
125 | 123, 124 | ifex 4509 |
. . . . . . . . 9
⊢ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V |
126 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
127 | 126 | fvmpt2 6886 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
128 | 80, 125, 127 | sylancl 586 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
129 | 75, 120, 128 | 3eqtrd 2782 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
130 | 10 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (abs‘𝑥) ∈
ℝ) |
131 | 15 | ad2antrr 723 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ) |
132 | 62 | nnred 11988 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℝ) |
133 | 11 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
134 | 133, 12 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
135 | 134 | simprd 496 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 0 ≤ (𝐹‘𝑥)) |
136 | 130, 64 | addge01d 11563 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (0 ≤ (𝐹‘𝑥) ↔ (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))) |
137 | 135, 136 | mpbid 231 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))) |
138 | 60 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ∈ ℕ) |
139 | 138 | nnred 11988 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ∈ ℝ) |
140 | | simplrr 775 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘) |
141 | 131, 139,
140 | ltled 11123 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑘) |
142 | | eluzle 12595 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘𝑘) → 𝑘 ≤ 𝑗) |
143 | 142 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ≤ 𝑗) |
144 | 131, 139,
132, 141, 143 | letrd 11132 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑗) |
145 | 130, 131,
132, 137, 144 | letrd 11132 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (abs‘𝑥) ≤ 𝑗) |
146 | 80, 132 | absled 15142 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) ≤ 𝑗 ↔ (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))) |
147 | 145, 146 | mpbid 231 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)) |
148 | 147 | simpld 495 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → -𝑗 ≤ 𝑥) |
149 | 147 | simprd 496 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ≤ 𝑗) |
150 | 132 | renegcld 11402 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → -𝑗 ∈ ℝ) |
151 | | elicc2 13144 |
. . . . . . . . . 10
⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))) |
152 | 150, 132,
151 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))) |
153 | 80, 148, 149, 152 | mpbir3and 1341 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ∈ (-𝑗[,]𝑗)) |
154 | 153 | iftrued 4467 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) = if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗)) |
155 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
156 | 155 | fveq2d 6778 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥)) |
157 | | simpl 483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑗) |
158 | 157 | oveq2d 7291 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑗)) |
159 | 156, 158 | oveq12d 7293 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑗))) |
160 | 159 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑗)))) |
161 | 160, 158 | oveq12d 7293 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
162 | | ovex 7308 |
. . . . . . . . . . . 12
⊢
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ V |
163 | 161, 3, 162 | ovmpoa 7428 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
164 | 62, 80, 163 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
165 | 108, 86 | nndivred 12027 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ ℝ) |
166 | | flle 13519 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ →
(⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))) |
167 | 99, 166 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))) |
168 | | ledivmul2 11854 |
. . . . . . . . . . . . 13
⊢
(((⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 <
(2↑𝑗))) →
(((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))) |
169 | 108, 64, 87, 113, 168 | syl112anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
(((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))) |
170 | 167, 169 | mpbird 256 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥)) |
171 | 9 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ∈ ℂ) |
172 | 171 | absge0d 15156 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 0 ≤
(abs‘𝑥)) |
173 | 64, 130 | addge02d 11564 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (0 ≤
(abs‘𝑥) ↔ (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))) |
174 | 172, 173 | mpbid 231 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))) |
175 | 64, 131, 132, 174, 144 | letrd 11132 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ≤ 𝑗) |
176 | 165, 64, 132, 170, 175 | letrd 11132 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ 𝑗) |
177 | 164, 176 | eqbrtrd 5096 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝑗𝐽𝑥) ≤ 𝑗) |
178 | 177 | iftrued 4467 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = (𝑗𝐽𝑥)) |
179 | 178, 164 | eqtrd 2778 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
180 | 129, 154,
179 | 3eqtrd 2782 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
181 | 117, 63, 180 | 3brtr4d 5106 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗)) |
182 | 180, 170 | eqbrtrd 5096 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ≤ (𝐹‘𝑥)) |
183 | 18, 20, 57, 59, 69, 82, 181, 182 | climsqz 15350 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
184 | 17, 183 | rexlimddv 3220 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
185 | 184 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
186 | 34 | mptex 7099 |
. . . 4
⊢ (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ∈ V |
187 | 4, 186 | eqeltri 2835 |
. . 3
⊢ 𝐺 ∈ V |
188 | | feq1 6581 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑔:ℕ⟶dom ∫1 ↔
𝐺:ℕ⟶dom
∫1)) |
189 | | fveq1 6773 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛)) |
190 | 189 | breq2d 5086 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (0𝑝
∘r ≤ (𝑔‘𝑛) ↔ 0𝑝
∘r ≤ (𝐺‘𝑛))) |
191 | | fveq1 6773 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1))) |
192 | 189, 191 | breq12d 5087 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1)) ↔ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1)))) |
193 | 190, 192 | anbi12d 631 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((0𝑝
∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ↔ (0𝑝
∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))))) |
194 | 193 | ralbidv 3112 |
. . . 4
⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ↔ ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))))) |
195 | 189 | fveq1d 6776 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛)‘𝑥) = ((𝐺‘𝑛)‘𝑥)) |
196 | 195 | mpteq2dv 5176 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))) |
197 | 196 | breq1d 5084 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
198 | 197 | ralbidv 3112 |
. . . 4
⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
199 | 188, 194,
198 | 3anbi123d 1435 |
. . 3
⊢ (𝑔 = 𝐺 → ((𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ (𝐺:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
200 | 187, 199 | spcev 3545 |
. 2
⊢ ((𝐺:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
201 | 5, 7, 185, 200 | syl3anc 1370 |
1
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |