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

Metamath Proof Explorer

Theorem itgrecl

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

Ref Expression
Hypotheses itgrecl.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
itgrecl.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
Assertion itgrecl ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 itgrecl.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 itgrecl.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 1 2 itgrevallem1 ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ) )
4 1 iblrelem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ∈ ℝ ) ) )
5 2 4 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ∈ ℝ ) )
6 resubcl ⊢ ( ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ∈ ℝ ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ) ∈ ℝ )
7 6 3adant1 ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ∈ ℝ ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ) ∈ ℝ )
8 5 7 syl ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) ) ) − ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - 𝐵 ) , - 𝐵 , 0 ) ) ) ) ∈ ℝ )
9 3 8 eqeltrd ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℝ )