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 ⊢ φ → F ∈ MblFn
mbfi1fseq.2 ⊢ φ → F : ℝ ⟶ 0 +∞
mbfi1fseq.3 ⊢ J = m ∈ ℕ , y ∈ ℝ ⟼ F ⁡ y ⁢ 2 m 2 m
mbfi1fseq.4 ⊢ G = m ∈ ℕ ⟼ x ∈ ℝ ⟼ if x ∈ − m m if m J x ≤ m m J x m 0
Assertion mbfi1fseqlem2 ⊢ A ∈ ℕ → G ⁡ A = x ∈ ℝ ⟼ if x ∈ − A A if A J x ≤ A A J x A 0

Proof

Step Hyp Ref Expression
1 mbfi1fseq.1 ⊢ φ → F ∈ MblFn
2 mbfi1fseq.2 ⊢ φ → F : ℝ ⟶ 0 +∞
3 mbfi1fseq.3 ⊢ J = m ∈ ℕ , y ∈ ℝ ⟼ F ⁡ y ⁢ 2 m 2 m
4 mbfi1fseq.4 ⊢ G = m ∈ ℕ ⟼ x ∈ ℝ ⟼ if x ∈ − m m if m J x ≤ m m J x m 0
5 negeq ⊢ m = A → − m = − A
6 id ⊢ m = A → m = A
7 5 6 oveq12d ⊢ m = A → − m m = − A A
8 7 eleq2d ⊢ m = A → x ∈ − m m ↔ x ∈ − A A
9 oveq1 ⊢ m = A → m J x = A J x
10 9 6 breq12d ⊢ m = A → m J x ≤ m ↔ A J x ≤ A
11 10 9 6 ifbieq12d ⊢ m = A → if m J x ≤ m m J x m = if A J x ≤ A A J x A
12 8 11 ifbieq1d ⊢ m = A → if x ∈ − m m if m J x ≤ m m J x m 0 = if x ∈ − A A if A J x ≤ A A J x A 0
13 12 mpteq2dv ⊢ m = A → x ∈ ℝ ⟼ if x ∈ − m m if m J x ≤ m m J x m 0 = x ∈ ℝ ⟼ if x ∈ − A A if A J x ≤ A A J x A 0
14 reex ⊢ ℝ ∈ V
15 14 mptex ⊢ x ∈ ℝ ⟼ if x ∈ − A A if A J x ≤ A A J x A 0 ∈ V
16 13 4 15 fvmpt ⊢ A ∈ ℕ → G ⁡ A = x ∈ ℝ ⟼ if x ∈ − A A if A J x ≤ A A J x A 0