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 23291 |
. 2
⊢ (𝜑 → 𝐺:ℕ⟶dom
∫1) |
6 | 1, 2, 3, 4 | mbfi1fseqlem5 23292 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(0𝑝 ∘𝑟 ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘𝑟 ≤ (𝐺‘(𝑛 + 1)))) |
7 | 6 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘𝑟 ≤ (𝐺‘(𝑛 + 1)))) |
8 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ) |
9 | 8 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℂ) |
10 | 9 | abscld 14023 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘𝑥) ∈
ℝ) |
11 | 2 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
12 | | elrege0 12149 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
13 | 11, 12 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
14 | 13 | simpld 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ) |
15 | 10, 14 | readdcld 9948 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ) |
16 | | arch 11166 |
. . . . 5
⊢
(((abs‘𝑥) +
(𝐹‘𝑥)) ∈ ℝ → ∃𝑘 ∈ ℕ
((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑘 ∈ ℕ
((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘) |
18 | | eqid 2610 |
. . . . 5
⊢
(ℤ≥‘𝑘) = (ℤ≥‘𝑘) |
19 | | nnz 11276 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
20 | 19 | ad2antrl 760 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℤ) |
21 | | nnuz 11599 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
22 | | 1zzd 11285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℤ) |
23 | | halfcn 11124 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℂ |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (1 / 2) ∈
ℂ) |
25 | | halfre 11123 |
. . . . . . . . . . . 12
⊢ (1 / 2)
∈ ℝ |
26 | | 0re 9919 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
27 | | halfgt0 11125 |
. . . . . . . . . . . . 13
⊢ 0 < (1
/ 2) |
28 | 26, 25, 27 | ltleii 10039 |
. . . . . . . . . . . 12
⊢ 0 ≤ (1
/ 2) |
29 | | absid 13884 |
. . . . . . . . . . . 12
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) |
30 | 25, 28, 29 | mp2an 704 |
. . . . . . . . . . 11
⊢
(abs‘(1 / 2)) = (1 / 2) |
31 | | halflt1 11127 |
. . . . . . . . . . 11
⊢ (1 / 2)
< 1 |
32 | 30, 31 | eqbrtri 4604 |
. . . . . . . . . 10
⊢
(abs‘(1 / 2)) < 1 |
33 | 32 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (abs‘(1 / 2))
< 1) |
34 | 24, 33 | expcnv 14435 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛)) ⇝
0) |
35 | 14 | recnd 9947 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℂ) |
36 | | nnex 10903 |
. . . . . . . . . 10
⊢ ℕ
∈ V |
37 | 36 | mptex 6390 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V |
38 | 37 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ∈ V) |
39 | | nnnn0 11176 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
40 | 39 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℕ0) |
41 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑗)) |
42 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
↦ ((1 / 2)↑𝑛)) =
(𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛)) |
43 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((1 /
2)↑𝑗) ∈
V |
44 | 41, 42, 43 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗)) |
45 | 40, 44 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗) = ((1 / 2)↑𝑗)) |
46 | | expcl 12740 |
. . . . . . . . . 10
⊢ (((1 / 2)
∈ ℂ ∧ 𝑗
∈ ℕ0) → ((1 / 2)↑𝑗) ∈ ℂ) |
47 | 23, 40, 46 | sylancr 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((1 / 2)↑𝑗) ∈
ℂ) |
48 | 45, 47 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗) ∈
ℂ) |
49 | 41 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → ((𝐹‘𝑥) − ((1 / 2)↑𝑛)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
50 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) = (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) |
51 | | ovex 6577 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ V |
52 | 49, 50, 51 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
53 | 52 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
54 | 45 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝐹‘𝑥) − ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗)) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
55 | 53, 54 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑗))) |
56 | 21, 22, 34, 35, 38, 48, 55 | climsubc2 14217 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ ((𝐹‘𝑥) − 0)) |
57 | 35 | subid1d 10260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) − 0) = (𝐹‘𝑥)) |
58 | 56, 57 | breqtrd 4609 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥)) |
59 | 58 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛))) ⇝ (𝐹‘𝑥)) |
60 | 36 | mptex 6390 |
. . . . . 6
⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V |
61 | 60 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ∈ V) |
62 | | simprl 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → 𝑘 ∈ ℕ) |
63 | | eluznn 11634 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝑘)) → 𝑗 ∈ ℕ) |
64 | 62, 63 | sylan 487 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℕ) |
65 | 64, 52 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) = ((𝐹‘𝑥) − ((1 / 2)↑𝑗))) |
66 | 14 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ∈ ℝ) |
67 | 64, 39 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℕ0) |
68 | | reexpcl 12739 |
. . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ 𝑗
∈ ℕ0) → ((1 / 2)↑𝑗) ∈ ℝ) |
69 | 25, 67, 68 | sylancr 694 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((1 / 2)↑𝑗) ∈
ℝ) |
70 | 66, 69 | resubcld 10337 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ∈ ℝ) |
71 | 65, 70 | eqeltrd 2688 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ∈ ℝ) |
72 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝐺‘𝑛) = (𝐺‘𝑗)) |
73 | 72 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → ((𝐺‘𝑛)‘𝑥) = ((𝐺‘𝑗)‘𝑥)) |
74 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) |
75 | | fvex 6113 |
. . . . . . . 8
⊢ ((𝐺‘𝑗)‘𝑥) ∈ V |
76 | 73, 74, 75 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥)) |
77 | 64, 76 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((𝐺‘𝑗)‘𝑥)) |
78 | 5 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝐺:ℕ⟶dom
∫1) |
79 | 78, 64 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐺‘𝑗) ∈ dom
∫1) |
80 | | i1ff 23249 |
. . . . . . . 8
⊢ ((𝐺‘𝑗) ∈ dom ∫1 → (𝐺‘𝑗):ℝ⟶ℝ) |
81 | 79, 80 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐺‘𝑗):ℝ⟶ℝ) |
82 | 8 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ∈ ℝ) |
83 | 81, 82 | ffvelrnd 6268 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) ∈ ℝ) |
84 | 77, 83 | eqeltrd 2688 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ∈ ℝ) |
85 | 35 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ∈ ℂ) |
86 | | 2nn 11062 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
87 | | nnexpcl 12735 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
88 | 86, 67, 87 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ∈
ℕ) |
89 | 88 | nnred 10912 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ∈
ℝ) |
90 | 89 | recnd 9947 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ∈
ℂ) |
91 | 88 | nnne0d 10942 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (2↑𝑗) ≠ 0) |
92 | 85, 90, 91 | divcan4d 10686 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) = (𝐹‘𝑥)) |
93 | 92 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) = (((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗))) |
94 | | 2cnd 10970 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 2 ∈
ℂ) |
95 | | 2ne0 10990 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
96 | 95 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 2 ≠
0) |
97 | | eluzelz 11573 |
. . . . . . . . . . 11
⊢ (𝑗 ∈
(ℤ≥‘𝑘) → 𝑗 ∈ ℤ) |
98 | 97 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℤ) |
99 | 94, 96, 98 | exprecd 12878 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗))) |
100 | 93, 99 | oveq12d 6567 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗)))) |
101 | 66, 89 | remulcld 9949 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ) |
102 | 101 | recnd 9947 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ∈ ℂ) |
103 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 1 ∈
ℂ) |
104 | 102, 103,
90, 91 | divsubdird 10719 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) / (2↑𝑗)) − (1 / (2↑𝑗)))) |
105 | 100, 104 | eqtr4d 2647 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) = ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗))) |
106 | | fllep1 12464 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)) |
107 | 101, 106 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1)) |
108 | | 1red 9934 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 1 ∈
ℝ) |
109 | | reflcl 12459 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ →
(⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ) |
110 | 101, 109 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ) |
111 | 101, 108,
110 | lesubaddd 10503 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((𝐹‘𝑥) · (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) + 1))) |
112 | 107, 111 | mpbird 246 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗)))) |
113 | | peano2rem 10227 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈
ℝ) |
114 | 101, 113 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈
ℝ) |
115 | 88 | nngt0d 10941 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 0 < (2↑𝑗)) |
116 | | lediv1 10767 |
. . . . . . . . 9
⊢
(((((𝐹‘𝑥) · (2↑𝑗)) − 1) ∈ ℝ
∧ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 <
(2↑𝑗))) →
((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤
(⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))) |
117 | 114, 110,
89, 115, 116 | syl112anc 1322 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) ≤ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ↔ ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)))) |
118 | 112, 117 | mpbid 221 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((((𝐹‘𝑥) · (2↑𝑗)) − 1) / (2↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
119 | 105, 118 | eqbrtrd 4605 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) − ((1 / 2)↑𝑗)) ≤ ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
120 | 1, 2, 3, 4 | mbfi1fseqlem2 23289 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))) |
121 | 64, 120 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐺‘𝑗) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))) |
122 | 121 | fveq1d 6105 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐺‘𝑗)‘𝑥) = ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥)) |
123 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑗𝐽𝑥) ∈ V |
124 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑗 ∈ V |
125 | 123, 124 | ifex 4106 |
. . . . . . . . . 10
⊢ if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) ∈ V |
126 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
127 | 125, 126 | ifex 4106 |
. . . . . . . . 9
⊢ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V |
128 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
129 | 128 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) ∈ V) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
130 | 82, 127, 129 | sylancl 693 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0))‘𝑥) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
131 | 77, 122, 130 | 3eqtrd 2648 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0)) |
132 | 10 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (abs‘𝑥) ∈
ℝ) |
133 | 15 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ∈ ℝ) |
134 | 64 | nnred 10912 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑗 ∈ ℝ) |
135 | 11 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
136 | 135, 12 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
137 | 136 | simprd 478 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 0 ≤ (𝐹‘𝑥)) |
138 | 132, 66 | addge01d 10494 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (0 ≤ (𝐹‘𝑥) ↔ (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))) |
139 | 137, 138 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (abs‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))) |
140 | 62 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ∈ ℕ) |
141 | 140 | nnred 10912 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ∈ ℝ) |
142 | | simplrr 797 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘) |
143 | 133, 141,
142 | ltled 10064 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑘) |
144 | | eluzle 11576 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘𝑘) → 𝑘 ≤ 𝑗) |
145 | 144 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑘 ≤ 𝑗) |
146 | 133, 141,
134, 143, 145 | letrd 10073 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) + (𝐹‘𝑥)) ≤ 𝑗) |
147 | 132, 133,
134, 139, 146 | letrd 10073 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (abs‘𝑥) ≤ 𝑗) |
148 | 82, 134 | absled 14017 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((abs‘𝑥) ≤ 𝑗 ↔ (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))) |
149 | 147, 148 | mpbid 221 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (-𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗)) |
150 | 149 | simpld 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → -𝑗 ≤ 𝑥) |
151 | 149 | simprd 478 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ≤ 𝑗) |
152 | 134 | renegcld 10336 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → -𝑗 ∈ ℝ) |
153 | | elicc2 12109 |
. . . . . . . . . 10
⊢ ((-𝑗 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))) |
154 | 152, 134,
153 | syl2anc 691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝑥 ∈ (-𝑗[,]𝑗) ↔ (𝑥 ∈ ℝ ∧ -𝑗 ≤ 𝑥 ∧ 𝑥 ≤ 𝑗))) |
155 | 82, 150, 151, 154 | mpbir3and 1238 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ∈ (-𝑗[,]𝑗)) |
156 | 155 | iftrued 4044 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → if(𝑥 ∈ (-𝑗[,]𝑗), if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗), 0) = if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗)) |
157 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
158 | 157 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (𝐹‘𝑦) = (𝐹‘𝑥)) |
159 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → 𝑚 = 𝑗) |
160 | 159 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (2↑𝑚) = (2↑𝑗)) |
161 | 158, 160 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((𝐹‘𝑦) · (2↑𝑚)) = ((𝐹‘𝑥) · (2↑𝑗))) |
162 | 161 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → (⌊‘((𝐹‘𝑦) · (2↑𝑚))) = (⌊‘((𝐹‘𝑥) · (2↑𝑗)))) |
163 | 162, 160 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑗 ∧ 𝑦 = 𝑥) → ((⌊‘((𝐹‘𝑦) · (2↑𝑚))) / (2↑𝑚)) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
164 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ V |
165 | 163, 3, 164 | ovmpt2a 6689 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℕ ∧ 𝑥 ∈ ℝ) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
166 | 64, 82, 165 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝑗𝐽𝑥) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
167 | 110, 88 | nndivred 10946 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ∈ ℝ) |
168 | | flle 12462 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) · (2↑𝑗)) ∈ ℝ →
(⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))) |
169 | 101, 168 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗))) |
170 | | ledivmul2 10781 |
. . . . . . . . . . . . 13
⊢
(((⌊‘((𝐹‘𝑥) · (2↑𝑗))) ∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ ∧ ((2↑𝑗) ∈ ℝ ∧ 0 <
(2↑𝑗))) →
(((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))) |
171 | 110, 66, 89, 115, 170 | syl112anc 1322 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
(((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥) ↔ (⌊‘((𝐹‘𝑥) · (2↑𝑗))) ≤ ((𝐹‘𝑥) · (2↑𝑗)))) |
172 | 169, 171 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ (𝐹‘𝑥)) |
173 | 9 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 𝑥 ∈ ℂ) |
174 | 173 | absge0d 14031 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → 0 ≤
(abs‘𝑥)) |
175 | 66, 132 | addge02d 10495 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (0 ≤
(abs‘𝑥) ↔ (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥)))) |
176 | 174, 175 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ≤ ((abs‘𝑥) + (𝐹‘𝑥))) |
177 | 66, 133, 134, 176, 146 | letrd 10073 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝐹‘𝑥) ≤ 𝑗) |
178 | 167, 66, 134, 172, 177 | letrd 10073 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) →
((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗)) ≤ 𝑗) |
179 | 166, 178 | eqbrtrd 4605 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → (𝑗𝐽𝑥) ≤ 𝑗) |
180 | 179 | iftrued 4044 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = (𝑗𝐽𝑥)) |
181 | 180, 166 | eqtrd 2644 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → if((𝑗𝐽𝑥) ≤ 𝑗, (𝑗𝐽𝑥), 𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
182 | 131, 156,
181 | 3eqtrd 2648 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) = ((⌊‘((𝐹‘𝑥) · (2↑𝑗))) / (2↑𝑗))) |
183 | 119, 65, 182 | 3brtr4d 4615 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐹‘𝑥) − ((1 / 2)↑𝑛)))‘𝑗) ≤ ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗)) |
184 | 182, 172 | eqbrtrd 4605 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) ∧ 𝑗 ∈ (ℤ≥‘𝑘)) → ((𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))‘𝑗) ≤ (𝐹‘𝑥)) |
185 | 18, 20, 59, 61, 71, 84, 183, 184 | climsqz 14219 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ ((abs‘𝑥) + (𝐹‘𝑥)) < 𝑘)) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
186 | 17, 185 | rexlimddv 3017 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
187 | 186 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
188 | 36 | mptex 6390 |
. . . 4
⊢ (𝑚 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚𝐽𝑥) ≤ 𝑚, (𝑚𝐽𝑥), 𝑚), 0))) ∈ V |
189 | 4, 188 | eqeltri 2684 |
. . 3
⊢ 𝐺 ∈ V |
190 | | feq1 5939 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝑔:ℕ⟶dom ∫1 ↔
𝐺:ℕ⟶dom
∫1)) |
191 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔‘𝑛) = (𝐺‘𝑛)) |
192 | 191 | breq2d 4595 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (0𝑝
∘𝑟 ≤ (𝑔‘𝑛) ↔ 0𝑝
∘𝑟 ≤ (𝐺‘𝑛))) |
193 | | fveq1 6102 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑔‘(𝑛 + 1)) = (𝐺‘(𝑛 + 1))) |
194 | 191, 193 | breq12d 4596 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1)) ↔ (𝐺‘𝑛) ∘𝑟 ≤ (𝐺‘(𝑛 + 1)))) |
195 | 192, 194 | anbi12d 743 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((0𝑝
∘𝑟 ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1))) ↔ (0𝑝
∘𝑟 ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘𝑟 ≤ (𝐺‘(𝑛 + 1))))) |
196 | 195 | ralbidv 2969 |
. . . 4
⊢ (𝑔 = 𝐺 → (∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1))) ↔ ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘𝑟 ≤ (𝐺‘(𝑛 + 1))))) |
197 | 191 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((𝑔‘𝑛)‘𝑥) = ((𝐺‘𝑛)‘𝑥)) |
198 | 197 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) = (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥))) |
199 | 198 | breq1d 4593 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
200 | 199 | ralbidv 2969 |
. . . 4
⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥) ↔ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
201 | 190, 196,
200 | 3anbi123d 1391 |
. . 3
⊢ (𝑔 = 𝐺 → ((𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) ↔ (𝐺:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘𝑟 ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))) |
202 | 189, 201 | spcev 3273 |
. 2
⊢ ((𝐺:ℕ⟶dom
∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝐺‘𝑛) ∧ (𝐺‘𝑛) ∘𝑟 ≤ (𝐺‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝐺‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |
203 | 5, 7, 187, 202 | syl3anc 1318 |
1
⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧
∀𝑛 ∈ ℕ
(0𝑝 ∘𝑟 ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘𝑟 ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥))) |