Metamath Proof Explorer

Theorem itgrecl

Description: Real closure of an integral. (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itgrecl.1 ⊢φ∧x∈A→B∈ℝ
itgrecl.2 ⊢φ→x∈A⟼B∈𝐿1
Assertion itgrecl ⊢φ→∫ABdx∈ℝ

Proof

Step Hyp Ref Expression
1 itgrecl.1 ⊢φ∧x∈A→B∈ℝ
2 itgrecl.2 ⊢φ→x∈A⟼B∈𝐿1
3 1 2 itgrevallem1 ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0
4 1 iblrelem ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
5 2 4 mpbid ⊢φ→x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
6 resubcl ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
7 6 3adant1 ⊢x∈A⟼B∈MblFn∧∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0∈ℝ∧∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
8 5 7 syl ⊢φ→∫2⁡x∈ℝ⟼ifx∈A∧0≤BB0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−B−B0∈ℝ
9 3 8 eqeltrd ⊢φ→∫ABdx∈ℝ