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⁢2m2m
mbfi1fseq.4 ⊢G=m∈ℕ⟼x∈ℝ⟼ifx∈−mmifmJx≤mmJxm0
Assertion mbfi1fseqlem2 ⊢A∈ℕ→G⁡A=x∈ℝ⟼ifx∈−AAifAJx≤AAJxA0

Proof

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