Theorem itgrecl

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

	Ref	Expression
Hypotheses	itgrecl.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	itgrecl.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
Assertion	itgrecl	$$⊢\phi \to {\int }_{A}Bdx\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		itgrecl.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
2		itgrecl.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
3	1 2	itgrevallem1	$$⊢\phi \to {\int }_{A}Bdx={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)-{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -B\right),-B,0\right)\right)\right)$$
4	1	iblrelem	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼B\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)\in ℝ\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -B\right),-B,0\right)\right)\right)\in ℝ\right)\right)$$
5	2 4	mpbid	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)\in ℝ\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -B\right),-B,0\right)\right)\right)\in ℝ\right)$$
6		resubcl	$$⊢\left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)\in ℝ\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -B\right),-B,0\right)\right)\right)\in ℝ\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)-{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -B\right),-B,0\right)\right)\right)\in ℝ$$
7	6	3adant1	$$⊢\left(\left(x\in A⟼B\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)\in ℝ\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -B\right),-B,0\right)\right)\right)\in ℝ\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)-{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -B\right),-B,0\right)\right)\right)\in ℝ$$
8	5 7	syl	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le B\right),B,0\right)\right)\right)-{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -B\right),-B,0\right)\right)\right)\in ℝ$$
9	3 8	eqeltrd	$$⊢\phi \to {\int }_{A}Bdx\in ℝ$$