Step |
Hyp |
Ref |
Expression |
1 |
|
mbfi1fseq.1 |
⊢ ( 𝜑 → 𝐹 ∈ MblFn ) |
2 |
|
mbfi1fseq.2 |
⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ) |
3 |
|
oveq2 |
⊢ ( 𝑗 = 𝑘 → ( 2 ↑ 𝑗 ) = ( 2 ↑ 𝑘 ) ) |
4 |
3
|
oveq2d |
⊢ ( 𝑗 = 𝑘 → ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) = ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) ) |
5 |
4
|
fveq2d |
⊢ ( 𝑗 = 𝑘 → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) ) ) |
6 |
5 3
|
oveq12d |
⊢ ( 𝑗 = 𝑘 → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) ) / ( 2 ↑ 𝑘 ) ) ) |
7 |
|
fveq2 |
⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) ) |
8 |
7
|
fvoveq1d |
⊢ ( 𝑧 = 𝑦 → ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) ) = ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑘 ) ) ) ) |
9 |
8
|
oveq1d |
⊢ ( 𝑧 = 𝑦 → ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑘 ) ) ) / ( 2 ↑ 𝑘 ) ) = ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑘 ) ) ) / ( 2 ↑ 𝑘 ) ) ) |
10 |
6 9
|
cbvmpov |
⊢ ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) = ( 𝑘 ∈ ℕ , 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑘 ) ) ) / ( 2 ↑ 𝑘 ) ) ) |
11 |
|
eleq1w |
⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) ↔ 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) ) ) |
12 |
|
oveq2 |
⊢ ( 𝑦 = 𝑥 → ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) = ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ) |
13 |
12
|
breq1d |
⊢ ( 𝑦 = 𝑥 → ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 ↔ ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 ) ) |
14 |
13 12
|
ifbieq1d |
⊢ ( 𝑦 = 𝑥 → if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) = if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) ) |
15 |
11 14
|
ifbieq1d |
⊢ ( 𝑦 = 𝑥 → if ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) , 0 ) = if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) , 0 ) ) |
16 |
15
|
cbvmptv |
⊢ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) , 0 ) ) |
17 |
|
negeq |
⊢ ( 𝑚 = 𝑘 → - 𝑚 = - 𝑘 ) |
18 |
|
id |
⊢ ( 𝑚 = 𝑘 → 𝑚 = 𝑘 ) |
19 |
17 18
|
oveq12d |
⊢ ( 𝑚 = 𝑘 → ( - 𝑚 [,] 𝑚 ) = ( - 𝑘 [,] 𝑘 ) ) |
20 |
19
|
eleq2d |
⊢ ( 𝑚 = 𝑘 → ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) ↔ 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) ) ) |
21 |
|
oveq1 |
⊢ ( 𝑚 = 𝑘 → ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) = ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ) |
22 |
21 18
|
breq12d |
⊢ ( 𝑚 = 𝑘 → ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 ↔ ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 ) ) |
23 |
22 21 18
|
ifbieq12d |
⊢ ( 𝑚 = 𝑘 → if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) = if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) ) |
24 |
20 23
|
ifbieq1d |
⊢ ( 𝑚 = 𝑘 → if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) , 0 ) = if ( 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) , if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) , 0 ) ) |
25 |
24
|
mpteq2dv |
⊢ ( 𝑚 = 𝑘 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑚 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) , if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) , 0 ) ) ) |
26 |
16 25
|
syl5eq |
⊢ ( 𝑚 = 𝑘 → ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) , if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) , 0 ) ) ) |
27 |
26
|
cbvmptv |
⊢ ( 𝑚 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( 𝑦 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) ≤ 𝑚 , ( 𝑚 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑦 ) , 𝑚 ) , 0 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑘 [,] 𝑘 ) , if ( ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) ≤ 𝑘 , ( 𝑘 ( 𝑗 ∈ ℕ , 𝑧 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑧 ) · ( 2 ↑ 𝑗 ) ) ) / ( 2 ↑ 𝑗 ) ) ) 𝑥 ) , 𝑘 ) , 0 ) ) ) |
28 |
1 2 10 27
|
mbfi1fseqlem6 |
⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : ℕ ⟶ dom ∫1 ∧ ∀ 𝑛 ∈ ℕ ( 0𝑝 ∘r ≤ ( 𝑔 ‘ 𝑛 ) ∧ ( 𝑔 ‘ 𝑛 ) ∘r ≤ ( 𝑔 ‘ ( 𝑛 + 1 ) ) ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑛 ∈ ℕ ↦ ( ( 𝑔 ‘ 𝑛 ) ‘ 𝑥 ) ) ⇝ ( 𝐹 ‘ 𝑥 ) ) ) |