This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mbfi1fseqlem2

Description: Lemma for mbfi1fseq . (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses mbfi1fseq.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfi1fseq.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
mbfi1fseq.3 ⊢ 𝐽 = ( 𝑚 ∈ ℕ , 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) )
mbfi1fseq.4 ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 𝐽 𝑥 ) ≤ 𝑚 , ( 𝑚 𝐽 𝑥 ) , 𝑚 ) , 0 ) ) )
Assertion mbfi1fseqlem2 ( 𝐴 ∈ ℕ → ( 𝐺 ‘ 𝐴 ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 mbfi1fseq.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 mbfi1fseq.2 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
3 mbfi1fseq.3 ⊢ 𝐽 = ( 𝑚 ∈ ℕ , 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( 𝐹 ‘ 𝑦 ) · ( 2 ↑ 𝑚 ) ) ) / ( 2 ↑ 𝑚 ) ) )
4 mbfi1fseq.4 ⊢ 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 𝐽 𝑥 ) ≤ 𝑚 , ( 𝑚 𝐽 𝑥 ) , 𝑚 ) , 0 ) ) )
5 negeq ⊢ ( 𝑚 = 𝐴 → - 𝑚 = - 𝐴 )
6 id ⊢ ( 𝑚 = 𝐴 → 𝑚 = 𝐴 )
7 5 6 oveq12d ⊢ ( 𝑚 = 𝐴 → ( - 𝑚 [,] 𝑚 ) = ( - 𝐴 [,] 𝐴 ) )
8 7 eleq2d ⊢ ( 𝑚 = 𝐴 → ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) ↔ 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) ) )
9 oveq1 ⊢ ( 𝑚 = 𝐴 → ( 𝑚 𝐽 𝑥 ) = ( 𝐴 𝐽 𝑥 ) )
10 9 6 breq12d ⊢ ( 𝑚 = 𝐴 → ( ( 𝑚 𝐽 𝑥 ) ≤ 𝑚 ↔ ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 ) )
11 10 9 6 ifbieq12d ⊢ ( 𝑚 = 𝐴 → if ( ( 𝑚 𝐽 𝑥 ) ≤ 𝑚 , ( 𝑚 𝐽 𝑥 ) , 𝑚 ) = if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) )
12 8 11 ifbieq1d ⊢ ( 𝑚 = 𝐴 → if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 𝐽 𝑥 ) ≤ 𝑚 , ( 𝑚 𝐽 𝑥 ) , 𝑚 ) , 0 ) = if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) )
13 12 mpteq2dv ⊢ ( 𝑚 = 𝐴 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝑚 [,] 𝑚 ) , if ( ( 𝑚 𝐽 𝑥 ) ≤ 𝑚 , ( 𝑚 𝐽 𝑥 ) , 𝑚 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) )
14 reex ⊢ ℝ ∈ V
15 14 mptex ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) ∈ V
16 13 4 15 fvmpt ⊢ ( 𝐴 ∈ ℕ → ( 𝐺 ‘ 𝐴 ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( - 𝐴 [,] 𝐴 ) , if ( ( 𝐴 𝐽 𝑥 ) ≤ 𝐴 , ( 𝐴 𝐽 𝑥 ) , 𝐴 ) , 0 ) ) )