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 ) ) )