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 24471 |
. 2
⊢ (𝜑 → 𝐺:ℕ⟶dom
∫1) |
6 | 1, 2, 3, 4 | mbfi1fseqlem5 24472 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(0𝑝 ∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1)))) |
7 | 6 | ralrimiva 3096 |
. 2
⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1)))) |
8 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
9 | 8 | recnd 10747 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
10 | 9 | abscld 14886 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈
ℝ) |
11 | 2 | ffvelrnda 6861 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
12 | | elrege0 12928 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
13 | 11, 12 | sylib 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
14 | 13 | simpld 498 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
15 | 10, 14 | readdcld 10748 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ) |
16 | | arch 11973 |
. . . . 5
⊢
(((abs‘𝑥) +
(𝐹‘𝑥)) ∈ ℝ → ∃𝑘 ∈ ℕ
((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑘 ∈ ℕ
((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘) |
18 | | eqid 2738 |
. . . . 5
⊢
(ℤ≥‘𝑘) = (ℤ≥‘𝑘) |
19 | | nnz 12085 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
20 | 19 | ad2antrl 728 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℤ) |
21 | | nnuz 12363 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
22 | | 1zzd 12094 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℤ) |
23 | | halfcn 11931 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℂ |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 2) ∈
ℂ) |
25 | | halfre 11930 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
26 | | halfge0 11933 |
. . . . . . . . . . . 12
⊢ 0 ≤ (1
/ 2) |
27 | | absid 14746 |
. . . . . . . . . . . 12
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) |
28 | 25, 26, 27 | mp2an 692 |
. . . . . . . . . . 11
⊢
(abs‘(1 / 2)) = (1 / 2) |
29 | | halflt1 11934 |
. . . . . . . . . . 11
⊢ (1 / 2)
< 1 |
30 | 28, 29 | eqbrtri 5051 |
. . . . . . . . . 10
⊢
(abs‘(1 / 2)) < 1 |
31 | 30 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘(1 / 2))
< 1) |
32 | 24, 31 | expcnv 15312 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛)) ⇝
0) |
33 | 14 | recnd 10747 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ) |
34 | | nnex 11722 |
. . . . . . . . . 10
⊢ ℕ
∈ V |
35 | 34 | mptex 6996 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V) |
37 | | nnnn0 11983 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
38 | 37 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0) |
39 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑗)) |
40 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
↦ ((1 / 2)↑𝑛)) =
(𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛)) |
41 | | ovex 7203 |
. . . . . . . . . . 11
⊢ ((1 /
2)↑𝑗) ∈
V |
42 | 39, 40, 41 | fvmpt 6775 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗)) |
43 | 38, 42 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗)) |
44 | | expcl 13539 |
. . . . . . . . . 10
⊢ (((1 / 2)
∈ ℂ ∧ 𝑗
∈ ℕ0) → ((1 / 2)↑𝑗) ∈ ℂ) |
45 | 23, 38, 44 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((1 / 2)↑𝑗) ∈
ℂ) |
46 | 43, 45 | eqeltrd 2833 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗) ∈
ℂ) |
47 | 39 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑥) − ((1 / 2)↑𝑛)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
48 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) |
49 | | ovex 7203 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ V |
50 | 47, 48, 49 | fvmpt 6775 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
51 | 50 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
52 | 43 | oveq2d 7186 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑥) − ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
53 | 51, 52 | eqtr4d 2776 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗))) |
54 | 21, 22, 32, 33, 36, 46, 53 | climsubc2 15086 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ ((𝐹‘𝑥) − 0)) |
55 | 33 | subid1d 11064 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) − 0) = (𝐹‘𝑥)) |
56 | 54, 55 | breqtrd 5056 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥)) |
57 | 56 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥)) |
58 | 34 | mptex 6996 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V |
59 | 58 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V) |
60 | | simprl 771 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℕ) |
61 | | eluznn 12400 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑘)) → 𝑗 ∈ ℕ) |
62 | 60, 61 | sylan 583 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℕ) |
63 | 62, 50 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
64 | 14 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ∈ ℝ) |
65 | 62, 37 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℕ0) |
66 | | reexpcl 13538 |
. . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ 𝑗
∈ ℕ0) → ((1 / 2)↑𝑗) ∈ ℝ) |
67 | 25, 65, 66 | sylancr 590 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((1 / 2)↑𝑗) ∈
ℝ) |
68 | 64, 67 | resubcld 11146 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ ℝ) |
69 | 63, 68 | eqeltrd 2833 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ∈ ℝ) |
70 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝐺‘𝑛) = (𝐺‘𝑗)) |
71 | 70 | fveq1d 6676 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → ((𝐺‘𝑛)‘𝑥) = ((𝐺‘𝑗)‘𝑥)) |
72 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) |
73 | | fvex 6687 |
. . . . . . . 8
⊢ ((𝐺‘𝑗)‘𝑥) ∈ V |
74 | 71, 72, 73 | fvmpt 6775 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥)) |
75 | 62, 74 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥)) |
76 | 5 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝐺:ℕ⟶dom
∫1) |
77 | 76, 62 | ffvelrnd 6862 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐺‘𝑗) ∈ dom
∫1) |
78 | | i1ff 24428 |
. . . . . . . 8
⊢ ((𝐺‘𝑗) ∈ dom ∫1 → (𝐺‘𝑗):ℝ⟶ℝ) |
79 | 77, 78 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐺‘𝑗):ℝ⟶ℝ) |
80 | 8 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ∈ ℝ) |
81 | 79, 80 | ffvelrnd 6862 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) ∈ ℝ) |
82 | 75, 81 | eqeltrd 2833 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ∈ ℝ) |
83 | 33 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ∈ ℂ) |
84 | | 2nn 11789 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
85 | | nnexpcl 13534 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
86 | 84, 65, 85 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ∈
ℕ) |
87 | 86 | nnred 11731 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ∈
ℝ) |
88 | 87 | recnd 10747 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ∈
ℂ) |
89 | 86 | nnne0d 11766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ≠ 0) |
90 | 83, 88, 89 | divcan4d 11500 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) = (𝐹‘𝑥)) |
91 | 90 | eqcomd 2744 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) = (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗))) |
92 | | 2cnd 11794 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 2 ∈
ℂ) |
93 | | 2ne0 11820 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
94 | 93 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 2 ≠
0) |
95 | | eluzelz 12334 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑘) → 𝑗 ∈ ℤ) |
96 | 95 | adantl 485 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℤ) |
97 | 92, 94, 96 | exprecd 13610 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗))) |
98 | 91, 97 | oveq12d 7188 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗)))) |
99 | 64, 87 | remulcld 10749 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ) |
100 | 99 | recnd 10747 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℂ) |
101 | | 1cnd 10714 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 1 ∈
ℂ) |
102 | 100, 101,
88, 89 | divsubdird 11533 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗)))) |
103 | 98, 102 | eqtr4d 2776 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗))) |
104 | | fllep1 13262 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)) |
105 | 99, 104 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)) |
106 | | 1red 10720 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 1 ∈
ℝ) |
107 | | reflcl 13257 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ →
(⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ) |
108 | 99, 107 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ) |
109 | 99, 106, 108 | lesubaddd 11315 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))) |
110 | 105, 109 | mpbird 260 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗)))) |
111 | | peano2rem 11031 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈
ℝ) |
112 | 99, 111 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈
ℝ) |
113 | 86 | nngt0d 11765 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 0 < (2↑𝑗)) |
114 | | lediv1 11583 |
. . . . . . . . 9
⊢
(((((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ
∧ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 <
(2↑𝑗))) →
((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤
(⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))) |
115 | 112, 108,
87, 113, 114 | syl112anc 1375 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))) |
116 | 110, 115 | mpbid 235 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
117 | 103, 116 | eqbrtrd 5052 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
118 | 1, 2, 3, 4 | mbfi1fseqlem2 24469 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))) |
119 | 62, 118 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))) |
120 | 119 | fveq1d 6676 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥)) |
121 | | ovex 7203 |
. . . . . . . . . . 11
⊢ (𝑗𝐽𝑥) ∈ V |
122 | | vex 3402 |
. . . . . . . . . . 11
⊢ 𝑗 ∈ V |
123 | 121, 122 | ifex 4464 |
. . . . . . . . . 10
⊢ if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) ∈ V |
124 | | c0ex 10713 |
. . . . . . . . . 10
⊢ 0 ∈
V |
125 | 123, 124 | ifex 4464 |
. . . . . . . . 9
⊢ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V |
126 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
127 | 126 | fvmpt2 6786 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
128 | 80, 125, 127 | sylancl 589 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
129 | 75, 120, 128 | 3eqtrd 2777 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
130 | 10 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (abs‘𝑥) ∈
ℝ) |
131 | 15 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ) |
132 | 62 | nnred 11731 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℝ) |
133 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
134 | 133, 12 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
135 | 134 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 0 ≤ (𝐹‘𝑥)) |
136 | 130, 64 | addge01d 11306 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (0 ≤ (𝐹‘𝑥) ↔ (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))) |
137 | 135, 136 | mpbid 235 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))) |
138 | 60 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ∈ ℕ) |
139 | 138 | nnred 11731 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ∈ ℝ) |
140 | | simplrr 778 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘) |
141 | 131, 139,
140 | ltled 10866 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑘) |
142 | | eluzle 12337 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘𝑘) → 𝑘 ≤ 𝑗) |
143 | 142 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ≤ 𝑗) |
144 | 131, 139,
132, 141, 143 | letrd 10875 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑗) |
145 | 130, 131,
132, 137, 144 | letrd 10875 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (abs‘𝑥) ≤ 𝑗) |
146 | 80, 132 | absled 14880 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) ≤ 𝑗 ↔ (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))) |
147 | 145, 146 | mpbid 235 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)) |
148 | 147 | simpld 498 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → -𝑗 ≤ 𝑥) |
149 | 147 | simprd 499 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ≤ 𝑗) |
150 | 132 | renegcld 11145 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → -𝑗 ∈ ℝ) |
151 | | elicc2 12886 |
. . . . . . . . . 10
⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))) |
152 | 150, 132,
151 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))) |
153 | 80, 148, 149, 152 | mpbir3and 1343 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ∈ (-𝑗[,]𝑗)) |
154 | 153 | iftrued 4422 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) = if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗)) |
155 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
156 | 155 | fveq2d 6678 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥)) |
157 | | simpl 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑗) |
158 | 157 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑗)) |
159 | 156, 158 | oveq12d 7188 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑗))) |
160 | 159 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑗)))) |
161 | 160, 158 | oveq12d 7188 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
162 | | ovex 7203 |
. . . . . . . . . . . 12
⊢
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ V |
163 | 161, 3, 162 | ovmpoa 7320 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
164 | 62, 80, 163 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
165 | 108, 86 | nndivred 11770 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ ℝ) |
166 | | flle 13260 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ →
(⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))) |
167 | 99, 166 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))) |
168 | | ledivmul2 11597 |
. . . . . . . . . . . . 13
⊢
(((⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 <
(2↑𝑗))) →
(((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))) |
169 | 108, 64, 87, 113, 168 | syl112anc 1375 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
(((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))) |
170 | 167, 169 | mpbird 260 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥)) |
171 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ∈ ℂ) |
172 | 171 | absge0d 14894 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 0 ≤
(abs‘𝑥)) |
173 | 64, 130 | addge02d 11307 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (0 ≤
(abs‘𝑥) ↔ (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))) |
174 | 172, 173 | mpbid 235 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))) |
175 | 64, 131, 132, 174, 144 | letrd 10875 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ≤ 𝑗) |
176 | 165, 64, 132, 170, 175 | letrd 10875 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ 𝑗) |
177 | 164, 176 | eqbrtrd 5052 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝑗𝐽𝑥) ≤ 𝑗) |
178 | 177 | iftrued 4422 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = (𝑗𝐽𝑥)) |
179 | 178, 164 | eqtrd 2773 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
180 | 129, 154,
179 | 3eqtrd 2777 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
181 | 117, 63, 180 | 3brtr4d 5062 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗)) |
182 | 180, 170 | eqbrtrd 5052 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ≤ (𝐹‘𝑥)) |
183 | 18, 20, 57, 59, 69, 82, 181, 182 | climsqz 15088 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
184 | 17, 183 | rexlimddv 3201 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
185 | 184 | ralrimiva 3096 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
186 | 34 | mptex 6996 |
. . . 4
⊢ (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ∈ V |
187 | 4, 186 | eqeltri 2829 |
. . 3
⊢ 𝐺 ∈ V |
188 | | feq1 6485 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑔:ℕ⟶dom ∫1 ↔
𝐺:ℕ⟶dom
∫1)) |
189 | | fveq1 6673 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛)) |
190 | 189 | breq2d 5042 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (0𝑝
∘r ≤ (𝑔‘𝑛) ↔ 0𝑝
∘r ≤ (𝐺‘𝑛))) |
191 | | fveq1 6673 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1))) |
192 | 189, 191 | breq12d 5043 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1)) ↔ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1)))) |
193 | 190, 192 | anbi12d 634 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((0𝑝
∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ↔ (0𝑝
∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))))) |
194 | 193 | ralbidv 3109 |
. . . 4
⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ↔ ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))))) |
195 | 189 | fveq1d 6676 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛)‘𝑥) = ((𝐺‘𝑛)‘𝑥)) |
196 | 195 | mpteq2dv 5126 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))) |
197 | 196 | breq1d 5040 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
198 | 197 | ralbidv 3109 |
. . . 4
⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
199 | 188, 194,
198 | 3anbi123d 1437 |
. . 3
⊢ (𝑔 = 𝐺 → ((𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ (𝐺:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
200 | 187, 199 | spcev 3510 |
. 2
⊢ ((𝐺:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝
∘r ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘r ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
201 | 5, 7, 185, 200 | syl3anc 1372 |
1
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |